lea -- leader election algorithms & formal verification

[See the Source Code!]

This assignment covered two leader election algorithms (LEAs) on ring topologies -- a class of distributed algorithms tasked with getting every node in a network to agree on a single "leader" using only local message passing, with no central coordinator and no shared memory.

The first algorithm, Chang-Roberts, is the simpler of the two: each node forwards a message only if it carries a higher ID than its own, purging anything lower. Eventually the highest ID makes a full round trip back to its origin, and that node knows it's the leader -- a correct but rather asymptotically slow approach with O(N²) message complexity.

The second algorithm, Dolev-Klawe-Rodeh, improves message complexity to O(N log N) by breaking execution into synchronous phases. Rather than every message racing around the whole ring, each phase lets active nodes compare themselves only against their two nearest active neighbors, promoting local maxima and demoting the rest to passive relays -- shrinking the "contest" by roughly half each round.

Not only were both algorithms implemented, but they also included several checks, verifying two properties held under *all* possible interleavings of message delivery: that the elected leader always has the maximum ID in the ring, and that exactly one leader is ever elected, no matter the ID ordering or timing of messages. Both were encoded as in-model assertions and checked exhaustively by Spin's model checker.

The provided promela source code is best showcased with a spin model checker, perhaps with a GUI like jSpin. For example, to verify the correctness of both algorithms' implementation, open each .pml file in jSpin and click Verify:

Chang-Roberts LEA:

Dolev-Klawe-Rodeh LEA:

This project was completed during the Fall 2024 semester as a challenging, optional extra credit assignment for CS 511 - Concurrent Programming @ Stevens Institute of Technology.