利用mn差分分解数据结构交换性证明

### 利用mn差分分解数据结构交换性证明 #### 1. 引言 数据结构方法的交换性在并行编译器、事务内存、推测执行和软件可扩展性等领域一直备受关注。交换性条件描述了两个方法在何种条件下可以交换执行顺序而不影响最终结果和返回值，它比完整规范更简洁，却能有效支持并发执行。然而，目前在交换性验证方面，现有的工作要么缺乏可靠性，要么依赖数据结构规范作为中介，可能导致不可靠的交换性结论。 本文旨在直接从方法的源代码验证交换性属性 $\phi_{m}^{n}$。首先提出了一种将问题转化为多轨迹（2 - 安全）问题的方法，即 `Reducen_m`。它是一个产品程序，强化了前置条件，仅考虑可达的数据结构状态，同时弱化了后置条件，采用观察等价性。但该方法未使用交换性特定的抽象，导致可达性求解器难以验证。 核心思想是引入 `mn` - 差分抽象 $(\alpha, R_{\alpha})$，它规定了抽象 $\alpha$ 的精度要求，使得在抽象域中推理并关联抽象后置状态 $R_{\alpha}$ 时，能保证具体域中的返回值一致。通过结合 $R_{\alpha}$、跟踪未修改克隆部分状态的关系 $C$ 以及特定于抽象数据类型（ADT）的观察等价关系 $I_{\beta}$，解决了交换性验证问题。还引入了 `DAReducen_m` 算法，它利用 `mn` - 差分，将可达性分析任务分解为两个自动机 $AA(m, n, \phi_{m}^{n}, I)$ 和 $AB(I)$，提高了交换性验证的可扩展性。 #### 2. 示例与问题分析 - **示例**：以 `SimpleSet` 和 `ArrayStack` 为例，展示了交换性条件的复杂性。例如，`SimpleSet` 中 `isin(x)` 和 `isin(y)` 总是可交换的，而 `add(x)` 和 `isin(y)` 的交换性条件则较为复杂。`ArrayStack` 中 `push(x)` 和 `pop` 的交换性条件为 $\phi_{push(x)}^{pop} \equiv top > -1 \land A[top] = x \land top < MAX$。 - **问题挑战**：尝试使用 Hoare 四元组和现有工具验证交换性时，会遇到具体相等性过于严格的问题。例如，对于 `ArrayStack`，自动化工具可能无法识别某些状态是等价的。使用规格说明也存在精度难以确定的问题，过粗的规格可能导致错误的交换性结论，而过细的规格又可能包含与交换性无关的细节。 #### 3. 预备知识 - **对象模型**：使用顺序面向对象语言的简单模型，对象有成员字段，方法的源代码从 C 解析为控制流自动机（CFA）。 - **交换性与交换性条件**：定义了对象的具体状态空间 $\Sigma$，以及大步骤语义 $\sigma \xrightarrow{m(\overline{a})/\overline{u}} \sigma'$。交换性定义为两个方法在任意顺序执行时，返回值一致且最终状态观察等价。交换性条件 $\phi_{m}^{n}$ 是一个逻辑公式，描述了两个方法可交换的初始状态和参数条件。 #### 4. 一次性归约到可达性 将交换性验证问题转化为可达性问题，提出了 `Reducen_m` 算法。它通过以下步骤实现： 1. **强化前置条件**：对对象状态 $\sigma_1$ 进行任意数量的方法实现，假设交换性条件 $\phi_{m}^{n}$ 成立，并将状态复制到 $\sigma_2$。前置条件可表示为 $\{Reachable(\sigma_1) \land \phi_{m}^{n}(\sigma_1, \overline{a}, \overline{b}) \land \sigma_1 = \sigma_2\}$。 2. **弱化后置条件**：后置条件要求返回值一致，并通过循环执行任意方法，确保后续执行也不会出现返回值不一致的情况。后置条件可表示为 $\{r_1^m = r_2^m \land r_1^n = r_2^n \land ObsEq(\sigma_1, \sigma_2)\}$。 如果输出的自动机 $A(\phi_{m}^{n})$ 中的错误状态不可达，则 $\phi_{m}^{n}$ 是有效的交换性条件。 以下是 `Reducen_m` 应用于 `SimpleSet` 的 `add(x)` 和 `isin(y)` 方法的伪代码示例： ```plaintext 1 SimpleSet s1 = new SimpleSet(); Pre - cond. 2 while(*) { int t = *; assume (t>0); switch(*) { 3 case 1: [add]1(t); case 2: [isin]1(t); 4 case 3: [size]1(); case 4: [clear]1(); }} 5 int x = *; int y = *; 6 assume( ϕ isin(y) add(x) (s1,x,y) ); 7 SimpleSet s2 = s1.clone(); 8 r1 m = [add]1(x); r2 n = [isin]2(y); Quad. r1 n = [isin]1(y); r2 m = [add]2(x); 9 assert(r1 m=r2 m && r1 n=r2 n); Post - cond. 10 while(true){ int t=*; assume(t>0); switch(*) { 11 case 1: assert([add]1(t) == [add]2(t)); 12 case 2: assert([isin]1(t) == [isin]2(t)); 13 case 3: assert([clear]1() == [clear]2()); 14 case 4: assert([size]1() == [size]2()); } } ``` #### 5. 利用 `mn` - 差分分解交换性 - **问题提出**：通用的可达性求解器在处理 `Reducen_m` 时，可能会搜索过于精确的抽象，导致不必要的计算。例如，在验证 `ArrayStack` 的 `push(x)` 和 `pop` 方法时，求解器可能会考虑深层栈值，而这些值在不同执行顺序下是相同的。 - **`mn` - 差分抽象**：通过以下图示说明 `mn` - 差分的思想： ```mermaid graph LR classDef startend fill:#F5EBFF,stroke:#BE8FED,stroke-width:2px; classDef process fill:#E5F6FF,stroke:#73A6FF,stroke-width:2px; classDef decision fill:#FFF6CC,stroke:#FFBC52,stroke-width:2px; A(σ1):::process -->|m(¯a); n(¯b)| B(σ′1):::process C(σ2):::process -->|n(¯b); m(¯a)| D(σ′2):::process A -->|α| E(ˆσ1):::process B -->|α| F(ˆσ′1):::process C -->|α| G(ˆσ2):::process D -->|α| H(ˆσ′2):::process E -->|ˆm(¯a); ˆn(¯b)| F G -->|ˆn(¯b); ˆm(¯a)| H style A stroke-dasharray: 5 5 style C stroke-dasharray: 5 5 linkStyle 0 stroke:#000,stroke-width:2px linkStyle 1 stroke:#000,stroke-width:2px linkStyle 2 stroke:#000,stroke-width:2px linkStyle 3 stroke:#000,stroke-width:2px linkStyle 4 stroke:#000,stroke-width:2px linkStyle 5 stroke:#000,stroke-width:2px linkStyle 6 stroke:#000,stroke-width:2px linkStyle 7 stroke:#000,stroke-width:2px ``` 从两个相等的状态 $\sigma_1$ 和 $\sigma_2$ 开始，经过不同顺序的方法执行得到后置状态 $\sigma_1'$ 和 $\sigma_2'$，要求返回值一致。引入特定于 `m/n` 对的抽象 $\alpha$ 和抽象域中的产品程序，关系 $R_{\alpha}$ 关联抽象后置状态，确保在抽象域中返回值一致时，具体域中也一致。 例如，对于 `isin(x)/clear`，定义抽象 $\alpha$ 包含谓词 $\{a = x, a \neq x, b = x, b \neq x\}$，则 $R_{1\alpha}(\sigma_1, \sigma_2) \equiv (a = x)_1 \lor (b = x)_1 \Leftrightarrow (a = x)_2 \lor (b = x)_2$。对于 `ArrayStack` 的 `pop/pop`，定义抽象 $\alpha$ 包含谓词 $\{top > 1, A[top - 1] = A[top]\}$，则 $R_{2\alpha} \equiv (top > 1)_1 = (top > 1)_2 \land (A[top - 1] = A[top])_1 = (A[top - 1] = A[top])_2$。 - **克隆未修改部分**：`mn` - 差分抽象忽略的状态部分在不同执行顺序下未被修改，通过克隆关系 $C$ 跟踪这些部分。例如，对于 `ArrayStack`，$C \equiv \forall i < top_1. A_1[i] = A_2[i]$。 - **后置状态等价性**：仅 $R_{\alpha} \land C$ 不能完全刻画交换性，还需要使用特定于 ADT 的观察等价关系 $I_{\beta}$。对于 `ArrayStack` 和 `SimpleSet`，分别有观察等价关系： - $I_{AS}(\sigma_1, \sigma_2) \equiv top_1 = top_2 \land (\forall i. 0 \leq i \leq top_1 \Rightarrow A_1[i] = A_2[i])$ - $I_{SS}(\sigma_1, \sigma_2) \equiv ((a_1 = a_2 \land b_1 = b_2) \lor (a_1 = b_2 \land b_1 = a_2)) \land (sz_1 = sz_2)$ 通过以下证明规则将各部分联系起来： ```plaintext (i) : {Iβ}[sm]1(¯x) | [sm]2(¯y){Iβ} (ii) : {Rch ∧ϕn m} [sm]1(¯x); [sn]1(¯x) | [sn]2(¯y); [sm]2(¯y) {Rα ∧C} (iii) : (Rα ∧C) =⇒Iβ ϕn m is a commut. cond. for m(¯x) ▷◁n(¯y) ``` #### 6. 基于自动机验证的 `mn` - 差分 `Reducen_m` 生成的编码使通用可达性求解器难以处理，因此引入 `DAReducen_m` 算法。它将推理过程分解为两个阶段： - **阶段 A**：找到足够的 $R_{\alpha}$ 和克隆框架 $C$，使得 $R_{\alpha} \land C \Rightarrow I$。自动机 $AA(m, n, \phi_{m}^{n}, I)$ 提前结束，通过断言返回值一致和 $I$ 必须成立，促使分析构建抽象 $\alpha$、`mn` - 差分关系 $R_{\alpha}$ 和克隆框架 $C$。 - **阶段 B**：证明 $I$ 是观察等价关系。自动机 $AB(I)$ 通过假设 $I$ 成立，然后对任意 ADT 方法进行非确定性选择，要求返回值一致且 $I$ 仍然成立。如果 $AA(m, n, \phi_{m}^{n}, I)$ 和 $AB(I)$ 都安全，则 $\phi_{m}^{n}$ 是有效的交换性条件。 `DAReducen_m` 的输出自动机可表示为： ```plaintext AA(m, n, ϕn m, I) AB(I) σ1.init(); while(∗){σ1.m(¯a); where m(¯a) chosen nondet.} assume(ϕn m(σ1, ¯a,¯b)); σ2 = σ1.clone(); r1 m := σ1.m(¯a); r2 n := σ2.n(¯b); r1 n := σ1.n(¯b); r2 m := σ2.m(¯a); assert(r1 m = r2 m ∧r1 n = r2 n); //Rα assert(I(σ1, σ2)); //Rα ∧C =⇒I assume(I(σ1, σ2)); let m(¯a) chosen nondet. in r1 = σ1.m(¯a); r2 = σ2.m(¯a); assert(r1 = r2 ∧I(σ1, σ2)); ``` #### 7. 评估 - **实验设置**：实现了概念验证工具 `CityProver`，它基于 `Ultimate` 和 `CPAchecker` 实现 `Reducen_m` 和 `DAReducen_m` 算法。输入为 C 风格的源代码、交换性条件 $\phi_{m}^{n}$ 和方法名。 - **实验结果**： - **单字段对象**：对内存单元、累加器和计数器等单字段对象进行实验，验证了不同方法对的交换性条件。结果表明，`DAReducen_m` 虽然在启动可达性分析时存在一定开销，但在某些情况下不会超时，而 `Reducen_m` 可能会出现超时问题。 - **简单数据结构**：对 `ArrayStack`、`SimpleSet`、队列和哈希表等简单数据结构进行实验。在大多数情况下，`DAReducen_m` 优于 `Reducen_m`，平均速度提升可达 3.88 倍。`Reducen_m` 在 15 个案例中出现超时或内存不足问题，而 `DAReducen_m` 仅在 6 个案例中出现超时。 - **观察等价关系的优势**：与前置/后置规格说明相比，观察等价关系更简单，不会导致不可靠的交换性结论。具有以下优点： - **可靠性**：观察等价关系保证了交换性证明的精度。 - **简单性**：只需要考虑关系所描述的抽象结构，避免了前置/后置规格说明可能带来的冗余和不必要的细节。 - **集中性**：单个观察等价关系适用于所有方法，更加集中且简洁。 - **自动化**：推断观察等价关系是一个更明确且可实现的目标，类似于许多验证技术合成循环不变式。 - **可用性**：降低了非专家进行交换性验证的难度，避免了因不精确规格说明导致的不可靠结论。 #### 8. 相关工作 在交换性推理、k - 安全、产品程序和归约等领域，已有许多相关工作。例如，Bansal 等人从提供的前置/后置规格说明合成交换性条件，但可能因规格过粗导致不可靠结论；Gehr 等人基于黑盒采样的方法缺乏可靠性保证。在 k - 安全和产品程序方面，有自组合、产品程序、笛卡尔 Hoare 逻辑等技术用于自动化验证 k - 安全属性。 #### 9. 讨论与未来工作 - **堆 ADT 的推理**：`mn` - 差分可以应用于堆 ADT 的推理，例如使用分离逻辑作为断言语言。但目前不清楚 `DAReducen_m` 是否是自动化堆断言 `mn` - 差分的最佳策略，将 `mn` - 差分集成到基于堆的工具是未来的研究方向。 - **并发执行的应用**：本文的交换性验证结果可用于现有的并发实现，如编译器、图算法和软件事务内存等。未来，并行编译器可以结合交换性证明和线性izability证明，实现更安全的并发执行。 ### 利用mn差分分解数据结构交换性证明（续） #### 10. 交换性推理相关技术总结 为了更好地理解交换性推理领域的技术发展，下面对一些关键技术进行总结对比： |技术名称|主要思路|优点|缺点| | ---- | ---- | ---- | ---- | |Bansal等人的方法|从提供的前置/后置规格说明合成交换性条件|可基于规格进行推理|规格过粗可能导致不可靠结论| |Gehr等人的方法|基于黑盒采样|实现相对简单|缺乏可靠性保证| |自组合|将某些形式的超属性转化为单个程序的属性|可简化超属性验证|可能增加程序复杂度| |产品程序|通过构建产品程序验证k - 安全属性|可自动化验证|可能对资源要求较高| |笛卡尔Hoare逻辑|用于推理k - 安全属性的程序逻辑|逻辑清晰|自动化实现有一定难度| #### 11. 不同数据结构交换性验证结果分析 下面详细分析不同数据结构在使用 `Reducen_m` 和 `DAReducen_m` 进行交换性验证时的结果： |数据结构|`Reducen_m`表现|`DAReducen_m`表现|速度提升情况| | ---- | ---- | ---- | ---- | |单字段对象（内存单元、累加器、计数器等）|部分情况出现超时问题|虽有启动开销，但部分情况不超时|部分案例有明显优势| |`ArrayStack`|部分案例能快速找到反例，部分案例内存不足|多数情况可完成验证|平均速度有提升| |`SimpleSet`|存在超时和内存问题|多数情况优于 `Reducen_m`|平均速度提升可达3.88倍| |队列|部分案例验证有困难|表现相对较好|有一定速度提升| |哈希表|Ultimate在部分阶段有问题，需结合CPAchecker|整体表现优于 `Reducen_m`|部分案例速度优势明显| 从这些数据可以看出，`DAReducen_m` 在大多数情况下都能更好地应对交换性验证问题，尤其是在处理复杂数据结构和避免超时方面表现出色。 #### 12. 观察等价关系在实际应用中的优势体现 在实际使用中，观察等价关系的优势可以通过以下流程进一步体现： ```mermaid graph LR classDef startend fill:#F5EBFF,stroke:#BE8FED,stroke-width:2px; classDef process fill:#E5F6FF,stroke:#73A6FF,stroke-width:2px; classDef decision fill:#FFF6CC,stroke:#FFBC52,stroke-width:2px; A(开始):::startend --> B(选择观察等价关系I):::process B --> C(使用I进行交换性验证):::process C --> D{验证是否成功}:::decision D -->|是| E(得出可靠交换性结论):::process D -->|否| F(调整观察等价关系I):::process F --> C E --> G(结束):::startend ``` 在这个流程中，选择合适的观察等价关系是关键。由于观察等价关系具有可靠性、简单性、集中性、自动化和可用性等优点，使得整个验证过程更加高效和可靠。例如，在验证 `ArrayStack` 的交换性时，使用观察等价关系 $I_{AS}(\sigma_1, \sigma_2) \equiv top_1 = top_2 \land (\forall i. 0 \leq i \leq top_1 \Rightarrow A_1[i] = A_2[i])$ 可以避免考虑不必要的细节，快速得出可靠的交换性结论。 #### 13. 未来研究方向的具体探索 - **堆ADT推理的深入研究**：将 `mn` - 差分集成到基于堆的工具中，需要解决以下几个关键问题： - **断言语言的选择**：除了分离逻辑，是否还有其他更适合的断言语言可以用于堆ADT的 `mn` - 差分推理。 - **自动化策略的优化**：探索如何优化 `DAReducen_m` 算法，使其更适合堆断言的 `mn` - 差分自动化。 - **工具集成的实现**：研究如何将 `mn` - 差分与现有的基于堆的工具（如 Infer static analyzer、Verifast等）进行有效集成。 - **并发执行应用的拓展**：在并行编译器中结合交换性证明和线性izability证明，实现更安全的并发执行，可从以下方面入手： - **算法融合的研究**：研究如何将交换性验证算法和线性izability证明算法进行有效融合，确保两者在并行编译器中的协同工作。 - **性能优化的探索**：在保证并发执行安全性的前提下，探索如何优化算法以提高并行编译器的性能。 - **实际应用的测试**：选择一些实际的程序进行测试，验证结合交换性证明和线性izability证明的并行编译器在实际应用中的效果。 #### 14. 总结 本文围绕数据结构方法的交换性验证展开研究，提出了 `mn` - 差分理论和 `DAReducen_m` 算法，并通过 `CityProver` 工具进行了实验验证。主要成果包括： - 引入 `mn` - 差分抽象 $(\alpha, R_{\alpha})$，解决了通用可达性求解器在交换性验证中搜索抽象过于精确的问题。 - 提出 `DAReducen_m` 算法，将交换性验证问题分解为两个阶段，提高了验证的可扩展性。 - 通过实验验证了 `DAReducen_m` 算法在多个简单数据结构上的有效性，证明其在大多数情况下优于 `Reducen_m` 算法。 - 强调了观察等价关系在交换性验证中的优势，与前置/后置规格说明相比，具有更高的可靠性、简单性、集中性、自动化和可用性。 未来，在堆ADT推理和并发执行应用等方面还有很大的研究空间，有望进一步推动数据结构交换性验证技术的发展，实现更高效、安全的并发执行。