并发编程中的声明式并发与并行程序竞态检测技术

### 并发编程中的声明式并发与并行程序竞态检测技术 在并发编程的领域中，有两个关键的研究方向值得深入探讨，一是声明式并发在 Java 中的应用，二是并行程序中竞态检测的可扩展监控技术。 #### 声明式并发在 Java 中的应用 在传统的并发编程提议中，方法执行通常被视为最小的并发单元，但在实际的并发编程里，我们往往需要更细粒度的并发控制。 ##### 时间约束 以往关于时间约束形式化的研究主要聚焦于实时系统的规范和验证，例如 RTL 和带时间的 Hoare 逻辑。同时，也有关于实时程序综合的语言表示研究，像 TCEL、CRL、TimeC 和 Tempo 等。其中，Tempo 是最相关的工作，它是一种声明式并发编程语言，将进程明确描述为部分有序的事件集合。而我们考虑的语言是将事件与程序中的关注点相关联，通过对事件施加时间约束来指定对象集合的安全属性。 ##### 并发编程的逻辑程序 我们提出了一种逻辑语言来陈述并发面向对象系统的安全属性。该语言一方面强调声明性，另一方面便于执行。与其他并发编程方法不同，我们的提议仅关注系统同步问题的规范，应用功能被抽象掉，因此可以用任何传统的面向对象编程语言编写。 - **事件和约束**：许多研究人员提出了使用部分有序事件集合来推理时间现象的方法。我们的并发编程方法基于相同的总体思路，使用约束逻辑程序来表示感兴趣的约束集合（通常是无限的）。约束的形式为 `X < Y`，表示“X 在 Y 之前”或“X 的执行时间小于 Y 的执行时间”，其中 X 和 Y 是事件，`<` 是偏序关系。 - 约束逻辑程序的定义如下：常量范围涵盖事件类 E、F 等，有一个特殊的（后缀）函子 `+`。除变量外，感兴趣的项有 e、e+、e++ 等。e 表示类 E 中的第一个事件，e+ 表示下一个事件，依此类推。对于任何事件 X，X+ 隐式地在 X 之后，即 `X < X+`。 - 程序事实的形式为 `p(t1, ..., tn)`，其中 p 是用户定义的谓词，ti 是基项。程序规则的形式为 `p(X1, ..., Xn) ← B`，其中 Xi 是不同的变量，B 是规则体，其变量在 `{X1, ..., Xn}` 中。一个程序是有限的规则集合，用于定义事件上的一族偏序关系。 - 例如： ```plaintext p(e,f). p(E, F) ← E < F, p(E+, F+). ``` 这个程序定义了一个偏序关系 `e < f, e+ < f+, e++ < f++` 等。而下面的程序： ```plaintext p(e,f). p(E, F) ← E < F, p(E+, F+). p(E, F) ← F < E, p(E+, F+). ``` 则定义了一族关于 `{e, f, e+, f+, e++, f++, e+++ ...}` 的偏序关系。 - 以生产者 - 消费者问题为例，如果假设是无限缓冲区，消费者永远不会尝试从空缓冲区中移除项目的安全属性可以表示为： ```plaintext p(append, remove). p(X, Y) ← X < Y, p(X+, Y+). ``` 对于有界缓冲区，生产者仅在缓冲区未满时尝试追加项目的安全属性，对于大小为 5 的缓冲区可以表示为： ```plaintext p(remove, append(+5)). p(X, Y) ← X < Y, p(X+, Y+). ``` - **标记和事件**：为了引用程序中关注点的访问时间，我们引入了标记。标记声明由尖括号括起来的事件名称组成，例如 `<e>`。如果仅考虑应用程序的功能语义，标记注释可以简单地视为程序注释。标记与指令之间的程序点相关联，可能在不同的线程中。可以在这些标记划定的程序点之间指定约束。对于标记 M，`time(M)` 表示紧接在 M 之前的指令刚刚完成的时间。在不太可能引起混淆的情况下，我们将 `time(M)` 简称为 M。给定一对标记，可以声明约束来指定它们在程序所有执行中的相对执行顺序。如果线程 T1 的执行到达一个程序点，其执行时间被约束为大于另一个线程 T2 中尚未执行的程序点的执行时间，线程 T1 将被迫暂停执行。在存在循环和过程调用的情况下，标记在程序执行期间通常会被多次访问。因此，一般来说，与程序点 p 相关联的标记 M 表示一个事件类 E，其每个实例 e、e+、e++ 等对应于程序执行期间对 p 的一次访问（e 表示第一次访问，e+ 表示第二次访问，依此类推）。 - **约束和方法**：有时，用面向对象程序的方法而不是代码中的特定程序点来表达同步方面更为方便。因此，我们的语言允许更高级别的约束形式 `p(c,m1,m2) ⇔ q(e1,e2, ... ek)`，其中 m1 和 m2 是类 c 中的方法，e1、e2 ... ek 是 m1 或 m2 代码中的程序点（即标记）。这可以看作是在之前定义的基础语言上添加了一些语法糖。 ##### 同步约束 以有界栈数据类型的 Java 实现为例，说明如何使用我们提出的语言来指定并发面向对象系统的并发问题（安全属性）。 - 没有同步代码的基本规范如下： ```java class BoundedStack { static final int MAX = 10; int pos = 0; Object[] contents = new Object[MAX]; public Object peek() { <a1> return contents[pos]; <a2> } public Object pop() { <a3> return contents[--pos]; <a4> } public void push(Object e) { <a5> contents[pos++] = e; <a6> } } ``` 添加同步代码后的规范如下： ```java public class BoundedStack { private static fina ```