- 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).
- Repeat above for Happens-before based data race detection algorithm.
- 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.
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
l1: Noncritical section l2: (yi,s) := (1,i);
l3: wait until (y1−i = 0) | (s != i);
l4: Critical section
l5: yi :=0;
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.
- 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.
- 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.
- 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.
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
- G (r ∨ q).