| << Chapter < Page | Chapter >> Page > |
Guarded statements are one of the most basic elements of the Promela language.
As this section will introduce, they introduce the ability tosynchronize processes.
In
the next section ,
we see how they are also fundamental parts of thelooping (
do ) and
conditional (
if ) constructs.
After that ,
we will return to the synchronization issues, exploring themin greater depth.
guard ->
body ,
consists of two parts.The
guard is a boolean expression.
The body is a statement.Execution of the body will
block ,
or wait, doing nothing, until the guard becomes true.1 bool ready = false;
2 int val;3
4 active proctype produce_one()5 {
6 /* Compute some information somehow. */7 val = 42;
89 ready = true;
1011 /* Can do something else. */
12 printf("produce_one done.\n");13 }
1415 active proctype consume_one()
16 {17 int v;
1819 /* Wait until the information has been computed. */
20 ready ->21
22 /* Now, we can use this. */23 v = val;
24 }
This program leads to the following state space,
illustrating two important traits about Promela's guards.
First, the guarded statement of
consume_one will
block sit and do nothinguntil
its guard is satisfied.This is seen by the behavior of the first three states in
the state space.Second, execution of the guard is itself a transition to
a state. This allows code, such as
produce_one 's
printf to be interleaved
between the guard and its body.(The otherwise unnecessary
printf is there solely to make this point.)
When such interruptions between the guard and body areundesired, they can be prevented, as
shown later .
consume_one process
cannot make progress until
produce_one sets the
ready variable.-> is just
alternate syntax for
; , and
an expression is a valid statement by itself.Thus, we more
properly define when each kind of Promela statement is enabled.In particular, boolean expressions are enabled when they evaluate
to true, assignment statements are always enabled, and a compoundstatement
stmt_1 ;;
stmt_n is enabled if its first statement is.
One simplification that this allows is that trivially true guardsare unnecessary in Promela.
The statement
true ->
stmt is equivalent to the simpler
stmt .Later we will explore the possibility that a process stays blocked forever, or equivalently,never becomes enabled.
Of course, few interesting programs are made simply of straight-line code.We generally need to have more interesting control flow, including conditionals and iteration.These are illustrated in the remaining examples of this section.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|