STeP Basic Tutorial
Bakery

The Bakery Algorithm

The program text below shows BAKERY[2], a program that implements Lamport's bakery algorithm for mutual exclusion. Two processes, P1 and P2, coordinate access to a critical section, where at most one process should reside at any given time. Deciding which process enters the critical section is similar to serving customers at a bakery, where the processes are the customers and the baker is the critical section, which can serve only one customer at a time. Each process selects a ``ticket number'' in y₁ and y₂, as the customers in a store would, and the process with the lowest number is allowed to enter the critical section. This is an infinite-state program, since the value of the integer variables y₁ and y₂ may grow arbitrarily large. A ticket with value 0 means that the respective process is not interested in accessing the critical section.

Program Bakery[2]

This informal description of the algorithm can be made precise if the system and its properties are modeled formally. The properties we would like to show are:

Mutual exclusion: control is never at locations l₃ and m₃ at the same time.
One-bounded overtaking: if one process wants to enter the critical section, the other process can enter the critical section at most once before the first one does.
Accessibility: if control resides at l₁ (resp.m₁ ), it will always eventually reach l₃ (resp. m₃). That is, once a process has expressed interest in entering the critical section, it will eventually do so.

Note that it is not immediately clear, from observation of the program, which of these properties hold. In fact, early solutions to mutual exclusion suffered from starvation, where a process could forever be denied access to the critical section, and other solutions do not satisfy one-bounded overtaking. The Bakery algorithm was the first solution that satisfied the three main properties above for the general N-process case.

step-comments@cs.stanford.edu

Last modified: Wed Jul 1 21:03:59 PDT 1998

STeP Basic Tutorial Bakery

The Bakery Algorithm

STeP Basic Tutorial
Bakery