Verifying Parallel Low-Level Programs for Multi-core Processor

ZHU Yun-min; ZHANG Li-wei; WANG Sheng-yuan; DONG Yuan; ZHANG Su-qin

您当前的位置：

首页 >

文章列表页 >

Verifying Parallel Low-Level Programs for Multi-core Processor

更新时间：2025-07-16

- Verifying Parallel Low-Level Programs for Multi-core Processor
- Acta Electronica Sinica Vol. 37, Issue S1, Pages: 1-6(2009)
- 作者机构：
  
  1. 清华大学计算机科学与技术系,北京,100084
  2. 清华大学软件学院,北京,100084
  3. 清华大学计算机科学与技术系,北京,100084
  4. 清华大学软件学院,北京,100084
- 作者简介：
- 基金信息：
- DOI：
  CLC： TP301
- Published：2009
- 稿件说明：
移动端阅览
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：

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

Views

1063

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Transactional Memory Architecture Supporting I/O Operations within Transactions

Termination Verification of Some Kinks Nondeterministic Quantum Programs

Related Author

LIU Yi

LI Ming-xiu

ZHANG Xin

LI He

JIAO Lin

QIAN De-pei

LEI Hong-xuan

PENG Jia-yin

Related Institution

School of Computer,Beihang University

Department of Computer,Xi’an Jiaotong University

School of ComputerBeihang UniversityBeijing 100083China

Department of ComputerXi’an Jiaotong UniversityXi’anShaanxi 710049China

School of Mathematics and Information Science of Neijiang Normal University

⁰