Description

Question 1- (25 points)

a) 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).

b) Repeat above for Happens-before based data race detection algorithm.

c) 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- (50 points)

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 Pi, i = 1,2, has a local variable yi, which can be read by the other process. The variable yi is initially 0, variable i contains the process id 0 or 1.
l0: loop forever do
begin
l1: Noncritical section l2: (yi,s) := (1,i);
l3: wait until (y1−i = 0) | (s != i);
l4: Critical section
l5: yi :=0;
end

Here, (yi,s) := (1,i) is a multiple assignment to variables yi and s taking place atomically. The variable y1−i denotes the local variable of the other process.
a) 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.
b) 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.
c) 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- (25 points)
Consider the system M represented in the transition system below.
(a) 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).
(b) Determine whether M, s0 |= φ and M, s2 |= φ hold and justify your answer, where φ is the LTL formula:
(i) ¬p → r
(ii) Ft
(iii) Fq
(iv) G (r ∨ q).

Guidelines:
1- Email your assignment solution.
2- Add the following to the start of your programs.
// your name // your student ID // your email address
// CMPE436-Assignment n – where n is the assignment number (1, 2, …)
3- Add comments to your programs. Program clarity is very important. You get graded on this.
4- Also add a README.txt file to explain your programs.
6- DO NOT DISCUSS WITH YOUR CLASSMATES. DO NOT USE SOLUTIONS FROM OTHERS. CHEATING WILL NOT BE TOLERATED.