面向多核处理器的低级并行程序验证

摘要：

随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求,多核并行程序验证的重要性日益凸显。本文提出了一个完整的基于多核的并行程序验证框架,该验证框架包括抽象机器定义、目标代码的形式规范、逻辑推理系统、可靠性定理及其证明。目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问。验证框架采用Hoare风格的推导方式,使用高阶逻辑来同时描述机器指令的操作语义和所需要的安全策略。在该框架下,程序员可以对多核并行程序的部分正确性进行验证。

关键词： 程序验证 多核处理器 并行程序

作者: 朱允敏 张丽伟 王生原 董渊 张素琴

作者单位: 清华大学计算机科学与技术系 北京 100084 清华大学软件学院 北京 100084

会议类型: 国内会议

会议名称: 2008全国软件与应用学术会议(NASAC”08)

会议地点: 广州

会议语种:中文

页码: 282-287

在线出版日期: 2008-11-11（万方平台首次上网日期，不代表论文的发表时间）