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.

  1. In C, ``;'' terminates statements. In Promela it separates them. Fortunately, more recent versions of Spin have become much more forgiving of ``extra'' semicolons.
  2. Promela's looping construct, the do statement, takes conditions. This do statement closely resembles a looping if-then-else statement.
  3. 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.
  4. 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.
  5. 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.
  6. 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!
  7. 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.
  8. 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