摘要: 1．本文的创新点
　　本文提出了一个用于验证基于惰性软件事务内存同步机制的并行程序的验证框架，它是一个携带证明的代码（Proof-Carrying Code，简称PCC）风格的验证框架。此框架中的事务内存模型比较贴近实际，且使用了一种结合并发分离逻辑（Concurrent Separation Logic）和带权限计数的分离逻辑（Permission Accounting in Separation Logic）的程序逻辑。该验证框架可以用于验证事务代码的部分正确性（partial correctness，程序的行为符合给定的安全规范）、共享内存的不变式属性、以及一些其他特殊的并行程序属性。本文最后通过实例证明来展示此验证框架的有效性。
 
2．实现方法
       在汇编层定义了一个使用惰性版本控制和冲突检测机制的软件事务内存模型的抽象机，包括指令集、机器状态和操作语义。该模型的主要特点是：1）使用一种轻量级的锁机制来保证对共享资源的互斥访问。锁与非锁单元无区别地存储在共享内存中。2）将事务代码的执行过程分成act（活动）、cmt（提交）、abt（异常中止）三个阶段，通过将不可回滚的操作（比如像系统调用、输入输出等）延迟到cmt阶段执行来支持它们在事务中出现。
在程序逻辑的设计上，结合了并发分离逻辑和带权限计数的分离逻辑，它可以将共享内存中的每个单元分成仅有只读权限的两个部分，在执行私有化时转移其中一个仅有只读权限的部分到线程的逻辑私有内存中，留下另一个在逻辑共享内存中，以支持事务代码中的投机读操作。
       之后将这些程序推理方法形式化到推理抽象机及其上执行的程序的推理规则中，并通过可靠性证明来体现推理规则遵循了抽象机的操作语义。最后在此验证框架中完成一些实例证明来展示验证框架的有效性。整个验证框架、可靠性证明以及实例证明都是在定理辅助工具Coq中完成的。
 
3．结论及未来待解决的问题
       本文提出了一个验证基于惰性软件事务内存实现机制的程序的验证框架，通过该框架可以验证事务代码的安全性以及一些其他属性。此验证框架的可靠性及有效性通过在定理证明辅助工具Coq中完成了机器可检查的验证框架可靠性证明及例子证明得到了保证。本文仅讨论了使用该验证框架验证程序的部分正确性，下一步研究将探讨在验证框架中支持活跃属性（Liveness Property）以及可线性化（linearizability）的验证。此外，我们也将考虑使用急切版本控制和冲突检测机制的软件事务内存程序的验证。
 
4．实用价值或应用前景
       随着超线程、多核多处理等新一代系统结构对并行的全面支持，软件开发方式产生了巨变，能够发挥其性能的并行程序得到了广泛的应用，逐渐成为主流的方向。但是其同时也给程序员带来了很大的挑战，开发并行程序要困难很多。以往主要是用锁同步技术来保证共享资源的互斥访问，传统的锁技术不仅编程复杂，也容易导致死锁、优先级倒置等一些问题。事务内存的出现为并发控制提供了新的渠道，它将并发控制管理转移给了开发语言支撑环境的系统设计者，从而释放了程序员的负担。现有的围绕事务内存的研究主要集中在支持事务内存机制系统的各种实现策略以及性能发面，关于事务内存代码的正确性和程序推理验证方面却很少。本文提出的PCC风格的基于事务内存的并行程序的验证框架正是关注于事务代码的安全性，使用多种程序验证技术来推理验证基于事务内存同步机制的并行程序的性质。