chore(Percolator): add Liveness property for locks

s12f · Dec 29, 2024 · 836dea4 · 836dea4
1 parent 4f01875
commit 836dea4
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/percolator/Percolator.tla b/percolator/Percolator.tla
@@ -170,8 +170,12 @@ Recover ≜ ∃k ∈ Key:
 AllCommittedOrAborted ≜
     ∀tx ∈ Tx: txs[tx].status ∈ { "committed", "aborted" }
 
+AllLocksCleaned ≜
+    ∀k ∈ Key: rows[k].lock = ⟨⟩
+
 Done ≜
     ∧ AllCommittedOrAborted
+    ∧ AllLocksCleaned
     ∧ UNCHANGED ⟨next_ts, rows, txs⟩
 
 -----------------------------------------------------------------------------
@@ -216,6 +220,6 @@ Spec ≜ Init ∧ □[Next]_⟨all_vars⟩ ∧ WF_⟨all_vars⟩(Next)
 
 TypeOK ≜ ∀tx ∈ Tx: txs[tx].status ∈ TxStatus
 
-Liveness ≜ ◇(AllCommittedOrAborted)
+Liveness ≜ ◇(AllCommittedOrAborted ∧ AllLocksCleaned)
 
 ============================================================================