“微秒级”“简洁区块链”“异步BFT”不是三档性能套餐。NOPaxos把排序能力下沉到网络设备，以特殊网络原语缩短崩溃容错快路径；Streamlet用epoch、leader和公证链给出易讲清的拜占庭共识；HoneyBadgerBFT用随机化和密码学组件在异步网络中获得概率活性。它们改变的是系统模型，不能只按吞吐或延迟排成一条榜单。

分布式系统（E04）：Lambda 与 SkyPilot 的执行和调度边界

比较协议前先固定四个条件

至少要写清网络时序、故障类型、成员/身份和完成定义。一个协议的“快”可能依赖可编程交换机；另一个协议的“活”可能只承诺概率1最终完成；BFT证书还依赖认证密钥没有被正确节点滥用。

flowchart LR
  P[协议主张] --> N[网络模型]
  P --> F[故障模型]
  P --> I[身份/密码学]
  P --> C[完成与测量口径]
  N --> J[可比较结论]
  F --> J
  I --> J
  C --> J

NOPaxos：网络排序换掉一部分协议工作

NOPaxos论文提出Ordered Unreliable Multicast。网络排序器给请求分配序号，正确副本在正常路径上看到相同顺序，从而避免传统共识为每个请求交换排序消息。低延迟来自把工作放进网络，不是“共识不再需要网络”。

unreliable一词很关键。副本可能看到序号缺口，排序器或leader也会故障；协议仍需gap recovery、view change和持久化边界。若普通网络不能提供论文要求的有序原语，NOPaxos的快路径前提就不成立。

sequenceDiagram
  participant C as Client
  participant S as Network Sequencer
  participant R1 as Replica1
  participant R2 as Replica2
  C->>S: request
  S->>R1: seq=4
  S->>R2: seq=4
  Note over R1: 若只见1,2,4则停在gap
  R1-->>R2: recovery/view change

论文中的微秒级数字绑定当时硬件、网络、批量、请求大小和实现。换成跨区域网络、软件交换或不同持久化设备后，数字不能直接迁移。

Streamlet：三段连续公证形成最终化证据

Streamlet把时间分成epoch，每个epoch选一个leader提出区块。区块获得超过三分之二投票后被notarized。若一条链上出现三个连续epoch的notarized blocks，中间块及其祖先可以finalize。只有两个公证块，或epoch编号有缺口，都不足以触发这条规则。

提案与投票还受两条前置规则约束。leader只能在自己epoch提案，并必须扩展它见过的最长已公证链之一；诚实参与者只给满足同一扩展条件的提案投票，而且每个epoch最多投一票。三连续规则离开这些约束就不能单独承担安全性证明。

flowchart LR
  B1[epoch e 已公证] --> B2[epoch e+1 已公证]
  B2 --> B3[epoch e+2 已公证]
  B3 --> F[finalize B2及祖先]
  X[epoch e 已公证] --> Y[epoch e+2 已公证]
  Y --> N[不能套三连续规则]

在4节点、至多1个Byzantine节点时，证书取3票。任意两个3票集合至少交2个节点；即使其中一个是故障节点，交集仍有正确节点。证明还要结合正确节点投票规则和链结构，不能只写交集算术。

安全性要证明的是中间块在自身高度上没有竞争的已公证块，不能假定相邻epoch的所有公证块天然在同一条链上。设一条已公证链上三个相邻块分别处于epoch e、e+1、e+2，中间块高度为h。同epoch的两个公证证书必交于诚实投票者，诚实节点每epoch至多投一票，因此另一条链上高度h的已公证竞争块X不可能属于这三个epoch。

若X的epoch早于e，它的已公证父块已经到达高度h-1。为X投票的证书中超过三分之一的节点是诚实节点；这些节点在e轮仍知道这条至少高h-1的已公证链，不会给只从高度h-2延伸的首块投票。首块因而凑不齐超过三分之二的票，与其已公证矛盾。若X的epoch晚于e+2，第三块的公证证书中超过三分之一的诚实投票者在投票时已见高度h的中间块获得公证；之后不会给从高度h-1延伸的X投票，X同样无法公证。中间块在高度h上唯一，其他更长的已公证链必须包含它，所以诚实节点最终化的前缀不会冲突。这里用的是每个投票者当时的局部视图及其不会遗忘的已公证证据，不要求全网同时看见同一条链。

随文有限状态机只有一份全局已公证集合，执行的是单条有利轨迹和几次规则拒绝；它不能枚举分叉后的局部视图，也没有执行上述按竞争块epoch分类的证明。安全性结论依赖论文的投票、证书与认证假设，不能从该轨迹的“最终化成功”直接推出。

活性依赖epoch足够长以容纳网络传输，并最终出现诚实leader。作者的证明使用连续五个诚实leader epoch作为保证推进与最终化的充分窗口，不是必要条件；在状态已对齐的有利执行中，三个连续诚实epoch就可能形成最终化证据。永久异步延迟可以让固定轮次无法推进，因此Streamlet与HoneyBadger的网络承诺不同。

