- Types of Objects
- Processes
- Provided Clauses
- Data Objects
- Data Structures
- Message Channels
- Channel Poll Operations
- Sorted Send And Random Receive
- Rendezvous Communication
- Rules For Executability
- Assignments And Expressions
- Control Flow: Compound Statements
- Atomic Sequences
- Deterministic Steps
- Selection
- Repetition
- Escape Sequences
- Inline Definitions
- Reading Input
- Special Features
- Finding Out More
This chapter is from the book
This chapter is from the book
This chapter is from the book
Rules For Executability
The definition of PROMELA centers on its semantics of executability, which provides the basic means in the language for modeling process synchronizations. Depending on the system state, any statement in a SPIN model is either executable or blocked. We have already seen four basic types of statements in PROMELA: print statements, assignments, i/o statements, and expression statements. A curiosity in PROMELA is indeed that expressions can be used as if they were statements in any context. They are “executable” (i.e., passable) if and only if they evaluate to the boolean value true, or equivalently to a non-zero integer value. The semantics rules of PROMELA further state that print statements and assignments are always unconditionally executable. If a process reaches a point in its code where it has no executable statements left to execute, it simply blocks.
For instance, instead of writing a busy wait loop
while (a != b) /* while is not a keyword in Promela */
skip; /* do nothing, while waiting for a==b */
we achieve the same effect in PROMELA with the single statement
(a == b); /* block until a equals b */
The same effect could be obtained in PROMELA with constructions such as
L: /* dubious */
if
:: (a == b) -> skip
:: else -> goto L
fi
or
do /* also dubious */ :: (a == b) -> break :: else -> skip od
but this is always less efficient, and is frowned upon by PROMELA natives. (We will cover selection and repetition structures in more detail starting at p. 56.)
We saw earlier that expressions in PROMELA must be side effect free. The reason will be clear: a blocking expression statement may have to be evaluated many times over before it becomes executable, and if each evaluation could have a side effect, chaos would result. There is one exception to the rule. An expression that contains the run operator we discussed earlier can have a side effect, and it is therefore subject to some syntactic restrictions. The main restriction is that there can be only one run operator in an expression, and if it appears it cannot be combined with any other operators. This, of course, still allows us to use a run statement as a potentially blocking expression. We can indicate this effect more explicitly if instead of writing
run you_run(0); /* potentially blocking */
without change of meaning, we write
(run you_run(0)) -> /* potentially blocking */
Consider, for instance, what the effect is if we use such a run expression in the following model, as a variation on the model we saw on p. 39.
active proctype new_splurge(int n)
{
printf("%d\n", n);
run new_splurge(n+1)
}
As before, because of the bound on the number of processes that can be running simultanesously, the 255th attempt to instantiate a new process will fail. The failure causes the run expression to evaluate to zero, and thereby it permanently blocks the process. The blocked process can now not reach the end of its code and it therefore cannot terminate or die. As a result, none of its predecessors can die either. The system of 255 processes comes to a grinding halt with 254 processes terminated but blocked in their attempt to die, and one process blocked in its attempt to start a new process.
If the evaluation of the run expression returns zero, execution blocks, but no side effects have occurred, so there is again no danger of repeated side effects in consecutive tests for executability. If the evaluation returns non-zero, there is a side effect as the execution of the statement completes, but the statement as a whole cannot block now. It would decidedly be dubious if compound conditions could be built with run operators. For instance,
run you_run(0) && run you_run(1) /* not valid */
would block if both processes could not be instantiated, but it would not reveal whether one process was created or none at all. Similarly,
run you_run(0) || run you_run(1) /* not valid */
would block if both attempts to instantiate a process fail, but if successful would not reveal which of the two processes was created.