feat(sib-isolation): add Read Atomic Isolation and fix newline (#7)

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

Hide file tree

Showing 12 changed files with 40 additions and 12 deletions.
diff --git a/isolation-models/ALL_TESTS.tla b/isolation-models/ALL_TESTS.tla
@@ -2,4 +2,4 @@
 
 EXTENDS SIB_TESTS
 
-======================================================
+======================================================
diff --git a/isolation-models/SIB_ISOLATION.tla b/isolation-models/SIB_ISOLATION.tla
@@ -19,6 +19,7 @@ SetToSeqs(S) ≜
 SeqToSet(S) ≜ { S[x] : x ∈ S}
 
 Max(S) ≜ CHOOSE x ∈ S: ∀ y ∈ S: x ≥ y
+Min(S) ≜ CHOOSE x ∈ S: ∀ y ∈ S: x ≤ y
 
 ----------------------------------------------------
 \* States
@@ -132,6 +133,22 @@ PSI_CT(t, txs, states) ≜
        IN ∧ ∀ t1 ∈ ps, ok ∈ ops:
             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,
+ all subsequent operations that read a key included in Ti ’s write set must
+ read from a state that includes Ti ’s effects.
+*)
+RA_CT(t, txs, states) ≜
+    ∧ RC_CT(t, txs, states)
+    ∧ LET read ≜ txs[t].read
+          sf(k) ≜ Min({ x ∈ 1 ‥ t : read[k] = states[x][k] })
+      IN ∀k1, k2 ∈ DOMAIN read:
+            LET sfr1 ≜ sf(k1)
+                sfr2 ≜ sf(k2)
+                tw_sfr1 ≜ IF sfr1 = 1 THEN {} ELSE DOMAIN txs[sfr1 - 1].write
+            IN k2 ∈ tw_sfr1 ⇒ sfr1 ≤ sfr2
+
+
 ----------------------------------------------------
 \* Isolation Executions
 
@@ -146,6 +163,7 @@ ReadCommittedExecution(e) ≜ IsolationExecution(e, RC_CT)
 ReadUncommittedExecution(e) ≜ IsolationExecution(e, RU_CT)
 ParallelSnapshotExecution(e) ≜ IsolationExecution(e, PSI_CT)
 StrictSerializableExecution(e) ≜ IsolationExecution(e, SSER_CT)
+ReadAtomicExecution(e) ≜ IsolationExecution(e, RA_CT)
 
 ----------------------------------------------------
 \* Isolation Levels
