Promela Reference -- atomic(3)





atomic - introduces a sequence of statements that is to be executed indivisibly.

atomic { sequence }

Within the semantics model (see Intro(0)), the effect of executing any statement within an atomic sequence (in addition to the effects specified in the effects clause for the basic statements) is to set global system variable exclusive to the instantiation number of the executing process.

A sequence of statements enclosed in parentheses prefixed with the keyword atomic 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, the atomicity is lost, and other processes are allowed to execute arbitrarily many statements. When the blocked statement becomes executable again, the execution of the atomic sequence can be resumed. To regain control and resume execution, however, the process competes with all other active processes.

If an atomic sequence contains a rendezvous send statement, control will pass from sender to receiver the moment that 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 flow with the rendezvous and is not interrupted (except that another process now holds the exclusive privilige to execute).

An atomic sequence can be used wherever a single statement can be used. The first statement of the sequence is called it's guard , because it determines when the sequence can be started. It is valid, 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 the atomicity is lost, unless the target of the jump is also contained within an atomic sequence.


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 a sequence of statement executions that is defined to be uninterruptable.

It is often useful to use atomic sequences to start op 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)


Atomic sequences can be used to reduce the complexity of a validation model.

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. The model checker can not recognize this, but the stack-limit will eventually break such cycles, which secures that a verification attempt can still be completed (be it inefficiently).

goto(3), d_step(3), sequence(3).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)