Promela Reference -- atomic(3)

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

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:

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.

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:

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:

In breadth-first search mode, though, this type of an infinite cycle will be detected.
Note that it is always an error if an infinite cycle appears inside an atomic sequence, since in that case the atomic sequence could not possibly be executed atomically in any real implementation.

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)