为系统构建者指定 Paxos：可执行伪代码
Specifying Paxos for System Builders: Pseudocode Made Executable
- Stony Brook University（石溪大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出将 Paxos for System Builders 协议的伪代码逐行映射为可执行的 DistAlgo 规范，实现精确执行、自动检查与可视化，并修复了伪代码中的遗漏和活性缺陷，同时保持性能可接受。
AI中文摘要：
本文提出了一种精确的可执行规范——作为伪代码的忠实映射——针对“为系统构建者的 Paxos”，一种用于分布式系统中复制和共识的实用协议。“为系统构建者的 Paxos”既有 C 语言的健壮实现，也有针对关键协议细节的清晰伪代码。本文展示了如何将协议伪代码几乎逐行地轻松表达为精确的高级语言 DistAlgo，以便在分布式系统中直接执行。精确的规范和直接执行极大地有助于理解协议逻辑，并自动检查、跟踪和可视化协议运行。它们还导致发现了伪代码中微小且难以捕获的遗漏和活性缺陷，并进行了修复，尽管 C 代码中没有这些问题。生成的程序在具有与伪代码相似规模的同时，也表现出可接受的性能。
英文摘要：
This paper presents a precise executable specification---as a faithful mapping from the pseudocode---of Paxos for System Builders, a practical protocol for replication and consensus in distributed systems. Paxos for System Builders has both a robust implementation in C and a clean pseudocode for critical protocol details. This paper shows how the protocol pseudocode can be expressed easily, essentially line-by-line, in a precise high-level language, DistAlgo, for direct execution in distributed systems. Precise specification and direct execution help significantly in understanding the protocol logic and in automatically checking, tracing, and visualizing protocol runs. They also led to discoveries and fixes of small, difficult-to-catch omissions and liveness bugs in the pseudocode though not the C code. The resulting program also has acceptable performance while having similar size as the pseudocode.
