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

　　摘要：随着多线程技术的发展，并行编程逐渐成为软件开发的主流，事务内存的出现有效的解决了并行编程中锁的使用不当带来的一系列问题，而如何保证事务内存程序的正确性也成为值得关注的问题。文章介绍了一种形式验证框架，用于验证使用事务内存的并行程序的正确性。框架基于Hoare风格的程序验证方式并结合了分离逻辑的思想，包括抽象机、程序规范、语法规则及可靠性定理，支持嵌套事务程序的正确性验证，并给出一个简单的程序实例说明其在该框架中的证明过程。
　　关键词：事务内存；程序验证；携带证明的汇编程序
　　中图分类号：TP301文献标识码：A文章编号：1009-3044(2011)25-6197-05
　　Research on Verification Framework of Multi-threaded Program using Nested Transactional Memory
　　LI Yi
　　(Department of Computer Science and Technol