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 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.
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
Now we are ready for more complex examples.
Paul E. McKenney 2011-12-16