Peterson算法在Isabelle/HOL中的互斥性证明

摘要

如何保证并发互斥的正确性，这是当代操作系统和各种大型应用软件设计中需要考虑的一个重要的问题。Peterson算法是互斥问题研究领域的一个经典算法,对该算法的安全性和活性目前缺乏完整严格的证明.基于交互式定理证明工具Isabelle/HOL证明了两个并发任务的Peterson算法的互斥属性.证明过程采用了Paulson的归纳法思想,将Peterson算法建模为所有可能事件序列的集合.该模型易于扩展用于活性的证明.