电子学报
電子學報
전자학보
ACTA ELECTRONICA SINICA
2009年
z1期
1-6
,共6页
朱允敏%张丽伟%王生原%董渊%张素琴
硃允敏%張麗偉%王生原%董淵%張素琴
주윤민%장려위%왕생원%동연%장소금
程序验证%多核处理器%自旋锁%汇编级代码%部分正确性
程序驗證%多覈處理器%自鏇鎖%彙編級代碼%部分正確性
정서험증%다핵처리기%자선쇄%회편급대마%부분정학성
随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求,多核并行程序验证的重要性日益凸显,本文提出了一个完整的基于多核的并行程序验证框架,该验证框架包括抽象机器定义、目标代码的形式规范、逻辑推理系统、可靠性定理及其证明.我们的目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问.验证框架采用Hoare风格的推导方式,使用高阶逻辑来同时描述机器指令的操作语义和所需要的安全策略.在该框架下,程序员可以对多核并行程序的部分正确性进行验证.
隨著多覈處理器的廣汎使用以及人們對軟件可靠性提齣更高要求,多覈併行程序驗證的重要性日益凸顯,本文提齣瞭一箇完整的基于多覈的併行程序驗證框架,該驗證框架包括抽象機器定義、目標代碼的形式規範、邏輯推理繫統、可靠性定理及其證明.我們的目標程序使用自鏇鎖機製來實現線程間對共享內存的互斥訪問.驗證框架採用Hoare風格的推導方式,使用高階邏輯來同時描述機器指令的操作語義和所需要的安全策略.在該框架下,程序員可以對多覈併行程序的部分正確性進行驗證.
수착다핵처리기적엄범사용이급인문대연건가고성제출경고요구,다핵병행정서험증적중요성일익철현,본문제출료일개완정적기우다핵적병행정서험증광가,해험증광가포괄추상궤기정의、목표대마적형식규범、라집추리계통、가고성정리급기증명.아문적목표정서사용자선쇄궤제래실현선정간대공향내존적호척방문.험증광가채용Hoare풍격적추도방식,사용고계라집래동시묘술궤기지령적조작어의화소수요적안전책략.재해광가하,정서원가이대다핵병행정서적부분정학성진행험증.
