Your solution for this assignment should terminate within 10 seconds (when running ./pan). If they exceed the time limit, you will get partial credit. Please also note how long your solutions take to run as a comment if they do exceed the time limit.

Anderson’s Queue Lock

The Peterson lock that we saw in class has two key flaws:

1. It works for only two threads at once;
2. It doesn’t provide any “first-in, first-out” guarantees.

In this assignment, you’ll model a different lock–Anderson’s queue lock– which works for an arbitrary number of threads. It also provides a FIFO guarantee as well as mutual exclusion and starvation-freedom. The algorithm assumes that we have some hardware support: an atomic “get and increment” action that lets us atomically read, and then increment, an integer variable.

Suppose you have n threads that can contend for access. The algorithm uses:

1. A global n-cell array of booleans (to serve as flags);
2. A global integer variable next;
3. For each thread, a local integer variable mySlot.

Initially, only flags[0] is true (the rest is false), and next = 0.

If a process wants access, it first gets-and-increments next, placing the result into its local mySlot variable. This gives it a unique index into the flags array: mySlot mod n. It then waits until flags[mySlot % n] is true. When it finishes, it sets its own flag to false and the next slot in the flag array to true.

Note that byte's range is 0-255. Thus, when 256 is assigned to next, spin queuelock.pml will show

Error: value (256->0 (8)) truncated in assignment

However, Spin’s output is misleading here: this actually a warning rather than an error. The simulation will continue running without any problem.

For more information, include pseudocode, see the “Spin Locks” slides (starting on slide 96) from Prof. Herlihy’s class.

The provided template has already set up most of this algorithm for you.

Please use the template (below). The variables for verification hint at one way to check the desired properties.

Deliverables

1. Augment this template model with asserts and other statements as needed to check (For NTHREADS = 2):
   • mutual exclusion in the critical section;
   • flag slots are used in order; and
   • starvation-freedom.
   If any of these properties fail, examine the trace(s) and explain why the failure occurs.
2. Change NTHREADS to 3 and check the same properties. One will fail. Make a one-line change to the template’s get_and_increment macro that corrects the issue, and document why this change is an acceptable abstraction decision.

Hint: as mentioned above, Spin will faithfully model overflow in the next variable. How does this interact with the modulo arithmetic?

More useful Spin commands

1. To create verifier C program: spin -a queuelock.pml
2. You might want breadth-first search or bitstate (approximate) verification: gcc -DBFS -DBITSTATE -o pan pan.c
3. To find shortest trace for assertion violation: ./pan -i
4. Spin defaults to a bound of 9999 on search depth. To change it (e.g., to

100000. do: ./pan -m100000

5. To see the trace (-l gives local variable values in trace, useful for mySlot): spin -t -p -l

Template

// Adjust this to change the number of threads (N=2 at first)
#define NTHREADS 2

/////////////////////////////////////////////////////////////////////

// Promela has C-macro like inlines. These are not helper functions;
// they can't return anything. Invocations get replaced with the
// code inside at compile time.

// A d_step is an optimized "atomic" statement: these blocks cannot 
// be interrupted by other processes, and thus simulate a 
// hardware-provided get_and_increment action.

inline get_and_increment(VAR, RESULT) {
  d_step {
    RESULT = VAR;
    VAR = VAR + 1;
  }
}

/////////////////////////////////////////////////////////////////////

// first is true; rest false (this repeats for the size of NTHREADS)
bool flags[NTHREADS];
byte next = 0; // the thread that gets slot 0 goes first

// Variables for verification.
byte num_in_crit = 0; // number of threads in the critical section
byte whichSlotExpectedNext = 0; // Hint: used to assert that the next slot is really used next

/////////////////////////////////////////////////////////////////////

// Processes contending for the lock. Start with N of them!
active [NTHREADS] proctype a_process()
{
  // Allocate a different mySlot for each a_process instance. Doing this, instead of
  // making a global array of length NTHREADS tells Spin that each mySlot can only be
  // accessed by its local thread, which speeds up verification.
  byte mySlot;

  do
     ::
        get_and_increment(next,mySlot);   // grab a slot
        flags[mySlot % NTHREADS];         // block until my slot is true 
        flags[mySlot % NTHREADS] = false; // reset this flag for re-use later

        /*
           Assertions and assignments to support them go here.
        */

        flags[(mySlot+1) % NTHREADS] = true; // next thread can progress
  od;
}

// Init is run first
init {
  flags[0] = true;
}

/*
  LTL properties here.
*/

Handing In

Run cs195y_handin mc2 from a directory holding your Promela file (queuelock.pml). You should receive an email confirming that your handin has worked.