Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

Tutorial 4: veriication

CSSE7610

The second exercise below is from chapter 4 of M. Ben-Ari PTinCiples  of con- CUTTent  and DistTibUted PTogTamming  (second edition), 2OO6.

1.  consider the following algorithm for the critical section problem which gives priority to process p over process q.

(a) provide a proof by induction that the algorithm ensures mutual ex- clusion.  If you require other invariants in your proof, they must appear as lemmas and also be proved by induction.

(b) prove whether or not the algorithm ensures freedom from starvation for process p, and also whether or not it ensures freedom from starvation for process q.

2.  prove that mutual exclusion is satisied by the following algorithm by encoding it in promela and running a spin veriication in safety mode. Note that the if statement is atomic.

Using spin, ind a scenario showing that the algorithm is not correct if the if statement is not atomic.