CelldRollout

---- MODULE CelldRollout ---- (***************************************************************************) (* Deploy -> restart rollout contract for a self-hosted Workers runtime *) (* (celld) running as a single-replica StatefulSet on k8s. *) (* *) (* Contract being modelled: *) (* 1. `celld deploy` uploads blobs, then atomically commits *) (* deploy/current.json to version v (Commit) *) (* 2. A node loads the deployment ONLY at process start and serves that *) (* version until it exits (Start/Serve) *) (* 3. The deploy script restarts the pod after the commit succeeds: *) (* SIGTERM -> draining (503, in-flight finish) -> exit -> k8s starts *) (* a new pod that reads deploy/current.json at startup *) (* (BeginDrain/Exit/Start/BecomeReady) *) (* 4. The script reports success only once the new pod is Ready and is *) (* serving the committed version (Report) *) (* *) (* 0 denotes the version deployed before any Commit in this run. *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Versions, \* versions that may be committed during the run MaxRestarts \* bound on pod restarts, keeps the state space finite ASSUME Versions \subseteq Nat /\ 0 \notin Versions /\ MaxRestarts \in Nat VARIABLES bucketCurrent, \* version named by deploy/current.json in the bucket nodeState, \* "stopped" | "starting" | "serving" | "draining" nodeVersion, \* version the running process loaded at start deployReported, \* versions for which the deploy script reported success lastServed, \* version that served the most recent request restarts \* number of restarts so far (bound) vars == <<bucketCurrent, nodeState, nodeVersion, deployReported, lastServed, restarts>> States == {"stopped", "starting", "serving", "draining"} AllVersions == Versions \cup {0} Max(S) == CHOOSE x \in S : \A y \in S : y <= x TypeOK == /\ bucketCurrent \in AllVersions /\ nodeState \in States /\ nodeVersion \in AllVersions /\ deployReported \subseteq Versions /\ lastServed \in AllVersions /\ restarts \in 0..MaxRestarts Init == /\ bucketCurrent = 0 /\ nodeState = "serving" /\ nodeVersion = 0 /\ deployReported = {} /\ lastServed = 0 /\ restarts = 0 \* (1) `celld deploy`: blobs are written first, then current.json flips \* atomically. Only the atomic flip is observable, and versions only \* move forward. Commit(v) == /\ v \in Versions /\ v > bucketCurrent /\ bucketCurrent' = v /\ UNCHANGED <<nodeState, nodeVersion, deployReported, lastServed, restarts>> \* (3) SIGTERM: health flips to 503, new requests are refused. BeginDrain == /\ nodeState = "serving" /\ restarts < MaxRestarts /\ nodeState' = "draining" /\ restarts' = restarts + 1 /\ UNCHANGED <<bucketCurrent, nodeVersion, deployReported, lastServed>> \* (3) In-flight requests finish, the process exits. Exit == /\ nodeState = "draining" /\ nodeState' = "stopped" /\ UNCHANGED <<bucketCurrent, nodeVersion, deployReported, lastServed, restarts>> \* (2)+(3) k8s starts a replacement pod; it reads deploy/current.json \* exactly once, here. Start == /\ nodeState = "stopped" /\ nodeState' = "starting" /\ nodeVersion' = bucketCurrent /\ UNCHANGED <<bucketCurrent, deployReported, lastServed, restarts>> \* Readiness probe passes; the node begins serving. BecomeReady == /\ nodeState = "starting" /\ nodeState' = "serving" /\ UNCHANGED <<bucketCurrent, nodeVersion, deployReported, lastServed, restarts>> \* A request is served. Only a node in state "serving" serves; the version \* it serves is the one loaded at start, never the bucket's current value. Serve == /\ nodeState = "serving" /\ lastServed' = nodeVersion /\ UNCHANGED <<bucketCurrent, nodeState, nodeVersion, deployReported, restarts>> \* (4) The deploy script reports success for v only when v is committed AND \* the node is Ready (serving) AND that node actually loaded v. Report(v) == /\ v \in Versions /\ bucketCurrent = v /\ nodeState = "serving" /\ nodeVersion = v /\ deployReported' = deployReported \cup {v} /\ UNCHANGED <<bucketCurrent, nodeState, nodeVersion, lastServed, restarts>> (***************************************************************************) (* DELIBERATELY WRONG VARIANT (not part of the checked spec). *) (* *) (* If the deploy script reported success as soon as the commit landed, *) (* before the restart, Report would read: *) (* *) (* ReportBeforeRestart(v) == *) (* /\ v \in Versions *) (* /\ bucketCurrent = v *) (* /\ deployReported' = deployReported \cup {v} *) (* /\ UNCHANGED <<bucketCurrent, nodeState, nodeVersion, *) (* lastServed, restarts>> *) (* *) (* Substituting it for Report makes TLC fail immediately (verified): *) (* Init (serving v0) -> Commit(1) -> ReportBeforeRestart(1) *) (* violates ReportedVersionIsServing after 2 steps (v1 reported while the *) (* node still runs v0), and one more step, Serve, violates *) (* ServedAfterReport: the request is served by v0 after v1 was reported. *) (* Because a node loads the deployment only at start (contract 2), a *) (* commit alone changes nothing the node serves; success is only true *) (* after the restart has completed and the new pod is Ready. *) (***************************************************************************) Next == \/ \E v \in Versions : Commit(v) \/ Report(v) \/ BeginDrain \/ Exit \/ Start \/ BecomeReady \/ Serve Spec == Init /\ [][Next]_vars (***************************************************************************) (* Properties *) (***************************************************************************) \* Safety1 (state form): once any version has been reported, a serving node \* is running at least the newest reported version. ReportedVersionIsServing == deployReported /= {} /\ nodeState = "serving" => nodeVersion >= Max(deployReported) \* Safety1 (action form): every request served after a report is served by \* a version >= the newest reported version. ServeRespectsReports == Serve => (deployReported = {} \/ nodeVersion >= Max(deployReported)) ServedAfterReport == [][ServeRespectsReports]_vars \* Safety2: a draining, starting or stopped node never serves. Any change \* to the served version can only originate from a node in "serving". ServeOnlyWhenServing == lastServed' /= lastServed => nodeState = "serving" NoServeWhileNotServing == [][ServeOnlyWhenServing]_vars \* A reported version has actually been committed. ReportedIsCommitted == \A v \in deployReported : v <= bucketCurrent ====

SPECIFICATION Spec CONSTANTS Versions = {1, 2} MaxRestarts = 3 INVARIANTS TypeOK ReportedVersionIsServing ReportedIsCommitted PROPERTIES ServedAfterReport NoServeWhileNotServing CHECK_DEADLOCK TRUE