E.3 Promela Example: Atomic Increment

Figure: Promela Code for Atomic Increment
\begin{figure}{ \scriptsize
\begin{verbatim}1 proctype incrementer(byte me)
...
...ounter = temp + 1;
8 }
9 progress[me] = 1;
10 }\end{verbatim}
}\end{figure}

Figure: Atomic Increment spin Output
\begin{figure}{ \scriptsize
\begin{verbatim}(Spin Version 4.2.5 -- 2 April 200...
...es)
unreached in proctype :init:
(0 of 24 states)\end{verbatim}
}\end{figure}

It is easy to fix this example by placing the body of the incrementer processes in an atomic blocks as shown in Figure [*]. One could also have simply replaced the pair of statements with counter = counter + 1, because Promela statements are atomic. Either way, running this modified model gives us an error-free traversal of the state space, as shown in Figure [*].



Subsections

Paul E. McKenney 2011-12-16