Here, http://spinroot.com/spin/Man/Manual.html, it is written that:
In Promela there is also another way to avoid the test and set problem: atomic sequences. By prefixing a sequence of statements enclosed in curly braces with the keyword atomic the user can indicate that the sequence is to be executed as one indivisible unit, non-interleaved with any other processes. It causes a run-time error if any statement, other than the first statement, blocks in an atomic sequence. This is how we can use atomic sequences to protect the concurrent access to the global variable state in the earlier example.
And here, http://spinroot.com/spin/Man/atomic.html, it is written that:
If any statement within the atomic sequence blocks, atomicity is lost 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.
So, what is the true? From the first citation we can learn that it is not allowed to block in atomic ( not the first statement)
From the second citation we learn that it is ok to block in atomic. You just lose the atomicity and that is it.
Contradictory Documentation:
My guess is that the contradiction is merely the result of parts of the documentation not being updated to reflect changes that occurred within Spin over the years.
In fact, in the release notes of Spin v. 2.0 we can find the following piece of text (emphasis is mine):
Atomic Statements in Promela:
In the current version of Promela/Spin there exist two atomic sequences:
atomic: from the docs, emphasis is mine:
d_step: from the docs, emphasis is mine:
Of course, one can actually test this behaviour with a simple Promela example.
TEST 1: loss of atomicity with
atomic {}
Take the following Promela Model, in which two processes
pippo
andpluto
execute anatomic {}
sequence of instructions up to10
times. Each process saves its unique_pid
inside a global variablep
when it starts executing the atomic sequence, and then checks aflag
variable:flag
istrue
,pippo
can execute butpluto
cannot, thereforepluto
should temporarily loose atomicity (in some execution trace)flag
isfalse
,pluto
can execute butpippo
cannot, thereforepippo
should temporarily loose atomicity (in some execution trace)We check the latest case by adding an
assert(p == _pid)
instruction at the end of the atomic sequence inpippo
. If the condition is not violated, then it means that there is no execution in whichpippo
looses atomicity from within the atomic sequence andpluto
starts executing instead. Otherwise, we proved that the description in the linked documentation foratomic {}
is accurate.If we perform formal verification with Spin, it finds an execution trace that violates the property:
The assertion is violated, as stated in the documentation. You can replay the invalid execution trace as follows:
Double Check. Now, if you comment the instruction
flag:
insidepippo
and you repeat the verification process, you'll see that there won't be any execution trace violating the assertion. This is because no other instruction in the atomic sequence ofpippo
can block, and therefore atomicity is never lost.TEST 2: blocking error with
d_step {}
Now, take the same code example and substitute the
atomic
keyword insidepippo
withd_step
:If you formally verify this model, you'll see that it still finds a counter-example, but this time with a different error:
Which corresponds to the following execution trace:
The problem is that
pippo
blocks inside thed_step
sequence, and this violates the third condition in the synopsis ofd_step
documentation, exactly as described.Double Check. Again, if you comment the
flag;
instruction you'll see that there won't be any error trace.