A Semi-Automatic Correctness Proof Procedure applied to Stoller's Leader Election Algorithm
TL;DRAbstract
In 1997, Stoller presented a leader election algorithm for a synchronous system with crash failures. The algorithm is an adaptation of Garcia-Molina's Bully Algorithm that uses failure detectors instead of explicit timeouts. Since the characteristics of the algorithm closely resemble the Bully Algorithm Stoller does not give a formal correctness proof. However, although the algorithms appear similar, there are non-trivial differences. The differences make it unclear if the original proof, by Garcia-Molina, actually carries over as indicated by Stoller. In this document we formalize the leader election algorithm using first-order logic, and prove its correctness with respect to the obvious safety property; it should not be possible to elect two different leaders at the same time.
Chat with Paper
AI Agents for this Paper
In 1997, Stoller presented a leader election algorithm for a synchronous system with crash failures. The algorithm is an adaptation of Garcia-Molina's Bully Algorithm that uses failure detectors instead of explicit timeouts. Since the characteristics of the algorithm closely resemble the Bully Algorithm Stoller does not give a formal correctness proof. However, although the algorithms appear similar, there are non-trivial differences. The differences make it unclear if the original proof, by Garcia-Molina, actually carries over as indicated by Stoller. In this document we formalize the leader election algorithm using first-order logic, and prove its correctness with respect to the obvious safety property; it should not be possible to elect two different leaders at the same time.
Keywords
Chat
Click to start Chat