E.5 Promela Example: Locking

Figure: Promela Code for Spinlock
\begin{figure}{ % \scriptsize
\begin{verbatim}1  ...

Since locks are generally useful, spin_lock() and spin_unlock() macros are provided in lock.h, which may be included from multiple Promela models, as shown in Figure [*]. The spin_lock() macro contains an infinite do-od loop spanning lines 2-11, courtesy of the single guard expression of ``1'' on line 3. The body of this loop is a single atomic block that contains an if-fi statement. The if-fi construct is similar to the do-od construct, except that it takes a single pass rather than looping. If the lock is not held on line 5, then line 6 acquires it and line 7 breaks out of the enclosing do-od loop (and also exits the atomic block). On the other hand, if the lock is already held on line 8, we do nothing (skip), and fall out of the if-fi and the atomic block so as to take another pass through the outer loop, repeating until the lock is available.

The spin_unlock() macro simply marks the lock as no longer held.

Note that memory barriers are not needed because Promela assumes full ordering. In any given Promela state, all processes agree on both the current state and the order of state changes that caused us to arrive at the current state. This is analogous to the ``sequentially consistent'' memory model used by a few computer systems (such as MIPS and PA-RISC). As noted earlier, and as will be seen in a later example, weak memory ordering must be explicitly coded.

Figure: Promela Code to Test Spinlocks
\begin{figure}{ % \scriptsize
\begin{verbatim}1  ...

These macros are tested by the Promela code shown in Figure [*]. This code is similar to that used to test the increments, with the number of locking processes defined by the N_LOCKERS macro definition on line 3. The mutex itself is defined on line 5, an array to track the lock owner on line 6, and line 7 is used by assertion code to verify that only one process holds the lock.

The locker process is on lines 9-18, and simply loops forever acquiring the lock on line 13, claiming it on line 14, unclaiming it on line 15, and releasing it on line 16.

The init block on lines 20-44 initializes the current locker's havelock array entry on line 26, starts the current locker on line 27, and advances to the next locker on line 28. Once all locker processes are spawned, the do-od loop moves to line 29, which checks the assertion. Lines 30 and 31 initialize the control variables, lines 32-40 atomically sum the havelock array entries, line 41 is the assertion, and line 42 exits the loop.

We can run this model by placing the above two code fragments into files named lock.h and lock.spin, respectively, and then running the following commands:



spin -a lock.spin
cc -DSAFETY -o pan pan.c
./pan


Figure: Output for Spinlock Test
\begin{figure}{ \scriptsize
\begin{verbatim}(Spin Version 4.2.5 -- 2 April 200...
...es)
unreached in proctype :init:
(0 of 22 states)\end{verbatim}
}\end{figure}

The output will look something like that shown in Figure [*]. As expected, this run has no assertion failures (``errors: 0'').

Quick Quiz E.1: Why is there an unreached statement in locker? After all, isn't this a full state-space search? End Quick Quiz

Quick Quiz E.2: What are some Promela code-style issues with this example? End Quick Quiz

Paul E. McKenney 2011-12-16