安全性与活性

安全性约束“坏事永远不会发生”。一旦有限历史已经出现两个进程同时进入临界区，任何未来都无法删除这个事实；这段历史已经是完整的反证。

活性关心承诺能否在无限执行中兑现。单凭一次请求已经等待很久，仍不能断言它永远不会完成；只有连同公平调度、消息最终送达等执行假设，才能排除永久拖延。永不响应的系统可以很安全却毫无活性，快速给出矛盾结果的系统则可能持续进展但不安全。

互斥锁的安全性是任意时刻至多一个进程进入临界区；若观察到两个进程同时进入，有限执行前缀已经永久否证它。无饥饿性公理库饥饿与公平性Starvation and fairness · 调度公平性 · 无饥饿用调度与服务选择的公平假设刻画持续请求者是否可能永久得不到完成机会。则要求合格的持续请求者最终进入临界区，正如“每个请求最终得到响应”一样属于活性：无论已经等待多久，都还不能据此断言它永远不会发生。

在记录时间的迹模型中，“每个请求在 $100$ ms 内完成”是安全性质：一旦时钟越过截止时间仍未完成，就出现了不可修复的有限坏前缀。要实现或证明这项安全约束，通常还需时钟精度、调度和网络延迟等环境假设，但这些假设不是把性质重新分成安全与活性。死锁自由也不自动推出无饥饿：系统可能一直有某个线程进展，却永久忽略另一个线程。

在固定 $\mathrm{\Omega }$ 及其前缀拓扑下，Alpern–Schneider 分解定理说明每个性质 $P\subseteq \mathrm{\Omega }$ 都可写成安全性质 $S$ 与活性质 $L$ 的交，即 $P=S\cap L$。分解一般不唯一。改变公平性、故障或调度假设会改变合法执行宇宙，也可能改变闭包、坏前缀和分类；有时限的请求响应会产生有限坏前缀，不能只凭“最终”二字归到活性一侧。

两类性质对应不同证明义务。在状态机公理库状态机State machine · Transition system用状态集合、初始状态和转移关系描述系统可能执行轨迹的模型。上，安全性通常证明初态满足不变式且每一步保持它；违反时，一条到达坏状态的有限前缀已经足够。活性则量化无限执行，需要说明持续使能的动作为什么不能永远被推迟；违反时，反例通常包含可无限重复的环。公平性公理库公平性约束Fairness constraint · Weak fairness · Strong fairness以弱公平、强公平等条件排除持续忽略可执行动作的不合理无限执行。既可写进性质，也可通过可容许执行公理库可容许执行Admissible execution满足给定调度、公平性和故障模型约束的执行。限制 $\mathrm{\Omega }$，但两种放置方式必须在结论中显式说明。

具体并发术语应回到各自页面核对完成事件、参与者量词和环境假设。本页只提供有限坏前缀与无限兑现这条分类轴，不把某个名称预先判成纯安全或纯活性，也不靠手工维护下游术语清单。