Towards an Automatic Proof of the Bakery Algorithm

Aman Goel, Stephan Merz, Karem Sakallah

Abstract

The Bakery algorithm is a landmark algorithm for ensuring mutual exclusion among N processes that communicate via shared variables. Starting from existing TLA+ specifications, we use the recently-developed IC3PO parameterized model checker to automatically compute inductive invariants for two versions of the algorithm. We compare the machine-generated invariants with human-written invariants that were used in an interactive correctness proof checked by the TLA+ Proof System. Our experience suggests that automated invariant inference is becoming a viable alternative to labor-intensive human-written proofs.

Available as: PDF

Reference

@InProceedings{goel:bakery,
  author =       {Aman Goel and Stephan Merz and Karem Sakallah},
  title =        {Towards an Automatic Proof of the {Bakery} Algorithm},
  booktitle = {43rd IFIP WG 6.1 Intl. Conf. Formal Techniques for Distributed Objects, Components, and Systems},
  year =      2023,
  editor =    {Marieke Huisman and Ant{\'o}nio Ravara},
  volume =    13910,
  series =    {Lecture Notes in Computer Science},
  pages =     {21-28},
  address =   {Lisbon, Portugal},
  publisher = {Springer},
}