E.4.2 Promela Coding Tricks

Promela was designed to analyze protocols, so using it on parallel programs is a bit abusive. The following tricks can help you to abuse Promela safely:

  1. Memory reordering. Suppose you have a pair of statements copying globals x and y to locals r1 and r2, where ordering matters (e.g., unprotected by locks), but where you have no memory barriers. This can be modeled in Promela as follows:



      1 if
      2 :: 1 -> r1 = x;
      3   r2 = y
      4 :: 1 -> r2 = y;
      5   r1 = x
      6 fi
    


    The two branches of the if statement will be selected nondeterministically, since they both are available. Because the full state space is searched, both choices will eventually be made in all cases.

    Of course, this trick will cause your state space to explode if used too heavily. In addition, it requires you to anticipate possible reorderings.

    Figure: Complex Promela Assertion
    \begin{figure}{ % \scriptsize
\begin{verbatim}1 i = 0;
2 sum = 0;
3 do
4 :...
...U_READERS ->
9 assert(sum == 0);
10 break
11 od\end{verbatim}
}\end{figure}

    Figure: Atomic Block for Complex Promela Assertion
    \begin{figure}{ % \scriptsize
\begin{verbatim}1 atomic {
2 i = 0;
3 sum = 0...
...RS ->
10 assert(sum == 0);
11 break
12 od
13 }\end{verbatim}
}\end{figure}

  2. State reduction. If you have complex assertions, evaluate them under atomic. After all, they are not part of the algorithm. One example of a complex assertion (to be discussed in more detail later) is as shown in Figure [*].

    There is no reason to evaluate this assertion non-atomically, since it is not actually part of the algorithm. Because each statement contributes to state, we can reduce the number of useless states by enclosing it in an atomic block as shown in Figure [*]

  3. Promela does not provide functions. You must instead use C preprocessor macros. However, you must use them carefully in order to avoid combinatorial explosion.

Now we are ready for more complex examples.

Paul E. McKenney 2011-12-16