CMPE 436: Assignment 3 Solved

CMPE 436: Assignment 3  


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.

5-  Demo your homework to the instructor. Bring your laptop.

6-  DO NOT DISCUSS WITH YOUR CLASSMATES. DO NOT USE SOLUTIONS FROM OTHERS. CHEATING WILL NOT BE TOLERATED.