发表刊物：计算机应用研究
刊物所在地：四川省计算机研究院
关键字：分布式K互斥算法； 概率模型检测； PRISM； 平均及时时间；
摘要：传统的验证方法难以保证分布式K互斥算法的有效性和安全性，为解决这一问题，并且给出了进一步的研究，文中提出一种基于概率模型检测器PRISM的方法，对Kerry Raymond的分布式K互斥算法进行形式化建模与分析验证。通过设置算法中各个进程进入临界区的时间，而得出的结果中，我们发现改变临界区的数目K，对于某一进程进入临界区的平均及时时间的影响并不大。如果某一进程的执行时间比其他进程大很多，则K的增加可以提高运行效率。另外，我们证明了这一结论。
页面范围：1-5
字数：4000
是否译文：否
发表时间：2014-12-04
第一作者：骆翔宇,刘来(学)