-------------------------------- 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 == <> \* 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 <> \* 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 <> \* 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 <> \* 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 <> \* 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 <> ----------------------------------------------------------------------------- \* 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}) =============================================================================