carlos / platform Public

sim: the files publisher from sequence 1, P's prepared manifest at 0, the release's final manifest, the files pin by exact version over the admitted chain, the files live set with the chain's newest manifest, timers declared only when no landed manifest carries them (INV-28), and no dead box's disk read in the two-box shape

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude agent, operated by paul@keymail.dev 55ab9c258007dd0381c55ea174a657dbb3048364 parent 3f51773
7 files changed, +379 −21
  • internal/sim/hostlife/moves_test.go +14 −0
  • internal/sim/hostlife/protocol_test.go +5 −3
  • internal/sim/hostlife/regionha_test.go +288 −13
  • internal/sim/hostlife/regionha_witness_test.go +52 −0
  • internal/sim/hostlife/rules_test.go +4 −0
  • internal/sim/hostlife/sim_test.go +1 −1
  • internal/sim/hostlife/world_test.go +15 −4
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index 4969dac74..a12678ab1 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -1886,6 +1886,9 @@ func locationOf(k string) string {
// in every region.
func (w *world) deadGeneration(c *claim, r int, k string) bool {
h := c.Holder
+ if w.filesLive(c, k) {
+ return false
+ }
e := w.execBox(c)
authoritative := e != nil && e.Region == r
if !on("live-set-region") {
@@ -1944,6 +1947,14 @@ func (w *world) deadGeneration(c *claim, r int, k string) bool {
}
return true // a dead generation's certificates
}
+ if isManifestKey(k) {
+ // a files manifest outside the files live set (region HA §5.6, L13):
+ // its generation's, as the data keys are
+ if genOf(h.Location, k) == h.Gen {
+ return !authoritative
+ }
+ return true
+ }
return isDataKey(k)
}
@@ -1953,6 +1964,9 @@ func (w *world) deadGeneration(c *claim, r int, k string) bool {
// the lock).
func genOf(loc, k string) string {
rest := strings.TrimPrefix(k, loc)
+ if strings.HasPrefix(rest, "files/") {
+ return "" // a files manifest of the origin generation (region HA §5.6)
+ }
if strings.HasPrefix(rest, "g-") {
if i := strings.Index(rest, "/"); i > 0 {
return rest[2:i]
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index 8ff23c13f..a0d45bd97 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -1146,7 +1146,7 @@ func (w *world) coverParkedPredecessors(n *claim, region int, gens []string) {
// that never had anything (INV-17).
func (w *world) hadFilesIn(r int, loc, gen string) bool {
for _, k := range w.buckets[r].keys(dataKey(loc, gen, "")) {
- if genOf(loc, k) == gen {
+ if genOf(loc, k) == gen && !isManifestKey(k) { // a files manifest is no database object (region HA §5.6)
return true
}
}
@@ -1158,7 +1158,7 @@ func (w *world) hadFilesIn(r int, loc, gen string) bool {
func (w *world) hasFilesIn(r int, loc, gen string) bool {
bk := w.buckets[r]
for _, k := range bk.keys(dataKey(loc, gen, "")) {
- if genOf(loc, k) == gen && bk.current(k) != nil {
+ if genOf(loc, k) == gen && bk.current(k) != nil && !isManifestKey(k) { // a files manifest is no database object (region HA §5.6)
return true
}
}
@@ -2360,7 +2360,9 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {
retire = "" // the origin generation's sentinel (claim rev 6.10)
}
inner := keep
- keep = func(k string) bool { return genOf(o.Prefix, k) != retire || inner != nil && inner(k) }
+ keep = func(k string) bool {
+ return genOf(o.Prefix, k) != retire || w.filesLive(w.claim, k) || inner != nil && inner(k)
+ }
}
if !w.parkStep(b, o.Prefix, o.Dest(), quiet, o.Scope, keep) {
return
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
index 66f63b268..2884f0524 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -1,6 +1,9 @@
package hostlife
-import "fmt"
+import (
+ "fmt"
+ "strings"
+)
// ---------- relocation (region HA spec 1 §5.8; claim rev 6.30 §4, L1; plan 1b-next rev 16) ----------
//
@@ -154,7 +157,29 @@ func (w *world) relocRelease(b *box, c *claim) *releaseEntry {
if files == nil || files.Inc != h.Inc {
files = w.relocFiles(c).clone()
}
- return &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, Flushed: flushed,
+ // 3. (Task 4) publish every pending file and wake-state mutation,
+ // whatever the app's files_durability, as one final manifest of the
+ // generation (ReleaseFlushFiles): create-only, acknowledged before the
+ // entry is journaled, its sequence journaled as manifest_seq
+ seq := 0
+ if w.perRegion > 1 {
+ if b.pubGen != h.Gen {
+ b.pubGen, b.pubSeq, b.releaseSeq = h.Gen, 0, 0
+ }
+ if b.releaseSeq == 0 {
+ b.pubSeq++
+ b.releaseSeq = b.pubSeq
+ }
+ w.issued++
+ bl := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: b.releaseSeq, Files: files.clone(), Timers: append([]int(nil), b.Timers...), Base: w.issued}
+ if !w.ackedPut(b, manifestKey(h.Location, h.Gen, b.releaseSeq), bl, true) {
+ w.stats["release: waits for its manifest"]++
+ return nil
+ }
+ seq, b.releaseSeq = b.releaseSeq, 0
+ b.published = filesState(b.Timers, files)
+ }
+ return &releaseEntry{Box: b.ID, Session: h.Session, Gen: h.Gen, FinalTX: n, ManifestSeq: seq, Flushed: flushed,
Files: files, Timers: append([]int(nil), b.Timers...), At: w.now}
}
@@ -207,7 +232,18 @@ func (w *world) selectPin(b *box, c *claim) *pinEntry {
w.markStuck(c, fmt.Sprintf("an empty listing of %q is no evidence of an empty database (session %d)", src, h.Session))
return nil
}
- return &pinEntry{Gen: src, TX: n, ClaimVer: c.Ver, At: w.now, Files: w.relocFiles(c).clone(), Timers: append([]int(nil), w.relocTimers(c)...)}
+ pin := &pinEntry{Gen: src, TX: n, ClaimVer: c.Ver, At: w.now, Files: w.relocFiles(c).clone(), Timers: append([]int(nil), w.relocTimers(c)...)}
+ // (Task 4) the files pin: the newest landed manifest of the admitted
+ // chain, by exact version, independently of the database baseline
+ // (B2-4); after a release it must reach the release's manifest_seq
+ if mk, mv, ms, mg, _ := w.newestManifest(b.Region, h.Location, h.Gen); mk != "" {
+ if r != nil && r.ManifestSeq > 0 && on("reloc-pin-reaches-release") && (mg != r.Gen || ms < r.ManifestSeq) {
+ w.stats["pin: waits for the release's manifest"]++
+ return nil
+ }
+ pin.ManKey, pin.ManVer, pin.ManSeq, pin.ManGen = mk, mv, ms, mg
+ }
+ return pin
}
// restoreUpTo restores generation gen of region r from its current
@@ -279,6 +315,9 @@ func (w *world) restoreUpTo(r, inc int, loc, gen string, upto int) *localDB {
// converted move's or the failover's stand-in for the files publisher
// (moves §14.2.6). Task 4 puts the pinned manifest first.
func (w *world) relocFiles(c *claim) *filesDir {
+ if m := w.pinnedManifest(c); m != nil && m.Files != nil {
+ return m.Files
+ }
if p := c.Op.Pin; p != nil && p.Files != nil {
return p.Files
}
@@ -290,6 +329,9 @@ func (w *world) relocFiles(c *claim) *filesDir {
// relocTimers is the wake state the local install replaces timers with.
func (w *world) relocTimers(c *claim) []int {
+ if m := w.pinnedManifest(c); m != nil {
+ return m.Timers
+ }
if p := c.Op.Pin; p != nil && p.Files != nil {
return p.Timers
}
@@ -364,6 +406,20 @@ func (w *world) markStuck(c *claim, why string) {
// source, when it is alive and its fence did not discharge it, and every
// other box this operation handed op.exec to.
func (w *world) relocationLeftovers(n *claim, op opState) {
+ // every prepared generation this operation built and no writer ever
+ // opened is a dead generation of holder.location: its remote build is
+ // retired by a park-generation queued here (model ruling 16; 1b-next's
+ // CompleteRelocation queues park-local chores only, and nothing else
+ // retires an abandoned P's objects before the at-rest sweep)
+ if h := n.Holder; h != nil {
+ for _, g := range op.Built {
+ if g == h.Gen || w.ancestorGen(h.Location, h.Gen, g) {
+ continue
+ }
+ n.Obl = append(n.Obl, w.scoped(obligation{ID: w.newID("ob"), Op: op.ID, Kind: "park-generation", Region: op.SrcRegion, Box: -1, Prefix: h.Location, Ret: g, Quiet: w.now + horizonH}, w.now, h.Inc))
+ w.stats["relocation: abandoned prepared generation parked"]++
+ }
+ }
owed := append([]int{op.Src}, op.InstalledOn...)
for _, id := range owed {
if id < 0 || id == op.Exec || contains(op.Discharged, id) {
@@ -538,6 +594,9 @@ func (w *world) handExec(n *claim, box int, phase, prepared string) {
n.Op.Receipt = nil
}
n.Op.Attempts = 0
+ if prepared != "" && !hasStr(n.Op.Built, prepared) {
+ n.Op.Built = append(n.Op.Built, prepared)
+ }
n.Op.InstalledOn = addUniq(n.Op.InstalledOn, box)
n.Boxes = addUniq(n.Boxes, box)
}
@@ -601,9 +660,30 @@ func (w *world) relocInstalling(b *box, c *claim) {
}
}
-// buildPreparedFiles is Task 4's prepared files manifest; before it, the
-// build has nothing to write for files.
-func (w *world) buildPreparedFiles(b *box, c *claim) bool { return true }
+// buildPreparedFiles writes P's prepared files manifest before anything
+// of the database (1b-next Task 8b; CopyPinnedManifest; claim rev 6.30
+// R18-1, moves rev 7.22 §7.6): create-only at sequence 0, bound to
+// {location, P, op id, install_stamp}, with the pinned manifest's files
+// and wake state; the installed CAS waits for its acknowledgement
+// (ToInstalled requires files_seq 0 and the pin's source sequence as
+// provenance). The first admission consumes it as the session
+// publisher's baseline, and the publisher starts at sequence 1 (rule
+// files-prepared-seq-zero); the mutation keeps the source manifest's
+// sequence, as rev 14 did, so the session's first manifests sort below
+// it. In the one-box shape there is no publisher (ruling 11) and nothing
+// to write.
+func (w *world) buildPreparedFiles(b *box, c *claim) bool {
+ if w.perRegion <= 1 {
+ return true
+ }
+ op, h := c.Op, c.Holder
+ seq := 0
+ if !on("files-prepared-seq-zero") && op.Pin != nil {
+ seq = op.Pin.ManSeq
+ }
+ bl := &blob{Kind: "files", Inc: h.Inc, Gen: op.Prepared, Seq: seq, Files: w.relocFiles(c).clone(), Timers: append([]int(nil), w.relocTimers(c)...), Text: fmt.Sprintf("%s/%d", op.ID, op.InstallStamp), Base: w.issued}
+ return w.ackedPut(b, manifestKey(h.Location, op.Prepared, seq), bl, true)
+}
// localInstall advances the executor's local install by one step (§5.8,
// B1-2; 1b-next Task 8c's Install) and reports whether it is whole: park
@@ -1071,6 +1151,9 @@ func (w *world) enrollStep() {
func (w *world) twoBoxStep() {
w.launchReplacements()
w.enrollStep()
+ for _, b := range w.liveBoxes() {
+ w.publishFiles(b)
+ }
if !w.calm && w.fail["terminate"] && w.rng.Intn(200) == 0 {
bs := w.liveBoxes()
if b := bs[w.rng.Intn(len(bs))]; w.regionHAOwnsLoss(b) {
@@ -1097,6 +1180,15 @@ func (w *world) regionHAOwnsLoss(b *box) bool {
}
switch c.Op.Kind {
case "serving", "relocating":
+ if c.Op.Exec == b.ID && w.perRegion > 1 {
+ // finding F2 (model ruling 17): an executor none of whose files
+ // manifests has landed (an adopted legacy host before its first
+ // publication, a new host before its first manifest lands) would
+ // fail over to a fresh instance.key; the sweep leaves it alone,
+ // and TestFailoverBeforeTheFirstManifest shows the loss
+ _, _, _, _, m := w.newestManifest(b.Region, c.Holder.Location, c.Holder.Gen)
+ return m != nil
+ }
return true
}
return !(c.Op.Exec == b.ID || contains(c.Op.Parts, b.ID) || c.Op.Src == b.ID || c.Op.Tgt == b.ID || c.Op.NewBox == b.ID)
@@ -1287,14 +1379,32 @@ func (w *world) declareTimers(x *box, h *holder) {
}
}
-// timerCarried is Task 4's: a landed manifest carries the timer. Before
-// the files publisher nothing does.
-func (w *world) timerCarried(x *box, h *holder, id int) bool { return false }
+// timerCarried: the newest landed manifest of the admitted chain carries
+// the timer (Task 4), so the install that follows restores it and the
+// fence does not declare it. INV-28 is the oracle beside it: a timer the
+// manifest published last of the generation carries is never declared,
+// whatever the sequences say.
+func (w *world) timerCarried(x *box, h *holder, id int) bool {
+ _, _, _, _, m := w.newestManifest(x.Region, h.Location, h.Gen)
+ if m != nil && contains(m.Timers, id) {
+ return true
+ }
+ if last := w.lastLandedManifest(x.Region, h.Location, h.Gen); last != nil && contains(last.Timers, id) {
+ w.violate("INV-28: box %d's timer %d is declared lost, but the manifest published last in generation %q carries it (seq %d)", x.ID, id, last.Gen, last.Seq)
+ }
+ return false
+}
// deadBoxFiles is what a fenced box's files directory contributes to the
-// recovery: until Task 4's files publisher, its local directory stands in
-// for what it published (L17), as convertToRelocating's does.
+// recovery: in the one-box shape, which has no files publisher (ruling
+// 11), its local directory stands in for what it published (L17), as
+// convertToRelocating's does; in the two-box shape nothing, because a
+// dead box's disk is never read: the files come from the pinned manifest
+// alone.
func (w *world) deadBoxFiles(x *box) *filesDir {
+ if w.perRegion > 1 {
+ return nil
+ }
return x.Files.clone()
}
@@ -1302,8 +1412,7 @@ func (w *world) deadBoxFiles(x *box) *filesDir {
// executor (§5.8 reason failover, StartRelocation with a fence; spec 3's
// placer supplies the decision): op.exec none, the stamp kept, at pinning
// with the target named there (ruling 4); the pin waits out
-// failoverPinDelay from the fence; deadBoxFiles is the files publisher's
-// stand-in until Task 4.
+// failoverPinDelay from the fence.
func (w *world) startFailover(n *claim, x *box) {
n.Op = opState{Kind: "relocating", ID: w.newID("rl"), Phase: "pinning", Exec: -1, Src: x.ID, Tgt: -1, SrcRegion: x.Region,
RelocReason: "failover", ReqAt: w.now, App: n.Holder.App, SrcGen: n.Holder.Gen, SrcStamp: n.Holder.Stamp, StopFiles: w.deadBoxFiles(x)}
@@ -1416,3 +1525,169 @@ func (w *world) fenceExhaustedTarget(n *claim, x *box) {
}
n.Op.Stuck = why
}
+
+// ---------- the files publisher and the files pin (region HA §5.6, L13, L17) ----------
+
+// manifestKey is a files manifest of generation gen within loc, by
+// sequence; isManifestKey recognizes one. genOf reads files/ under the
+// origin generation as "".
+func manifestKey(loc, gen string, seq int) string {
+ return dataKey(loc, gen, fmt.Sprintf("files/m-%06d", seq))
+}
+
+func isManifestKey(k string) bool { return strings.Contains(k, "files/m-") }
+
+// filesState is what a manifest carries, as the publisher compares it.
+func filesState(timers []int, f *filesDir) string {
+ if f == nil {
+ return fmt.Sprint(timers)
+ }
+ return fmt.Sprint(timers, f.Key, f.Env)
+}
+
+// publishFiles is the files publisher (§5.6, H6: platform-managed files
+// and wake state sync continuously on every plan): the executor
+// publishes a manifest, files and timers as they stand, whenever that
+// state changed since its last one, at the generation's next sequence
+// (the publisher of a generation starts at 1; a relocation's P has its
+// prepared manifest at 0). The PUT goes through issue, so it may complete
+// late, after the box is terminated: the late-file-upload case. A
+// relocation's target publishes its probe session's state under P
+// (B2-4). Only the two-box shape runs it (ruling 11).
+func (w *world) publishFiles(b *box) {
+ c := w.claim
+ if c == nil || c.Holder == nil || !w.agentUp(b) || b.Row == nil || b.Files == nil || b.Files.Inc != c.Holder.Inc {
+ return
+ }
+ if c.Op.Exec != b.ID || !(c.Op.Kind == "serving" || c.Op.Kind == "relocating" && (b.ID == c.Op.Src || preparedOpened(c))) {
+ return // a relocation's target publishes only once P is opened, into its own generations
+ }
+ h := c.Holder
+ if b.pubGen != h.Gen {
+ b.pubGen, b.pubSeq, b.releaseSeq = h.Gen, 0, 0
+ }
+ state := filesState(b.Timers, b.Files)
+ if state == b.published {
+ return
+ }
+ b.pubSeq++
+ w.issued++
+ bl := &blob{Kind: "files", Inc: h.Inc, Gen: h.Gen, Seq: b.pubSeq, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...), Base: w.issued}
+ w.issue(b.ID, &request{kind: rPut, region: b.Region, key: manifestKey(h.Location, h.Gen, b.pubSeq), b: bl})
+ b.published = state
+ w.stats["files manifests published"]++
+}
+
+// newestManifest is the files pin's choice (§5.8, B2-4; StorePinner): the
+// newest landed manifest in the admitted chain, holder.generation first,
+// then each generation it superseded (genParent: the files live set's
+// chain, which no trim of holder.admissions shortens; 1b-next rev 12
+// finding 1), by sequence; not the database baseline's generation.
+// Nothing landed: "" and nil.
+func (w *world) newestManifest(r int, loc, gen string) (key string, ver, seq int, mgen string, m *blob) {
+ bk := w.buckets[r]
+ seen := map[string]bool{}
+ for p := dataKey(loc, gen, ""); !seen[p]; {
+ seen[p] = true
+ var best *blob
+ for _, k := range bk.keys(p + "files/") {
+ v := bk.current(k)
+ if v == nil || v.B == nil || v.B.Kind != "files" {
+ continue
+ }
+ if best == nil || v.B.Seq > seq {
+ key, ver, seq, mgen, best = k, v.ID, v.B.Seq, v.B.Gen, v.B
+ }
+ }
+ if best != nil {
+ return key, ver, seq, mgen, best
+ }
+ next, ok := w.genParent[p]
+ if !ok {
+ break
+ }
+ p = next
+ }
+ return "", 0, 0, "", nil
+}
+
+// lastLandedManifest is INV-28's ground truth: of the first generation in
+// the chain that holds a landed manifest, the one published last (the
+// issue order the model records in the blob), whatever its sequence.
+func (w *world) lastLandedManifest(r int, loc, gen string) *blob {
+ _, _, _, mg, m := w.newestManifest(r, loc, gen)
+ if m == nil {
+ return nil
+ }
+ bk := w.buckets[r]
+ last := m
+ for _, k := range bk.keys(dataKey(loc, mg, "files/")) {
+ if v := bk.current(k); v != nil && v.B != nil && v.B.Kind == "files" && v.B.Gen == mg && v.B.Base > last.Base {
+ last = v.B
+ }
+ }
+ return last
+}
+
+// filesLive is the files live set (L13; claim §6.2a "Files in the live
+// set"): a manifest of holder.generation, of a relocation's prepared
+// generation, the one a running relocation's pin names, and the newest
+// landed manifest of the admitted chain (the live manifest, which an
+// unchanged file keeps referencing generations after it was published)
+// is never archived by a park-generation or read as residue. The
+// mutation of files-live-set protects nothing, so a park-generation of an
+// older generation archives the live or the pinned manifest.
+func (w *world) filesLive(c *claim, k string) bool {
+ return on("files-live-set") && w.filesLiveSet(c, k)
+}
+
+// filesLiveSet is the files live set itself, which the residue oracle
+// reads whatever is mutated.
+func (w *world) filesLiveSet(c *claim, k string) bool {
+ if c == nil || c.Holder == nil || !isManifestKey(k) {
+ return false
+ }
+ loc := c.Holder.Location
+ if !strings.HasPrefix(k, loc) {
+ return false
+ }
+ g := genOf(loc, k)
+ if g == c.Holder.Gen {
+ return true
+ }
+ if c.Op.Kind == "relocating" {
+ if c.Op.Pin != nil && k == c.Op.Pin.ManKey {
+ return true
+ }
+ if c.Op.Prepared != "" && g == c.Op.Prepared {
+ return true
+ }
+ }
+ for r := 0; r < nRegions; r++ {
+ if mk, _, _, _, _ := w.newestManifest(r, loc, c.Holder.Gen); mk == k {
+ return true
+ }
+ }
+ return false
+}
+
+// pinnedManifest is the manifest the local install applies: the exact
+// version the pin names (rule files-pin-exact; the model's versioned
+// bucket reads it by version id, where the real store, which has none,
+// reads the pinner's retained copy, 1b-next ruling 21); the mutation
+// reads the newest manifest at install time, which a late PUT from the
+// dead box may have changed since the pin.
+func (w *world) pinnedManifest(c *claim) *blob {
+ p := c.Op.Pin
+ if p == nil || p.ManKey == "" || c.Holder == nil {
+ return nil
+ }
+ if !on("files-pin-exact") {
+ _, _, _, _, m := w.newestManifest(c.Op.SrcRegion, c.Holder.Location, c.Holder.Gen)
+ return m
+ }
+ if v := w.buckets[c.Op.SrcRegion].byID(p.ManKey, p.ManVer); v != nil && !v.Marker {
+ return v.B
+ }
+ return nil
+}
diff --git a/internal/sim/hostlife/regionha_witness_test.go b/internal/sim/hostlife/regionha_witness_test.go
index 4552c10b5..790220b5d 100644
--- a/internal/sim/hostlife/regionha_witness_test.go
+++ b/internal/sim/hostlife/regionha_witness_test.go
@@ -62,6 +62,8 @@ func TestUnenrolledReferenceNeverChosen(t *testing.T) {
w := twoBoxWitness()
from, peer := w.boxes[0], w.boxes[3]
w.serve(from, 1, app0)
+ w.publishFiles(from) // its files are in S3 before it dies (Task 4: a dead box's disk is never read)
+ w.completeDue(true)
peer.HasKey = false
w.terminate(from)
w.now += replaceDelay
@@ -114,3 +116,53 @@ func TestTwoWorkersOneChore(t *testing.T) {
t.Fatalf("residue after both workers ran the chore: %v", r)
}
}
+
+// TestLateFileUploads (§5.6, §5.8; Review Focus 5): the executor
+// registers a timer, its manifest PUT is held by the witness, and it is
+// terminated. The failover pins the previous manifest, the install
+// applies exactly that version, the held PUT lands after the pin, and
+// the timer it carried is declared, never silently dropped; the late
+// manifest is parked with generation_from.
+func TestLateFileUploads(t *testing.T) {
+ w := twoBoxWitness()
+ w.perRegion = 2
+ from, to := w.boxes[0], w.boxes[3]
+ w.serve(from, 1, app0)
+ w.reach(t, 50, "the host runs on box 0", func() bool { return hasMain(from) }, w.actAll(), func() { w.wake(from) })
+ w.publishFiles(from) // the first manifest lands
+ w.completeDue(true)
+ w.nextW++
+ late := w.nextW
+ from.Timers = append(from.Timers, late)
+ w.acks = append(w.acks, ack{W: late, Inc: 1, Box: from.ID, Session: w.claim.Holder.Session, At: w.now, Kind: "timer"})
+ w.holdKey(w.claim.Holder.Location + "files/")
+ w.publishFiles(from) // the second manifest, held
+ w.hold = nil
+ w.terminate(from)
+ w.reach(t, 1500, "serving on box 3", func() bool {
+ c := w.claim
+ return c.Op.Kind == "serving" && c.Op.Exec == to.ID
+ }, w.actAll(), w.recoveryPass, w.operator, func() { w.wake(to) })
+ if contains(to.Timers, late) {
+ t.Fatalf("the install applied a manifest that had not landed at the pin")
+ }
+ declared := false
+ for _, a := range w.acks {
+ if a.W == late && a.Exempt {
+ declared = true
+ }
+ }
+ if !declared {
+ t.Fatalf("the timer the late manifest carried was not declared with the fence")
+ }
+ if n := w.completeHeld(w.claim.Holder.Location + "files/"); n != 1 {
+ t.Fatalf("held manifest PUTs completed: %d, want 1", n)
+ }
+ w.finish(t)
+ if len(w.violations) > 0 {
+ t.Fatalf("%s", w.violations[0])
+ }
+ if r := w.residue(); len(r) > 0 {
+ t.Fatalf("the late manifest was never parked: %v", r)
+ }
+}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 2516bf2ff..ac25284a9 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -177,4 +177,8 @@ var allRules = []string{
"reloc-replacement-table", // region HA §5.8 (ReplaceTarget): a target lost after P's first admission is a nested failover from holder.generation; the mutation resumes at installed with the same P (the admission rules refuse the reopening: expected miss, see expected-outcomes.txt)
"reloc-replace-not-owing", // 1b-next rev 6 finding 1 (replaceTargetSlot's ErrPendingChore, Worker.next's LocalChoreBoxes): a replacement target never owes a park-local for the host, in the chooser and inside the CAS; the mutation lifts both for a relocation's target
"reloc-exhausted-fence", // 1b-next ruling 23 as rev 9 amended it (FenceExhaustedTarget): an exhausted target's fence while the live source is op.exec records stuck and changes nothing else; the mutation is rev 8's, op.exec none at pinning, revoking the source without its stop evidence
+ // the files publisher, the files pin and the files live set (Task 4)
+ "files-pin-exact", // region HA §5.8 the pinned recovery set, B2-4 (RecoveryPin.FilesManifest, StorePinner, ruling 21's retained copy): the local install applies the manifest version the pin names; the mutation reads the newest at install time. A determinism rule: a later PUT adds a version nothing reads (expected miss)
+ "files-live-set", // region HA §5.6, L13, claim §6.2a (the classifier's files live set, 1b-next rev 12 finding 1's referenced origins): a park-generation never archives the live manifest of the chain, holder.generation's, P's or the pinned one; the mutation archives them with their dead generation
+ "files-prepared-seq-zero", // claim rev 6.30 R18-1, moves rev 7.22 §7.6, 1b-next rev 15 finding 1 (CopyPinnedManifest, PreparedAuthority.FilesSeq 0): P's prepared manifest is at sequence 0 and the session publisher starts at 1; the mutation keeps the source's sequence, so a later pin takes the stale prepared manifest over the session's (INV-28)
}
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
index 1a3584888..da4a709fb 100644
--- a/internal/sim/hostlife/sim_test.go
+++ b/internal/sim/hostlife/sim_test.go
@@ -454,7 +454,7 @@ func (w *world) residueOf(exceptStragglers bool) []string {
bk := w.buckets[r]
for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} {
for _, k := range bk.keys(p) {
- if strings.HasSuffix(k, "lock.json") || (r == serving && (live[k] || isDataKey(k) && live[genPrefixOf(k)] || isClosedKey(k) && live[k[:strings.LastIndex(k, "closed/")+7]])) {
+ if strings.HasSuffix(k, "lock.json") || (r == serving && (live[k] || isDataKey(k) && live[genPrefixOf(k)] || isClosedKey(k) && live[k[:strings.LastIndex(k, "closed/")+7]] || w.filesLiveSet(c, k))) {
continue
}
if exceptStragglers && w.owed(r, k) {
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index f76c22333..7426cd5fc 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -370,6 +370,13 @@ type box struct {
// VerifyReceipt): durable, it survives an agent restart; a park of the
// installation removes it, and so does a lost volume (a witness)
receipt *receiptEntry
+ // the files publisher (§5.6, Task 4): the generation it publishes in,
+ // its sequence there, the state its last manifest carried (in memory),
+ // and the release's final manifest while its PUT is outstanding
+ pubGen string
+ pubSeq int
+ published string
+ releaseSeq int
// attemptTag is the probe attempt this agent process has counted and
// not yet ended (memory: a restart forgets it, and the next attempt is
// counted again, ruling 19)
@@ -815,10 +822,11 @@ type opState struct {
Discharged []int // fenced boxes whose park-local chores the fence CAS discharged (L3, H19)
Stuck string
// 1b-next rev 16's journal additions
- ReleasingSince int // releasing_since: the release deadline's start (ruling 14)
- Attempts int // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19)
- PreparedOpened string // prepared_opened: journaled by the admission that opened P (rev 12 S1)
- Resolved bool // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted
+ ReleasingSince int // releasing_since: the release deadline's start (ruling 14)
+ Attempts int // probe_attempts.<op.exec>: counted before each attempt, at most probeTries (ruling 19)
+ PreparedOpened string // prepared_opened: journaled by the admission that opened P (rev 12 S1)
+ Resolved bool // an operator's resolve (model ruling 13): the source is eligible as a target again, and an empty listing is accepted
+ Built []string // every prepared generation this operation built: one no writer opened is parked at serving (model ruling 16)
// journal
ReportAt int
@@ -931,6 +939,7 @@ type pinEntry struct {
// Task 4's manifest: the release's, or a failover's stand-in
Files *filesDir
Timers []int
+ ManGen string // the generation whose manifest the files pin names (Task 4)
}
// receiptEntry is the local install receipt (§5.8 local_install): the
@@ -1042,6 +1051,7 @@ type intner interface{ Intn(n int) int }
type world struct {
perRegion int // boxes per region at the start (region HA L18): 1, today's model, or 2
+ issued int // files manifests issued, in order: INV-28's ground truth (blob.Base)
t testingT
seed int64
rng intner
@@ -1207,6 +1217,7 @@ func (c *claim) clone() *claim {
n.Op.Excluded = append([]int(nil), c.Op.Excluded...)
n.Op.InstalledOn = append([]int(nil), c.Op.InstalledOn...)
n.Op.Discharged = append([]int(nil), c.Op.Discharged...)
+ n.Op.Built = append([]string(nil), c.Op.Built...)
if r := c.Op.Release; r != nil {
cp := *r
cp.Files = r.Files.clone()