Formal Verification of the MCS List-Based Queuing Lock

Formal Verification of the MCS List-Based Queuing Lock
复制标题

基于MCS列表的排队锁的形式化验证

DOI：
10.1007/3-540-46674-6_24
复制
发表时间：
1999
期刊：
--
影响因子：
--
通讯作者：
K. Futatsugi
K. Futatsugi
中科院分区：
--
文献类型：
--
作者：
K. Ogata;K. Futatsugi

文献摘要

被引文献

相似文献

使用CafeOBJ和Unity对MCS基于列表的排队锁算法(MCS)进行了形式化验证。我们已经展示的是，它具有两个性质：一个以上的进程永远不能同时进入它们的临界区，而一个想要进入临界区的进程最终会进入那里。首先，采用统一计算模型在CafeOBJ中描述了一种简单排队锁算法(MCS0)，并用统一逻辑进行了验证。其次，借助CafeOBJ证明了MCS1到MCS0之间存在模拟关系，从而验证了一个与MCS0相同的排队锁算法(MCS1)。最后，MCS是由稍作修改的MCS1衍生而来的。
We have formally verified the MCS list-based queuing lock algorithm (MCS) with CafeOBJ and UNITY. What we have shown is that it has the two properties that more than one process can never enter their critical section simultaneously and a process wanting to enter a critical section eventually enters there. First a simple queuing lock algorithm (MCS0) has been specified in CafeOBJ by adopting UNITY computational model, and verified with UNITY logic. Secondly a queuing lock algorithm (MCS1) specified in the same way as MCS0 has been verified by showing the existence of a simulation relation from MCS1 to MCS0 with the help of CafeOBJ. Lastly MCS has been derived from a slightly modified MCS1.