<< 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 n processes

As the comments suggest, references to 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 ( e.g. smallest process ID number ( _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
Note that the particular value ticket == 1 is importantit corresponds toI'm still calculating max of others, and doing so has priorityover anybody entering the process.
in your head, to compare your brain's horsepower with SPIN's steam-engine technology.

Get Jobilize Job Search Mobile App in your pocket Now!

Get it on Google Play Download on the App Store Now




Source:  OpenStax, Model checking concurrent programs. OpenStax CNX. Oct 27, 2005 Download for free at http://cnx.org/content/col10294/1.3
Google Play and the Google Play logo are trademarks of Google Inc.

Notification Switch

Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?

Ask