<< Chapter < Page | Chapter >> Page > |
A different algorithm for mutual exclusion, the Bakery algorithm, can be thought of as having a roll of sequentially-numbered tickets;when a process wants access to the critical section (the bakery clerk),they take a number, and then look around to be sure they have the lowest ticket number of anybody, before striding up to the counter.The tricky bit is thattaking a numbermeans both copying the value of a global counter, and updating that counter,in the presence of other processes who might be doing so simultaneously.It seems like it's begging the question, to even do that much!
Promela code for a two-process implementaton of the Bakery algorithm is below; it can be generalized to processes
ticket[peer]
must
be replaced by looping to find the maximum ticket-number amongall peers. Moreover, it becomes possible for two processes to
grab the same ticket-number in this way.This situation has to be checked for, and some way of breaking ties
included (
_pid
) wins).1 /* A correct attempt at Mutual exclusion.
2 * Lamport's "Bakery algorithm"3 * Procs which communicate only through ticket[].4 */
56 byte ticket[2]; /* `byte' ranges from 0..255. Initialized to 0. */7 int data = 0;
89 active [2] proctype customer()10 {
11 pid me = _pid;12 pid peer = 1-_pid; /* Special case for 2 procs only. */
1314 skip; /* Doing some non-critical work... */
1516 ticket[me] = 1; /* Declare desire to enter crit section. */17 ticket[me] = ticket[peer]+1; /* In general: max(all-your-peers)+1. */
18 ((ticket[peer]== 0) || (ticket[me]<ticket[peer])) ->19
20 /* Entering critical section. */21 data++;
22 assert(data == 1);23 data--;
24 /* Leaving critical section. */25
26 ticket[me]= 0; /* Relinquish our ticket-number. */
27 }28
2930 /* The meaning of ticket[], for each process:31 * ticket[me]==0 means I am not contending for crit section.32 * ticket[me]==1 means I am in the process of taking a ticket33 * (I am looking at all other ticket holders)
34 * ticket[me]>1 means I have received a ticket and will
35 * enter the critical section when my turn comes up.36 *
37 * A problem still present, when trying to generalize to>2 procs:
38 * Two procs may choose the same ticket-number;39 * when nobody has a smaller ticket than you, check them all for equal tix;
40 * must break any ties reasonably (eg by smaller _pid).41 *
42 * It's a bit sneaky, that 0 and 1 have special meanings43 * (and the fact that 1 is less than any other "valid" ticket-number
44 * is important -- while anybody is calculating their ticket,45 * nobody else will enter the critical section.
46 * This inefficiency can be avoided by being cleverer.)47 */
SPIN can be used to verify this code.
But it is worth taking the time to reason through the code
ticket == 1
is
importantit corresponds toI'm still calculating max of others,
and doing so has priorityover anybody entering the process.Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?