E.4.1 Promela Peculiarities
Although all computer languages have underlying similarities,
Promela will provide some surprises to people used to coding in C,
C++, or Java.
- In C, ``;'' terminates statements. In Promela it separates them.
Fortunately, more recent versions of Spin have become
much more forgiving of ``extra'' semicolons.
- Promela's looping construct, the do statement, takes
conditions.
This do statement closely resembles a looping if-then-else
statement.
- In C's switch statement, if there is no matching case, the whole
statement is skipped. In Promela's equivalent, confusingly called
if, if there is no matching guard expression, you get an error
without a recognizable corresponding error message.
So, if the error output indicates an innocent line of code,
check to see if you left out a condition from an if or do
statement.
- When creating stress tests in C, one usually races suspect operations
against each other repeatedly. In Promela, one instead sets up
a single race, because Promela will search out all the possible
outcomes from that single race. Sometimes you do need to loop
in Promela, for example, if multiple operations overlap, but
doing so greatly increases the size of your state space.
- In C, the easiest thing to do is to maintain a loop counter to track
progress and terminate the loop. In Promela, loop counters
must be avoided like the plague because they cause the state
space to explode. On the other hand, there is no penalty for
infinite loops in Promela as long as the none of the variables
monotonically increase or decrease - Promela will figure out
how many passes through the loop really matter, and automatically
prune execution beyond that point.
- In C torture-test code, it is often wise to keep per-task control
variables. They are cheap to read, and greatly aid in debugging the
test code. In Promela, per-task control variables should be used
only when there is no other alternative. To see this, consider
a 5-task verification with one bit each to indicate completion.
This gives 32 states. In contrast, a simple counter would have
only six states, more than a five-fold reduction. That factor
of five might not seem like a problem, at least not until you
are struggling with a verification program possessing more than
150 million states consuming more than 10GB of memory!
- One of the most challenging things both in C torture-test code and
in Promela is formulating good assertions. Promela also allows
never claims that act sort of like an assertion replicated
between every line of code.
- Dividing and conquering is extremely helpful in Promela in keeping
the state space under control. Splitting a large model into two
roughly equal halves will result in the state space of each
half being roughly the square root of the whole.
For example, a million-state combined model might reduce to a
pair of thousand-state models.
Not only will Promela handle the two smaller models much more
quickly with much less memory, but the two smaller algorithms
are easier for people to understand.
Paul E. McKenney
2011-12-16