fix(percolator): incorrect snapshot read (#2)

s12f · Nov 30, 2024 · bd61272 · bd61272
1 parent fef3bbd
commit bd61272
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 6 deletions.
diff --git a/.github/workflows/tlc.yaml b/.github/workflows/tlc.yaml
@@ -24,6 +24,7 @@ jobs:
           - multi-paxos-eb0/MultiPaxos.tla
           - paxos-eb0/PaxosEb0.tla
           - percolator/Transfer.tla
+          - percolator/SnapshotRead.tla
           - sequencer/Sequencer.tla
           - simplified-fast-paxos/SimplifiedFastPaxos.tla
     steps:

diff --git a/percolator/Percolator.tla b/percolator/Percolator.tla
@@ -44,8 +44,9 @@ CanRead(k, ts) ≜
 
 ReadKey(key, ts) ≜ 
     LET data ≜ rows[key].data
-        max_before_ts ≜ MaxUnder(DOMAIN data, ts)
-    IN data[max_before_ts]
+        write ≜ rows[key].write
+        max_before_ts ≜ MaxUnder(DOMAIN write, ts)
+    IN data[write[max_before_ts]]
 
 StartPreWrite(tx) ≜ 
     LET read ≜ txs[tx].read

diff --git a/percolator/PhantomP3.cfg → percolator/SnapshotRead.cfg b/percolator/PhantomP3.cfg → percolator/SnapshotRead.cfg
@@ -1,4 +1,4 @@
 CONSTANTS
   None = None
-INVARIANT PhantomP3Inv
+INVARIANT SnapshotReadInv
 SPECIFICATION Spec
diff --git a/percolator/PhantomP3.tla → percolator/SnapshotRead.tla b/percolator/PhantomP3.tla → percolator/SnapshotRead.tla
@@ -1,4 +1,4 @@
--------------------------------- MODULE PhantomP3 ----------------------------
+-------------------------------- MODULE SnapshotRead ----------------------------
 EXTENDS Integers, TLC, FiniteSets
 
 -----------------------------------------------------------------------------
@@ -35,7 +35,7 @@ TxOp ≜
 
 INSTANCE Percolator
 
-PhantomP3Inv ≜
+SnapshotReadInv ≜
     ∨ txs["t2"].status ≠ "committed"
     ∨ LET r ≜ txs["t2"].read
       IN 20 = r["k1"] + r["k2"]

diff --git a/percolator/readme.md b/percolator/readme.md
@@ -6,4 +6,4 @@ this project only specifies the core transaction part(without the notifications)
 
 - Percolator.tla: Percolator Specification
 - Transfer.tla: Verify the transfer transactions in the Percolator Specification.
-- PhantomP3.tla: an example that Percolator allows Phantom P3 history(https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-95-51.pdf), so the tlc will fail, and outputs the state history.
+- SnapshotRead.tla: Verify SnapshotRead.