A Tiny Issue in "Paxos Made Simple"

[hengxin]

Paxos 采用 maxBal 优化后对 P2c 的影响

在 Paxos Made Simple 中,

在 Phase2b 阶段，自然语言描述的 Paxos 协议没有要求更新 maxBal[a]。然而，可以通过反例（使用 TLC）说明，如果不同时更新maxBal[a]，则 Paxos 并不能保证论文中的不变式 P2c 成立。

写作: A Little Issue in Paxos Made Simple. (arXiv)