> If you look at _Lamport's paxos proofs_ he treats an accept as a promise... But this is not pointed out in _Paxos Made Simple_. In fact, it appears Lamport took great pains to specify that an accept was not a promise.
> The problem is when you combine the weaker portions of both variants; as the OP did and several implementations do. Then you run into this catastrophic bug.
That is, Lamport's proofs and Paxos Made Simple contradict each other ever so slightly to trip everyone all at the same time:
> What's more I looked through several proprietary and open-source paxos implementations and they all had the bug submitted by the OP!
Lamport acknowledges the report, not the error. I'm still not convinced there even is an error.
The state after step 9 should be the same as after step 7, i.e. `A(-:-,100) B(100:b,100) C(100:b,-)` because C needs to retain the "highest-numbered proposal" it accepted, not the one it accepted last. That means the nine steps outlined in the post/on StackOverflow do not, by themselves, demonstrate any problem.
So what additional steps are missing/what alternative steps actually produce an inconsistency/divergence?
There isn't an "error" / "bug" in either papers when one looks at them in isolation. Together, they seem to have a very subtle difference in the algorithm to trip most distributed systems practioners.
> If you look at _Lamport's paxos proofs_ he treats an accept as a promise... But this is not pointed out in _Paxos Made Simple_. In fact, it appears Lamport took great pains to specify that an accept was not a promise.
> The problem is when you combine the weaker portions of both variants; as the OP did and several implementations do. Then you run into this catastrophic bug.
That is, Lamport's proofs and Paxos Made Simple contradict each other ever so slightly to trip everyone all at the same time:
> What's more I looked through several proprietary and open-source paxos implementations and they all had the bug submitted by the OP!
https://stackoverflow.com/questions/29880949/contradiction-i...
Lamport himself acknowledges as much: https://www.youtube.com/watch?t=4398&v=8-Bc5Lqgx_c