fix(sib-isolation): add write conflict test and fix PSI_CT (#8)

s12f · Dec 19, 2024 · e694276 · e694276
1 parent 380d48b
commit e694276
Show file tree

Hide file tree

Showing 3 changed files with 35 additions and 19 deletions.
diff --git a/isolation-models/ANSI_ISOLATION.tla b/isolation-models/ANSI_ISOLATION.tla
@@ -18,7 +18,7 @@ TxOps(h, idx, result) ≜
     ELSE LET op ≜ h[idx]
              tx ≜ op.tx
              entry ≜ [ op ↦ op, idx ↦ idx ]
-         IN IF tx ∉ DOAMIN result
+         IN IF tx ∉ DOMAIN result
             THEN TxOps(h, idx + 1, tx :> ⟨entry⟩ @@ result)
             ELSE TxOps(h, idx + 1, tx :> Append(result[tx], entry) @@ result)
 

diff --git a/isolation-models/SIB_ISOLATION.tla b/isolation-models/SIB_ISOLATION.tla
@@ -110,28 +110,34 @@ SSER_CT(t, txs, states) ≜
 (* Parallel Snapshot Isolation Commit Test:
 *)
 
-TxPrecede(tx1, tx2) ≜ 
-    DOMAIN tx1.write ∩ (DOMAIN tx2.read ∪ DOMAIN tx2.write) ≠ {}
+TxPrecede(txs, states, t1, t2) ≜
+    LET sf(t, k) ≜ Min({ x ∈ 1 ‥ t : txs[t].read[k] = states[x][k] })
+    IN ∨ ∃k ∈ DOMAIN txs[t2].read: t1 = sf(t2, k) - 1
+       ∨ ∧ t1 < t2
+         ∧ DOMAIN txs[t1].write ∩ DOMAIN txs[t2].write ≠ {}
+
 \* ts: transaction set
-ComputeDirectPrecedeSet(txs, tx, pending) ≜ { t1 ∈ pending : TxPrecede(txs[t1], txs[tx]) }
+ComputeDirectPrecedeSet(txs, states, tx, pending) ≜
+    { t1 ∈ pending : TxPrecede(txs, states, t1, tx) }
+
 \* compute a precede set of some transactions
-RECURSIVE ComputePrecedeSet(_, _, _)
-ComputePrecedeSet(txs, pending, result) ≜
-    LET new ≜ UNION { ComputeDirectPrecedeSet(txs, tx, pending) : tx ∈ result } IN 
-    IF new = {}
-    THEN result
-    ELSE ComputePrecedeSet(txs, pending \ new, result ∪ new )
+RECURSIVE ComputePrecedeSet(_, _, _, _)
+ComputePrecedeSet(txs, states, pending, result) ≜
+    LET new ≜ UNION { ComputeDirectPrecedeSet(txs, states, tx, pending) : tx ∈ result }
+    IN IF new = {}
+       THEN result
+       ELSE ComputePrecedeSet(txs, states, pending \ new, result ∪ new )
 
 PSI_CT(t, txs, states) ≜
     ∧ RC_CT(t, txs, states)
     ∧ LET rs ≜ DOMAIN txs[t].read
-           ws ≜ DOMAIN txs[t].write
-           ps ≜ ComputePrecedeSet(txs, 1 ‥ t - 1, {t})
-           \* operation set
-           ops ≜ rs ∪ ws
-           slo(ok) ≜ Max({ x ∈ 1 ‥ t: ok ∉ rs ∨ txs[t].read[ok] = states[x][ok] })
+          ws ≜ DOMAIN txs[t].write
+          ps ≜ ComputePrecedeSet(txs, states, 1 ‥ t - 1, {t}) \ {t}
+          \* operation set
+          ops ≜ rs ∪ ws
+          slo(ok) ≜ Max({ x ∈ 1 ‥ t: ok ∉ rs ∨ txs[t].read[ok] = states[x][ok] })
        IN ∧ ∀ t1 ∈ ps, ok ∈ ops:
-            ok ∈ DOMAIN txs[t1].write ⇒ t1 + 1 ≤ slo(ok)
+                ok ∈ DOMAIN txs[t1].write ⇒ t1 + 1 ≤ slo(ok)
 
 (* Read Atomic Isolation Commit Test:
  Intuitively, if an operation o1 observes the writes of a transaction Ti ’s,

diff --git a/isolation-models/SIB_TESTS.tla b/isolation-models/SIB_TESTS.tla
@@ -1,5 +1,7 @@
 --------------------- MODULE SIB_TESTS ------------------
 
+SI ≜ INSTANCE SIB_ISOLATION
+
 \* Write Skew
 init ≜ [ k1 ↦ 0, k2 ↦ 0, k3 ↦ 0 ]
 
@@ -8,11 +10,9 @@ txs ≜
     , [ tid ↦ "t2", read ↦ [ k2 ↦ 0 ], write ↦ [ k1 ↦ 1 ] ]
     }
 
-SI ≜ INSTANCE SIB_ISOLATION
-
+ASSUME SI!ParallelSnapshotIsolation(init, txs)
 ASSUME SI!SnapshotIsolation(init, txs)
 ASSUME ¬ SI!SerializableIsolation(init, txs)
-ASSUME ¬ SI!ParallelSnapshotIsolation(init, txs)
 
 \* StrictSerializableExecution Tests1
 \* failed_sser_init == [ k1 |-> 0, k2 |-> 0 ]
@@ -33,5 +33,15 @@ pr_txs ≜
 
 ASSUME SI!ReadCommittedIsolation(init, pr_txs)
 ASSUME ¬ SI!ReadAtomicIsolation(init, pr_txs)
+ASSUME ¬ SI!ParallelSnapshotIsolation(init, pr_txs)
+
+\* Write Conflict(Lost Update)
+wc_txs ≜
+    { [ tid ↦ "t1", read ↦ [k1 ↦ 0], write ↦ [k1 ↦ 1]]
+    , [ tid ↦ "t2", read ↦ [k1 ↦ 0], write ↦ [k1 ↦ 2]]
+    }
+
+ASSUME SI!ReadAtomicIsolation(init, wc_txs)
+ASSUME ¬ SI!ParallelSnapshotIsolation(init, wc_txs)
 
 ======================================================