论文研究一个分布式.pdf

传统的验证方法难以保证分布式K互斥算法的有效性和安全性。为解决这一问题，给出了进一步的研究，提出一种基于概率模型检测器PRISM的方法，对KerryRaymond的分布式K互斥算法进行形式化建模与分析验证。通过设置算法中各个进程进入临界区的时间而得出的结果中发现，改变临界区的数目K，对于某一进程进入临界区的平均及时时间的影响并不大。如果某一进程的执行时间比其他进程大很多，则K的增加可以提高运行效率。最后证明了这一结论。