| << Chapter < Page | Chapter >> Page > |
To get started, we revisit the fundamental race condition,
phrased in terms of two processes simultaneously each beingin their critical section.
1 /* An INCORRECT attempt at Mutual exclusion.
2 * Adapted from Ruys 2002: SPIN Beginner's Tutorial.3 */
45 bool flag = false; /* Is some process in its crit section? */
6 int data = 0;7
8 active[2]proctype proc()
9 {10 do
11 :: flag == false ->/* Wait until nobody in crit section. */
12 flag = true;13
14 /* Entering critical section. */15 data++;
16 assert(data == 1);17 data--;
18 /* Leaving critical section. */19
20 flag = false;21 od;
22 }
Take a moment to run SPIN's verifier, and confirm that
the
assert statement indeed might be violated.
Here is another attempt which doesn't work.
Can you see how it might go awry?
1 /* An INCORRECT attempt at Mutual exclusion.
2 * Version 2.3 * Adapted from Ruys 2002: SPIN Beginner's Tutorial.
4 */5
6 bool flagA = false; /* A wants to enter its crit section. */7 bool flagB = false; /* B, similarly. */
8 int data = 0;9
10 active proctype A()11 {
12 do13 :: flagA = true; /* Declare intent to enter crit section. */
14 flagB == false ->/* Wait for B to leave their crit section, if in. */
1516 /* Entering critical section. */
17 data++;18 assert(data == 1);
19 data--;20 /* Leaving critical section. */
2122 flagA = false;
23 od;24 }
2526
27 active proctype B()28 {
29 do30 :: flagB = true; /* Declare intent to enter crit section. */
31 flagA == false ->/* Wait for A to leave their crit section, if in. */
3233 /* Entering critical section. */
34 data++;35 assert(data == 1);
36 data--;37 /* Leaving critical section. */
3839 flagB = false;
40 od;41 }
Again, use SPIN to verify that the assertion can be violated.
(Keep in mind that we can't use
atomic (or
d_step )
here; the entire point of a mutex algorithmis to be able to implement multi-statement atomicity
using nothing but shared memoryand the atomicity of simple-assignment.)
By being substantially more clever though,
interacting flags can be usedto get two processes to share a critical section:
1 /* A correct attempt at Mutual exclusion, huzzah!
2 * Peterson, 1981.3 */
45 bool flagA = false; /* A wants to enter its crit section? */
6 bool flagB = false; /* B, similarly. */7 pid turn; /* For politeness, offer other people a turn. */
8 int data = 0;9
1011 active proctype A()
12 {13 do
14 :: flagA = true; /* Declare intent to enter crit section. */15 turn = 1 - _pid; /* Offer the turn to the other. */
1617 ((flagB == false) || (turn == _pid)) ->18
19 /* Entering critical section. */20 data++;
21 assert(data == 1);22 data--;
23 /* Leaving critical section. */24
25 flagA = false;26 od;
27 }28
29 active proctype B()30 {
31 do32 :: flagB = true; /* Declare intent to enter crit section. */
33 turn = 1 - _pid; /* Offer the turn to the other. */34
35 ((flagA == false) || (turn == _pid)) ->36
37 /* Entering critical section. */38 data++;
39 assert(data == 1);40 data--;
41 /* Leaving critical section. */42
43 flagB = false;44 od;
45 } Processes
A and
B are using their
flags in symmetric ways, and we can certainly factortheir common code to get two instances of the same proctype:
1 /* A correct attempt at Mutual exclusion, huzzah!
2 * Peterson, 1981.3 */
45 bool flag[2] = false; /* Process #i wants to enter its crit. section? */6 pid turn; /* For politeness, offer other people a turn. */
7 int data = 0;8
9 active[2]proctype P()
10 {11 pid me, peer;
1213 me = _pid;
14 peer = 1 - _pid;15
16 do17 :: flag[me] = true; /* Declare intent to enter crit section. */18 turn = peer; /* Politely give others a chance, first. */
1920 ((flag[peer] == false) || (turn == me)) ->21
22 /* Entering critical section. */23 data++;
24 assert(data == 1);25 data--;
26 /* Leaving critical section. */27
28 flag[me]= false;
29 od;30 } A paper proof of this algorithm requires careful thought;
fortunately verifying this with SPIN is much easier.Note that if you wanted to tweak an innocuous line or two
of Peterson's algorithm, without SPIN you'd have toreason extremely carefully
to be sure you didn't lose mutual exclusion.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|