Question 1 (15 marks)

The algorithm below attempts to solve the critical section problem for two threads, p and q.  Remember the assumption of the critical section problem that the critical section must progress, and the non-critical section need not progress.

(i) Prove that the algorithm ensures mutual exclusion.  If you require any invariants in your proof, they must appear as lemmas and also be proved. (6 marks)

(ii) Is the following formula an invariant: p6 ∧ (g1 = P) ⇒ ¬(q4 ^ q5 ^ q7). If yes, prove it; otherwise, give a fragment of the state diagram as a counterexample (4 marks)

(iii) Use Linear Temporal Logic (LTL) to state the starvation freedom in this algorithm. Does the algorithm satisfy this property? If yes, prove it; otherwise, give a fragment of the state diagram as a counterexample. (5 marks)

Question 2 (10 marks)

(Spaghetti Sauce Chefs Problem) Consider a scenario with three chef processes and one supplier process. Each chef loops forever, first waiting for ingredients and then making spaghetti sauce. The ingredients are meat, oil and salt. One of the chefs has infinite amount of meat, another has infinite amount of oil and the third has infinite amount of salt. The supplier has infinite amount of all three ingredients.

The supplier repeatedly places two different ingredients at random on the table.  The chef who has the complementary ingredient then picks up them and makes sauce.  For example, if the supplier puts out meat and salt, the chef who has the oil will pick up both ingredients.

(i) First, assume the supplier notifies the chef who has the complementary ingredient. Solve this synchronisation problem with semaphores. Any semaphore used must be a weak semaphore, i.e., the processes  blocked on the semaphore are in a set, not a queue. Use language-independent notation. Clearly state your assumptions if any. (4 marks)

(ii) Now,  the following restriction  is  imposed:   the  supplier  does not notify the  chef who has the complementary ingredient.  Solve this problem with semaphores.  Any semaphore  used  must  be  a  weak  semaphore,  i.e.,  the  processes  blocked  on  the semaphore are  in  a  set,  not  a  queue.  Use  language-independent  notation.  Your solution must be deadlock-free. Clearly state your assumptions if any. (6 marks)

Question 4 (12 marks)

Danielle is writing a concurrent program to operate a shared linked list data structure. To achieve mutual exclusion, she selects to use fine-grained synchronization to synchronize    the access to objects. By following the standard implementation of fine-grained                    synchronisation as we introduced in the lecture, Danielle implements the data structure  of each node and function add() as below.  Unfortunately, she implements an incorrect   hashcode generator which causes the hashcode of each node to not be unique.

1      //  Data  structure  of  each  node

2      public  class  Node<T>  {

3                    T  item;

4                    int  key;

5                    Node<T>  next; 6      }

1      //  Standard  fine-grained  sychronization  -  add

2      public  boolean  add  (T  item){

3                    Node<T>  pred,  curr;

4                    int  key  =  item .hashCode();

5                    head .lock();

6                    try  {

7                                 pred  =  head;  curr  =  pred .next;

8                                  curr .lock();

9                                 try  {

10                                               while  (curr .key  <  key)  {

11                                                            pred .unlock();

12                                                            pred  =  curr;  curr  =  curr .next;

13                                                             curr .lock(); 14                                               }

15                                               if(key  ==  cyrr .key)  {

16                                                            return  false ;

17                                               }

18                                               Node<T>  newNode  =  new  Node<T>(item);

19                                               pred .next  =  newNode;

20                                               newNode .next  =  curr;

21                                               return  true ; 22                                 }

23                                 finally  {

24                                               curr .unlock(); 25                                 }

26                    }

27                    finally  {

28                                 pred .unlock(); 29                    }

30      }