TwinPublish

------------------------------ MODULE TwinPublish ------------------------------ (***************************************************************************) (* Publish protocol for a Gaussian-splat scene host backed by an object *) (* store (R2) with per-object atomic writes and strong read-after-write *) (* consistency. One scene slug, three logical objects: *) (* *) (* ARTIFACT the splat bytes *) (* META scene metadata naming/describing the artifact *) (* INDEX the global scene listing *) (* *) (* The publisher writes, in strict order, ARTIFACT=v then META=v then *) (* INDEX=v. A republish repeats the sequence with v+1, overwriting in *) (* place. Readers discover via INDEX, then read META, then ARTIFACT; *) (* each read is a separate non-atomic step, so a republish can *) (* interleave anywhere. *) (* *) (* Version 0 means "object does not exist". *) (***************************************************************************) EXTENDS Naturals CONSTANTS MaxV, \* number of publishes the publisher performs (versions 1..MaxV) Readers \* set of reader identities ASSUME MaxV \in Nat /\ MaxV >= 1 VARIABLES artifact, \* version currently stored in the ARTIFACT object (0 = absent) meta, \* version currently stored in the META object (0 = absent) index, \* version the INDEX entry points at (0 = unlisted) pubV, \* version the publisher is currently publishing (MaxV+1 = done) pubPhase, \* next object the publisher will write rpc, \* per-reader program counter rMeta, \* version each reader observed when it read META rArt \* version each reader observed when it read ARTIFACT vars == <<artifact, meta, index, pubV, pubPhase, rpc, rMeta, rArt>> Versions == 0..MaxV TypeOK == /\ artifact \in Versions /\ meta \in Versions /\ index \in Versions /\ pubV \in 1..(MaxV + 1) /\ pubPhase \in {"artifact", "meta", "index"} /\ rpc \in [Readers -> {"index", "meta", "artifact", "done"}] /\ rMeta \in [Readers -> Versions] /\ rArt \in [Readers -> Versions] Init == /\ artifact = 0 /\ meta = 0 /\ index = 0 /\ pubV = 1 /\ pubPhase = "artifact" /\ rpc = [r \in Readers |-> "index"] /\ rMeta = [r \in Readers |-> 0] /\ rArt = [r \in Readers |-> 0] (***************************************************************************) (* Publisher: one atomic object write per step, in strict order. *) (***************************************************************************) PubWriteArtifact == /\ pubV <= MaxV /\ pubPhase = "artifact" /\ artifact' = pubV /\ pubPhase' = "meta" /\ UNCHANGED <<meta, index, pubV, rpc, rMeta, rArt>> PubWriteMeta == /\ pubV <= MaxV /\ pubPhase = "meta" /\ meta' = pubV /\ pubPhase' = "index" /\ UNCHANGED <<artifact, index, pubV, rpc, rMeta, rArt>> PubWriteIndex == /\ pubV <= MaxV /\ pubPhase = "index" /\ index' = pubV /\ pubV' = pubV + 1 /\ pubPhase' = "artifact" /\ UNCHANGED <<artifact, meta, rpc, rMeta, rArt>> (***************************************************************************) (* Readers: INDEX, then META, then ARTIFACT, one non-atomic read per *) (* step. A reader that finds the scene unlisted stops. *) (***************************************************************************) ReadIndex(r) == /\ rpc[r] = "index" /\ rpc' = [rpc EXCEPT ![r] = IF index = 0 THEN "done" ELSE "meta"] /\ UNCHANGED <<artifact, meta, index, pubV, pubPhase, rMeta, rArt>> ReadMeta(r) == /\ rpc[r] = "meta" /\ rMeta' = [rMeta EXCEPT ![r] = meta] /\ rpc' = [rpc EXCEPT ![r] = "artifact"] /\ UNCHANGED <<artifact, meta, index, pubV, pubPhase, rArt>> ReadArtifact(r) == /\ rpc[r] = "artifact" /\ rArt' = [rArt EXCEPT ![r] = artifact] /\ rpc' = [rpc EXCEPT ![r] = "done"] /\ UNCHANGED <<artifact, meta, index, pubV, pubPhase, rMeta>> (***************************************************************************) (* Allow stuttering once everything has finished (avoids a spurious *) (* deadlock report in this terminating model). *) (***************************************************************************) Terminating == /\ pubV > MaxV /\ \A r \in Readers : rpc[r] = "done" /\ UNCHANGED vars Next == \/ PubWriteArtifact \/ PubWriteMeta \/ PubWriteIndex \/ \E r \in Readers : ReadIndex(r) \/ ReadMeta(r) \/ ReadArtifact(r) \/ Terminating Spec == Init /\ [][Next]_vars (***************************************************************************) (* Invariants *) (***************************************************************************) \* If the INDEX lists the scene, its META and ARTIFACT objects exist. NoDanglingIndex == index /= 0 => (meta /= 0 /\ artifact /= 0) \* The stored META never describes an artifact that has not been written: \* at every state, META's version is at most ARTIFACT's version. This is \* exactly what the artifact-before-meta write order buys. MetaNeverAheadOfArtifact == meta <= artifact \* A reader that completed its sequence may have seen stale meta with newer \* bytes (rMeta <= rArt), but never meta describing bytes newer than what \* it fetched. Readers that stopped at an empty index have 0 <= 0. ReaderSafety == \A r \in Readers : rpc[r] = "done" => rMeta[r] <= rArt[r] =================================================================================

SPECIFICATION Spec CONSTANTS MaxV = 2 Readers = {r1, r2} INVARIANTS TypeOK NoDanglingIndex MetaNeverAheadOfArtifact ReaderSafety