分布式共识

每个进程只有局部消息前缀，却要作出全局唯一且不可撤销的决定。早决定可能漏掉相反提议，永久等待又违背终止。协议把安全证据做成跨轮次可继承的投票记录，并把活性押在某种最终协调条件上。

多数相交只提供证据相遇的机会。交点进程若可以在两个轮次无条件支持不同值，两个多数仍可能分别批准冲突结果；ballot、任期、锁定或继承规则才决定交点携带什么。

二值共识中，“总决定 $0$”满足完整性、一致性和终止性，却在所有进程输入 $1$ 时违反有效性。相反，“决定自己输入”满足有效性与终止性，却在不同输入执行中违反一致性。三类性质排除了两种平凡逃避。

三个投票者 $A,B,C$ 展示 quorum 仍需状态规则。若第一轮 $A,B$ 都投 $x$，第二轮 $B,C$ 又可无条件投 $y$，则多数 $\{A,B\}$ 与 $\{B,C\}$ 虽在 $B$ 相交，$x,y$ 仍分别获多数。安全协议必须让 $B$ 的旧证据约束第二轮提案，或禁止它作不相容投票。

两阶段提交公理库两阶段提交Two-phase commit · 2PC协调者先收集准备结果再统一决定提交或中止的原子提交协议。决定分布式事务提交或中止，prepared 参与者在协调者故障后可能阻塞。用共识复制提交决定可消除单协调者这一故障点，但 2PC 本身没有在异步 crash 模型中提供 nonblocking consensus。

FLP 不可能性公理库FLP 不可能性定理FLP impossibility · Fischer–Lynch–Paterson theorem完全异步系统中即使只允许一个进程崩溃，也不存在保证所有可容许执行终止的确定性共识协议。说明完全异步、确定性、可靠消息且允许一次 crash 时，某个可容许调度可以永不决定。Paxos公理库PaxosPaxos consensus通过相交 quorum、递增 ballot 与已接受值继承规则，在崩溃故障下为单个共识实例选择唯一值。与Raft公理库Raft 共识协议Raft consensus algorithm以任期、选主和复制日志实现崩溃容错共识的协议。仍能在所有这类时序下保持安全；它们的终止证明另加稳定领导、可达多数与部分同步条件。拜占庭共识又需更大交集与认证假设，不能把 crash 多数公式直接搬过去。

消息传递中，最终领导者检测器 $\mathrm{\Omega }$ 刻画异步 crash consensus 所需的最终协调信息；Paxos、Raft 与 Viewstamped Replication 把一系列实例填入复制日志。共享内存的共识数层级则按对象类型能为多少进程 wait-free 地解共识分类原语，执行模型与可用对象不同，不能直接沿用消息阈值。

共识与原子广播公理库原子广播Atomic broadcast · Total-order broadcast所有正确进程以同一总序交付广播消息。在固定成员、可靠通信和相同 crash/终止假设下相互归约。原子广播到共识：广播各自提议并决定第一条全序交付消息。共识到原子广播：可靠传播待排序消息，按日志索引反复调用共识决定下一批，并用确定规则排列批内消息；终止还要保证待处理消息不被永久饿死。等价指可解性相互归约，不表示一个 one-shot 实例自动提供无限日志。

协议验证常把 agreement 化为配置上的归纳不变式，把 termination 写成对公平无限执行的性质。模型检查可以找出双决定或永不进展的调度，却不能替规格补入遗漏的公平性与故障上界。