Objectives

• To consolidate your understanding of parallel composition and mutual exclusion and monitors.
• To improve your understanding of Peterson's algorithm (low-level modelling of mutual exclusion).
• To improve your understanding of how deadlock arises.

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 (5, 6) of the Magee&Kramer.
• follow this up by studying with the LTSA tool some examples from Chapters 5 and 6 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 SYS (printer-scanner), DINERS (including the deadlock free version), SingleLaneBridge (including the congested and deadlock versions_.
• 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 6.2 Magee & Kramer) Consider the Dining Philosopher problem.

   PHIL = (sitdown -> right.get -> left.get
           -> eat -> left.put -> right.put  -> arise -> PHIL).
   FORK = (get -> put -> FORK).
   ||DINERS(N=5) = forall [i:0..N-1] 
                  (  phil[i]:PHIL 
                  || {phil[i].left, phil[((i-1)+N)%N].right}::FORK).
   

   One solution permits only 4 philosophers to sit down at any time. Specify a BUTLER process which, when composed with DINERS, implements this, i.e. permits a maximum of four philosophers to engage in a sitdown action before an arise action occurs. Specify an extended sysem, being the composition of the diners with the butler process.
   Show your solution to your tutor when done. Worth 1 Prac Point.

3. Consider the modelling of Peterson's algorithm as an FSP process.
   
   Model the algorithm in FSP, capturing the essential characteristics for mutual exclusion.

   Hint: seperate FSP processes will model each thread. For thread 0, model the execution of the critical and non-critical regions by the actions t0.crit.enter, t0.crit.exit and t0.noncrit.enter and t0.noncrit.exit (and similarly for thread 1). The other actions are the reading and writing of the turn, inCS0 and inCS1 variables. These can be modelled as {t0,t1}::turn:VAR etc, using a simplified version of the VARIABLE process for TuteLab-1.
   

     VAR  = VAR[0],
     VAR[i:0..1] = ( read[i] -> VAR[i]
                   | write[j:0..1] -> VAR[j] ).
   

   The if-else construct will be useful for modelling the sub-process corresponding to the while loops, e.g.
   ... -> t0.turn.read[t:0..1] -> if (t==...) then ... else ...
   Note that the processes modelling each thread share no common actions; they however communicate though the shared variables {t0,t1}::turn:VAR etc, i.e. after t0.turn.write[1], when thread 1 offers the choice of actions t1.turn.read[t:0..1], it will only be able to engage in t1.turn.read[1], i.e. t==1.
   Finally, while thread 0 never engages in inCS1.write[0..1] or turn.write[0], it must have its alphabet extended to include these: otherwise it cannot prevent {t0,t1}::inCS1:VAR or {t0,t1}::turn:VAR in freely engaging in these actions! (and similarly for thread 1). It is cleanest to extend them with the suitably prefixed alphabets of the variables. The alphabet of the variables is:
   set VarAlpha = {{turn, inCS0, inCS1}.{read[0..1], write[0..1]}}
   as this stops spurious read actions as well. Alphabet extension can be done by adding by the set of extended events (+ { ... }) just before the full stop (.) in the processes' definition.

Laboratory Exercises

1. *In the (terminal-based) Dining Philosopher's program:
   1. Inspect the file; note how the monitor (array of Fork) is implemented.

   2. Compile and run the program. Verify that deadlock occurs. The usage is
      java RunPhilosophers r
      where the ratio 0.0≤r≤1.0 (default value 1.0) influences how quickly deadlock is likely to occur (r=0.0 fastest).

   3. Modify the Philosopher classes so that the odd numbered philosophers pick up their forks in the opposite order. Check that this does not deadlock.

   4. *Using the original Philosopher class, implement the Butler as part of the monitor. Check that this does not deadlock.
      Show your solution to your tutor when done. Worth 1 Prac Point.

2. Verify using the LTSA tool that your implementation of the Dining Philosophers with a Butler is deadlock free (if not already done so).

Homework