----------------------------- MODULE RoostReleaseSync ----------------------------- (***************************************************************************) (* Two-store release sync: a configuration store and a git-shaped history *) (* store, kept consistent across crashes and racing writers. *) (* *) (* A tenant's configuration ("the manifest": a set of items, each active *) (* or archived) is applied in one single-threaded store (the config store) *) (* and versioned as commits in a second store (the repo). Changes arrive *) (* two ways: *) (* *) (* Interface change (three steps under a mutex held by the config store) *) (* Change1 apply the mutation to the live configuration (one *) (* transaction; the mutex is taken) *) (* Change2 write a commit whose tree is the new configuration and *) (* move the repo's main ref to it *) (* Change3 record that commit as `head` in the config store; release *) (* *) (* Push (a client pushes a commit it built on a base it cloned) *) (* Push0 the repo imports the commit's objects (content-addressed: *) (* harmless if the push is later rejected) *) (* Push2 the config store takes the mutex and does the real *) (* compare-and-set: head must equal the pusher's base; *) (* validates the tree (a known item may be archived, never *) (* dropped) and applies it; records head := new *) (* Push3 still under the mutex, main := new; release *) (* *) (* A crash may hit between any two steps. On restart, before serving *) (* anything, Reconcile runs three idempotent rules: (a) if main's tree *) (* equals the live configuration, adopt main as head; else (b) if head's *) (* tree differs from the live configuration, commit the configuration on *) (* top of main and point both at it; else (c) if main differs from head, *) (* move main to head. *) (* *) (* Rollback is "revert to": a change whose new configuration is an older *) (* commit's tree with every item known since then archived, never dropped. *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Items, \* configuration items (objects, tools, pages, ...) Pushers, \* clients that each push once MaxCommits, \* commit ids 1..MaxCommits; 0 = the empty initial commit MaxChanges, \* bound on interface changes (incl. rollbacks) per run NoObs \* model value: no tool-call observation States == {"absent", "active", "archived"} Manifests == [Items -> States] Empty == [i \in Items |-> "absent"] CommitIds == 0..MaxCommits Kinds == {"create", "archive", "unarchive"} Muts == Kinds \X Items VARIABLES applied, \* the live configuration (the truth) head, \* commit the config store believes it is at main, \* the repo's main ref objects, \* commit ids present in the repo (1..MaxCommits) tree, \* CommitIds -> Manifests (tree of each commit; Empty when unallocated) nextCommit, \* next free commit id lock, \* "free" | "change" | a pusher phase, \* interface change in flight: "idle" | "applied" | "committed" pending, \* commit written by Change2, awaiting Change3 changes, \* interface changes started so far booted, \* FALSE from a crash until Reconcile has run pst, \* Pushers -> "idle" | "imported" | "applied" | "done" | "rejected" | "crashed" pbase, \* Pushers -> base commit the push was built on pnew, \* Pushers -> the pushed commit padopted, \* Pushers -> TRUE once the config store applied this push known, \* Items -> TRUE once the item has ever been active obs \* observation: the configuration a tool call saw, cleared by other steps vars == <> PushStates == {"idle", "imported", "applied", "done", "rejected", "crashed"} TypeOK == /\ applied \in Manifests /\ head \in CommitIds /\ main \in CommitIds /\ objects \subseteq 1..MaxCommits /\ tree \in [CommitIds -> Manifests] /\ nextCommit \in 1..(MaxCommits + 1) /\ lock \in {"free", "change"} \cup Pushers /\ phase \in {"idle", "applied", "committed"} /\ pending \in CommitIds /\ changes \in 0..MaxChanges /\ booted \in BOOLEAN /\ pst \in [Pushers -> PushStates] /\ pbase \in [Pushers -> CommitIds] /\ pnew \in [Pushers -> CommitIds] /\ padopted \in [Pushers -> BOOLEAN] /\ known \in [Items -> BOOLEAN] /\ obs \in Manifests \cup {NoObs} Init == /\ applied = Empty /\ head = 0 /\ main = 0 /\ objects = {} /\ tree = [c \in CommitIds |-> Empty] /\ nextCommit = 1 /\ lock = "free" /\ phase = "idle" /\ pending = 0 /\ changes = 0 /\ booted = TRUE /\ pst = [p \in Pushers |-> "idle"] /\ pbase = [p \in Pushers |-> 0] /\ pnew = [p \in Pushers |-> 0] /\ padopted = [p \in Pushers |-> FALSE] /\ known = [i \in Items |-> FALSE] /\ obs = NoObs (* ---------------------------------------------------------------- helpers *) Enabled(M, m) == CASE m[1] = "create" -> M[m[2]] = "absent" [] m[1] = "archive" -> M[m[2]] = "active" [] m[1] = "unarchive" -> M[m[2]] = "archived" Mutate(M, m) == [M EXCEPT ![m[2]] = IF m[1] = "archive" THEN "archived" ELSE "active"] (* Rollback semantics: an item active in the target is active; an item the live configuration knows but the target does not have active is archived; nothing is dropped. *) RevertTo(M, T) == [i \in Items |-> IF T[i] = "active" THEN "active" ELSE IF M[i] # "absent" THEN "archived" ELSE "absent"] (* The validator: a pushed tree may not drop an item the configuration has. *) Valid(T) == \A i \in Items : applied[i] # "absent" => T[i] # "absent" Known(M) == [i \in Items |-> known[i] \/ M[i] # "absent"] Quiet == booted /\ lock = "free" (* -------------------------------------------------------- interface change *) Change1(m) == /\ Quiet /\ phase = "idle" /\ changes < MaxChanges /\ Enabled(applied, m) /\ applied' = Mutate(applied, m) /\ known' = Known(applied') /\ lock' = "change" /\ phase' = "applied" /\ changes' = changes + 1 /\ obs' = NoObs /\ UNCHANGED <> Rollback1(c) == /\ Quiet /\ phase = "idle" /\ changes < MaxChanges /\ c \in objects \cup {0} /\ RevertTo(applied, tree[c]) # applied /\ applied' = RevertTo(applied, tree[c]) /\ known' = Known(applied') /\ lock' = "change" /\ phase' = "applied" /\ changes' = changes + 1 /\ obs' = NoObs /\ UNCHANGED <> Change2 == /\ booted /\ phase = "applied" /\ nextCommit <= MaxCommits /\ LET c == nextCommit IN /\ tree' = [tree EXCEPT ![c] = applied] /\ objects' = objects \cup {c} /\ main' = c /\ pending' = c /\ nextCommit' = c + 1 /\ phase' = "committed" /\ obs' = NoObs /\ UNCHANGED <> Change3 == /\ booted /\ phase = "committed" /\ head' = pending /\ pending' = 0 /\ phase' = "idle" /\ lock' = "free" /\ obs' = NoObs /\ UNCHANGED <> (* -------------------------------------------------------------------- push *) (* The pusher clones main, edits, and pushes: objects land first. It may push a valid mutation or an invalid tree that drops an item. *) PushTrees(B) == {Mutate(tree[B], m) : m \in {m \in Muts : Enabled(tree[B], m)}} \cup {[tree[B] EXCEPT ![i] = "absent"] : i \in {i \in Items : tree[B][i] # "absent"}} Push0(p) == /\ booted /\ pst[p] = "idle" /\ nextCommit <= MaxCommits /\ \E T \in PushTrees(main) : LET c == nextCommit IN /\ tree' = [tree EXCEPT ![c] = T] /\ objects' = objects \cup {c} /\ pbase' = [pbase EXCEPT ![p] = main] /\ pnew' = [pnew EXCEPT ![p] = c] /\ nextCommit' = c + 1 /\ pst' = [pst EXCEPT ![p] = "imported"] /\ obs' = NoObs /\ UNCHANGED <> (* The compare-and-set lives here, in the single-threaded config store. *) Push2(p) == /\ Quiet /\ pst[p] = "imported" /\ IF head = pbase[p] /\ Valid(tree[pnew[p]]) THEN /\ applied' = tree[pnew[p]] /\ known' = Known(applied') /\ head' = pnew[p] /\ lock' = p /\ pst' = [pst EXCEPT ![p] = "applied"] /\ padopted' = [padopted EXCEPT ![p] = TRUE] ELSE /\ pst' = [pst EXCEPT ![p] = "rejected"] /\ UNCHANGED <> /\ obs' = NoObs /\ UNCHANGED <> Push3(p) == /\ booted /\ pst[p] = "applied" /\ lock = p /\ main' = pnew[p] /\ pst' = [pst EXCEPT ![p] = "done"] /\ lock' = "free" /\ obs' = NoObs /\ UNCHANGED <> (* ---------------------------------------------------------- crash/recover *) Crash == /\ booted /\ booted' = FALSE /\ lock' = "free" /\ phase' = "idle" /\ pending' = 0 /\ pst' = [p \in Pushers |-> IF pst[p] \in {"imported", "applied"} THEN "crashed" ELSE pst[p]] /\ obs' = NoObs /\ UNCHANGED <> Reconcile == /\ ~booted /\ IF main # 0 /\ tree[main] = applied THEN /\ head' = main /\ UNCHANGED <> ELSE IF tree[head] # applied THEN /\ nextCommit <= MaxCommits /\ LET c == nextCommit IN /\ tree' = [tree EXCEPT ![c] = applied] /\ objects' = objects \cup {c} /\ main' = c /\ head' = c /\ nextCommit' = c + 1 ELSE /\ main' = head /\ UNCHANGED <> /\ booted' = TRUE /\ obs' = NoObs /\ UNCHANGED <> (* ------------------------------------------------------------- observation *) ToolCall == /\ booted /\ obs' = applied /\ UNCHANGED <> Next == \/ \E m \in Muts : Change1(m) \/ \E c \in CommitIds : Rollback1(c) \/ Change2 \/ Change3 \/ \E p \in Pushers : Push0(p) \/ Push2(p) \/ Push3(p) \/ Crash \/ Reconcile \/ ToolCall Spec == Init /\ [][Next]_vars (***************************************************************************) (* Invariants *) (***************************************************************************) (* Whenever the store has booted and no change is in flight, the repo's main names exactly the applied configuration and the pointer agrees. *) AppliedMatchesMainAfterReconcile == Quiet => (main = head /\ tree[head] = applied) (* A tool call sees the whole applied configuration, and when nothing is in flight that configuration is a committed release. *) CallSeesOneRelease == obs # NoObs => (obs = applied /\ (lock # "free" \/ \E c \in objects \cup {0} : tree[c] = obs)) (* An item that was ever active is still present (active or archived). *) NothingDropped == \A i \in Items : known[i] => applied[i] # "absent" RefNeverDangles == /\ main \in objects \cup {0} /\ head \in objects \cup {0} (* Two pushes built on the same base cannot both be applied: one must be told it is stale. *) NoLostPush == \A p, q \in Pushers : p # q => ~(padopted[p] /\ padopted[q] /\ pbase[p] = pbase[q]) =============================================================================