HoneyBadger：不用时钟上界，但要随机性与密码学

HoneyBadgerBFT组合可靠广播、异步二元一致和异步共同子集，让n >= 3f+1的副本在异步拜占庭模型下输出共同批次。对手可以任意延迟消息，但不能永久阻止正确节点之间的消息交付；随机化打破FLP式确定性僵局，终止是概率性质。

flowchart TD
  TX[加密交易批] --> RBC[可靠广播]
  RBC --> ABA[异步二元一致]
  ABA --> ACS[异步共同子集]
  ACS --> DEC[共同解密与输出]

“不假设已知延迟上界”不表示有限时间SLA。某个有限前缀没有决定，既可能是允许的消息延迟，也可能是实现故障。安全性与概率终止需按完整模型判断。

条件矩阵比性能榜单更有用

协议 网络关键前提 故障 核心快/活性来源 不能直接声称
NOPaxos 网络提供有序不可靠多播 crash 网络序号缩短正常路径 普通网络也有相同延迟
Streamlet 认证且epoch最终覆盖消息延迟 Byzantine < 1/3 leader、公证与三链规则 完全异步仍确定推进
HoneyBadger 异步、消息最终交付 Byzantine < 1/3 随机化ACS与密码学 固定截止时间或最低延迟

工程选择还要算实现复杂度、密钥管理、批量等待、恢复路径和硬件依赖。只比较论文峰值会把不同任务、不同年份和不同故障模型混在一起。

论文报告值的实验条件

NOPaxos论文§6的Figure 5使用5个副本、2.5 GHz Xeon E5-2680服务器和64 GB内存。测试床用3台物理交换机通过VLAN模拟Figure 3的12交换机三级fat-tree；序列器是Cavium Octeon II CN68XX网络处理器，图中链路同时有1 Gb/s与10 Gb/s，不能概括为全部10 Gb/s。Figure 5的closed-loop客户端负载中，Paxos batching自适应调整批量并保持至少一批在途；该图报告NOPaxos为111微秒，Paxos为240微秒，Fast Paxos为193微秒。Figure 9的sequencer failover约110毫秒恢复、约270毫秒回到峰值。Figure 10在10毫秒SLO下报告事务KV吞吐超过Paxos的4倍、比Speculative Paxos高45%，与无副本系统相差4%以内。这些是论文原型在对应请求、批量和网络设置下的报告值，本地实验没有复测。

HoneyBadger论文§5与Figures 5–8使用250字节交易，在8个区域、5大洲的32/40/48/56/64/104台EC2 t2.medium实例上测试，按f=N/4设置容错数，每节点提案批量从256到131072笔。论文报告不超过40节点时吞吐超过20,000 tx/s，104节点仍超过1,500 tx/s；104节点最大批量在6分钟内完成。这些结果来自论文prototype的乐观无故障实验，不是本地模型或生产保证。Streamlet论文没有对应的实测evaluation，本篇不为它补造性能数字。

运行有限检查

1
2
3
4
mkdir -p examples/distributed-systems/.build/e05/tmp
export TMPDIR="$PWD/examples/distributed-systems/.build/e05/tmp"
export TMP="$TMPDIR" TEMP="$TMPDIR" PYTHONDONTWRITEBYTECODE=1
python3 -B examples/distributed-systems/consensus-e05/check.py --output examples/distributed-systems/.build/e05/observations.json

程序枚举4节点3票证书所有配对和故障位置，检查交集仍含正确节点；最小Streamlet状态机依次公证epoch 1、2、3并最终化中间块，同时拒绝错误leader、没有扩展最长已公证链的陈旧父块，以及同一投票者在epoch 4的第二票。有序网络场景按序号实际计算已应用前缀、缺失序号和缓冲请求：收到1、2、4时只应用1、2，把4保留在缓冲区；收到1、2、3、4时则全部应用。输出还保存安全性与活性证明骨架。HoneyBadger部分明确标为DOC_ONLY，只说明概率终止的理论边界，不运行协议或活性检查；单独运行--scenario async返回0只表示说明成功输出。完整结果见观察结果，来源见实验证据，限制见验证说明。

两个推演练习

NOPaxos副本收到1、2、4，为什么不能直接执行4？

序号3可能只是延迟，也可能已经被其他副本看到。越过缺口会让副本执行不同前缀，必须按协议恢复缺失请求或切换视图。

HoneyBadger运行十秒没有输出，能否证明活性违例？

不能。异步概率活性没有固定十秒截止；需要区分允许的有限延迟、随机选择和实现卡死。运维SLA仍须另设监控与超时策略。

Streamlet leader在epoch 4提议一个只扩展epoch 1公证块的分支，可以投票吗？

若参与者已经见到更长的epoch 1–3公证链，就应拒绝。合法leader身份只决定谁能提案，不会豁免“扩展最长已公证链之一”的提案与投票条件；同一参与者在epoch 4已经投过另一提案时也必须拒绝第二票。

E06把“证明程序应该满足什么”推进到可执行规格与实现级证明，比较TLA+/PlusCal有限模型和IronFleet。

参考资料