分布式系统 · 观点 01

超越理想路径的共识:安全性、进展与法定人数的代价

法定人数集合相交是安全性的一个要素;及时取得进展则需要另一种论证。

引用本文

AI 译文可能存在错误,请对照原文核实。

AI 辅助译文 · AI 译文可能存在错误,请对照原文核实。 阅读原文
数学符号、代码、参考文献身份和图内文字保留原始形式。

《超越理想路径的共识:安全性、进展与法定人数的代价》的概念性编辑插图
概念插图 · 内置 ImageGen · 非实验证据

摘要

采用副本机制的服务,只有在维持一致历史的同时,能在明确条件下持续响应请求,才具有实用价值。这些要求往往被压缩成单一的容错声明,从而掩盖了安全性与进展之间的区别。本综述将异步共识不可能性结果、Paxos 和 Raft 与一个刻意保持小规模的法定人数可用性模型联系起来,推导多数规模如何改变收集到确认响应的概率,并构造一个反例,说明不能将法定人数集合相交视为完整的共识证明。分析将崩溃恢复、成员变更、客户端重试和读取,与选择一个值这一更简单的任务区分开来。其主要结论是方法论层面的:每项运行可用性声明都应指明故障模型、持久化边界、通信假设和观测区间。所提供的示例是数学构造,而非对生产环境共识实现的测量。

容错声明必须回答的问题

考虑一项存储科学论文稿件当前版本的服务。编辑者发送替换版本后失去连接,随后从另一个副本读取。重要的问题不在于还有多少台服务器运行,而在于新的读取必须反映哪些已完成操作、结果不确定的写入是否可能在之后变得可见,以及服务必须在何种通信条件下响应。仅仅统计健康进程数量,无法回答其中任何一个问题。

我们区分对已选定日志条目达成一致与应用程序的可线性化执行。一致性约束副本;可线性化性还将已完成的客户端操作与实时顺序联系起来。某个协议可以保护其已提交日志,却仍通过保护不足的读取路径暴露过时的读取结果。这一区分界定了本综述的范围:安全性证明涉及允许出现的历史,而可用性模型涉及到达其中某种历史的概率,或最终是否能够到达。 [2], [3]

三项主要成果,三种不同作用

Fischer、Lynch 和 Paterson 证明,在完全异步的消息传递模型中,即使只有一次崩溃故障,确定性共识也可能无法终止。他们的定理并不是说共识通常无法完成,也不是说随机化协议或借助时间条件的协议不可能存在。Lamport 对 Paxos 的阐述解释了带编号的提案与接受者的持久信息如何维持一致,并将进展另行讨论。Ongaro 和 Ousterhout 围绕领导者选举、复制与安全性组织复制日志共识,并采用基于重叠多数集合的成员变更机制。

这些来源回答的是不同问题。不可能性结果限制了普遍终止的承诺;协议则提供维持既定决策的机制。单独考虑多数计数或选举超时的存在,都不足以确立完整系统的所有性质。我们将这种区分作为设计规范,而不是对协议进行排名。 [1], [2], [3]

关于多数集合相交的一个简短证明

设某一配置包含 n 个副本,每项决策都要求该配置中 q 个不同副本的确认响应。两个法定人数集合必须至少共享 2q 减 n 个成员,否则其并集就会包含超过 n 个不同副本。因此,严格多数保证交集非空。对于五个副本、法定人数为三个的情况,最小重叠为一个;若法定人数为两个,则存在互不相交的决策组。

这一基本计数论证在许多多数派协议中是必要的,但不足以保证一致。共享副本必须遵守将先前响应与后续响应关联起来的规则。如果它能在重启后遗忘已接受的提案,或在缺乏单调投票编号规则的情况下确认相互冲突的决策,那么交集就不承载任何有用信息。因此,审查实现时应追踪交集副本的持久状态,而不应止步于集合论引理。

针对常见论证捷径的一个明确反例

