可容许执行

转移规则只回答系统"能做什么"，不回答环境"会做什么"。同一套代码，放进消息可能永远丢失的网络与放进最终必达的网络，能证明的结论完全不同，所以规格里必须有一个明确位置存放"环境承诺"。可容许性就是这个位置：状态机先枚举一切物理上可能的动作交错，可容许条件再筛掉模型明确不打算处理的场景——超过 $f$ 个故障、永远不调度某进程的调度器、无限期扣押消息的信道。可以把它理解为算法与环境之间的契约：算法只对遵守契约的对手负责。契约必须写进规格而不是藏在证明中，否则"算法正确"这句话就没有确定的量化范围，不同读者会默认不同的环境假设。

取异步消息传递模型，假设"至多一个进程崩溃、发给正确进程的消息最终交付、每个正确进程被调度无穷多次"。此时所有进程都走无穷多步且无消息丢失的执行是可容许的；进程 $p$ 在第 10 步后永久停止的执行同样可容许（把 $p$ 计入故障预算即可）；而两个进程都永久停止的执行不可容许，算法无须对它负责。反过来，若删去公平性假设，"调度器从此只运行进程 $q$"的执行就成为可容许的，一切依赖其他进程推进的活性性质随之失去证明可能。这说明活性结论对公平性极其敏感；安全性则通常对更宽的执行集合成立，因为"坏事不发生"是对每个有限前缀的断言，与调度是否公平无关。

两个常见误用值得单独指出。其一，"异步可靠信道允许任意长但有限的延迟"不同于"延迟存在已知上界"：前者是异步模型，后者已经是同步假设，混同二者等于偷换时间模型。其二，FLP 不可能性公理库FLP 不可能性定理FLP impossibility · Fischer–Lynch–Paterson theorem完全异步系统中即使只允许一个进程崩溃，也不存在保证所有可容许执行终止的确定性共识协议。所构造的永不终止执行完全满足其模型的可容许条件——每个进程走无穷多步、每条消息最终交付、实际可以无故障——因此以"这种调度不现实"为由拒绝它不能反驳定理；想绕开定理，只能显式修改模型，即收紧可容许执行的集合。

在异步系统公理库异步系统Asynchronous distributed system消息延迟和进程相对速度没有已知有限上界的系统模型。的可靠信道模型中，可容许执行通常允许任意有限延迟，却要求发给非故障进程的消息最终到达。一个执行若永久不调度某个正确进程，可能违反进程公平性。FLP 证明构造的无限执行需同时保持相应公平条件，不能简单理解为“攻击者停止所有消息”。

可容许执行是分布式算法规格的承重结构：故障模型、调度公平性与网络假设全部经由它进入定理陈述。分布式共识公理库分布式共识Distributed consensus · Consensus problem多个进程在可能故障和通信延迟下对一个值达成一致的任务。、领导者选举公理库选主问题Leader election使所有正确进程最终一致输出同一唯一进程为领导者的分布式任务。与自稳定算法的正确性都写成“在所有可容许执行中满足某性质”的形式，其中安全性与活性公理库安全性与活性Safety and liveness · Correctness properties把系统正确性分为坏事永不发生与好事最终发生两类性质。分别承担“任何前缀不出错”与“最终有好事发生”两类断言。轨迹语义公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。给出被量化的执行对象，公平性约束公理库公平性约束Fairness constraint · Weak fairness · Strong fairness以弱公平、强公平等条件排除持续忽略可执行动作的不合理无限执行。从中筛选环境承诺允许的无限轨迹；时序逻辑或模型检查算法再判断性质，不能反过来替规格偷偷补入公平假设。证明 deadlock-free、lock-free 或个体无饥饿时，必须明确进程是否持续取步骤、动作是持续使能还是反复使能，以及故障进程是否仍在量化范围内。

可解性与不可能性的分界同样由可容许集合的大小决定：加入同步界或故障检测器等假设会收紧集合，使更多任务可解；放宽假设则相反。比较两个算法或两条不可能性结果时，第一步永远是核对它们的可容许执行集合是否一致。