The Bakery Algorithm: Yet Another Specification and Verification
- Egon Börger ,
- Yuri Gurevich ,
- Dean Rosenzweig
1995 Oxford University Press book, Specification and Validation Methods |
The so-called bakery algorithm of Lamport is an ingenious and sophisticated distributed mutual-exclusion algorithm. First we construct a mathematical model A1 which reflects the algorithm very closely. Then we construct a more abstract model A2 where the agents do not interact and the information is provided by two oracles. We check that A2 is safe and fair provided that the oracles satisfy certain conditions. Finally we check that the implementation A1 of A2 satisfies the conditions and thus A1 is safe and fair.