Figure
demonstrates the textbook race condition
resulting from non-atomic increment.
Line 1 defines the number of processes to run (we will vary this
to see the effect on state space), line 3 defines the counter,
and line 4 is used to implement the assertion that appears on
lines 29-39.
Lines 6-13 define a process that increments the counter non-atomically. The argument me is the process number, set by the initialization block later in the code. Because simple Promela statements are each assumed atomic, we must break the increment into the two statements on lines 10-11. The assignment on line 12 marks the process's completion. Because the Spin system will fully search the state space, including all possible sequences of states, there is no need for the loop that would be used for conventional testing.
Lines 15-40 are the initialization block, which is executed first. Lines 19-28 actually do the initialization, while lines 29-39 perform the assertion. Both are atomic blocks in order to avoid unnecessarily increasing the state space: because they are not part of the algorithm proper, we loose no verification coverage by making them atomic.
The do-od construct on lines 21-27 implements a Promela loop, which can be thought of as a C for (;;) loop containing a switch statement that allows expressions in case labels. The condition blocks (prefixed by ::) are scanned non-deterministically, though in this case only one of the conditions can possibly hold at a given time. The first block of the do-od from lines 22-25 initializes the i-th incrementer's progress cell, runs the i-th incrementer's process, and then increments the variable i. The second block of the do-od on line 26 exits the loop once these processes have been started.
The atomic block on lines 29-39 also contains a similar do-od loop that sums up the progress counters. The assert() statement on line 38 verifies that if all processes have been completed, then all counts have been correctly recorded.
You can build and run this program as follows:
spin -a increment.spin # Translate the model to C cc -DSAFETY -o pan pan.c # Compile the model ./pan # Run the model |
This will produce output as shown in
Figure .
The first line tells us that our assertion was violated (as expected
given the non-atomic increment!).
The second line that a trail file was written describing how the
assertion was violated.
The ``Warning'' line reiterates that all was not well with our model.
The second paragraph describes the type of state-search being carried out,
in this case for assertion violations and invalid end states.
The third paragraph gives state-size statistics: this small model had only
45 states.
The final line shows memory usage.
The trail file may be rendered human-readable as follows:
spin -t -p increment.spin |
This gives the output shown in
Figure .
As can be seen, the first portion of the init block created both
incrementer processes, both of which first fetched the counter,
then both incremented and stored it, losing a count.
The assertion then triggered, after which the global state is displayed.
Paul E. McKenney 2011-12-16