中文摘要：

多核处理器的应用和并发软件的需求要求我们对并发系统和程序员之间的接口- - 内存一致性模型- - 进行准确描述和使用。然而，当前对内存模型的描述，要么采用非形式化语言、准确性和完整性差，要么过于抽象、难以理解，或者描述能力单一、通用性差、无法兼顾处理器和编译优化两个方面对内存操作的影响。弱内存模型下的形式化验证更是刚刚处于起步阶段，可用成果较少。本项目拟提出一种内存一致性模型的通用描述及验证框架。从描述角度而言，我们首次提出将程序变换和分布式共享内存协议相结合的抽象机模型。该模型的形式操作语义可以用来描述处理器和并发语言两类内存模型，通用性强，且更加直观简单。从验证角度看，框架提供弱模型下并发程序等价性证明理论和新型的程序验证逻辑，分别支持编译器优化验证和并发程序验证。作为框架的应用，我们还将描述现实中的主流处理器和并发语言的内存模型，并验证代表性编译优化算法和无锁并发同步算法。

结论摘要：

内存一致性模型是并发系统和程序员之间的接口，模型的形式化描述对于有效的并发程序设计和验证有着重要意义，该问题也是程序设计语言领域的一大研究热点。本项目针对现有模型不够精确、难以理解、通用性差等问题，提出一个内存一致性模型的通用描述及验证框架，在该框架下统一形式化描述常用处理器和并发程序设计语言的内存一致性模型，并验证弱内存模型下并发算法及编译器优化的正确性。 项目的开展按照研究计划进行，并基本实现了预期目标。具体而言，我们的贡献包括（1）提出一种新型的基于抽象机操作语义的通用描述框架，该框架易于程序员理解，且具有较好的通用性。我们已经基于该框架成功给出了JMM和x86-TSO模型的描述。（2）首次提出将rely-guarantee和simulation技术相结合的模块化并发程序精化验证技术RGSim。RGSim可以作为并发程序精化验证的理论基础。基于RGSim，我们完成对若干经典并发编译优化算法的验证。（3）扩充RGSim以支持具有非固定线性化点的无所并发算法的可线性化验证，并提出一种新的支持可线性化验证的程序逻辑。完成了对经典并发队列、栈和集合算法的验证，其中一些算法直接来自于Java的java.util.concurrency库函数包，体现了程序逻辑的实用性。 本项目共发表论文8篇，包括CCF的A类会议论文2篇，其中的POPL 2012论文是第一篇第一单位来自中国大陆科研院所的POPL论文。项目培养博士后1人、博士生5人、硕士生3人。