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

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

您当前的位置：

首页 >

文章列表页 >

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

学术论文 | 更新时间：2025-07-16

- 面向多核处理器的低级并行程序验证
- Verifying Parallel Low-Level Programs for Multi-core Processor
- 电子学报 2009年37卷第S1期页码：1-6
- 作者机构：
  
  1. 清华大学计算机科学与技术系,北京,100084
  2. 清华大学软件学院,北京,100084
  3. 清华大学计算机科学与技术系,北京,100084
  4. 清华大学软件学院,北京,100084
- 作者简介：
- 基金信息：
  
  国家自然科学基金 (No.60573017)
- DOI：
  中图分类号： TP301
- 纸质出版：2009
- 稿件说明：
移动端阅览
朱允敏, 张丽伟, 王生原, 等. 面向多核处理器的低级并行程序验证[J]. 电子学报, 2009,37(S1):1-6.

ZHU Yun-min, ZHANG Li-wei, WANG Sheng-yuan, et al. Verifying Parallel Low-Level Programs for Multi-core Processor[J]. Acta Electronica Sinica, 2009, 37(S1): 1-6.
朱允敏, 张丽伟, 王生原, 等. 面向多核处理器的低级并行程序验证[J]. 电子学报, 2009,37(S1):1-6. DOI：

ZHU Yun-min, ZHANG Li-wei, WANG Sheng-yuan, et al. Verifying Parallel Low-Level Programs for Multi-core Processor[J]. Acta Electronica Sinica, 2009, 37(S1): 1-6. DOI：

摘要

随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求

多核并行程序验证的重要性日益凸显.本文提出了一个完整的基于多核的并行程序验证框架

该验证框架包括抽象机器定义、目标代码的形式规范、逻辑推理系统、可靠性定理及其证明.我们的目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问.验证框架采用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.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.Pro grammers can verify the partial correctness of multi-core parallel programs in our framework.

关键词

Keywords

references

浏览量

1063

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

一种支持事务内I/O操作的事务存储系统结构

几类非确定型量子程序的终止验证