dimgigov
422df08ab9
Build warnings cleanup (0 warnings): - Suppress threadpool deprecation warning (baradadb.nim) - Remove unused 'os' import (logging.nim) - Fix ImplicitDefaultValue for newNode params (ast.nim) - Add explicit cstring cast for posix.open (wal.nim) - Fix HoleEnumConv for MsgKind parsing (server.nim) TLA+ Formal Verification: - Add symmetry reduction (Permutations) to all 9 existing specs - Add SYMMETRY directive to all .cfg files - New crossmodal.tla: cross-modal consistency spec * MetadataVectorConsistency, HybridResultValid * CommittedAtomicity, AbortedAtomicity, TxnStateValid - New models/crossmodal.cfg Tests: - Add Cross-Modal TLA+ Faithfulness tests (4 tests) Docs: - Update PLAN.md and BUG_AUDIT.md with completed tasks
184 lines
6.6 KiB
Plaintext
184 lines
6.6 KiB
Plaintext
-------------------------------- MODULE backup --------------------------------
|
||
(*
|
||
TLA+ specification of the Backup & Restore subsystem as implemented
|
||
in BaraDB (core/backup.nim).
|
||
|
||
Key properties verified:
|
||
- BackupSnapshotsValid: every backup snapshot is a valid file->content mapping.
|
||
- RestoreIntegrity : restoring from a valid backup yields the exact
|
||
data directory that was backed up at restore time.
|
||
- VerifyIntegrity : a verified backup is a known backup.
|
||
- RetentionInvariant : after cleanup, at most keepCount backups exist.
|
||
- HistoryConsistency : restore history only records known archive names.
|
||
- BackupIdValid : all backup IDs are less than the next ID counter.
|
||
*)
|
||
|
||
EXTENDS Integers, Sequences, FiniteSets, TLC
|
||
|
||
CONSTANTS Files, \* set of file IDs
|
||
Contents, \* set of possible file contents
|
||
MaxBackups, \* bound number of backups for model checking
|
||
KeepCount, \* retention count (must be >= 1)
|
||
MaxSteps, \* bound total actions for model checking
|
||
Nil \* distinguished nil value (model value)
|
||
|
||
ASSUME IsFiniteSet(Files) /\ IsFiniteSet(Contents)
|
||
ASSUME KeepCount >= 1 /\ MaxSteps >= 1
|
||
|
||
VARIABLES
|
||
dataDir, \* dataDir[f] ∈ Contents ∪ {Nil} — current live data
|
||
backups, \* backups ⊆ 1..MaxBackups — existing backup IDs
|
||
backupContent, \* backupContent[b][f] ∈ Contents ∪ {Nil} — snapshot of dataDir
|
||
verified, \* verified ⊆ 1..MaxBackups — backups that passed verify
|
||
history, \* history ∈ Seq(1..MaxBackups ∪ {Nil}) — restore history
|
||
nextBackupId, \* nextBackupId ∈ 1..MaxBackups+1 — monotonic ID counter
|
||
steps \* steps ∈ 0..MaxSteps — action counter bound
|
||
|
||
vars == <<dataDir, backups, backupContent, verified, history, nextBackupId, steps>>
|
||
|
||
\* Helper operators
|
||
|
||
Max(a, b) == IF a > b THEN a ELSE b
|
||
|
||
-----------------------------------------------------------------------------
|
||
\* Helper operators
|
||
|
||
\* Is backup b a valid, known backup?
|
||
IsKnownBackup(b) == b \in backups
|
||
|
||
\* Does backup b contain exactly the dataDir at the time it was taken?
|
||
BackupMatchesData(b, dir) ==
|
||
\A f \in Files : backupContent[b][f] = dir[f]
|
||
|
||
-----------------------------------------------------------------------------
|
||
\* Initial state
|
||
|
||
Init ==
|
||
/\ dataDir = [f \in Files |-> Nil]
|
||
/\ backups = {}
|
||
/\ backupContent = [b \in 1..MaxBackups |-> [f \in Files |-> Nil]]
|
||
/\ verified = {}
|
||
/\ history = << >>
|
||
/\ nextBackupId = 1
|
||
/\ steps = 0
|
||
|
||
-----------------------------------------------------------------------------
|
||
\* State transitions
|
||
|
||
\* Modify a file in the live data directory.
|
||
ModifyFile(f, c) ==
|
||
/\ f \in Files
|
||
/\ c \in Contents
|
||
/\ steps < MaxSteps
|
||
/\ dataDir' = [dataDir EXCEPT ![f] = c]
|
||
/\ steps' = steps + 1
|
||
/\ UNCHANGED <<backups, backupContent, verified, history, nextBackupId>>
|
||
|
||
\* Create a backup of the current data directory.
|
||
CreateBackup ==
|
||
/\ nextBackupId <= MaxBackups
|
||
/\ steps < MaxSteps
|
||
/\ backups' = backups \cup {nextBackupId}
|
||
/\ backupContent' = [backupContent EXCEPT ![nextBackupId] = dataDir]
|
||
/\ nextBackupId' = nextBackupId + 1
|
||
/\ steps' = steps + 1
|
||
/\ UNCHANGED <<dataDir, verified, history>>
|
||
|
||
\* Verify a backup: mark it as verified if it is known.
|
||
VerifyBackup(b) ==
|
||
/\ b \in backups
|
||
/\ steps < MaxSteps
|
||
/\ verified' = verified \cup {b}
|
||
/\ steps' = steps + 1
|
||
/\ UNCHANGED <<dataDir, backups, backupContent, history, nextBackupId>>
|
||
|
||
\* Restore from a verified backup: overwrite dataDir with backup contents.
|
||
RestoreBackup(b) ==
|
||
/\ b \in verified
|
||
/\ steps < MaxSteps
|
||
/\ dataDir' = backupContent[b]
|
||
/\ history' = Append(history, b)
|
||
/\ steps' = steps + 1
|
||
/\ UNCHANGED <<backups, backupContent, verified, nextBackupId>>
|
||
|
||
\* Cleanup old backups, keeping only the KeepCount most recent ones.
|
||
\* The "most recent" are the largest IDs (monotonic counter).
|
||
CleanupBackups ==
|
||
/\ steps < MaxSteps
|
||
/\ LET toKeep == IF Cardinality(backups) <= KeepCount
|
||
THEN backups
|
||
ELSE CHOOSE s \in SUBSET backups :
|
||
/\ Cardinality(s) = KeepCount
|
||
/\ \A b1 \in s, b2 \in backups \ s : b1 > b2
|
||
IN backups' = toKeep
|
||
/\ verified' = verified \cap backups'
|
||
/\ steps' = steps + 1
|
||
/\ UNCHANGED <<dataDir, backupContent, history, nextBackupId>>
|
||
|
||
-----------------------------------------------------------------------------
|
||
\* Next-state relation
|
||
|
||
Next ==
|
||
\/ \E f \in Files : \E c \in Contents : ModifyFile(f, c)
|
||
\/ CreateBackup
|
||
\/ \E b \in 1..MaxBackups : VerifyBackup(b)
|
||
\/ \E b \in 1..MaxBackups : RestoreBackup(b)
|
||
\/ CleanupBackups
|
||
|
||
-----------------------------------------------------------------------------
|
||
\* Safety properties
|
||
|
||
\* All backup snapshots are valid file->content mappings (enforced by TypeOk).
|
||
\* This property ensures backups only contain valid Contents or Nil.
|
||
BackupSnapshotsValid ==
|
||
\A b \in backups :
|
||
\A f \in Files : backupContent[b][f] \in Contents \cup {Nil}
|
||
|
||
\* After restore, dataDir matches the backup that was restored.
|
||
\* This is only true immediately after restore; we express it as a
|
||
\* temporal property: whenever a restore happens, dataDir equals backup.
|
||
RestoreIntegrity ==
|
||
\A b \in verified :
|
||
(history /= << >> /\ history[Len(history)] = b) =>
|
||
BackupMatchesData(b, dataDir)
|
||
|
||
\* Verified backups are always known backups.
|
||
VerifyIntegrity ==
|
||
verified \subseteq backups
|
||
|
||
\* After cleanup, the number of backups is at most KeepCount.
|
||
RetentionInvariant ==
|
||
Cardinality(backups) <= Max(KeepCount, nextBackupId - 1)
|
||
|
||
\* History only records valid backup IDs (may reference deleted backups).
|
||
HistoryConsistency ==
|
||
\A i \in 1..Len(history) : history[i] \in 1..(nextBackupId - 1)
|
||
|
||
\* All backup IDs are valid (less than the monotonic counter).
|
||
BackupIdValid ==
|
||
\A b \in backups : b < nextBackupId
|
||
|
||
\* Type invariant
|
||
TypeOk ==
|
||
/\ dataDir \in [Files -> Contents \cup {Nil}]
|
||
/\ backups \subseteq 1..MaxBackups
|
||
/\ backupContent \in [1..MaxBackups -> [Files -> Contents \cup {Nil}]]
|
||
/\ verified \subseteq 1..MaxBackups
|
||
/\ history \in Seq(1..MaxBackups \cup {Nil})
|
||
/\ nextBackupId \in 1..(MaxBackups + 1)
|
||
/\ steps \in 0..MaxSteps
|
||
|
||
\* Liveness properties
|
||
|
||
\* Any backup that is created can eventually be verified.
|
||
VerifyProgress ==
|
||
\A b \in 1..MaxBackups : b \in backups ~> b \in verified
|
||
|
||
\* Specification with weak fairness.
|
||
Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
|
||
|
||
\* Symmetry reduction for model checking.
|
||
Symmetry == Permutations({f1, f2}) \cup Permutations({c1, c2})
|
||
|
||
=============================================================================
|