TLA+/PlusCal modeling of Synchronized Round Consensus Algorithm

In my distributed systems class for Fall 17, I assigned modeling of the synchronized round consensus algorithm as the first project. I have been assigning TLA+/PlusCal modeling projects in my class for the last 4 years and releasing the projects and their solutions. I believe this is useful for the distributed systems community, because at this point the barrier before wider adoption of TLA+ tools seems to be the lack of more TLA+ modeling examples of algorithms/systems. My goal is to provide a TLA+/PlusCal example for everything I teach in the class. This way the students will get a hands-on experience in algorithms design and dealing with the intrinsic complexities of distributed systems: concurrent execution, asymmetry of information, concurrency bugs, and a series of untimely failures.

Here is some previous discussion/context about why I started assigning TLA+/PlusCal modeling projects in distributed systems classes.

Timing of the project

I think I timed this project well. In the first month of the semester, I have covered reasoning about distributed programs in terms of safety and progress properties and gave them sufficient introduction to TLA+/PlusCal as well. While the students worked on the project, I covered time/state in distributed systems (logical/vector clocks, distributed snapshots, asynchrony concerns), and distributed mutual exclusion and dining philosophers.

The submission deadline for the project was just before I cover consensus. Working on the project prepared the students to appreciate the challenges of consensus, and primed them about the issues with some hands on practice. So, this is in some sense this is my poor man's implementation of a flipped classroom.

The Project 1 makes unrealistic assumptions of synchronized rounds and reliable channels. Last week I told the students about why and how these needs to be relaxed further, and that made a very nice introduction to Paxos and the failure detectors discussion that comes after.

Synchronized consensus

Every process broadcasts (to all other processes, including itself) its initial value v. In a synchronous network, this can be done in a single "round" of messages. After this round, each process decides on the minimum value it received.

If no faults occur, this algorithm is correct. In the presence of a crash fault, however, a problem can arise. In particular, if a process crashes during a round, some processes may have received its (low) initial value, but others may not have. (Note that the channels are always assumed to be fault-free; they deliver messages reliably once a message is put to the channel.)

Use the template below as your starting point, and fill in the redacted parts. Write and test an invariant property to capture the Agreement property of the consensus protocol. The agreement property should be satisfied when FAILNUM=0, i.e., when no node is allowed to fail. The property will fail to be satisfied when FAILNUM>0. In that case, write in the comments section, after the "================" line, your findings/observations about how the Agreement property is violated.

Extending the algorithm to address crash faults

To address crash faults, consider this simplifying assumption: say that at most 1 process can crash. How can we modify the algorithm to handle such a failure? (Note again that the channels are always fault-free; they deliver messages reliably once a message is put to the channel.)

Answer: by using 2 rounds. In the 1st round, processes broadcast their own initial value. In the 2nd round, processes broadcast the minimum value they heard. Each process then decides on the min value among all the sets of values it received in the 2nd round.

If the one crash occurs during the first round, the second round ensures that all processes have the same set of values from which to decide. Else, if the one crash occurs during the second round, the first round must have completed without a crash and hence all processes have the same set of values from which to decide.

Without knowing/referring-to FAILNUM, modify your first PlusCal algorithm to achieve consensus in the presence of crash faults. The key observation is that if no crash occurs during a round, all processes have the same set of values from which to decide and they correctly decide on the same minimum value.

Future projects

For the second project, I am assigning two phase transaction commit modeling. There are already models of this available from Lamport's webpage, and I ask students to model what happens when the initiator/transaction manager (TM) fails, how would a backup (TM) take over, and what type of problems would arise in an asynchronous system where failure-detection timeouts may fail.

I don't know what projects I will assign next year. Viewstamped replication modeling maybe? Another interesting one would be modeling blockchains and consensus? Feel free to suggest me ideas in the comments or via email.

While the projects may change every year, one thing is invariant: My class enables you to start a lifelong career in modeling, regardless of your looks.  And as I continue my career in modeling, I find that, yes, the night life is pretty exciting: TLA+ has a way of enticing people to burn midnight oil.