Objectives

• To improve your understanding of the modelling of mutual exclusion.
• To understand how how monitors may be modelled as FSP process and how to implement these in Java.
• To understand what are the appropriate condition synchronizations associated with a monitor.
• To understand semaphores and their relation with condition synchronization.
• To understand more deeply the semantics of synchonized objects and methods.

Preparation

• revise the exercises in the previous session (including the Homework!), and get ready any questions you might have from it.
• read through these exercises to familiarize yourself with their content.
• revise the corresponding lecture notes and corresponding chapters (3, 4 and 5) of the Magee&Kramer. In particular, ||RESOURCE_SHARE (Ch 3, slide 13) and ||SEMADEMO (Ch 5, slide 20) - process prefixing for shared resources under || composition for Tute Q2.2; and the implementation of the Buffer monitor (Ch 5, slide 30) for Tute Q4.
• follow this up by studying with the LTSA tool some examples from Chapters 4 & 5 of the textbook. Remember, to check the `Multiple LTS in Draw Window' option and to use Composite to compile a composite process. Suggested examples are Garden_lockvar, Counter_lockvar, Carpark, SemaDemo and BoundedBuffer.
• remember to bring a pen and paper for the Tutorial Exercises.

Tutorial Exercises

1. Discuss any outstanding issues from the previous session (including Homework).

2. (Ex 4.3 Magee & Kramer) A central computer with a number of terminals is used to reserve seats in a concert hall. A seat, initially unreserved, can be reserved (only once) and respond to the respective query action corresponding to its state:

     SEAT = SEAT[0],    // unreserved
     SEAT[res: 0..1] 
        = ( query[res] -> SEAT[res]
          | when (res==0) reserve -> SEAT[1] // now reserved 
          | when (res==1) reserve -> ERROR   // error of being reserved twice
          ).
     range S = 0..1
     ||SEATS = (seat[S]:SEAT).            
   

   At each terminal, a clerk can choose[s:S] any of the existing S seats and then makes a query on whether it is reserved; is not reserved, they can then reserve it. However, a double-booking from another terminal must be avoided! This requires the clerk to acquire a lock before the query on the seat and release it after either reserving it or finding out it is already reserved.
   1. Model in the FSP process TERMINAL the actions of a clerk at the terminal.
      Hint: to query if the chosen seat s is reserved can be modelled by the choice
      (seat[s].query[0] -> ... | seat[s].query[1] -> ...).

   2. Using the process LOCK = (acquire -> release -> LOCK) from lectures, compose a system CONCERT_HALL for a concert hall booking system with 2 terminals.
      Hint: use prefix labelling for the LOCK and (composite) SEATS processes so that they can `talk' to both terminals. As in the ||COUNTER example from lectures, it is not actually the prefixed LOCK process that enforces mutual exclusion, it is the acquire ... release discipline in TERMINAL.

3. (Ex 5.4 Magee & Kramer) The dining savages. A tribe of savages eats communal dinners from a large pot which can hold M servings of the meal of the day. When a savage wants to eat, he/she gets a serving from the pot if it is not empty, otherwise they wait. When the pot is empty, the cook refills the pot with M servings. The (unconstrained) behaviour of each savage and the cook can be described by the following FSP processes:

     SAVAGE = (getServing -> SAVAGE).
     COOK = (fillPot -> COOK).
   

   Model the behavior of the pot as an FSP process POT which would impose the respective constraints on the savage and cook processes.
   Hint: POT will have M states.

4. (Ex 5.1 Magee & Kramer) A single-slot buffer may be modelled by
   ONEBUFF = (put -> get -> ONEBUF).
   Outline the code in a Java class OneBuf that implements this as a monitor.
   Hint: for a buffer containing a single integer, it would have a void put(int c) method which could only proceed when the buffer was empty and an int get() method which could only proceed if the buffer had a value in it.

5. (Ex 5.2 Magee & Kramer) Outline how your would re-write the OneBuf to use the Semaphore class from lectures. It can be used as follows

   sema = new Semaphore(v); // create new semaphore with value v (=0,1) 
   sema.down();             // must wait if value is 0 
   sema.up();               // release other threads waiting on this semaphore 
   

   Hint: have 2 semaphores, one to signify full the other to signify empty. Which one should be initially available (value=1)?

6. (Ex 5.4 Magee & Kramer) Outline the code in a Java class Pot which would implement as a monitor the process POT above.

Laboratory Exercises

1. BufferSem.java implements a bounded integer buffer monitor using semaphores. Inspect the file; you will notice that it checks the monitor invariant at the end of every update (why should the check only be at the very beginning or very end of the synchronized block?). The program RunBufferSem.java implements the rest of the bounded buffer. Download both and Semaphore.java and compile. Run the program with assertion checking enabled; let it run for a few seconds before interrupting it:
   java -ea RunBufferSem 10
   Repeat this a few times. If the assertion was violated, the program would have aborted before you interrupted it.

   Now comment out synchronized(this) in both BufferSem methods, recompile, and re-run the program a few times? What do you observe now (and conclude)?

2. Implement and test in Java the single-shot buffer system with a producer thread continually trying to fill the buffer with random integers, a consumer thread continually trying to drain a buffer, and a OneBuf class as a monitor. The threads should print an appropriate message every time they complete a put() or get action.
   Hint: use RunBufferSem.java as a template for the non-monitor part of the system.

3. Repeat this using a Semaphore version.

Homework

1. FSP allows processes to synchronize on the fundamental mechanism of shared actions, e.g. a composite set of processes with the action sync in their alphabets must all engage in this action before proceeding. A set of P threads in FSP performing independent work actions and then synchronizing can be expressed as:
   const P=2
   THREAD = (work -> sync -> THREAD).
   ||THREADS = (forall[p:1..P] thr[p]:THREAD) / {sync / thr[1..P].sync}.
   To model such a synchronization for threads running on a computer (called a barrier synchronization, an important operation in many areas of CDS), each thread will independently arrive at a barrier method, and only when all have arrive, can they all exit. Extend the above system to reflect this.
   Hint: replace sync with barrier.arrive -> barrier.exit. Add a monitor process BARRIER to count when the threads arrive and only allow them to exit when all have done so. When composing the system, the specify the appropriate renaming (barrier.exit will be the shared action corresponding to sync).

2. (Ex 5.5 Magee & Kramer) Write a Java class Barrier which contains a monitor to implement BARRIER.

3. When a Java object is synchronized, the associated lock is recursive: once acquired by a thread, it can be repeatedly required and the lock implementations keeps count of the number of acquisitions. Only when this thread is released the lock for the corresponding number of times can another thread acquire the lock. For example, the following method increments the attribute value of a shared object by n:

     public synchronized void increment(int n) {
         if (n > 0) {
             value++;
             increment(n-1);
         }
     }
   

   If the object's associated lock was not recursive, a thread initially entering the method (and hence acquiring the lock) would block on the recursive call (when it has to re-acquire it).

   (Ex 4.2 Magee & Kramer) Given the following declarations:

     const N = 3
     range P = 1..2
     range C = 0..N
   

   Model a recursive lock as an FSP process RECURSIVE_LOCK which can support up to N levels of recursion for P possible threads. It will have the alphabet {acquire[p:P], release[p:P]} where acquire[p] represents thread p acquiring the lock.