符号说明
\(<_{\forall}\) ：如果两个同维行向量 \(A\)、\(B\) 中，\(A\) 中任意一个元素都小于 \(B\) 中对应位置上的元素，则 \(A <_{\forall}B\) 为真。
\(<_{\exist}\)：如果两个同维行向量 \(A\)、\(B\) 中，\(A\) 中存在一个元素小于 \(B\) 中对应位置上的元素，则 \(A <_{\exist}B\) 为真。
\(=\) 、\(>\)、\(\neq\) 等同理。
\(R_0\) ：系统初始资源向量
\(Need\)：如果作业 \(i\) 能够被释放，则需要 \(R_0 \geq_{\forall} Need_i\)
\(A\) ：作业当前占有的资源向量，作业 \(i\) 释放后，\(A_i\) 将累加到资源向量 \(R_0\) 中
证明：
设安全性检查算法无法找到合法的安全序列时，已经释放的作业的集合为 \(W'\) 。此时，系统资源向量 \(R' = R_0 + \sum^{W'} A_{w_i}\)
此时无法找到安全序列，这说明，对于所有剩余未释放的作业 \(w \in W-W'\)，\(Need_{w} >_{\exist} R'\)。
- 不可能通过调整 \(W'\) 中作业释放的顺序改变 \(R'\) 的值。
因为 \(W'\) 中的作业的任何一种可能的释放顺序所释放的资源都是 \(\sum^{W'}A_{w_i}\) 。
- 不可能改变 \(W'\) 。
设 \(W''\) 是 \(W'\) 的一个子集，那么，必有
\[\sum^{w_i \in W''} A_{w_i} \leq_{\forall} \sum^{w_i \in W'}A_{w_i} \]因此，\(R'' \leq_\forall R'\)，释放 \(W'\) 的任何一个子集都不能把 \(W - W'\) 中的作业某一作业纳入集合，因为 \(\forall w \in W - W',Need_{w} >_{\exist} R' \geq_{\forall} R''\)。
因此我们证明了，对于一个给定的状态，如果系统中不存在安全序列，那么一定能被释放的作业的集合 \(W'\) 和不可能被释放的作业的集合 \(W - W'\) 是确定的，不因为算法的不同而不同。
在安全检查算法中，内层循环遍历所有未释放的作业，发现没有任何一个作业可被释放，就是上述的情况，已经证明了，在这种情况下，判定系统不存在安全序列是正确的。反之不出现上述情况，则系统存在安全序列的判定也是正确的。
标签：释放,Need,安全检查,作业,正确性,算法,forall,sum From： https://www.cnblogs.com/sarfish/p/17056385.html