1. Introduction

This draft presents an introduction to CPU syncronization algorithms with empasys on mutual exclusion problems. You can extract the code contained in text with:

./tex2code.pl < mutex.tex

That will create 3 files: dekker.busywait, dekker.blocking, and bakery.

2. Critical sections and mutual exclusion

The problem of mutual exclusion can be stated as: given at least two concurrent process, sharing a resource, one must must provide for the mutually exclusive access to the resource: at most one process is accessing the resource at any given time. There are many solutions, each one tries to guarantee, at least:

• mutual exclusion;

• deadlock absence;

• liveness. Any solution must be valid under any interleaving of steps.

3. Dekker’s solution

In this section, we use Pomella, the language of spin, to model a version of the Dekker’s solution for the mutual exclusion problem, when two processes are involved. To understand the solutions is important to remember that the semantics of Pomella assumes:

• each statement is atomic;

• send/receive are blocking;

• any boolean statement until it is true;

• the do–od and if–fi commands are nondeterministic;

• if the only statement for a process to execute is blocked then the whole process blocks.

3.1. A busy wait solution. The first soultion is borrowed from [?]. The do–od in the user process implements a busy wait. Extract the code from this document and run it under xspin to discover that this solution does not ensure progress under any interleaving. Why? Is the version of the Dekker’s solution presented by [?] incorrect?

1 #define true 1
2 #define false 0
3 bool in[2];
4 bool c[2];
5 int turn;

6 7

 8 proctype user(int i)
 9 {
10  int next;

11

12  next  = (i+1) % 2;
13  c[i]=true;
14  turn = next;

15

16  do
17  :: c[next] && turn != i ->
18 accept: skip;
19  :: !c[next] || turn==i ->
20 progress: break;
21  od;

22

23  in[i]=true;
24  assert(in[next]==false);
25  in[i]=false;
26  c[i]=false;

27 }

28 29 30

31 init

32 {

33  c[0]=false;c[1]=false;
34  turn=0;
35  in[0]=false;
36  in[1]=false;
37  atomic{
38  run user(0);
39  run user(1);

40 } 41 }

42

3.2. A solution with blocking. In this section, we avoid the problems with interleaving by forcing one process to yield the processor when it finds that it cannot enter its critical section. The statement (!c[next] —— turn == i);

suspends process i until one C[next] or (turn==i) is true.

 1 #define true 1
 2 #define false 0
 3 bool in[2];
 4 bool c[2];
 5 int turn;

6 7

 8 proctype user(int i)
 9 {
10  int next;

11

12  next  = (i+1)%2;
13  c[i]=true;
14  turn = next;
15  (!c[next] || turn == i);
16 progress:
17  in[i]=true;
18  assert(in[next]==false);
19  in[i]=false;
20  c[i]=false;

21 }

22 23 24

25 init

26 {

27  c[0]=false;c[1]=false;
28  turn=0;
29  in[0]=false;
30  in[1]=false;
31  atomic{
32  run user(0);
33  run user(1);

34 } 35 }

37 38

4. The bakey algorithm

The bakery algorithm was introduced by Leslie Lamport in the 1974, and is certainly a classic in Computer Science. It is a solution for the mutual exclusion problem that contemplates the case when more than one process compete for the same resource.

A constant NP is introduced to define the number of processes. Each process i uses two variables:

• chossing[i] that is used to mark the beginning and ending of the ticket acquisition phase: region delimited in try(i).

• number[i] to hold a ticket number.

 1 #define true 1
 2 #define false 0
 3 #define NP 3

4

 5 bool choosing[NP];
 6 byte number[NP];
 7 byte count;

8

Process i chooses a ticket number in try(i), and it is the maximum ticket of all processes incremented by one.

 9 inline try(i){
10  choosing[i]=true;
11  int j,mx;
12  mx=number[0];
13  j=0;
14  do
15  :: j==NP -> break;
16  :: j<NP && mx<number[j] -> mx=number[j];j=j+1;
17  :: else -> j=j+1;
18  od;
19  number[i]=mx+1;
20  choosing[i]=false

21 }

Given a ticket number[i], process i passes door(i) and enters the critical section if it it has a better ticket number than any other competitor. A ticket cannot be compared if its owner is still acquiring it, try region.

22 inline door(i){
23  int j;
24  j=0;
25  do
26  :: j<NP -> (!choosing[j]);
27  (number[j] == 0 ||
28  number[i]<number[j] ||
29  (number[i]==number[j] && i < j));
30  j=j+1;
31  :: j==i -> j=j+1;
32  :: j==NP -> break;
33  od

34 }

A process leaves the critical section by returning its ticket number to zero.

35 inline exit(i){
36  number[i]=0

37 }

The proctype user models processes that would use the bakery algorithm to achieve mutual exclusion. The variable count is used to assert that the number of processes in the critical section is less than 2.

38 proctype user(byte i)

39 {

40  try(i);
41  door(i);

42

43 progress:
44  count=count+1;
45  skip;
46  count=count-1;
47  exit(i)

48 }

49

Process monitor implements an invariant for the system asserting that either 0 or 1 process is in the critical section.

50 proctype monitor(){
51  assert(count == 0 | count == 1);

52 }

Process init starts NP copies of user and one copy of monitor.

1 init{
2  count = 0;
3  atomic{
4  int j;
5  j=0;
6  do
7  :: j<NP -> run user(j); j=j+1;
8  :: else break;
9  od;
10  run monitor();

11 } 12 }

13

5. The Joint Smokers problem

Bill, Osama and Yasser would like to forget old differences, and smoke the pot of peace. The problem is that each one of them needs pot, wrapper, and matches, and if they don’t get them from time to time, they may start plotting new wars in the name of God and freedom. Now, Bill has got the pot (of course), Osama will always have the matches, and poor Yasser has bad quality wapper. There come George, Tony, and Ariel and they seem to have the solution for this much unbecoming situation. George produces pot and matches (and guns, in case you need them); Tony supplies matches and wrapper (well... and guns; you would never know when you need them with all these arabs and latin americans around); Ariel supplies wapper and pot (and, of course, he is great at burning guns and bloody arab meat. And jewish meat as well. Why not? What if you must burn a few thousand of your own just to ensure that even more of the other kind get killed?) Can you help Bill, Osama and Yasser to get supplies from the three God’s angels to start getting comfortably numb? Use a strong semaphores in your solution. Can you improve this game to find a part for Fernando, where he does not play the joker? And if Osama and George decide to renew old family ties and restart their old sacred association for selling guns and oil? Can you find them a market before they burn us all?

References

[1] Abraham Silberschatz, Peter Baer Gavin, and Greg Gagne, Operating system concepts, sixth ed., John Wiley & Sons, Inc., New York, 2002.