## The bakery protocol

*June 22, 2010 – 6 years, 9 months ago, by vladimir*

### Short Description:

Lamport's bakery protocol: prove the safety property, that no two customers can be in the critical section at the same time.

### Long Description:

The bakery algorithm is a popular textbook algorithm for realising mutual exclusion. It involves a number n of customers that aim to enter a crictical section and the goal is to give a distributed algorithm that guarantees that no two costumers are at the same time in the critical section.

The problem at hand is not a typical theorem-proving task. Verifying protocols is usually the realm of model checkers. But, model checkers can only verify the bakery protocol with a (rather small) limit on the number of customers, and a limit on the ticket size.

### Supplementary Materials:

L. Lamport. A new solution of Dijkstra’s concurrent programming. Communications of the ACM, 17(8):453–455, august 1974.

### Subbmitted by:

Peter H. Schmitt <pschmitt@ira.uka.de>

## Solution 1

### Tool/method

KeY

### Tool version

### Code/spec

Implementation in Java, specified in JML.

### Solution-problem relationship

### Tool output

### Interactivity, effort needed

### How to reproduce

### Published

### Submitted by

Peter H. Schmitt <pschmitt@ira.uka.de>