考虑副本 A、B 和 C。A 与 B 确认值 x;随后 B 与 C 确认值 y。两个组都是多数。如果允许 B 确认不相容的决策,且两个决策过程都不检查先前的提交,那么 x 与 y 都可能被宣布为已选定。这与多数集合相交引理并不矛盾:B 恰好就是重叠成员,但协议未赋予这一重叠成员维持已有决策的义务。

可执行附录枚举了 n 从三到九时的每一对法定人数子集,并检查最小交集。它还记录了这个三副本反例见证。这种有界枚举是对计数模型的检查,而非对 Paxos 或 Raft 的证明。其价值在于诊断:它可以防止将看似有说服力的法定人数示意图误认为完整的协议论证。

副本独立故障下的可用性

假设在指定观测窗口内,每个副本可达的概率为 p,且与其他所有副本相互独立。将至少 q 个副本可达的二项概率求和,就得到一个理想化的法定人数可用概率。当 p 等于 0.9 时,三成员配置中多数可用的概率为 0.972;五成员配置中则为 0.99144。这些数值描述的是一个合成的独立性模型,而非正常运行时间承诺。

独立性是脆弱的假设。共享电源、共同路由、错误部署,或单个过载的存储依赖,都可能影响所有成员。如果一个共同事件以概率 c 使整个配置失效,且与各副本剩余故障相互独立,那么可用性就变为二项模型结果乘以一减 c。增加副本无法消除这一共模因素造成的上限。因此,选择故障域与在单个故障域内增加副本数量,具有不同的意义。

在假设失效之前,延迟是一种次序统计量

作为第二个构造,设 n 个相互独立的确认响应时间服从均值为十毫秒的指数分布。如果一项决策等待第 q 个确认响应,其完成时间分布就是在时刻 t 之前或恰于该时刻至少已有 q 个单独确认响应到达的概率。将单个响应的到达时间分布代入同一个二项表达式,即得到图示曲线。

该模型刻意省略领导者的请求处理、持久日志刷盘、客户端往返、重传和选举工作。它是抽象法定人数收集器的模型,而非对 Raft 提交延迟的预测。相关的磁盘暂停会破坏独立性,固定的串行化延迟会使所有曲线发生平移。报告实测延迟分布时,必须说明计时覆盖哪个区间,以及哪些存储操作在确认响应前已经完成。若没有这一边界,两个看似可比较的延迟数值可能描述的是不同的持久性契约。

超时提供的是怀疑,而非对历史事实的裁定

超时表示某个响应未在一段时间内到达。它无法区分进程崩溃、进程延迟、数据包延迟或接收方过载。在完全异步模型中,不存在能够绝对可靠地区分这些情况的有限超时时长。不过,实用协议仍可以在更强的最终时间条件或领导者假设下取得进展,同时在错误怀疑期间维持安全性。

其运行层面的含义是,应分别评估这两种性质。较短的选举超时可能改善单次明确崩溃后的恢复,却在共享暂停期间导致领导者反复更替。较长的超时可能减少不必要的选举,却延长真正的服务中断。有用的实验会改变延迟分布和持续负载,记录未成功的选举,并在全过程中检查客户端历史。排除不稳定区间的吞吐量图,无法确立恢复行为。 [1], [2]

恢复、成员变更与读取扩展了必须履行的义务

崩溃恢复改变了确认响应的含义,因为内存内容会消失,而已确认的承诺必须继续有效。成员变更改变了哪些集合有权作出决策。被移出某个配置的副本,不得在之后与旧同伴组成独立的权威。读取又引入了另一个问题:曾经领导集群的进程,在失去与法定人数通信的能力后,仍可能继续运行。

这些是彼此不同的义务,而非可从正常路径追加操作中推断出的实现细节。审查应识别每项决策所关联的配置、重启后所需的持久化元数据,以及读取者据以确立其权限仍然有效的机制。具体方案可能采用协议专用屏障,或经过严谨论证的租约;必须在其自身的时钟和故障假设下进行检查。仅仅读取某个可达服务器的本地日志并不充分。 [2], [3]

一项可证伪该声明的评估提案

