The Bakery Algorithm

Entering Bakery

Loading Bakery

When loaded..

Generating Invariants

Proving mutual exclusion

Using the proof-editor

Proving overtaking

Using the diagram editor

Using the diagram proof

Proving accessibility

Back to the tutorial pages