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

SYNTAX
atomic { sequence }

EFFECT
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.

DESCRIPTION
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.

EXAMPLES

atomic {	/* swap the values of a and b */

	tmp = b;

	b = a;

	a = tmp

}

NOTES
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)

}

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).

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