可容许执行

局部转移规则回答某一步能否发生，可容许性回答一条完整执行是否遵守环境承诺。把同一套发送代码放入永久丢包的网络与最终必达的网络，允许的有限发送步骤相同，能够保证的无限期结果却不同。

环境条件与算法结论应分开写。例如“每个正确进程持续获得步骤”是调度承诺，“每个正确进程最终决定”才是算法要证明的结果。若把后一条直接塞进可容许性的定义，共识终止就变成循环论证；若证明中临时假定领导者最终稳定，而规格没有该条件，则是悄悄缩小了被量化的执行集合。

有限前缀通常不能单独判定无限公平性。一个进程等待一百万步后仍可在后续继续运行，消息久未到达也可下一步送达。验证器因此常把活性反例表示成可无限重复的环，并检查这个环是否违反已声明的公平条件，而不是把一次超时直接当作永久饥饿。

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

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

进程公平与动作公平也不同。设 P 每轮都可选择 retry，仅在锁空闲时可选 acquire；调度器每轮运行 P，却总在其他线程持锁时运行它。P 取得无穷多步，仍未必获得锁。若 acquire 只是无穷多次短暂使能，弱公平不能排除饥饿，针对该动作的强公平才有相应约束；若它从某刻起一直使能，弱公平已足够。应先确定使能条件，再选择公平性量词。

可容许执行是分布式算法规格的承重结构：故障模型、调度公平性与网络假设全部经由它进入定理陈述。分布式共识理路分布式共识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 或个体无饥饿时，必须明确进程是否持续取步骤、动作是持续使能还是反复使能，以及故障进程是否仍在量化范围内。

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