弱事务一致性模型间的鲁棒性检查

### 弱事务一致性模型间的鲁棒性检查 在并发编程中，事务一致性模型是确保数据一致性和程序正确性的重要概念。不同的一致性模型对事务的执行顺序和数据可见性有不同的要求，因此在实际应用中，需要检查程序在不同一致性模型之间的鲁棒性。本文将介绍如何检查程序在不同弱事务一致性模型（如 CC、PC 和 SI）之间的鲁棒性，并提供相应的理论和技术。 #### 1. 检查 CC 相对于 PC 的鲁棒性 鲁棒性检查的一个重要方面是检查程序在 CC（Causal Consistency）相对于 PC（Prefix Consistency）的鲁棒性。我们可以通过以下步骤来完成这个检查： - **引理和定理**：首先，有引理表明一个跟踪 τ 是 PC 当且仅当 τ♣ 是 SER（Serializable）。基于这个引理，我们可以证明定理 1：一个程序 P 对 CC 相对于 PC 是鲁棒的，当且仅当 P♣ 对 CC 相对于 SER 是鲁棒的。 - **复杂度分析**：检查 CC 相对于 PC 的鲁棒性可以在多项式时间内归约到 SER 下的可达性问题。对于有限状态程序（有界数据域），当进程数量有界时，检查鲁棒性是 PSPACE - 完全的；否则，是 EXPSPACE - 完全的。 #### 2. 检查 PC 相对于 SI 的鲁棒性 检查 PC 相对于 SI（Snapshot Isolation）的鲁棒性也可以归约到 SER 语义下的可达性问题。具体步骤如下： - **特征刻画**：我们发现，在 PC 相对于 SI 的鲁棒性违反中，发生前（happens - before）循环必须包含一个 WW（Write - Write）依赖后跟一个 RW（Read - Write）依赖，并且不包含两个连续的 RW 依赖。 - **定理证明**：定理 2 表明，一个程序 P 对 PC 相对于 SI 是鲁棒的，当且仅当 P 在 PC 下的每个发生前循环都包含两个连续的 RW 依赖。通过引理 5 和引理 6 可以证明该定理。 - **程序插桩**：为了检查鲁棒性，我们定义了一个插桩程序 [[P]]。当 [[P]] 在 SER 下违反一个断言时，程序 P 对 PC 相对于 SI 不是鲁棒的。插桩程序通过重写 P 的每个事务来模拟 PC 语义，并使用辅助变量跟踪发生前依赖。 ```plaintext Transaction “begin ⟨read⟩∗⟨test⟩∗⟨write⟩∗commit” is rewritten to: 1 if ( !done# ) 2 if ( * ) 3 begin <read>∗<test>∗commit 4 if ( !done# ) 5 begin <write>∗commit 6 else 7 I(begin) (I(<write>))∗I(commit) 8 else 9 begin (I#(<read>))∗<test>∗(I#(<write>))∗I#(commit) 10 assume false; 11 else if ( * ) 12 rdSet’ := ∅; 13 wrSet’ := ∅; 14 I(begin) (I(<read>))∗<test>∗I(commit) 15 I(begin) (I(<write>))∗I(commit) I#( r := x ): 16 r := x; 17 hbR[’x’] := 0; 18 rdSet := rdSet ∪{ ’x’ }; I#( x := e ): 19 if ( varW == ⊥and * ) 20 varW := ’x’; I#( commit ): 21 assume ( varW != ⊥) 22 done# := true I( begin ): 23 begin 24 hb := ⊥ 25 if ( hbP != ⊥and hbP < 2 ) 26 hb := 0; 27 else if ( hbP = 2 ) 28 hb := 2; I( commit ): 29 assume ( hb != ⊥) 30 assert ( hb == 2 or varW ̸∈wrSet’ ); 31 if ( hbP == ⊥or hbP > hb ) 32 hbP = hb; 33 for each ’x’ ∈wrSet’ 34 if ( hbW[’x’] == ⊥or hbW[’x’] > hb ) 35 hbW[’x’] = hb; 36 for each ’x’ ∈rdSet’ 37 if ( hbR[’x’] == ⊥or hbR[’x’] > hb ) 38 hbR[’x’] = hb; 39 rdSet := rdSet ∪rdSet’; 40 wrSet := wrSet ∪wrSet’; 41 commit I( r := x ): 42 r ```