协定性与终止性是共识算法的两种正交安全属性

[[Multi Paxos靠选主把并发提案竞争简化为主节点单向复制]]里”如何保证过程是 安全的”这个子问题看起来模糊，其实对应分布式理论中两个预定义术语：协定性 （Safety，”所有的坏事都不会发生”）和终止性（Liveness，”所有的好事都终将 发生，但不知道是什么时候”）。以选主为例，协定性要求选主结果一定有且只有 一个主节点，绝不能同时出现两个主节点同时生效；终止性要求选主过程一定会 在某个时刻结束。这两个属性并不总能同时严格保证——正如[[Basic-Paxos的 活锁问题及为何不直接用于工业实践]]描述的，理论上活锁可能导致选主过程 永远无法终止，这正是终止性上的理论瑕疵；但协定性（不会同时出现两个主 节点）是可以被严格证明成立的。这也是为什么Raft论文只正式证明了Safety、 而没有证明Liveness——因为工程实现（引入随机超时打破活锁对称性）能让 终止性问题在实践中几乎不会出现，但理论上无法给出绝对保证。理解这个 区分的价值在于：评价一个分布式算法”安不安全”，要分别检查它在”绝不做 错事”和”最终能做完事”这两个正交维度上分别给出了什么保证，而不是笼统地 问”它安全吗”。