首先给出应用的顺序规范,并收集调用与响应的时间区间,将超时视为结果不确定,而非自动判定为失败。在持久化边界处制造故障,而不是仅仅停止空闲进程。让领导者确认一次写入后失去连接,随后在另一个组进行领导者选举时接收读取请求。再结合成员转换以及来自早期配置的延迟消息重复这一过程。

应基于同一组历史报告正确性与服务质量。可用性的分母必须包含恢复期间发出的请求。记录故障检测器参数、重试策略、日志刷盘策略和拓扑。历史检查器可以拒绝错误执行,但有限历史集合全部通过,并不能确立普遍正确性。形式规范与有界模型检查器可以提供互补证据,前提是它们的抽象未排除任何与所主张性质相关的行为。

结论:让每项保证都附带其假设

当每项陈述都明确其量词时,共识就更容易评估。安全性声明约束模型允许的所有执行;进展声明指出哪些时间条件或公平性条件能够导出完成;实证可用性声明则涉及某种工作负载与观测周期。混淆这些形式,是许多夸大的可靠性承诺的来源。

我们的定量示例说明,为何更多副本可以改善独立故障模型中的表现,却对共同原因作用甚微,以及为何等待法定人数只是端到端延迟的一个组成部分。反例说明了交集为何必须承载持久的协议状态。可辩护的部署论证应将这些要素结合起来,而不以任何一项替代其他项:数学、实现边界与实测环境必须描述同一项服务。

本地执行 · 范围有界

法定人数交集的枚举与一致性反例

子集运算与刻意设置的无效投票规则;不是 Raft 或 Paxos 的证明。

20596 项断言通过。 这些检查验证的是所提供的示例,而非所引用的系统。

检查已记录的反例见证
{
  "quorum_pairs": 20587,
  "unsafe_witness": "B votes x then y without a persistence rule"
}

明确声明的分析模型

四个方程,明确的假设

∣Q1∩Q2∣≥2q−n|Q_1\cap Q_2|\ge 2q-n

(1) 针对同一 n 成员配置中两个大小为 q 的子集。正的下界确保交集存在,但若无额外协议规则,并不能保证一致。

A(n,q,p)=∑k=qn(nk)pk(1−p)n−kA(n,q,p)=\sum_{k=q}^{n}\binom{n}{k}p^k(1-p)^{n-k}

(2) 在明确的时间窗口内,各副本独立地以概率 p 可达;故障指崩溃或通信不可用,而非拜占庭行为。

Ac=(1−c)A(n,q,p)A_c=(1-c)A(n,q,p)

(3) 某个共同事件以概率 c 使所有副本失效;剩余的独立可达性以未发生共同事件为条件。

Pr⁡[T(q)≤t]=A ⁣(n,q,1−e−t/τ)\Pr[T_{(q)}\le t]=A\!\left(n,q,1-e^{-t/\tau}\right)

(4) 理想法定人数收集器,确认响应时间独立同分布,服从均值为 tau 的指数分布;图中使用 tau = 10 毫秒。

构造示例 · 可复现数据

检查定量论证

这些曲线根据所声明的模型计算得出,并非所引用研究中的观测结果。每幅图都包含其数值数据和矢量版本。

独立可用性下的多数。各副本的可用性相互独立且相同;仅考虑多数确认响应。持久投票规则、网络分区与共同原因故障不在此概率模型范围内。
图 1。独立可用性下的多数。 各副本的可用性相互独立且相同;仅考虑多数确认响应。持久投票规则、网络分区与共同原因故障不在此概率模型范围内。
理想法定人数收集器。确认响应时间独立,服从均值为 10 毫秒的指数分布。不包含领导者选举、排队、重传或相关延迟;这不是实测的 Raft 延迟。
图 2。理想法定人数收集器。 确认响应时间独立,服从均值为 10 毫秒的指数分布。不包含领导者选举、排队、重传或相关延迟;这不是实测的 Raft 延迟。

哪种证据回答哪类问题?

声明所需证据无法确立的内容
相交的法定人数集合子集论证加持久响应规则任意延迟下的进展
可线性化应用顺序规范与客户端历史无限吞吐量
运行可用性故障、工作负载、窗口与分母普遍终止定理

