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

2009-10-6 09:56:26 2397

0 面向多核处理器的低级并行程序验证要随着多核处理器的广泛使用以及人们对软件提出了更高的可靠性要求，多核并行程序验证的重要性日益凸显。本文提出了一个完整的基于多核的并行程序验证框架，该验证框架包括抽象机器定义、目标代码的形式规范、逻辑推理系统、该系统的可靠性定理及其证明。我们的目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问。验证框架采用Hoare风格的推导方式，使用高阶逻辑来同时描述机器指令的操作语义和所需要的安全策略，使得在该框架下可以验证多核并行程序的部分正确性。关键词多核处理器，自旋锁，程序验证，汇编级，部分正确性 Abstract As the multi-core processor is widely used and advanced high-trusted software is required, the verification of parallel programs for multi-core processor becomes more and more important. This paper presents a proof framework about the verification of parallel programs, including the definition of our abstract machine, the formal specification for object code, logic inference rules and the proof of soundness theory. We certify the code at an assembly-level directly in order to disregard the correctness of compilers. The classic spin-lock technology is introduced to implement the mutually exclusive access to shared memory. Our proof framework supports Hoare-logic style reasoning. In addition, we use high-order logic to describe both operational semantics and security-policy, so the partial correctness of multi-core parallel programs can be verified in our system. Key words multi-core processor, spin lock, verification, assembly level, partial correctness. 游客，如果您要查看本帖隐藏内容请回复 0
2009-10-6 09:56:26　　评论淘帖0 举报相关推荐 • 程序验证研究综述 0 • 如何使用OpenMP实现电磁场FDTD多核并行程序的设计 0 • 基于OpenMP应用层开发多核并行程序的机制 1 • 多核处理器视频编码并行加速算法 41 • 长安航空成功完成了CCO/CDO飞行程序验证试飞工作 1263 • 航空电子认证中的正式程序验证 877 • 多核处理器的优点 4625 • 多核处理器是指什么 1099 • 多核加速串行程序威廉希尔官方网站综述 17 • 通信Petri网的异步通信程序验证 0