-------------------------- MODULE GitOnObjectStore -------------------------- (***************************************************************************) (* Formal model of git refs over object storage, accompanying *) (* docs/git-on-object-storage.md. Model-checks the three safety *) (* properties under the conditional-write (CAS) axiom A3 by construction: *) (* the PUT/If-Match action is the only writer of the pointer and is atomic *) (* per step (TLC interleaves at action granularity), modeling A3 directly. *) (* *) (* Pushers race to advance a single manifest pointer holding a ref value. *) (* We assert (see SAFETY PROPERTIES for the full set and per-invariant docs):*) (* T1 fence: observed success => the obligated push is durably published *) (* T2 closure: a published manifest either covers its parent's packs or *) (* names a trusted full-closure compaction pack *) (* T3 ref linearizability: installs form a fork-free chain, each commits *) (* exactly the value it proposed, derived from the pointer it read *) (* Each invariant is mutation-tested non-vacuous; see docs/ Mechanized ยง. *) (***************************************************************************) EXTENDS Naturals, FiniteSets, Sequences CONSTANTS Pushers, \* set of concurrent pusher ids MaxManifests \* bound on distinct manifests (model finiteness) VARIABLES pointer, \* current manifest id held by M_R (a natural; 0 = empty repo) published, \* set of manifest ids ever installed as pointer (durable history) packs, \* function: manifest id -> set of pack ids it names pc, \* pusher id -> control state readEtag, \* pusher id -> pointer value it last read (its CAS precondition) staged, \* pusher id -> manifest id it intends to install parent, \* manifest id -> the manifest id it was derived from (history) refs, \* manifest id -> objectId that this manifest binds the ref "main" to compacted, \* manifests whose own pack is a full closure of their refs newVal, \* pusher id -> objectId this push proposes for "main" (its effect) snapErr, \* pusher id -> did either ref-snapshot read fail? (BOOLEAN) observed \* set of pusher ids that have observed success (fence passed) vars == <> \* We model a single ref, "main", whose value is an objectId in ObjIds. This is \* enough to exhibit ref-update linearizability: a lost update is the published \* value of "main" reverting or skipping a committed predecessor's value. \* (Dawn's point: prove ref VALUES survive, not just that effect tokens are \* monotone.) refs[m] is the value "main" holds in manifest m. ObjIds == 0..MaxManifests \* A push CHANGES refs iff the value it proposes differs from the value in the \* manifest it READ. This is now DERIVED from real ref state, not a free boolean. DidChange(p) == newVal[p] # refs[readEtag[p]] ManifestIds == 0..MaxManifests TypeOK == /\ pointer \in ManifestIds /\ published \subseteq ManifestIds /\ packs \in [ManifestIds -> SUBSET ManifestIds] /\ pc \in [Pushers -> {"idle","staged","done","lost"}] /\ readEtag \in [Pushers -> ManifestIds] /\ staged \in [Pushers -> ManifestIds] /\ parent \in [ManifestIds -> ManifestIds] /\ refs \in [ManifestIds -> ObjIds] /\ compacted \subseteq ManifestIds /\ newVal \in [Pushers -> ObjIds] /\ snapErr \in [Pushers -> BOOLEAN] /\ observed \subseteq Pushers Init == /\ pointer = 0 /\ published = {0} /\ packs = [m \in ManifestIds |-> {}] /\ pc = [p \in Pushers |-> "idle"] /\ readEtag = [p \in Pushers |-> 0] /\ staged = [p \in Pushers |-> 0] /\ parent = [m \in ManifestIds |-> 0] /\ refs = [m \in ManifestIds |-> 0] \* "main" starts at objectId 0 (empty) /\ compacted = {} /\ newVal = [p \in Pushers |-> 0] /\ snapErr = [p \in Pushers |-> FALSE] /\ observed = {} \* A fresh manifest id, distinct from every published manifest AND every \* concurrently-staged one (Perci): distinct pushes mint distinct content-addressed \* manifests, so two concurrent stages never alias the same id. This keeps the \* no-lost-update counterexamples about CAS serialization, not id collision. StagedIds == { staged[q] : q \in Pushers } FreshId == CHOOSE m \in ManifestIds : m \notin published /\ m \notin StagedIds /\ m # 0 CanStage == \E m \in ManifestIds : m \notin published /\ m \notin StagedIds /\ m # 0 \* The publish-skip decision (the fallible-snapshot fence, Quinn #2 / Dawn's case). \* A push skips publish ONLY if its snapshots succeeded AND showed no ref change. \* If either snapshot errored (snapErr), it must NOT skip -- it falls through to CAS. \* This is "Ok(b) = Ok(a)", never "b = a" with errors silently equal. MustPublish(p) == DidChange(p) \/ snapErr[p] \* Steps 3-6: read pointer; nondeterministically this push either changes refs or \* is a no-op, and its ref-snapshot reads either succeed or fail. Stage a manifest. Begin(p) == /\ pc[p] = "idle" /\ CanStage \* This push proposes some value v for "main" (v = current value models a \* no-op push; v # current models a real ref change); its snapshot reads may \* fail (e). The staged manifest binds "main" to v and is derived from the \* manifest the push READ -- so a stale reader builds on stale ref state, and \* only the CAS guard stops it from clobbering a newer published value. /\ \E v \in ObjIds, e \in BOOLEAN, compact \in BOOLEAN : /\ newVal' = [newVal EXCEPT ![p] = v] /\ snapErr' = [snapErr EXCEPT ![p] = e] /\ LET m == FreshId IN /\ readEtag' = [readEtag EXCEPT ![p] = pointer] /\ staged' = [staged EXCEPT ![p] = m] /\ parent' = [parent EXCEPT ![m] = pointer] \* A compact stage models `pack-objects` over every post-push \* ref tip. Its own pack is therefore trusted to cover the full \* reachable closure; a normal stage extends the parent pack set. /\ packs' = [packs EXCEPT ![m] = IF compact THEN {m} ELSE packs[pointer] \union {m}] /\ refs' = [refs EXCEPT ![m] = v] /\ compacted' = IF compact THEN compacted \union {m} ELSE compacted \ {m} /\ pc' = [pc EXCEPT ![p] = "staged"] /\ UNCHANGED <> \* No-op fast path: a push that must NOT publish (no change, snapshots ok) goes \* straight to done WITHOUT touching the pointer -- zero CAS/publish latency. SkipPublish(p) == /\ pc[p] = "staged" /\ ~MustPublish(p) /\ pc' = [pc EXCEPT ![p] = "done"] /\ UNCHANGED <> \* Step 7: CAS. Succeeds iff pointer still equals the etag this pusher read (A3). CasSucceed(p) == /\ pc[p] = "staged" /\ MustPublish(p) /\ pointer = readEtag[p] /\ pointer' = staged[p] /\ published' = published \union {staged[p]} /\ pc' = [pc EXCEPT ![p] = "done"] /\ UNCHANGED <> CasFail(p) == /\ pc[p] = "staged" /\ MustPublish(p) /\ pointer # readEtag[p] /\ pc' = [pc EXCEPT ![p] = "lost"] \* will retry from idle /\ UNCHANGED <> \* Step 8: the fence. Observe success ONLY after the push reached "done" \* (either via successful CAS or a legitimate skip). Observe(p) == /\ pc[p] = "done" /\ observed' = observed \union {p} /\ UNCHANGED <> \* A loser retries: back to idle, ready to re-read the advanced pointer. Retry(p) == /\ pc[p] = "lost" /\ pc' = [pc EXCEPT ![p] = "idle"] /\ UNCHANGED <> Next == \E p \in Pushers : Begin(p) \/ SkipPublish(p) \/ CasSucceed(p) \/ CasFail(p) \/ Observe(p) \/ Retry(p) Spec == Init /\ [][Next]_vars /\ WF_vars(Next) ------------------------------------------------------------------------------ \* SAFETY PROPERTIES \* T1 (Durability-Ordering): any observed push that was obligated to publish \* (it changed refs, or its snapshot reads errored) has its staged manifest in \* the durable published history before the client observes success. A \* legitimately-skipped no-op push (no change, snapshots ok) is exempt -- it \* publishes nothing and is correct to do so. Inv_Fence == \A p \in observed : MustPublish(p) => staged[p] \in published \* The bite for the fallible-snapshot case (Quinn #2 / Dawn): if a push actually \* changed refs and was observed, its change is durably published -- regardless of \* snapshot outcome. This is what breaks if SkipPublish ignores snapErr (i.e. if \* the skip predicate were "b = a" instead of "Ok(b) = Ok(a) /\ no change"). \* \* NOTE (Dawn): this is NOT redundant with Inv_Fence, even though \* MustPublish == DidChange \/ snapErr makes Inv_Fence look strictly stronger. \* Inv_Fence is predicated on the OPERATOR MustPublish; mutate that operator (the \* skip-on-error bug) and Inv_Fence's own predicate moves with it, so the mutated \* Inv_Fence stops catching the bug. Inv_ChangedPublished is predicated on \* DidChange directly, independent of MustPublish, so it stays load-bearing under \* exactly the mutation we care about. Do not delete it as "redundant." Inv_ChangedPublished == \A p \in observed : DidChange(p) => staged[p] \in published Installed(p) == (p \in observed) /\ MustPublish(p) /\ (staged[p] \in published) \* (A former Inv_NoLost -- "distinct installs never share a manifest id" -- was \* removed: with FreshId excluding in-flight staged ids, Inv_NoFork implies it, so \* it caught only a model aliasing artifact, not a real failure mode. Verified by \* checking that no mutation trips it without also tripping Inv_NoFork.) \* T3b (Ref-update linearizability -- Dawn's user-visible theorem): the model \* now carries the REAL ref value (refs[m] = the objectId "main" holds in manifest \* m), not just effect tokens. Two properties bind the proof to ref VALUES: \* \* (i) Every installed push's own proposed value is exactly what its manifest \* commits -- the push's effect is applied, not dropped. Inv_RefEffectApplied == \A p \in Pushers : Installed(p) => (refs[staged[p]] = newVal[p]) \* (ii) An installed push computed its new value from the manifest that was the \* pointer AT INSTALL TIME (its parent is the pointer it read, and the CAS \* guard forced read == current). So no install builds "main" on top of a \* value that a concurrent winner already superseded -- the lost-update of a \* ref value. Operationally: an installed manifest's parent is published and \* its value was derived from that parent, giving a single serial line of ref \* values. (The fork ban, Inv_NoFork, plus this, is ref linearizability.) Inv_RefDerivedFromParent == \A p \in Pushers : Installed(p) => (parent[staged[p]] = readEtag[p] /\ readEtag[p] \in published) \* T2 (Reconstruction coverage -- non-vacuous): every published non-root \* manifest either names its trusted full-closure compaction pack, or covers its \* published parent's pack set plus its own delta pack. The model abstracts \* Git's reachability walk as the `compacted` marker; production earns that \* marker only by feeding every post-push ref tip to `git pack-objects --revs`. Inv_Closed == \A m \in published : (m # 0 /\ parent[m] \in published) => (m \in packs[m] /\ (m \in compacted \/ packs[parent[m]] \subseteq packs[m])) \* Parent integrity: every published non-root manifest's parent is also published \* (the install chain is grounded in durable history, never in vapor). Inv_ParentPublished == \A m \in published : (m = 0) \/ (parent[m] \in published) \* The pointer is always itself a published manifest (never points at vapor). Inv_PointerPublished == pointer \in published \* T3c (Linear history -- the real no-lost-update): the published manifests form \* a single chain ending at the current pointer; there is no fork. A lost update \* is precisely a fork: two installs sharing a parent, so one's effects are \* dropped from the surviving line. Reachability of every published manifest from \* the pointer via parent edges rules that out. With MaxManifests bound, we check \* the contrapositive directly: no two distinct published non-root manifests share \* a parent (a shared parent = a fork = a lost update). The A3 CAS guard is what \* makes this hold; removing it lets two pushers install off the same parent. Inv_NoFork == \A m1, m2 \in published : (m1 # m2 /\ m1 # 0 /\ m2 # 0) => (parent[m1] # parent[m2]) \* Finiteness bound: at most MaxManifests distinct manifests may be published. \* Without it the Retry loop lets pushers churn newVal/FreshId unboundedly. BoundedManifests == Cardinality(published) <= MaxManifests Safety == /\ TypeOK /\ Inv_Fence /\ Inv_ChangedPublished /\ Inv_RefEffectApplied /\ Inv_RefDerivedFromParent /\ Inv_NoFork /\ Inv_Closed /\ Inv_ParentPublished /\ Inv_PointerPublished =============================================================================