论文部分内容阅读
带参并发系统广泛存在于各类计算机系统的核心模块中，验证带参系统的正确性是形式验证领域中的一个热点问题。验证带参系统的难点在于:我们可以验证带参的一个很小规模的实例，却无法保证任意规模下系统的正确性。本文在带参并发系统的模型检测方面开展了工作，在工具设计和实现以及复杂系统的建模和验证方面取得了一定的进展。
本文创造性的工作主要有三个方面:
(1)基于参数抽象和卫士增强的带参系统模型检测是一种有效且通用的用于验证带参系统的模型检测方法。通过一种启发式的计算参数抽象的不变量技术，可以使得带参系统的参数抽象和卫士增强自动化进行。以该方法和技术为理论基础，开发了一个用于验证带参系统正确性的模型检测工具PaMC。
(2)Godson-T缓存一致性协议是中国科学院计算技术研究所设计并实现的众核处理器系统Gonson-T所使用的缓存一致性协议。Godson-T协议没有使用业界经典的内存模型和缓存一致性协议，其协议内存模型和缓存一致性协议具有强耦合性，是一个很有特色的协议。使用Murphi语言对Godson-T协议进行了形式建模和验证。
(3)使用PaMC工具对一些典型的带参系统进行了建模和验证。验证的实例包括MUXSEM互斥协议、MESI协议、MOESI协议、German协议、German-2004协议以及Godson-T协议。在PaMC工具中成功验证了这些系统的安全性质。同时，将PaMC和同类工具进行了实验数据的对比和分析。