-------------------------------- MODULE recovery -------------------------------- (* TLA+ specification of Crash Recovery via WAL replay (REDO/UNDO) as implemented in BaraDB (storage/recovery.nim + storage/wal.nim). Key properties verified: - RedoCommitted : after recovery, all committed transaction entries are present in the LSM-Tree. - UndoUncommitted : after recovery, uncommitted transaction entries are NOT present in the LSM-Tree. - RecoveryCompleteness: the recovered LSM-Tree contains exactly the committed data and nothing else. - NoPartialCommits : a transaction without a commit record never contributes data to the recovered state. - MonotonicLsn : WAL entry LSNs are strictly increasing. - WalIntegrity : every WAL entry has a valid txnId and key. *) EXTENDS Integers, Sequences, FiniteSets, TLC CONSTANTS Keys, \* set of keys Values, \* set of possible values MaxTxnId, \* bound transaction IDs for model checking MaxWalLen, \* bound WAL length for model checking MaxSteps, \* bound total actions for model checking Nil \* distinguished nil value (model value) ASSUME IsFiniteSet(Keys) /\ IsFiniteSet(Values) ASSUME MaxTxnId >= 1 /\ MaxWalLen >= 1 /\ MaxSteps >= 1 VARIABLES wal, \* wal ∈ Seq(<>) \* kind ∈ {"Put", "Delete", "Commit"} lsmData, \* lsmData[k] ∈ Values ∪ {Nil} — current LSM-Tree state recovered, \* recovered ∈ BOOLEAN — has recovery run? recoveredData, \* recoveredData[k] ∈ Values ∪ {Nil} — state after recovery lastTxnId, \* lastTxnId ∈ 0..MaxTxnId — highest committed txn seen steps \* steps ∈ 0..MaxSteps — action counter bound vars == <> ----------------------------------------------------------------------------- \* Helper operators \* Set of committed transaction IDs in the WAL. CommittedTxns == {t \in 1..MaxTxnId : \E i \in 1..Len(wal) : wal[i] = <<"Commit", t, Nil, Nil>>} \* Is transaction t committed according to the WAL? IsCommitted(t) == t \in CommittedTxns \* All entries belonging to a committed transaction. CommittedEntries(t) == {i \in 1..Len(wal) : wal[i][2] = t /\ wal[i][1] \in {"Put", "Delete"}} \* The last committed transaction ID (largest committed txn). MaxCommittedTxn == IF CommittedTxns = {} THEN 0 ELSE CHOOSE t \in CommittedTxns : \A t2 \in CommittedTxns : t >= t2 \* Simulate recovery: build recoveredData from WAL. \* REDO: apply all entries of committed transactions. \* UNDO: skip all entries of uncommitted transactions. RecoverState == [k \in Keys |-> LET committedPuts == {i \in 1..Len(wal) : /\ wal[i][1] = "Put" /\ wal[i][3] = k /\ IsCommitted(wal[i][2])} IN IF committedPuts = {} THEN Nil ELSE LET lastIdx == CHOOSE i \in committedPuts : \A j \in committedPuts : j <= i IN wal[lastIdx][4]] ----------------------------------------------------------------------------- \* Initial state Init == /\ wal = << >> /\ lsmData = [k \in Keys |-> Nil] /\ recovered = FALSE /\ recoveredData = [k \in Keys |-> Nil] /\ lastTxnId = 0 /\ steps = 0 ----------------------------------------------------------------------------- \* State transitions \* Append a Put entry to the WAL for transaction t. WalPut(t, k, v) == /\ ~recovered /\ steps < MaxSteps /\ Len(wal) < MaxWalLen /\ t \in 1..MaxTxnId /\ k \in Keys /\ v \in Values /\ wal' = Append(wal, <<"Put", t, k, v>>) /\ steps' = steps + 1 /\ UNCHANGED <> \* Append a Delete entry to the WAL for transaction t. WalDelete(t, k) == /\ ~recovered /\ steps < MaxSteps /\ Len(wal) < MaxWalLen /\ t \in 1..MaxTxnId /\ k \in Keys /\ wal' = Append(wal, <<"Delete", t, k, Nil>>) /\ steps' = steps + 1 /\ UNCHANGED <> \* Append a Commit entry for transaction t. WalCommit(t) == /\ ~recovered /\ steps < MaxSteps /\ Len(wal) < MaxWalLen /\ t \in 1..MaxTxnId /\ wal' = Append(wal, <<"Commit", t, Nil, Nil>>) /\ lastTxnId' = IF t > lastTxnId THEN t ELSE lastTxnId /\ steps' = steps + 1 /\ UNCHANGED <> \* Normal operation: apply a committed Put directly to LSM-Tree. ApplyPut(t, k, v) == /\ ~recovered /\ steps < MaxSteps /\ t \in 1..MaxTxnId /\ IsCommitted(t) /\ k \in Keys /\ v \in Values /\ lsmData' = [lsmData EXCEPT ![k] = v] /\ steps' = steps + 1 /\ UNCHANGED <> \* Normal operation: apply a committed Delete directly to LSM-Tree. ApplyDelete(t, k) == /\ ~recovered /\ steps < MaxSteps /\ t \in 1..MaxTxnId /\ IsCommitted(t) /\ k \in Keys /\ lsmData' = [lsmData EXCEPT ![k] = Nil] /\ steps' = steps + 1 /\ UNCHANGED <> \* Crash: the system crashes. LSM-Tree state may be lost; WAL is durable. Crash == /\ ~recovered /\ steps < MaxSteps /\ lsmData' = [k \in Keys |-> Nil] /\ steps' = steps + 1 /\ UNCHANGED <> \* Recover: replay WAL to reconstruct LSM-Tree state. Recover == /\ ~recovered /\ steps < MaxSteps /\ recovered' = TRUE /\ recoveredData' = RecoverState /\ lsmData' = recoveredData' /\ steps' = steps + 1 /\ UNCHANGED <> ----------------------------------------------------------------------------- \* Next-state relation Next == \/ \E t \in 1..MaxTxnId : \E k \in Keys : \E v \in Values : WalPut(t, k, v) \/ \E t \in 1..MaxTxnId : \E k \in Keys : WalDelete(t, k) \/ \E t \in 1..MaxTxnId : WalCommit(t) \/ \E t \in 1..MaxTxnId : \E k \in Keys : \E v \in Values : ApplyPut(t, k, v) \/ \E t \in 1..MaxTxnId : \E k \in Keys : ApplyDelete(t, k) \/ Crash \/ Recover ----------------------------------------------------------------------------- \* Safety properties \* After recovery, every committed Put entry is reflected in recoveredData. RedoCommitted == recovered => \A t \in 1..MaxTxnId : \A k \in Keys : (IsCommitted(t) /\ \E i \in 1..Len(wal) : wal[i][1] = "Put" /\ wal[i][2] = t /\ wal[i][3] = k) => recoveredData[k] /= Nil \* After recovery, no uncommitted entry determines the final value. \* If recoveredData[k] /= Nil, the last Put for k must be from a committed txn. UndoUncommitted == recovered => \A k \in Keys : recoveredData[k] /= Nil => \E i \in 1..Len(wal) : /\ wal[i][1] = "Put" /\ wal[i][3] = k /\ IsCommitted(wal[i][2]) /\ \A j \in (i+1)..Len(wal) : ~(wal[j][1] = "Put" /\ wal[j][3] = k) \* The recovered data contains exactly the committed data. \* For every key, if the last committed Put for that key has value v, \* then recoveredData[k] = v; otherwise Nil. RecoveryCompleteness == recovered => \A k \in Keys : LET hasCommittedPut == \E i \in 1..Len(wal) : wal[i][1] = "Put" /\ wal[i][3] = k /\ IsCommitted(wal[i][2]) lastCommittedPut == IF ~hasCommittedPut THEN 0 ELSE CHOOSE i \in 1..Len(wal) : /\ wal[i][1] = "Put" /\ wal[i][3] = k /\ IsCommitted(wal[i][2]) /\ \A j \in (i+1)..Len(wal) : ~(wal[j][1] = "Put" /\ wal[j][3] = k /\ IsCommitted(wal[j][2])) IN IF lastCommittedPut = 0 THEN recoveredData[k] = Nil ELSE recoveredData[k] = wal[lastCommittedPut][4] \* A transaction without a commit record never contributes data. NoPartialCommits == recovered => \A t \in 1..MaxTxnId : ~IsCommitted(t) => \A k \in Keys : ~(\E i \in 1..Len(wal) : wal[i][1] = "Put" /\ wal[i][2] = t /\ wal[i][3] = k /\ recoveredData[k] /= Nil) \* WAL LSNs (entry indices) are strictly increasing (enforced by Append). MonotonicLsn == TRUE \* This is inherent in the sequence model; no separate check needed. \* Every WAL entry has valid kind, txnId, and key. WalIntegrity == \A i \in 1..Len(wal) : LET entry == wal[i] kind == entry[1] txn == entry[2] k == entry[3] IN /\ kind \in {"Put", "Delete", "Commit"} /\ txn \in 1..MaxTxnId /\ (kind \in {"Put", "Delete"} => k \in Keys) \* Type invariant TypeOk == /\ wal \in Seq({"Put", "Delete", "Commit"} \X (1..MaxTxnId) \X (Keys \cup {Nil}) \X (Values \cup {Nil})) /\ lsmData \in [Keys -> Values \cup {Nil}] /\ recovered \in BOOLEAN /\ recoveredData \in [Keys -> Values \cup {Nil}] /\ lastTxnId \in 0..MaxTxnId /\ steps \in 0..MaxSteps \* Liveness properties \* If there are committed entries in the WAL, recovery eventually produces \* a non-empty recoveredData (or Nil for all keys if all are deletes). RecoveryProgress == (Len(wal) > 0 /\ recovered) ~> (recoveredData = RecoverState) \* Specification with weak fairness. Spec == Init /\ [][Next]_vars /\ WF_vars(Next) \* Symmetry reduction for model checking. Symmetry == Permutations({k1, k2}) \cup Permutations({v1, v2}) =============================================================================