会议专题

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

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

程序验证 多核处理器 并行程序

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

清华大学计算机科学与技术系 北京 100084 清华大学软件学院 北京 100084

国内会议

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

广州

中文

282-287

2008-11-11(万方平台首次上网日期,不代表论文的发表时间)