@@ -160,5 +178,6 @@ ReadCommittedIsolation(init, transactions) ≜ Isolation(init, transactions, Rea
 ReadUncommittedIsolation(init, transactions) ≜ Isolation(init, transactions, ReadUncommittedExecution)
 ParallelSnapshotIsolation(init, transactions) ≜ Isolation(init, transactions, ParallelSnapshotExecution)
 StrictSerializableIsolation(init, transactions) ≜ Isolation(init, transactions, StrictSerializableExecution)
+ReadAtomicIsolation(init, transactions) ≜ Isolation(init, transactions, ReadAtomicExecution)
 
-================================================
+================================================
diff --git a/isolation-models/SIB_TESTS.tla b/isolation-models/SIB_TESTS.tla
@@ -25,4 +25,13 @@ failed_sser_txs ≜
 ASSUME SI!SerializableIsolation(init, failed_sser_txs)
 ASSUME ¬ SI!StrictSerializableIsolation(init, failed_sser_txs)
 
-======================================================
+\* Partial Read
+pr_txs ≜
+    { [ tid ↦ "t1", read ↦ ⟨⟩, write ↦ [k1 ↦ 1, k2 ↦ 1]]
+    , [ tid ↦ "t2", read ↦ [k1 ↦ 1, k2 ↦ 0], write ↦ ⟨⟩]
+    }
+
+ASSUME SI!ReadCommittedIsolation(init, pr_txs)
+ASSUME ¬ SI!ReadAtomicIsolation(init, pr_txs)
+
+======================================================
diff --git a/multi-paxos-eb0/MultiPaxos.tla b/multi-paxos-eb0/MultiPaxos.tla
@@ -188,4 +188,4 @@ Spec ≜ Init ∧ □[Next]_vars
 Inv ≜ ∧ TypeOK
       ∧ ∀c1, c2 ∈ committed:
             c1.seq = c2.seq ⇒ c1.val = c2.val
-============================================================================
+============================================================================
diff --git a/paxos-eb0/PaxosEb0.tla b/paxos-eb0/PaxosEb0.tla
@@ -108,4 +108,4 @@ Spec ≜ Init ∧ □[Next]_vars
 
 Inv ≜ ∧ TypeOK
       ∧ ∀ v1 ∈ committed, v2 ∈ committed: v1 = v2
-============================================================================
+============================================================================
diff --git a/percolator/MC_SIB_SNAPSHOT.tla b/percolator/MC_SIB_SNAPSHOT.tla
@@ -43,4 +43,4 @@ SnapshotInv ≜ AllTxsDone ⇒
     \* SerializableIsolation will fail, Because exists write skew executions
     \* ∧ SI!SerializableIsolation(InitState, MappedTxs)
 
-============================================================================
+============================================================================
diff --git a/percolator/Percolator.tla b/percolator/Percolator.tla
@@ -215,4 +215,4 @@ TypeOK ≜
 
 Inv ≜ TypeOK
 
-============================================================================
+============================================================================
diff --git a/percolator/SnapshotRead.tla b/percolator/SnapshotRead.tla
@@ -40,4 +40,4 @@ SnapshotReadInv ≜
     ∨ LET r ≜ txs["t2"].read
       IN 20 = r["k1"] + r["k2"]
 
-============================================================================
+============================================================================
diff --git a/percolator/Transfer.tla b/percolator/Transfer.tla
@@ -37,4 +37,4 @@ AtomicRead ≜
 
 TransferInv ≜ Inv ∧ AtomicRead
 
-============================================================================
+============================================================================
diff --git a/sequencer/MCSequencer.tla b/sequencer/MCSequencer.tla
@@ -15,4 +15,4 @@ Constraint ≜
     ∧ nextRid < 7
     ∧ storage < 7
 
-====
+====
diff --git a/sequencer/Sequencer.tla b/sequencer/Sequencer.tla
@@ -128,4 +128,4 @@ LinearizableHistory ≜
 
 Inv ≜ LinearizableHistory
 
-============================================================================
+============================================================================
diff --git a/simplified-fast-paxos/SimplifiedFastPaxos.tla b/simplified-fast-paxos/SimplifiedFastPaxos.tla
@@ -123,4 +123,4 @@ Spec ≜ Init ∧ □[Next]_vars
 
 Inv ≜ ∧ TypeOK
       ∧ ∀ v1 ∈ committed, v2 ∈ committed: v1 = v2
-============================================================================
+============================================================================
Original file line number	Diff line number	Diff line change
Expand Up		@@ -2,4 +2,4 @@

		EXTENDS SIB_TESTS

		======================================================
		======================================================
Original file line number	Diff line number	Diff line change
Expand Up		@@ -215,4 +215,4 @@ TypeOK ≜

		Inv ≜ TypeOK

		============================================================================
		============================================================================
Original file line number	Diff line number	Diff line change
Expand Up		@@ -37,4 +37,4 @@ AtomicRead ≜

		TransferInv ≜ Inv ∧ AtomicRead

		============================================================================
		============================================================================
-Original file line number
+Diff line change
@@ Expand Up / @@ -15,4 +15,4 @@ Constraint ≜ @@
         ∧ nextRid < 7
         ∧ storage < 7
-    ====
+    ====
Original file line number	Diff line number	Diff line change
Expand Up		@@ -128,4 +128,4 @@ LinearizableHistory ≜

		Inv ≜ LinearizableHistory

		============================================================================
		============================================================================