Promela |
Control-Flow |
atomic |
NAME
atomic -
for defining a fragment of code that is to be executed indivisibly.
SYNTAX
atomic { sequence }
EFFECT
In the semantics model, a side effect of the execution of any statement, except
the last, from an atomic sequence is to set global system variable
exclusive to the instantiation number of the executing process,
thus preserving the exclusive privilige to execute.
If atomicity is lost, for instance when a statement blocks,
the exclusive variable returns to its default value.
If any statement in the atomic sequence (including the last) has another statement
as a successor that is also part of an atomic sequence, then atomicity is not lost.
(The latter can happen for goto jumps that transition from one atomic sequence into
another, or when atomic sequences are nested.)
DESCRIPTION
If a sequence of statements is enclosed in
parentheses and prefixed with the keyword
atomic , this indicates that the sequence is to be executed
as one indivisible unit, non-interleaved with other
processes.
In the interleaving of process executions, no
other process can execute statements from the moment
that the first statement of an atomic
sequence is executed until the last one has completed.
The sequence can contain arbitrary Promela statements,
and may be non-deterministic.
If any statement within the atomic sequence blocks, atomicity is lost, and other processes are then allowed to start executing statements. When the blocked statement becomes executable again, the execution of the atomic sequence can be resumed at any time, but not necessarily immediately. Before the process can resume the atomic execution of the remainder of the sequence, the process must first compete with all other active processes in the system to regain control, that is, it must first be scheduled for execution.
If an atomic sequence contains a rendezvous send statement, control passes from sender to receiver when the rendezvous handshake completes. Control can return to the sender at a later time, under the normal rules of nondeterministic process interleaving, to allow it to continue the atomic execution of the remainder of the sequence. In the special case where the recepient of the rendezvous handshake is also inside an atomic sequence, atomicity will be passed through the rendezvous handshake from sender to receiver and is not interrupted (except that another process now holds the exclusive privilige to execute).
An atomic sequence can be used wherever a Promela statement can be used. The first statement of the sequence is called its guard , because it determines when the sequence can be started. It is allowed, though not good style, to jump into the middle of an atomic sequence with a goto statement, or to jump out of it in the same way. After jumping into the sequence, atomic execution may begin when the process gains control, provided that the statement jumped to is executable. After jumping out of an atomic sequence, atomicity is lost, unless the target of the jump is also contained in an atomic sequence.
EXAMPLES
atomic { /* swap the values of a and b */ tmp = b; b = a; a = tmp }In the example, the values of two variables a and b are swapped in an uninterruptable sequence of statement executions. The execution of this sequence cannot be blocked, since all the statements it contains are always unconditionally executable.
An example of a non-deterministic atomic sequence is the following:
atomic { if :: a = 1 :: a = 2 fi; if :: b = 1 :: b = 2 fi }In this example, the variables a and b are assigned a single value, with no possible intervening statement from any other process. There are four possible ways to execute this atomic sequence.
It is possible to create a global atomic chain of executions, with two or more processes alternately executing, by passing control back and forth with rendezvous operations.
chan q = [0] of { bool }; active proctype X() { atomic { A; q!0; B } } active proctype Y() { atomic { q?0 -> C } }In this example, for instance, execution could start in process X with the program block named A . When the rendezvous handshake is executed, atomicity would pass to process Y , which now starts executing the block named C . When it terminates, control can pass back to X , which can then atomically execute the block named B.
It is often useful to use atomic sequences to start a series of processes in such a way that none of them can start executing statements until all of them have been initialized:
atomic { run A(1,2); run B(2,3); run C(3,1) }
NOTES
Atomic sequences can be used to reduce
the complexity of a verification.
If an infinite loop is accidentily included
in an atomic sequence, the verifier cannot always
recognize the cycle.
In the default depth-first search mode, the occurrence
of such an infinite cycle will ultimately lead to the
depth limit being exceeded, which will truncate the loop,
but likely the result will still be a notable increase
of complexity in redundant states being repeatedly matched.
In general, make sure that do-loops included in atomic
or d_step sequences terminate. Therefore a non-deterministic
selection cycle such as the one below should never be enclosed
in an atomic sequence:
do // do not make this atomic :: a++ :: break odIn breadth-first search mode, though, this type of an infinite cycle will be detected.
Promela d_step sequences can be executed significantly more efficiently by the verifier than atomic sequences, but do not allow non-determinism.
SEE ALSO
d_step
goto
receive
send
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page updated: 10 May 2019) |