公平性约束

公平性筛选无限执行 ​

系统模型通常允许调度器在多个使能动作中选择。公平性约束从全部无限路径中选出一部分 admissible paths，再只在这些路径上判断活性；它不改变某一步是否属于转移关系。

设动作 $a$ 在状态 $s_i$ 使能，若存在 $s^{\prime }$ 使 $s_i\stackrel{a}{\to }{s}^{\prime }$。弱公平要求：若从某个位置起 $a$ 持续使能，则 $a$ 最终执行。可写成路径条件

$$FGenabled(a)⟹GFtaken(a).$$

强公平要求：若 $a$ 无限多次使能，即使中间反复失效，它也无限多次执行：

$$GFenabled(a)⟹GFtaken(a).$$

因此强公平排除的路径更多；两者名称在部分文献中对应 justice 与 compassion，但术语映射需随工具定义确认。

间歇使能区分强弱 ​

两个进程竞争锁。进程 P 的 enter 在锁空闲时使能，但进程 Q 每次释放后立刻重新获取，使 P 的动作只在离散瞬间反复使能，从未持续使能。

这条无限执行不违反 P 的弱公平，因为不存在一个后缀让 enter_P 一直使能；它违反强公平，因为 enter_P 无限多次获得机会却从不执行。

若调度器从某时刻起始终把 P 留在 runnable 队列却从不调度，弱公平已经足以排除。例子必须跟踪 enabled 状态，而不能只统计某动作“看起来等了很久”。

公平不是模型自动属性 ​

异步模型允许任意有限延迟，往往也允许某进程永远不被调度。仅因为所有进程在现实操作系统中“通常会运行”，不能在证明里无声删除饥饿路径。

可采纳执行公理库可容许执行Admissible execution满足给定调度、公平性和故障模型约束的执行。会同时约束故障数、消息交付和调度公平。公平性应写成环境或调度器假设；系统算法的保证通常是“对所有满足这些假设的执行”。

若实现运行在没有相应调度保证的平台上，模型内活性证明不适用。相反，安全性质通常对删除路径保持：即使不假设公平，互斥也应对所有执行成立。

justice、compassion 与状态集合 ​

符号模型检查常用 fairness sets。justice 条件给出状态集合 $J_i$，要求路径无限多次访问每个 $J_i$。compassion 对 $(P_i,Q_i)$ 要求：若路径无限多次访问 $P_i$，也必须无限多次访问 $Q_i$。

动作公平可通过增加“动作刚执行”命题编码成状态公平。这个转换会扩展状态，且 enabled/taken 的标记必须准确；漏标使能状态会把不公平路径误判为公平。

多个公平条件取合取。条件越多，保留路径越少，活性越容易成立，也越可能依赖不现实假设。公平假设应最小化并单独审查。

与安全—活性的关系 ​

安全—活性公理库安全性与活性Safety and liveness · Correctness properties把系统正确性分为坏事永不发生与好事最终发生两类性质。分解说明公平性本身通常是对无限行为的 liveness 型限制：任意有限前缀还可以通过未来调度修复，无法仅凭一个有限坏前缀判定永远不公平。

加入公平性可能使“每个请求最终响应”成立，但不会修复“两个进程同时进入临界区”的安全反例。后者一旦发生，即使未来调度完美公平也无法撤销。

公平也不等于概率一事件。随机调度下某动作以概率 $1$ 最终执行，仍可能存在概率零的不公平路径；普通公平语义是集合上的全称筛选，不带概率测度。

验证与反例边界 ​

检查公平 liveness 时，反例常是一个可达循环：循环满足系统转移，却持续违反某 fairness set 或在公平前提下避免目标。算法必须同时检查接受条件和公平条件，单找任意 SCC 不够。

公平性若写得过强，模型检查会“证明”实际上做不到的响应。诊断报告应显示反例是否因不公平被排除，并把 fairness assumptions 与系统 guarantees 分栏呈现。

选择公平对象 ​

公平性可以施加在进程、动作或具体转移上，三者不总等价。一个进程被无限调度，仍可能每次只执行不相关动作；一个动作标签在多个组件中共享，也无法说明究竟哪个实例获服务。证明饥饿自由时，应把公平对象细化到真正承担进展义务的 transition instance，并明确使能谓词在何种原子状态上求值。

参考资料

• Leslie Lamport, “Proving the Correctness of Multiprocess Programs,” IEEE Transactions on Software Engineering SE-3(2), 1977, pp. 125–143。
• Zohar Manna and Amir Pnueli, The Temporal Logic of Reactive and Concurrent Systems, Springer, 1992, Chs. 3–4。
• Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press, 2008, §§3.5, 4.6, 6.7。