|
OALib Journal期刊
ISSN: 2333-9721
费用：99美元
|
|
|
|
面向多核处理器的低级并行程序验证
, PP. 1-6
Keywords: 程序验证,多核处理器,自旋锁,汇编级代码,部分正确性
Abstract:
随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求,多核并行程序验证的重要性日益凸显.本文提出了一个完整的基于多核的并行程序验证框架,该验证框架包括抽象机器定义、目标代码的形式规范、逻辑推理系统、可靠性定理及其证明.我们的目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问.验证框架采用Hoare风格的推导方式,使用高阶逻辑来同时描述机器指令的操作语义和所需要的安全策略.在该框架下,程序员可以对多核并行程序的部分正确性进行验证.
| [1] | G Necula.Proof-carrying code[A].In Proc ACM POPL''97[C].New York:ACM Press,1997.106-119.
|
| [2] | A W Appel.Foundational proof-carrying code[A].In Proc 16th IEEE Syrup on Logic in Computer Science[C].IEEE Computer Society,2001.247-258.
|
| [3] | Y Bertot,P Casteran.Coq''Art:The Calculus of Inductive Constuctions[M].Berlin:Springer-Verlag,2004.
|
| [4] | Xinyu Feng,Zhong Shao,et al.Modular verification of assembly code with stack-based control abstractions[A].In Proc ACM PLDI''06[C].New York:ACM Press,2006.401-414.
|
| [5] | Hongxu Cai,Zhong Shao,et al.Certified self-modifying code[A].In Proc ACM PLDI''07[C].New York:ACM Press,2007.66-77.
|
| [6] | Xinyu Feng,Zhong Shao,Yuan Dong,Yu Guo.Certifying lowlevel programs with hardware Interrupts and preemptive threads[A].In Proc ACM PLDI''08[C].New York:ACM Press,2008.170-182.
|
| [7] | G Morrisett,D Walker,K Crary,N Glew.From system F to typed assembly language[A].In Proc ACM POPL''98[C].New YOrk:ACM Press,1998.85-97.
|
| [8] | C Colby,P Lee,G Necula,et al.A certifying compiler for Java[A].In Proc ACM PLDI''00[C].New York:ACM Press,2000.95-107.
|
Full-Text
|
|
Contact Us
service@oalib.com QQ:3279437679 
WhatsApp +8615387084133
|
|