拟议的验证方案

这是一项拟议的评估设计,未进行生产系统或硬件基准测试。另行执行的有限模型记录在可执行检查中。

  1. 在生成负载前,明确应用的精确状态机与完成边界。
  2. 枚举法定人数交集,并记录每个共享副本的持久性义务。
  3. 在持久确认响应前后注入崩溃与通信故障。
  4. 在收集的历史中纳入过时领导者、重配置、重试和读取。
  5. 依据顺序规范检查历史;将超时操作保留为可能已完成的操作。
  6. 报告可用性与延迟时,纳入恢复区间和共同原因故障。

一手来源确立了什么

Michael J. Fischer, Nancy A. Lynch, Michael S. Paterson · 1985 [1]

贡献。 在可能发生一次崩溃的情况下,确定性异步共识可能允许不终止的执行。

边界。 定理所采用的模型和普遍终止要求至关重要;它并非对典型延迟给出的界限。

来源定位。 摘要;异步模型与不可能性证明。

Diego Ongaro, John Ousterhout · 2014 [2]

贡献。 Raft 分离了复制日志的各项职责,并描述了采用重叠多数集合的配置变更。

边界。 该论文并未确立任意读取路径或修改后实现的正确性。

来源定位。 USENIX 论文;领导者选举、日志复制、安全性与成员管理章节。

Leslie Lamport · 2001 [3]

贡献。 Paxos 使用带编号的提案和保留的接受者状态,以维持已选定的值。

边界。 进展是另一个独立问题;不遵循所述规则的确认响应并不充分。

来源定位。 第 2.1–2.5 节及状态机讨论。

本分析的局限

  • 除一个明确建模的共同事件外,二项模型假设可达性相互独立。
  • 延迟模型是法定人数收集器的抽象,不包含实际存储、网络和领导者实现的开销。
  • 可执行的子集枚举并不验证共识实现。
  • 选取的三项来源并未涵盖所有共识家族、拜占庭模型或近期优化。

这是一篇聚焦于三项选定的奠基性一手来源的分析性综述,包含原创的详细示例。它不是对截至 2026 年文献的穷尽性或系统性调查。来源访问与版本说明随参考文献一并记录。

可能改变结论的问题

  1. 在预期部署的实际故障域之间,故障的相关性有多强?
  2. 配置变更与过时领导者读取期间,客户端历史中会出现哪些行为?
  3. 哪些持久化与调度延迟主导了观测到的法定人数延迟?

参考文献

  1. Michael J. Fischer, Nancy A. Lynch, Michael S. Paterson. Impossibility of distributed consensus with one faulty process. Journal of the ACM (1985). 10.1145/3149.214121.
  2. Diego Ongaro, John Ousterhout. In Search of an Understandable Consensus Algorithm. USENIX ATC (2014). Primary source.
  3. Leslie Lamport. Paxos Made Simple. ACM SIGACT News (2001). Primary source.

来源 [1] 访问情况。 一手记录、摘要与选定的可访问文本;并非对全文或补充材料的穷尽性审查。

来源 [2] 访问情况。 一手记录、摘要与选定的可访问文本;并非对全文或补充材料的穷尽性审查。

来源 [3] 访问情况。 一手记录、摘要与选定的可访问文本;并非对全文或补充材料的穷尽性审查。

书目身份已对照 Crossref 及出版方、作者或机构的一手记录核验。下方的来源访问与版本说明描述了范围;这并非对全文的穷尽性审查。

作者身份与来源

由 Codex(人工智能)撰写并进行技术自审。参考文献标明原始研究者;分析性构造与拟议评估设计归属于本文。

封面为 ImageGen 概念插图。技术图表依据明确声明的模型或有限示例计算,并附有 Python 与 CSV。它们不是对已部署产品的测量,也不是复现的性能基准测试。

此本地草稿没有独立同行评审或期刊录用记录。有界可执行示例检查的是所述小型模型,并非对引用系统的形式验证。

委托研究综述 · v5. 引用本文 · 原始来源记录 · 发布记录