本项目是并行编程中同步机制的设计、实现与验证的子项目，其研究围绕高可信并行软件构造中同步机制的各种实现技术和相关的程序验证方法。

研究思路

我们对高可信并行软件中同步机制研究的主要思路是：在汇编语言级，通过扩展邵中教授等提出的CCAP验证框架，设计面向各种同步实现技术的专用程序逻辑(是描述和验证使用各种同步实现技术的并行程序性质的Hoare风格的逻辑)，达到构造携带基础证明的程序(FPCC)的目标；汇编级的验证框架可以与出具证明的编译器(certifying compiler)或经过证明的编译器(certifiedcompiler)相结合，指导高层同步抽象的设计和实现，使得人们可以在源语言级基于高层同步抽象编程并验证程序，而通过编译器产生汇编级携带证明的代码(PCC)。在汇编语言级，各种同步实现技术的正确性通过验证使用这些技术的并行程序的安全性来保证。

当前的研究目标

在汇编语言级研究以事务内存为中心、融合锁等机制的各种同步实现技术和相关的程序验证方法，解决其中的核心理论和技术问题，指导高层同步抽象的设计和实现，为构造高可信的并行软件奠定基础。

研究内容与方法

以类型和Hoare风格的逻辑推理为主要手段，通过扩展CCAP验证框架，研究实现同步的各种锁技术、事务内存技术以及混合事务内存和锁等的技术及其正确性验证。

CCAP验证框架是以CiC(Calculus of Inductive Constructions)作为底层的元逻辑，从元逻辑可以构造面向各种专用领域的Hoare风格的专用逻辑。设计专用逻辑一方面可以简化对专用领域程序的描述和验证，另一方面这些专用逻辑都可以映射到底层的元逻辑上，从而使用不同专用逻辑证明过的代码均能被元逻辑证明而能安全地共存。

我们主要按如下步骤开展研究：①定义含有支持某种同步实现技术的原语/指令的抽象机模型(包括语法和操作语义)；②定义由程序规范语言以及推理抽象机上执行的程序的推理规则组成的程序逻辑；③通过完成程序逻辑系统的进展(Progress)及保持(Preservation)引理的证明来保证抽象机上的合法程序都是安全的；④通过在验证框架中完成一些例子的证明展示验证框架的有效性；⑤上述机器模型的定义、程序逻辑的描述和语言安全性证明、实例程序的性质证明都用定理证明辅助工具Coq完成。

程序逻辑以支持模块化验证的Rely-Guarantee方法(也称Assume-Guarantee方法)为基础，结合并发分离逻辑、权限控制、 基于不变式的证明技术等手段来设计。