面向嵌套事务内存的多线程程序验证框架研究

• 作者: 李弋
• 来源期刊: 电脑知识与技术
• 学科: 工学
• 关键词: 事务内存 程序验证 携带证明的汇编程序
• 年，卷（期）: 2011,（25）
• 所属期刊栏目: 人工智能及识别技术
• 页码范围: 6197-6201
• 分类号: TP301
• 字数: 6043字
• 语种: 中文
• DOI: 10.3969/j.issn.1009-3044.2011.25.053

摘要

随着多线程技术的发展,并行编程逐渐成为软件开发的主流,事务内存的出现有效的解决了并行编程中锁的使用不当带来的一系列问题,而如何保证事务内存程序的正确性也成为值得关注的问题.文章介绍了一种形式验证框架,用于验证使用事务内存的并行程序的正确性.框架基于Hoare风格的程序验证方式并结合了分离逻辑的思想,包括抽象机、程序规范、语法规则及可靠性定理,支持嵌套事务程序的正确性验证,并给出一个简单的程序实例说明其在该框架中的证明过程.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	李弋	同济大学电子与信息工程学院计算机科学与技术系	2	1	1.0	1.0