AI 中文总结
本文对 PaxosLease 协议进行机器检查的重新验证，提出重启隔离期、定时器放置和遗留消息三个关键发现，并给出 TLA+ 形式化与可执行参考模型。
AI 中文摘要
PaxosLease 是一种协议，通过该协议，一个由接受者组成的法定人数授予有时间限制的独占所有权，而无需持久的接受者租约状态，也无需在租约获取路径上进行磁盘写入。本文给出了该协议及其标准用途（选举一个每纪元恢复一次、然后通过单轮追加提交的 Multi-Paxos 领导者）的精确且经机器检查的陈述。有三个新结果。首先，接受者在丢失其易失状态后必须遵守的重新启动隔离期是提议者尝试持续时间，这个界限在检查模型中是最紧的，并且在两个方向上都在边界处经过了机器检查。其次，定时器的放置对安全性至关重要：在收到准备法定人数时启动尝试定时器可能会产生两个同时的租约所有者。第三，当提议者放弃一次获取尝试并重试时，被放弃尝试遗留的消息可能使接受者报告一个提议者自身似乎拥有的租约；除非此类报告仅在提议者正在续订该确切租约时才被视为开放，否则在任何隔离期长度下都会出现两个同时的所有者。租约转换系统在 TLA+ 中形式化，并由 TLC 检查，定时算术在 TLAPS 中证明。一个可执行的参考模型独立于 TLA+ 第二次编码相同的规则，因此一个错误的规则必须通过两次独立的编码才能存活。一个单文件的可运行演示以可读的 Python 代码给出了该算法。
英文摘要
PaxosLease is a protocol by which a quorum of acceptors grants time-bounded exclusive ownership with no durable acceptor lease state and no disk write on the lease acquisition path. This paper gives a precise, machine-checked statement of the protocol and of its standard use, electing a Multi-Paxos leader. Formalizing and model checking the original protocol changes three rules of its acceptor: two are required for safety, the third allows shorter restart quarantines. The protocol is formalized in TLA+ and checked by TLC, its timing arithmetic is proved in TLAPS, and an executable Python model demonstrates the distributed algorithm for human readers.
Comments15 pages, 1 figure, 3 tables
