CMPE436 Assignment3 Solved

Description

Question 1

1. Give examples of multithreaded Java programs where the Lockset based race detection algorithm finds a potential race and another one where it does not find the data race (examples should be different than the lecture notes).
2. Repeat above for Happens-before based data race detection algorithm.

1. Download and install Road Runner tool. https://github.com/stephenfreund/RoadRunner

The tool supports various race detection algorithms including the above two. Use Road Runner to verify races/no races you listed in part a and b.

Question 2- 

The following is a mutual exclusion algorithm for two processes developed by A. Pnueli. The two processes share a boolean variable s which is initially 1, and each process P_i, i = 1,2, has a local variable y_i, which can be read by the other process. The variable y_i is initially 0, variable i contains the process id 0 or 1.

l0: loop forever do

begin

l1:  Noncritical section  l2:  (y_i,s) := (1,i);

l3:  wait until (y_1−i = 0) | (s != i);

l4: Critical section

l5: y_i :=0;

end

 

Here, (y_i,s) := (1,i) is a multiple assignment to variables y_i and s taking place atomically. The variable y_1−i denotes the local variable of the other process.

1. Model this algorithm in Promela and formulate the property of mutual exclusion as LTL formula and check it with Promela. Use never claims in Promela.
2. Check whether Pnueli’s protocol ensures absence of unbounded overtaking, i.e., when a process wants to enter its critical section, it eventually will be able to do so. Provide a counterexample (and an explanation thereof) in case this property is violated.
3. Express in LTL that each process will occupy its critical section infinitely often. Check the property.

SPIN model checker and its documentation is freely available at http://spinroot.com. Use the graphical interface jspin or ispin.

Question 3- 

Consider the system M represented in the transition system below.

• Beginning from state s0, unwind this system into an infinite tree, and draw all computation paths up to length 4 (= the first four layers of that tree).
• Determine whether M, s0 |= φ and M, s2 |= φ hold and justify your answer, where φ is the LTL formula:
  • ¬p → r
  • Ft
  • Fq
  • G (r ∨ q).