面向多核处理器的低级并行程序验证
随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求,多核并行程序验证的重要性日益凸显。本文提出了一个完整的基于多核的并行程序验证框架,该验证框架包括抽象机器定义、目标代码的形式规范、逻辑推理系统、可靠性定理及其证明。目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问。验证框架采用Hoare风格的推导方式,使用高阶逻辑来同时描述机器指令的操作语义和所需要的安全策略。在该框架下,程序员可以对多核并行程序的部分正确性进行验证。
程序验证 多核处理器 并行程序
朱允敏 张丽伟 王生原 董渊 张素琴
清华大学计算机科学与技术系 北京 100084 清华大学软件学院 北京 100084
国内会议
广州
中文
282-287
2008-11-11(万方平台首次上网日期,不代表论文的发表时间)