CS511 – Concurrent Programming Exercise Booklet 9
Concurrent Programming
Exercise Booklet 9: Promela and Spin1
Solutions to selected exercises (♦) are provided at the end of this document. Important: You should first
try solving them before looking at the solutions. You will otherwise learn nothing. 1 Basic Promela
Exercise 1. (♦) Implement the following entry/exit protocol (Attempt I) seen in class, in Promela. Use the Promela code in the slides as an aid in understanding Promela syntax.
1 int turn = 1;
Exercise 2.
Draw the transition system of the following two programs separately and then compare them (note: you can use SpinSpider as a guide):
Thread.start { // P while (true) {
} }
await (turn==1);
turn = 2;
Thread.start { // Q while (true) {
await (turn==2);
turn = 1;
} }
2
4
6
2
4
6
% Program 1
byte state = 1; 2 active proctype A(){
atomic { 4 (state==1) ->
state = state +1 6
} 8}8
% Program 2
byte state = 1; active proctype A(){
(state==1) -> state = state +1
}
active proctype B() {
(state==1) -> state = state -1
}
active proctype B() { atomic { 10
(state==1) -> state = state -1
}
Exercise 3. Check whether the following algorithm guarantees mutual exclusion by adding an auxiliary variable critical and appropriate statements. Do you recognize this algorithm?
1Sources include: http://www.cs.toronto.edu/~chechik/courses01/csc2108/lectures/spin.2up.pdf 1
10
12
14
}
bool flag[2] bool turn
active [2] proctype user () {
flag[_pid] = true turn = _pid
8
10
12
2
4
6
8
10
Exercise 4. What happens in the previous algorithm if you exchange the line flag[_pid]= true with the line turn = _pid?
Exercise 5. Consider the following simplified presentation of the Bakery Algorithm for two processes: int np,nq =0;
CS511 – Concurrent Programming Exercise Booklet 9
(flag[1-_pid] == false || turn == 1-_pid) crit: skip // critical section
}
flag[_pid] = false
Thread.start { // P 2 while (true) {
// non-critical section 4 np = nq + 1;
await nq==0 or np<=nq; 6 // CRITICAL SECTION
np = 0; 8
// non-critical section
} 10 }
Thread.start { // Q while (true) {
// non-critical section nq = np + 1;
await np==0 or nq
sem–
} }
inline release(sem) { sem ++
}
Answer to exercise 9
• Init sends qforb to A on qname
• A sends 123 to qforb
• B receives 123 on qforb and prints it
Answer to exercise 10
#define acquire 0
#define release 1
chan sema = [0] of { bit }; proctype semaphore () {
byte count = 1; do
:: (count == 1) -> sema!acquire; count = 0
:: (count == 0) -> sema?release; count = 1 od
}
proctype user () { do
:: sema?acquire;
/* crit. sect */
sema!release;
/* non-crit. sect. */
od }
init {
1
3
5
7
9
11
13
15
17
19
5
CS511 – Concurrent Programming
Exercise Booklet 9
run semaphore (); run user ();
run user ();
}
21
23
6