本项目是并行编程中同步机制的设计、实现与验证的子项目，其研究围绕高生产率的基于共享内存的并行编程语言的设计、实现和程序验证。

研究思路

我们对高生产率并行编程语言研究的总体思路是：要想获得易编程的语言且能生成高质量的代码，程序员相应地要多提供一些简单的抽象描述，编译器利用这些信息可以提高自身的能力。其中代码的高质量指高可信、高效率、易排错等，程序员的抽象描述指共享易变数据结构(shared mutable data structure，指结构中含有通过指针访问并更新的域，如各种链表、二叉树等)的形状信息、共享资源的需求信息、函数的前后断言等，编译器的高能力指通过程序分析综合出程序更多的信息、完成程序满足规范的证明、产生携带证明的代码(PCC)等。

研究目标

研究基于共享资源需求描述的并行编程语言的设计、实现和程序验证，解决其中的核心理论和技术问题，为设计易于共享内存编程的并行编程语言奠定基础。

研究内容与方法

设计一种研究性的包含指针类型并允许使用共享易变数据结构的并行编程小语言，其特点是用共享资源需求描述来代替对共享变量访问控制的直接编程。研究从共享资源需求描述收集每个共享变量维持区间（即共享变量不能被其他线程访问的程序区间）的程序分析理论和技术，以及依据共享变量维持区间信息来生成共享变量访问控制代码的代码生成技术。扩展并行程序的Rely-Guarantee验证技术，使之能用到基于共享资源需求描述的并行程序的验证。

我们将在现有的支持C程序分析的编译基础设施上开展工作，通过实现源语言－源语言的翻译器来完成对这种研究性小语言的实现。研究中的关键问题是：

• 程序分析中的别名分析和循环不变式的推导：由于指针类型的存在，导致必须考虑访问路径(指p->front->next形式的表达式)的别名问题，因为只有获取精确的别名信息，才有可能准确得到共享变量的维持区间。精确的指针分析依赖于循环不变式。要求程序员提供循环不变式则难以被接受，而循环不变式的自动推导是个古老的问题，迄今为止只取得有限的成功。因此我们尝试要求在程序中增加一些额外的声明信息(如指针指向的数据结构形状特征、函数的前后断言等)，来降低程序分析的难度。
• 有效的共享变量访问控制代码的生成：生成锁代码的算法相对比较容易研究，其关键是结合共享变量的特征及锁开销为共享变量分配合适粒度的锁以及锁定次序。而事务内存则需要考虑与现有操作系统、编程语言和程序代码等构成的丰富且复杂的开放世界的衔接。我们将继续深化事务允许的各种操作及其语义、事务代码同非事务代码之间的交互语义等的研究，这是我们首先要做好的事情，然后才能研究什么样的程序应该生成事务代码。
• 操作共享易变数据结构的并行程序的验证：分离逻辑是目前验证使用共享易变数据结构的串行 程序所使用的最有影响的逻辑，而验证相应的并行程序则需要进一步设计逻辑。分离逻辑把堆视为互不影响的若干部分，不提供描述它们之间联系的机制，因此在描述共享易变数据结构时，难以直观地表达它们的形状特点。指针逻辑也是一种证明指针程序的专用逻辑，其优点是便于刻画各种共享易变数据结构的特 性，其缺点是证明过程复杂，因为用其规则进行推导时有繁琐的别名演算。