Names: Pledge: Section:
Code Peterson’s algorithm in Promela:
1 int last = 1;
2 boolean wantP = false; 3 boolean wantQ = false;
1 Thread.start { // P
4 December 2020
Exercise 1
2 3 4 5 6 7 8 9
10
11 }
1 Thread.start { // Q
2 while (true) {
3 // non-critical section
4 wantQ = true;
5 last = 2;
6 await !wantP or last==1;
7 // CRITICAL SECTION
8 wantQ = false;
9 // non-critical section
10 }
11 }
Exercise 2
Show that it enjoys mutex using assertions in spin.
Exercise 3
while (true) {
// non-critical section wantP = true;
last = 1;
await !wantQ or last==2; // CRITICAL SECTION wantP = false;
// non-critical section
}
CS 511 – Quiz 7: Model-Checking/Spin
Show that if lines lines 4 and 5 are interchanged, then mutex does not hold. Show this using assertions in spin.
Submission instructions:
A file q9.zip file containing:
• Exercise 1: A file pet.pml
• Exercise 2: A file pet2.pml and output2.txt with a copy of the text in the upper tight pane from jSpin (indicating there are no errors).
• Exercise 3: A file pet3.pml and output3.txt with a of the offending trail (click on “Guided” to get it)
1