Safety of the Synod algorithm

The Synod algorithm is the one-decree foundation of the Paxos distributed consensus algorithm.

I’m of the school of thought that you can’t really understand an algorithm without understanding the proof of why it works correctly. The clearest proof that I know of for why the Synod algorithm works is in Paxos made simple, but even that is not all that clear. Here’s an illustrated presentation of that proof that helped me to understand it better. It’s a fairly informal outline of the proof, but there is a more formal version in Appendix B of the Unbounded pipelining in Paxos paper that shows there are no gaps in this argument.

Proof

Suppose values have been learned for terms P and Q:

It is simplest to argue by contradiction so suppose that the values for these terms are distinct and denote them respectively X and Y:

Learned values must have been proposed, so this means that value X was proposed in term P and value Y was proposed in term Q by sending proposed (a.k.a. phase 2a) messages:

It may be that values were proposed in terms between P and Q too:

Find the earliest term R later than P but no later than Q in which a proposal was made whose value is not X:

R must exist since the proposals made in terms P and Q had different values. Put differently, all the proposals made in terms earlier than R but no earlier than P have value X:

The value in term P must have been learned because a majority S of acceptors sent acceptance (a.k.a. phase 2b) messages:

Also, the value in term R was proposed because of promises from another majority of acceptors:

Since these majorities overlap, there is at least one node a which belongs to both sets: it accepted a value in term P and then sent a promise for term R. It must have happened in that order as, having sent a promise for term R, a would then not have been able to accept a value in term P since P < R:

Of course a may also have accepted some proposals in terms later than P before sending a promise for term R, but in any case, the highest-numbered term accepted by a before it sent its promise for term R is no earlier than P and is strictly earlier than R, and therefore has value X:

Therefore when a sent its promise for term R, the promise must have included the last-accepted term which is no earlier than P and is strictly earlier than R, and whose value is therefore X.

Other nodes also sent promises for term R and some of these may have included a previously-accepted term, all of which are strictly less than R:

In any case, the value proposed in term R must be the value of the promise with greatest last-accepted term, which must be X as the greatest last-accepted term is no earlier than P and is strictly earlier than R. This means that R didn’t have a different value from P, which is a contradiction, so the original assumption that P and Q had different values was wrong, as required.