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

Link

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>