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

• 作者: 张丽伟 张素琴 朱允敏 王生原 董渊
• 来源期刊: 电子学报
• 学科: 工学
• 关键词: 程序验证 多核处理器 自旋锁 汇编级代码 部分正确性
• 年，卷（期）: 2009,（z1）
• 所属期刊栏目: 学术论文
• 页码范围: 1-6
• 页数: 6页
• 分类号: TP301
• 字数: 5771字
• 语种: 中文
• DOI: 10.3321/j.issn:0372-2112.2009.z1.001

摘要

随着多核处理器的广泛使用以及人们对软件可靠性提出更高要求,多核并行程序验证的重要性日益凸显,本文提出了一个完整的基于多核的并行程序验证框架,该验证框架包括抽象机器定义、目标代码的形式规范、逻辑推理系统、可靠性定理及其证明.我们的目标程序使用自旋锁机制来实现线程间对共享内存的互斥访问.验证框架采用Hoare风格的推导方式,使用高阶逻辑来同时描述机器指令的操作语义和所需要的安全策略.在该框架下,程序员可以对多核并行程序的部分正确性进行验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张素琴	清华大学计算机科学与技术系	43	714	14.0	26.0
2	董渊	清华大学计算机科学与技术系	33	386	10.0	18.0
3	王生原	清华大学计算机科学与技术系	33	235	8.0	14.0
4	朱允敏	清华大学计算机科学与技术系	2	12	2.0	2.0
5	张丽伟	清华大学软件学院	3	12	2.0	3.0