[neuronsguy]

I'm including the Gryadka author's rebuttal here, for completeness:

Thank you for the analysis of my post but it seems that you didn't get it correctly. Even to read a value you have to execute the full cycle (prepare, accept) of consensus (in the case of the stable leader we can skip prepare), so when you read the nil value the state of the system will be:

A: (value=foo ballot=1 promised=2) B: (value=nil ballot=2 promised=2) C: (value=nil ballot=2 promised=2)

Not the one you mentioned in the post:

A: (value=foo ballot=1 promised=2) B: (value=nil ballot=0 promised=2) C: (value=nil ballot=0 promised=2)

So the counter example is incorrect.

I proved the algorithm mathematically by hand and used very aggressive property based testing with fault injections so I'm pretty confident in its correctness.

[tschottdorf]

I'm not really on wifi good enough to reply extensively, but I pushed an update to the post explaining this better. If you carry out the read explicitly, you can still get the anomaly in much the same way. I should've done so from the beginning, but I tried to simplify the argument and went too far.