Spin Assignments

Assignment Prisoners' Problem

• whenever one of the prisoners claims that they have all visited the interrogation room, then this is correct;
• eventually, one of the prisoners will claim. (Hint: use acceptance labels and check for acceptance cycles)

Various Assignments

Most of the following assignments are based on my lecture notes Concurrent Programming, referred to below as CP.

Assignment "Bounded Buffer"

This assignment is based on the bounded buffer for several producers and several consumers, described in Section 4.5, Exercise 9 (p. 28), of CP.

Model the synchronization by semaphores for several producers and several consumers in Promela. Show that products are always stored in empty slots and are always retrieved from full slots. Show that deadlock does not occur. Show that deadlock can occur when the producers, or the consumers can terminate. What choices for the numbers can you accommodate?

Assignment "Readers and Writers"

Model the synchronization by semaphores in Promela. Allow readers and writers to terminate. Show mutual exclusion and absence of deadlock. What choices for the numbers can you accommodate? Explain the warnings for superfluous code. Model, formulate, and verify the LTL property that whenever some writer wants to write, eventually nobody reads anymore or this writer writes. You may choose a specific writer.

Assignment "Exercise 7.2"

Given are two shared integer variables, x and y, initially 0, and the integer constants a,b > 0 and c,d >= 0. These actions are to be synchronized in such a way that they are executed atomically and preserve the safety conditions x <= y + c and y <= x + d; this should be done as nodeterminately as possible. Reduce the problem to a problem with a finite state space, and write in Promela an algorithm based on split binary semaphores, satisfying the requirements. Show that it does not lead to unnecessary deadlock. Use SPIN to determine the number of reachable states for some choices of the parameters. Can you generalize and prove some facts about this number?

Assignment "Two chambers" (about fairness)

Since semaphores (see section 4 of CP) are not necessarily fair, one may want to enforce fairness by additional measures. The following idea seems to be quite generally applicable.
In order to make the standard semaphore implementation of mutual exclusion fair, we introduce two chambers, indexed by a shared variable toggle: bit. A process that needs to enter CS, first enters chamber[toggle]. Processes in chamber[toggle] have to wait until toggle is modified. Therefore, all processes in the other chamber can enter CS consecutively. When the other chamber is empty, toggle is toggled. In this way, all processes that have entered a chamber, will eventually be able to enter CS. This is called fairness.
Implement this idea. The chamber where a process is waiting, can be implemented as a private variable. Use two shared variables to count the processes in the chambers. Use a single semaphore to enforce mutual exclusion. The shape of your algorithm is as follows:

   proctype user(self) {
     do
     :: skip  /* processes may perform innocent private actions */
     :: enter chamber[toggle], possibly changing toggle ;
        wait until toggle has changed ;
        P(sema) ;
        CS ;
        V(sema) ;
        exit chamber, possibly changing toggle
     od
   }

Assignment "Leader Election in a Ring"

Model the protocol in Promela and test it with Spin. Set the values of priv.self by means of a function like f(self) = (a*self+b) % 17, for some pairs a, b. Argue that your testing indicates (in)correctness of the protocol. Discuss safety and liveness.

Assignment "Bloom's register"

Bloom's algorithm simulates a read-write register for two writing processes and one reading process as explained in section 3 of my paper An assertional criterion for atomicity, Acta Informatica 38 (2002) 343-366. Verify that the reader always reads a legal value. To keep the state space small enough, let the writers not write too many different values. The report must carefully explain what you could verify, and what you could not verify, and why.

Assignment "Self stabilization in a ring of processes"

This goes back to Dijkstra (Comm. ACM, November 1974). There are N+1 processes in a ring. Each process has an integer S with 0<=S<3, and can inspect the integers of its neighbours: L (left) and R (right). It can only modify S according to the following rules:
Process 0: whenever (S+1)mod3 = R do S:= (S-1)mod3.
Process N: whenever L=R and (L+1)mod3 != S do S:=(L+1)mod3.
Process i (0 < i < N): whenever (S+1)mod3 = L do S:=L, and
whenever (S+1)mod3 = R do S:= R.
Here 3 mod3 = 0 and (-1)mod3 = 2.

Verify that, whatever the initial state, eventually there is always precisely one process that can do a step, and also that every process will do infinitely many steps. Characterize these eventual states. What values of N can you handle? How many steps does it take to reach the eventual states?

Assignment "Mutual exclusion for K processes"

In the entrance protocol, every process sets its level to the number of processes interested in the critical section. A process with level 0 can enter CS, and then leave. Every positive level has a unique slot. A process with a positive level can decide to enter the slot of its level. Whenever a process enters an occupied slot, the current occupier is pushed out of the slot to the next lower level. Whenever a process observes that there are cnt interested processes other than itself, it can proceed to level cnt. A process counts the number of interested processes one by one. It need not count processes that entered after it began counting. It may discount processes that leave and were counted already. After entering a slot, a process needs to start counting again from 0.

Verify that there is never more than one process in CS. How many processes can you accommodate? It is conjectured that, while some process is in its entrance protocol, no other process can start the entrance protocol and enter CS more than once. Verify this conjecture for some small value of K. (Let me know if you can prove the conjecture!)

Assignment "Barrier synchronization for possibly terminating threads"

Given are N environment threads (see below). At certain points in the computation, these threads need to wait for all other threads before they proceed with the next part of the computation. The environment threads can also nondeterministically terminate. Implement this synchronization by N barrier threads, that each communicate with its own environment thread by means of synchronous channels out[p] and in[p], and with each other via channels or shared variables. Accomplish this by implementing "synchronizer" and "logout". These program fragments are not allowed to access the shared variables activeCnt, wCnt, toggle, out, and in.

Test the safety of your solution with the "assert" that is given. Test its liveness also.
Hint: see Sections 2.5, 4.4, etc. of CP.

#define Nproc 4
byte activeCnt = Nproc ; 
byte wCnt = 0 ;
bit toggle ;
chan out[Nproc] = [0] of {bit} ;
chan in[Nproc] = [0] of {bit} ;

proctype environ(byte self) {
  bit tog ;
  do
  :: // noncritical activity ;
     atomic {
       assert tog == toggle ;
       tog = ! tog ;
       wCnt ++ ;
       if 
       :: wCnt == activeCnt -> 
          toggle = ! toggle ;
          wCnt = 0 
       :: else
       fi ;
       out[self]!1
     } 
     // AWAIT:
     in[self]?_ 
  :: atomic {   // announce termination:
       activeCnt -- ;
       if 
       :: activeCnt == wCnt ->
          toggle = ! toggle ;
          wCnt = 0 
       :: else
       fi ;
       out[self]!0 ;
       break 
     }
  od 
}

proctype barrier(byte self) {
  do 
  :: out[self]?1 -> 
     "synchronizer" ;
     in[self]!0 
  :: out[self]?0 ->
     "logout" ;
     break
  od 
}