安全性与活性

安全性约束“坏事永远不会发生”。一旦有限历史已经出现两个进程同时进入临界区，任何未来都无法删除这个事实；这段历史已经是完整的反证。这里判断的是整条历史，而非当前状态：后来只剩一人，不能使已经违规的历史重新合格。

活性定义说“每个前缀存在一个好延伸”，不是说任意延伸都成功。前者用来分类性质；证明实现满足该性质，则要证明实现的每条可容许执行都在 $P$ 中。展示一次成功运行，不能代替这个全称证明。

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

互斥锁的安全性是任意时刻至多一个进程进入临界区；若观察到两个进程同时进入，有限执行前缀已经永久否证它。无饥饿性理路饥饿与公平性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 }$，但两种放置方式必须在结论中显式说明。

分解还可具体构造。令 $S=\bar{P}$ 为前缀拓扑中的闭包，即其每个有限前缀都仍有满足 $P$ 的延伸；令 $L=P\cup (\mathrm{\Omega }\setminus \bar{P})$。则 $S$ 封闭而是安全性质，$L$ 稠密而是活性质，且 $S\cap L=P$。对任意前缀，若它有 $P$ 中的延伸就已遇到 $L$；若没有，它的全部延伸都在闭包外，也遇到 $L$。这说明分解不是把每个需求句子硬贴成两类之一。

有限终止执行可通过无限重复末状态纳入上述模型；是否允许这种停顿，仍需在 $\mathrm{\Omega }$ 中声明。具体并发术语也应回到各自页面核对完成事件、参与者量词和环境假设。

工作流网健全性理路工作流网的健全性Workflow net soundness给工作流网明确的可完成、干净完成和无死任务条件，用分支同步错误与允许无限循环的例子解释健全性的量词。把完成规格拆成任意可达状态仍可完成、到达终点时无残留、没有永久死任务。这里“仍可完成”是每个状态存在一条好未来；带重试循环的健全流程仍可能在不公平选择下永远不退出，不能据此宣称所有执行都终止。