Objectives

• To improve your understanding of Peterson's algorithm (low-level modelling of mutual exclusion).
• To improve your understanding of safety and progress properties, and the underlying issues in concurrency.
• To improve your understanding of ow these properties can be implemented in a monitor.

Preparation

• revise the exercises in the previous session, 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 (7) of the Magee&Kramer.
• follow this up by studying with the LTSA tool some examples from Chapters 7 of the textbook. Suggested examples are SingleLaneBridge and ReadersWriters.
• remember to bring a pen and paper for the Tutorial Exercises.

Tutorial Exercises

1. Discuss any outstanding issues from the previous session (including Homework). Raise any questions related to Assignment 1 and discuss.

2. (Ex 7.1 Magee & Kramer) What action trace violates the following safety property?

   property PS = (a -> (b -> PS | a -> PS) | b -> a -> PS).
   

3. (Ex 7.3 Magee & Kramer) Consider the car park example from Chapter 5:

   CARPARKCONTROL(N=4) = SPACES[N],
   SPACES[i:0..N] = ( when(i>0) arrive -> SPACES[i-1]
                    | when(i<N) depart -> SPACES[i+1]
                    ).
   ARRIVALS   = (arrive -> ARRIVALS).
   DEPARTURES = (depart -> DEPARTURES).
   
   ||CARPARK = (ARRIVALS || CARPARKCONTROL(4) || DEPARTURES).
   

   Specify a safety property that asserts that the car park does not overflow. Specify a progress property which asserts that cars eventually enter the park. If car departure has lower priority than car arrival, does starvation occur? Specify an FSP composition with action priority that you could use to check this (via LTSA's Check Property facility).

4. Consider the FSP model of Petersen's algorithm that we developed in TuteLab-4. Recall that the trace for thread 0 through the cycle, assuming it got immediate access to its critical region, would:

    
   t0.noncrit.enter -> t0.noncrit.exit -> 
   t0.inCS0.write[1] -> t0.turn.write[1] ->            
   t0.inCS1.read[0] -> t0.turn.read[0] ->
   t0.crit.enter -> t0.crit.exit -> t0.inCS0.write[0]
   

   and similarly for Thread 1.

   1. What sequence of events (actions) would indicate that mutual exclusion was violated in the system?

   2. Specify an FSP safety property which expresses that mutual exclusion is preserved. Write a composition of that property with the other processes; why is it necessary to extend the alphabets for thread 0 and thread 1?

   3. Describe a sequence of events (actions) that would indicate that one thread is being starved of entry into its critical region?

   4. Specify an FSP progress property which states that, once a thread is waiting to enter its critical region, it will eventually be allowed to enter.

Laboratory Exercises

1. Verify using the LTSA tool that the CarPark safety and progress properties are kept.

2. Verify using the LTSA tool that your model of Peterson's Algorithm satisfies its safety and liveness properties. (if not already done so). What does this prove about (our implementation of) Peterson's Algorithm?

3. Time to start driving some applets! Download and unzip the Book Applets zip file. Go to the book_applets sub-directory and run the applet:
   appletviewer ReadWriteFair.html &
   Give the Readers low priority (sliders to left) and Writers high priority; start the Writers first. You will (hopefully) notice that the Readers can still be starved! This is because ReadWriteFair.java in concurrency/readwrite is still not fully fair to the readers!!! Your task is to edit this to fully implement the fair(er) RW_LOCK monitor (which has an added requestRead action and an added waitingR component to the RW_LOCK state, see below). Note that you do not explicitly implement the requestRead action in the monitor (in the same way as the requestWrite action is not explicitly implemented in the existing code. Compile your file from the book_applets sub-directory:
   javac concurrency/readwrite/ReadWriteFair.java
   and re-run the applet as above to check that you have properly implemented this. Also check the converse situation with Readers having high priority to see that the Writers now don't get starved.
   Hint: you only need to implement the waitingR component of RW_LOCK; all of the other 4 components are already implemented in the code.
   Note: to re-run the applet, you may need access the applet via your browser, as appletviewer on the CS student system is rather broken. To do this, open the File Manager in the book_applets sub-directory and double click on ReadWriteFair.html .

   RW_LOCK = RW[0][False][0][0][False],
   RW[readers:0..Nread][writing:Bool]
      [waitingW:0..Nwrite][waitingR:0..Nread][readersturn:Bool] =
       ( when (!writing && (waitingW==0||readersturn)) 
           acquireRead ->  RW[readers+1][writing][waitingW][waitingR-1][readersturn]
       | releaseRead ->    RW[readers-1][writing][waitingW][waitingR][False]
       | requestRead ->    RW[readers][writing][waitingW][waitingR+1][False]
       | when (readers==0 && !writing && (waitingR==0||!readersturn)) 
           acquireWrite -> RW[readers][True][waitingW-1][waitingR][readersturn]
       | releaseWrite ->   RW[readers][False][waitingW][waitingR][True]
       | requestWrite ->   RW[readers][writing][waitingW+1][waitingR][readersturn]
       ).
   

Challenge Problem!