amadan

carlos / platform Public

sim: hostlife: pure restore oracle, acknowledged anchors, claim rev 6.5 stamps, the budget's verify pass (rev 7.7)

R6-1: restoreCalc is the restore contract as a pure calculation and the
only restore the oracles call; restoreInit is the activator's, which
writes the anchor, opens replication only once the PUT is acknowledged
(rule anchor-acked, retrying the same bytes after uploadTimeout) and reads
the position from the listing, never from the restored TXID. The oracles
assert their purity: the buckets' versions, the pending requests, the
upload queues, the anchors, the console and the random source's draw
count are fingerprinted before and after. canStart initializes the stamp
record on a copy of the box. Witness: a push whose anchor PUT is held
across attempted opens.

R6-4 (claim rev 6.5, d36adcfa): holder.stamp always names the
installation op.exec should run. The flip keeps the source's stamp in
the journal (op.SrcStamp); the CAS that returns execution to the source
writes it back (rule return-stamp); initRecord on the source then changes
nothing, the dirty install runs under S, and activation of the probe
CAS's new stamp retires S and tags the return generation's artifacts.
Every issued stamp records the box it names; activating another box's
stamp is INV-6. retire-artifacts parks by tag (database and files, or the
database alone where the files are carried) and its callers assert the
tags they expect. A reboot can lose the local stamp record, which the
next fresh read re-initializes. Witness: a dirty return with a lost local
record.

R6-3: the budget prices regional S3 and the disk separately, and the
`restored` phase verifies the database the build produced instead of
restoring it again; the review's 3 GiB workload is reproduced at 108.68
and 124.04 s and refused by rev 7.7's arithmetic.

Compaction keeps the newest level-0 input, as litestream's retention
does.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
claude 445628595f49853adf660da81524ee5db9001b70 parent 39ddcfb
10 files changed, +487 −147
  • internal/sim/hostlife/background_test.go +15 −3
  • internal/sim/hostlife/budget_test.go +68 −28
  • internal/sim/hostlife/console_test.go +3 −3
  • internal/sim/hostlife/ltx_test.go +6 −2
  • internal/sim/hostlife/moves_test.go +87 −25
  • internal/sim/hostlife/protocol_test.go +74 −46
  • internal/sim/hostlife/rules_test.go +5 −3
  • internal/sim/hostlife/sim_test.go +73 −6
  • internal/sim/hostlife/witness_test.go +99 −3
  • internal/sim/hostlife/world_test.go +57 −28
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go
index a5d37f7b7..f345765d4 100644
--- a/internal/sim/hostlife/background_test.go
+++ b/internal/sim/hostlife/background_test.go
@@ -150,8 +150,12 @@ func (w *world) adopt() bool {
if eb == nil {
return false
}
- n := &claim{Ver: 1, Holder: &holder{Inc: w.rec.Inc, App: w.rec.App, Legacy: true, Location: locationFor(w.rec.Inc, true), Stamp: 1}, // adoption writes holder.stamp (claim rev 6.4 §2)
+ n := &claim{Ver: 1, Holder: &holder{Inc: w.rec.Inc, App: w.rec.App, Legacy: true, Location: locationFor(w.rec.Inc, true), Stamp: 1}, // adoption writes holder.stamp (claim rev 6.5 §2)
Op: opState{Kind: "serving", Exec: eb.ID, Parts: []int{eb.ID}}, Regions: []int{w.rec.Region}, Boxes: []int{eb.ID}, Complete: false}
+ if w.stampBox == nil {
+ w.stampBox = map[int]int{}
+ }
+ w.stampBox[1] = eb.ID // the adoption's stamp names the serving box's installation (claim rev 6.5 §2)
if on("legacy-discovery") {
// every other region parks whatever it holds: it cannot be the
// live lineage, because the record names another region
@@ -197,7 +201,7 @@ func (w *world) reconcileClaimed(b *box, c *claim) {
}
if b.Row == nil && c.Op.Kind == "serving" {
b.Row = &row{Inc: h.Inc, App: h.App, Status: "ready"}
- w.initRecord(b, c) // the local record from holder.stamp, on this fresh read (claim rev 6.4 §6.4)
+ w.initRecord(b, c) // the local record from holder.stamp, on this fresh read (claim rev 6.5 §6.4)
}
} else if b.Row != nil && !(on("participant-rows") && w.ownsLocalObligation(c, b)) {
w.retireRow(b)
@@ -255,7 +259,7 @@ func (w *world) passExec(b *box) {
return // the selected bundle is no longer the held one
}
}
- // the local record (claim rev 6.4 §6.4): the writer carries the stamp
+ // the local record (claim rev 6.5 §6.4): the writer carries the stamp
// it selected under, admitted only if it is still the active one
if !b.admitsStamp(p.Inc, p.Stamp) {
return
@@ -344,6 +348,14 @@ func (w *world) fault() {
b.plans = nil // a reboot ends every process
b.AgentDown, b.Frozen, b.AgentPaused = false, false, false
b.forget()
+ if w.rng.Intn(8) == 0 && len(b.Stamps) > 0 {
+ // the local stamp record is lost with the reboot: the box
+ // refuses every writer until it re-initializes from a fresh
+ // claim read naming it (claim rev 6.5 §6.4; rev 7.7, R6-4)
+ b.Stamps = nil
+ w.logf("box %d lost its local stamp record", b.ID)
+ w.stats["stamp records lost"]++
+ }
if !on("floor-boot-recovery") && w.rng.Intn(3) == 0 {
b.Old = true
w.logf("box %d boot-recovered an old executable", b.ID)
diff --git a/internal/sim/hostlife/budget_test.go b/internal/sim/hostlife/budget_test.go
index 54f5142a0..3987ae088 100644
--- a/internal/sim/hostlife/budget_test.go
+++ b/internal/sim/hostlife/budget_test.go
@@ -2,20 +2,25 @@ package hostlife
import "testing"
-// The readiness arithmetic of moves spec §7.3 T11 (rev 7.6, R3-7, R5-5), in
-// seconds. Rev 7.3's T11 required every one of three probe attempts, each
-// with its settle, to fit the window beside the fixed costs: 150 s of
-// probing alone, against a default window of 120 s, so no default move
-// was ever eligible. Rev 7.4 made the permitted attempt count depend on
-// the admitted budget. Rev 7.5 then made the sealed transfer a full
-// snapshot but still priced the final mirror at the 16 MiB bar (R5-5).
-// Rev 7.6 prices what the cut really does: the final delta mirror within
-// the bar, then on the target a restore of the staged replica, the
-// construction of the generation's snapshot and its level-0 anchor, each
-// at the measured local rate for the whole database.
+// The readiness arithmetic of moves spec §7.3 T11 (rev 7.7; R3-7, R5-5,
+// R6-3), in seconds. Rev 7.3's T11 required every one of three probe
+// attempts, each with its settle, to fit the window beside the fixed costs:
+// 150 s of probing alone, against a default window of 120 s, so no default
+// move was ever eligible. Rev 7.4 made the permitted attempt count depend
+// on the admitted budget. Rev 7.5 made the sealed transfer a full snapshot
+// but still priced the final mirror at the 16 MiB bar (R5-5). Rev 7.6
+// built the snapshot on the target and priced three local passes, then
+// restored the generation cold a fourth time without pricing it (R6-3).
+// Rev 7.7 prices what the cut does, with regional S3 and the disk as
+// separate rates: the final delta mirror within the bar across regions;
+// on the target the restore of the staged replica (S3 read, disk write),
+// the snapshot write and the anchor write (disk read, S3 write each), and
+// the verification of the database the build produced (a disk read: its
+// sha256 against the install manifest), which is what the `restored`
+// phase does instead of a second cold restore.
type cutEstimate struct {
Stop, Checkpoint, Mirror, Archive, Render, Open float64
- RestoreStaged, SnapshotBuild, Anchor float64 // target-side, local, whole database
+ RestoreStaged, SnapshotBuild, Anchor, Verify float64 // target-side, whole database
Probe, Settle float64 // one attempt
}
@@ -28,7 +33,7 @@ const (
)
func (e cutEstimate) fixed() float64 {
- return e.Stop + e.Checkpoint + e.Mirror + e.Archive + e.RestoreStaged + e.SnapshotBuild + e.Anchor + e.Render + e.Open
+ return e.Stop + e.Checkpoint + e.Mirror + e.Archive + e.RestoreStaged + e.SnapshotBuild + e.Anchor + e.Verify + e.Render + e.Open
}
// attemptsAdmitted is T11 as rev 7.4 states it: the attempts permitted are
@@ -51,22 +56,34 @@ func (e cutEstimate) fitsRev73(window float64) bool {
return e.fixed()+probeAttemptsMax*(e.Probe+e.Settle) <= window
}
-// estimate prices a cut for a database of dbMiB over a cross-region path
-// of crossMiBps and a local disk of localMiBps, as rev 7.6 §7.3 does.
-func estimate(dbMiB, crossMiBps, localMiBps float64) cutEstimate {
+// rates are the measured rates T11 reads, in MiB/s: the cross-region copy
+// path, regional S3 (reads and writes from a box in the bucket's region)
+// and the box's disk.
+type rates struct{ cross, s3, disk float64 }
+
+// estimate prices a cut for a database of dbMiB at the given rates, as
+// rev 7.7 §7.3 does. Every target-side pass moves the whole database once
+// across S3 and once across the disk, bar the verification, which reads
+// the disk alone.
+func estimate(dbMiB float64, r rates) cutEstimate {
return cutEstimate{
Stop: 2, Checkpoint: 1, Archive: 2, Render: 1, Open: 5,
- Mirror: mirrorBarMiB / crossMiBps,
- RestoreStaged: dbMiB / localMiBps,
- SnapshotBuild: dbMiB / localMiBps,
- Anchor: dbMiB / localMiBps,
+ Mirror: mirrorBarMiB / r.cross,
+ RestoreStaged: dbMiB/r.s3 + dbMiB/r.disk,
+ SnapshotBuild: dbMiB/r.disk + dbMiB/r.s3,
+ Anchor: dbMiB/r.disk + dbMiB/r.s3,
+ Verify: dbMiB / r.disk,
Probe: probeSeconds, Settle: settleSeconds,
}
}
+// exampleRates are the rates the spec's worked example uses (§7.3 T11):
+// 10 MiB/s across regions, 250 MiB/s to regional S3, 500 MiB/s on disk.
+var exampleRates = rates{cross: 10, s3: 250, disk: 500}
+
func TestReadinessBudget(t *testing.T) {
// a tiny instance: every fixed cost at the floor of its measured rate
- tiny := estimate(1, 10, 200)
+ tiny := estimate(1, exampleRates)
if tiny.fitsRev73(cutWindowDefault) {
t.Fatalf("rev 7.3's formula admits a tiny instance in the default window: R3-7 is stale")
}
@@ -86,17 +103,19 @@ func TestReadinessBudget(t *testing.T) {
if n := tiny.attemptsAdmitted(600); n != probeAttemptsMax {
t.Fatalf("a 600 s window admits %d attempts, want %d", n, probeAttemptsMax)
}
- // R5-5: a 2 GiB database over a 10 MiB/s cross-region path. Rev 7.5's
- // full-snapshot transfer alone takes 205 s and could never fit; rev
- // 7.6 ships the final delta within the bar and builds the snapshot on
- // the target at the local rate
- big := estimate(2048, 10, 200)
- fullTransfer := 2048.0 / 10
+ // R5-5: the spec's example, a 2 GiB database at the example rates. Rev
+ // 7.5's full-snapshot transfer alone takes 205 s and could never fit;
+ // the delta within the bar and the target's build do, with one attempt
+ big := estimate(2048, exampleRates)
+ fullTransfer := 2048.0 / exampleRates.cross
if fullTransfer < cutWindowDefault {
t.Fatalf("the example no longer illustrates R5-5")
}
if n := big.attemptsAdmitted(cutWindowDefault); n != 1 {
- t.Fatalf("a 2 GiB database over 10 MiB/s with the snapshot built on the target admits %d attempts, want 1 (fixed %.1f s)", n, big.fixed())
+ t.Fatalf("a 2 GiB database at the example rates admits %d attempts, want 1 (fixed %.1f s)", n, big.fixed())
+ }
+ if big.fixed() < 53 || big.fixed() > 54 {
+ t.Fatalf("the example's fixed costs are %.1f s; the spec says 53.6 s", big.fixed())
}
// and a cross-region snapshot transfer, if a builder did that instead,
// is refused by the same arithmetic
@@ -105,4 +124,25 @@ func TestReadinessBudget(t *testing.T) {
if n := naive.attemptsAdmitted(cutWindowDefault); n != 0 {
t.Fatalf("a full cross-region snapshot transfer admits %d attempts, want 0", n)
}
+ // R6-3: rev 7.6 priced three passes at one local rate and then restored
+ // the generation cold a fourth time, unpriced. The review's workload: 3
+ // GiB, 200 MiB/s local, 10 MiB/s across regions, one probe. Three passes
+ // admit one attempt (108.68 s with the probe); the fourth pass takes the
+ // same workload to 124.04 s, past the window
+ r := rates{cross: 10, s3: 200, disk: 200}
+ three := estimate(3072, r)
+ three.RestoreStaged, three.SnapshotBuild, three.Anchor, three.Verify = 3072/200.0, 3072/200.0, 3072/200.0, 0 // rev 7.6's arithmetic
+ if n := three.attemptsAdmitted(cutWindowDefault); n != 1 {
+ t.Fatalf("rev 7.6's three passes admit %d attempts for the review's workload, want 1 (the finding's premise; fixed %.2f s)", n, three.fixed())
+ }
+ four := three
+ four.Verify = 3072 / 200.0 // the unpriced cold restore, at the same rate
+ if n := four.attemptsAdmitted(cutWindowDefault); n != 0 || four.fixed()+probeSeconds+settleSeconds < 124 {
+ t.Fatalf("with the fourth pass priced the review's workload admits %d attempts at %.2f s with one probe, want 0 past 124 s", n, four.fixed()+probeSeconds+settleSeconds)
+ }
+ // rev 7.7 verifies the built database instead of restoring it again:
+ // the same workload is refused honestly, by its own arithmetic
+ if n := estimate(3072, r).attemptsAdmitted(cutWindowDefault); n != 0 {
+ t.Fatalf("rev 7.7 admits %d attempts for the review's workload, want 0 (fixed %.1f s)", n, estimate(3072, r).fixed())
+ }
}
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index 86b796fce..3675012b9 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -315,7 +315,7 @@ func (w *world) createSteps(p *consolePlan) bool {
return false
}
n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}}
- n.Holder.Stamp = w.nextGen() // create step 4: holder.stamp is this CAS's gen (claim rev 6.4 §2)
+ n.Holder.Stamp = w.issueStamp(n, n.Op.Exec) // create step 4: holder.stamp is this CAS's gen (claim rev 6.5 §2)
return true
}) {
delete(ad.Reg, p.OpID)
@@ -570,7 +570,7 @@ func (w *world) orphanSteps(p *consolePlan) bool {
// deleteSteps: record DeleteIfMatch on the version the intent names, then
// parking with obligations, then free once every obligation is
-// acknowledged (claim §5.2). Under a purge (claim rev 6.4 §5.3 step 4,
+// acknowledged (claim §5.2). Under a purge (claim rev 6.5 §5.3 step 4,
// R4-4) the same steps run under the purge's own claim: the record version
// is recorded in op.intent first, the delete is conditional on it, and
// purging → parking is legal only with the record authoritatively gone
@@ -1025,7 +1025,7 @@ func (w *world) recoveryPass() {
return false
}
n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}}
- n.Holder.Stamp = w.nextGen() // the recovery pass finishing create step 4 writes holder.stamp too
+ n.Holder.Stamp = w.issueStamp(n, n.Op.Exec) // the recovery pass finishing create step 4 writes holder.stamp too (claim rev 6.5 §2)
return true
}) {
delete(w.admit[c.Holder.App].Reg, c.Op.ID)
diff --git a/internal/sim/hostlife/ltx_test.go b/internal/sim/hostlife/ltx_test.go
index fa9bff3d8..ae6fb2d50 100644
--- a/internal/sim/hostlife/ltx_test.go
+++ b/internal/sim/hostlife/ltx_test.go
@@ -317,7 +317,8 @@ func (w *world) currentLTX(bk *bucket, prefix string, level int) []*version {
}
// compact merges the current level-0 files of b's generation into one
-// level-1 file when there are at least three, deletes the inputs, then
+// level-1 file when there are at least three, deletes the inputs bar the
+// newest, then
// writes a new snapshot and enforces retention (litestream's store after
// a compaction at the snapshot level): only the newest snapshot stays,
// and level-1 and level-0 files whose range ends below the previous
@@ -355,7 +356,10 @@ func (w *world) compact(b *box) {
if v := w.issue(b.ID, &request{kind: rPut, region: b.Region, key: ltxKey(db.Loc, db.Gen, 1, out.Min, out.Max), b: out}); v <= 0 {
return
}
- for _, k := range keys {
+ // the inputs are deleted bar the newest: litestream's level-0 retention
+ // never removes the newest level-0 file, which is where a fresh box
+ // reads its position (facts R5-1f to h; R6 review)
+ for _, k := range keys[:len(keys)-1] {
w.issue(b.ID, &request{kind: rDelKey, region: b.Region, key: k})
}
w.stats["ltx compactions"]++
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index b24af297b..23e157b1a 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -48,7 +48,7 @@ func (w *world) workerMode(b *box, obl bool) {
w.role(b, c)
}
-// initRecord is claim rev 6.4 §6.4's initialization (R5-4): a box creates
+// initRecord is claim rev 6.5 §6.4's initialization (R5-4): a box creates
// or refreshes its local stamp record only from a fresh claim read, and
// only when that claim names it as op.exec or as the landing participant;
// it sets active_stamp = holder.stamp. A create's first wake, adoption on
@@ -68,11 +68,55 @@ func (w *world) initRecord(b *box, c *claim) {
if s := b.Stamps[inc]; s != nil && contains(s.Retired, c.Holder.Stamp) {
return
}
- b.install(inc, c.Holder.Stamp)
+ w.activate(b, inc, c.Holder.Stamp, c.Holder.Gen)
c.readStamp = c.Holder.Stamp
w.logf("box %d: local record for inc %d initialized from holder.stamp %d", b.ID, inc, c.Holder.Stamp)
}
+// activate is activation on box b (claim rev 6.5 §6.4): the old active
+// stamp retires, the new one is set, and the artifacts of the generation
+// the claim names, installed under the predecessor's stamp, are tagged
+// with the new one (R6-4: a dirty rollback's return database is installed
+// under S and tagged R when R activates). The oracle refuses a stamp the
+// claim issued for another box's installation (INV-6).
+func (w *world) activate(b *box, inc, stamp int, gen string) {
+ if bx, ok := w.stampBox[stamp]; ok && bx != b.ID {
+ w.violate("INV-6: box %d activates stamp %d, issued for box %d's installation (claim rev 6.5: holder.stamp names the installation op.exec should run)", b.ID, stamp, bx)
+ }
+ b.install(inc, stamp)
+ if b.DB != nil && b.DB.Inc == inc && b.DB.Gen == gen {
+ b.DB.Stamp = stamp
+ }
+ if b.Files != nil && b.Files.Inc == inc && b.Files.Gen == gen {
+ b.Files.Stamp = stamp
+ }
+}
+
+// issueStamp is the stamp an installing CAS writes into holder.stamp: the
+// gen the CAS produces, recorded as box's (claim rev 6.5 §2).
+func (w *world) issueStamp(n *claim, box int) int {
+ s := w.nextGen()
+ if w.stampBox == nil {
+ w.stampBox = map[int]int{}
+ }
+ w.stampBox[s] = box
+ return s
+}
+
+func dbStamp(d *localDB) int {
+ if d == nil {
+ return 0
+ }
+ return d.Stamp
+}
+
+func filesStamp(f *filesDir) int {
+ if f == nil {
+ return 0
+ }
+ return f.Stamp
+}
+
// resumeStale is a stalled worker goroutine of b resuming with a claim it
// read long ago (rev 4's actor). With claim C3's revalidation it re-reads
// under its lease, sees the world moved, and stops; the mutation acts on
@@ -214,7 +258,7 @@ func (w *world) snapshotBlobOf(b *box, c *claim, gen string) (*blob, *blob) {
}
w.ship(b)
db = snapshotOf(b.DB, b.DB.Inc)
- } else if r := w.restore(b, c.Holder.Inc, c.Holder.Location, gen); r != nil {
+ } else if r := w.restoreCalc(b.Region, c.Holder.Inc, c.Holder.Location, gen); r != nil {
db = snapshotOf(r, c.Holder.Inc)
} else {
db = &blob{Kind: "snap", Level: 9, Min: 1, Inc: c.Holder.Inc, Pages: map[string]int{}}
@@ -692,7 +736,8 @@ func (w *world) followRecord(c *claim) bool {
return false
}
n.Op.Kind, n.Op.Exec, n.Op.LandPhase, n.Op.FlipAt = "landing", op.Tgt, "checking", w.now
- n.Holder.Stamp = w.nextGen() // holder.stamp: the gen this CAS produces, the landing's installation stamp (claim rev 6.4 §2)
+ n.Op.SrcStamp = n.Holder.Stamp // the source installation's stamp, kept in the journal for the return (claim rev 6.5)
+ n.Holder.Stamp = w.issueStamp(n, op.Tgt) // holder.stamp: the gen this CAS produces, the landing's installation stamp (claim rev 6.5 §2)
n.Op.FlipGen = n.Holder.Stamp
return true
})
@@ -751,7 +796,7 @@ func (w *world) landTarget(b *box, c *claim) {
// the new installation sets this box's active stamp to its own
// captured stamp, the claim gen of the CAS that made the landing
// current, under the guard, on a fresh read showing its operation
- // current and this box the landing participant (claim rev 6.4
+ // current and this box the landing participant (claim rev 6.5
// §6.4, R3-3, R4-2): a move back to a region the instance left is
// admitted at its own stamp while the retired installation's
// writers stay refused
@@ -839,10 +884,16 @@ func (w *world) landTarget(b *box, c *claim) {
case "restore":
if b.DB == nil || b.DB.Gen != op.ID {
if b.DB != nil {
- b.retireArtifacts(c.Holder.Inc, b.DB.Stamp)
- b.Parked++
+ // an earlier stay's database: retire-artifacts of its stamp,
+ // never of the installation checking activated
+ if b.DB.Stamp == b.stampOf(c.Holder.Inc) {
+ w.violate("INV-6: landing on box %d would park a database tagged with its own active stamp %d", b.ID, b.DB.Stamp)
+ }
+ w.retireDatabase(b, c.Holder.Inc, b.DB.Stamp)
+ }
+ if b.DB = w.restoreInit(b, c.Holder.Inc, loc, op.ID); b.DB == nil && w.restoreCalc(b.Region, c.Holder.Inc, loc, op.ID) != nil {
+ return // the anchor is outstanding: try again
}
- b.DB = w.restore(b, c.Holder.Inc, loc, op.ID)
}
if b.DB == nil {
w.rollback(c, "restore failed")
@@ -926,15 +977,22 @@ func (w *world) installLocal(b *box, c *claim, gen string, seal ref, _ string, n
}
if b.Files == nil || b.Files.Gen != gen {
// fresh extraction: park whatever is there first, as
- // retire-artifacts of the predecessor's stamp (claim rev 6.4
- // §6.4): the new installation's active stamp is untouched
- if b.DB != nil {
- b.retireArtifacts(c.Holder.Inc, b.DB.Stamp)
- b.Parked++
- }
- if b.Files != nil {
- b.retireArtifacts(c.Holder.Inc, b.Files.Stamp)
- b.Parked++
+ // retire-artifacts of the predecessor's stamp (claim rev 6.5
+ // §6.4): the new installation's active stamp is untouched. A
+ // landing parks an earlier stay, never its own installation; a
+ // dirty rollback's install on the source parks the pre-move
+ // database while its stamp is still the active one (R6-4)
+ for _, st := range []int{dbStamp(b.DB), filesStamp(b.Files)} {
+ if st == 0 {
+ continue
+ }
+ if c.Op.Kind == "restoring" && st != b.stampOf(c.Holder.Inc) {
+ w.violate("INV-6: the dirty install on box %d parks an artifact tagged %d while the active stamp is %d (claim rev 6.5 §6.4)", b.ID, st, b.stampOf(c.Holder.Inc))
+ }
+ if c.Op.Kind == "landing" && st == b.stampOf(c.Holder.Inc) {
+ w.violate("INV-6: landing on box %d would park an artifact tagged with its own active stamp %d", b.ID, st)
+ }
+ w.retireArtifacts(b, c.Holder.Inc, st)
}
b.DB = nil
b.Files = nil
@@ -1126,6 +1184,12 @@ func (w *world) recoverSource(b *box, c *claim) {
return false
}
n.Op.Exec, n.Op.SrcPhase = op.Src, "claimed"
+ // return to source (claim rev 6.5): the CAS that makes the
+ // source's existing installation current again writes its
+ // stamp back, from the journal; never the target's F
+ if on("return-stamp") {
+ n.Holder.Stamp = op.SrcStamp
+ }
return true
})
}
@@ -1200,7 +1264,7 @@ func (w *world) recoverSource(b *box, c *claim) {
w.cas(c, func(n *claim) bool {
w.newGen(n.Holder.Location, n.Holder.Gen, op.RollbackID)
n.Holder.Gen = op.RollbackID
- n.Holder.Stamp = w.nextGen() // a dirty rollback installs a new generation: a new stamp, never the predecessor's (claim rev 6.4 §6.4)
+ n.Holder.Stamp = w.issueStamp(n, op.Src) // a dirty rollback installs a new generation: a new stamp, never the predecessor's (claim rev 6.5 §6.4)
n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.SrcRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.RollbackID), "", op.ReturnQuiet))
return sameOp(n.Op.ID, op.ID)
})
@@ -1271,12 +1335,10 @@ func (w *world) pushStep(b *box, c *claim) {
}
case "restore":
if b.DB != nil && b.DB.Gen != op.ID {
- b.retireArtifacts(c.Holder.Inc, b.DB.Stamp)
- b.Parked++
- b.DB = nil
+ w.retireDatabase(b, c.Holder.Inc, b.DB.Stamp) // the files are carried (F7)
}
if b.DB == nil {
- b.DB = w.restore(b, c.Holder.Inc, loc, op.ID)
+ b.DB = w.restoreInit(b, c.Holder.Inc, loc, op.ID)
}
if b.DB == nil {
return
@@ -1302,7 +1364,7 @@ func (w *world) pushStep(b *box, c *claim) {
n.Op.Phase = "probed"
w.newGen(n.Holder.Location, n.Holder.Gen, op.ID)
n.Holder.Gen = op.ID
- n.Holder.Stamp = w.nextGen() // a push's commit installs a new generation: a new stamp (claim rev 6.4 §2)
+ n.Holder.Stamp = w.issueStamp(n, n.Op.Exec) // a push's commit installs a new generation: a new stamp (claim rev 6.5 §2)
q := op.StopAt + horizonH
if q > n.Quiet[b.Region] {
n.Quiet[b.Region] = q
@@ -1413,7 +1475,7 @@ func locationOf(k string) string {
// characters; the model's decimal ids) is an incarnation location.
// A level directory (0000 to 0009, litestream's layout) or a
// generation prefix (g-<op>/) directly under the host belongs to
- // the legacy location, the host prefix itself (claim rev 6.4 §6.2a)
+ // the legacy location, the host prefix itself (claim rev 6.5 §6.2a)
digits := len(child) > 0 && !isLevelDir(child)
for _, r := range child {
if r < '0' || r > '9' {
@@ -1429,7 +1491,7 @@ func locationOf(k string) string {
// deadGeneration: within holder.location, everything but the live set.
// The live set is {authoritative region, holder.location,
-// holder.generation} (claim rev 6.4 §6.2a, R4-3): the generation's
+// holder.generation} (claim rev 6.5 §6.2a, R4-3): the generation's
// objects are live only in the authoritative region's bucket, the region
// of the holder's current installation; a matching key in any other
// region is residue. The mutation of live-set-region exempts matching keys
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index e156fd0cf..8d8c9bbc8 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -23,7 +23,7 @@ func (w *world) readClaim(b *box) (*claim, bool) {
}
c := w.claim.clone()
if c != nil && c.Holder != nil {
- c.readStamp = b.stampOf(c.Holder.Inc) // the installation stamp this read carries (claim rev 6.4 §6.4)
+ c.readStamp = b.stampOf(c.Holder.Inc) // the installation stamp this read carries (claim rev 6.5 §6.4)
}
b.snap = c.clone()
return c, true
@@ -164,27 +164,14 @@ func (w *world) evidence(b *box, opID string) bool {
// ---------- restore and spawn ----------
-// restore rebuilds a database from location loc, generation gen, in b's own
-// bucket (claim C3a; moves rev 7.6 §5.1, R4-1, R5-1, R5-3), as the pinned
-// litestream does: it roots at the newest current snapshot of the
-// generation at or past the pinned one (the executor's own rotation
-// writes successors; the pinned version is the fallback when none is
-// current), applies the files the planner selects (ltx_test.go plan),
-// and fails closed on a gap or a missing root. There is no database
-// checksum to compare (R5-2): a file is verified by decoding, and the
-// restored database by SQLite's integrity check, which the model's files
-// never fail. Then, when no level-0 file at or past the restored position
-// is current (a snapshot-only install), the activator writes the level-0
-// anchor [cur, cur] before replication starts, so litestream's position
-// is cur (R5-1); the mutation of restore-anchor leaves the position to
-// litestream's open, which takes the newest remote level-0 file, or
-// nothing. The mutation of root-advance roots at the pinned snapshot only
-// (rev 7.5), and refuses once retention has expired its continuation. The
-// mutation of restore-by-generation restores the newest single object
-// anywhere under the location, which is what a prefix restore without
-// generation identity does.
-func (w *world) restore(b *box, inc int, loc, gen string) *localDB {
- bk := w.buckets[b.Region]
+// restoreCalc is the restore contract as a pure calculation (moves spec
+// §5.1 steps 4, 5 and 8; rev 7.7, R6-1): it reads region r's bucket and
+// writes nothing, so every oracle may call it. It returns the database the
+// contract yields, with Pos the position it restored to, or nil when the
+// contract refuses. With restore-by-generation off it is the mutation: the
+// newest object under the location.
+func (w *world) restoreCalc(r int, inc int, loc, gen string) *localDB {
+ bk := w.buckets[r]
db := &localDB{Inc: inc, Loc: loc, Gen: gen, State: map[string]int{}}
if !on("restore-by-generation") {
var best *version
@@ -207,7 +194,6 @@ func (w *world) restore(b *box, inc int, loc, gen string) *localDB {
db.Inc = best.B.Inc
}
}
- db.Stamp = b.stampOf(inc)
return db
}
prefix := dataKey(loc, gen, "")
@@ -237,8 +223,7 @@ func (w *world) restore(b *box, inc int, loc, gen string) *localDB {
m := bk.current(genMarkerKey(loc))
snap := bk.byID(m.B.SnapKey, m.B.Base)
if snap == nil || snap.Marker || snap.B.Max != m.B.TX {
- w.stats["restore refused: snapshot missing or not at the marker's TXID"]++
- return nil
+ return nil // the snapshot version is missing or not at the marker's TXID
}
root = snap.B
}
@@ -264,9 +249,7 @@ func (w *world) restore(b *box, inc int, loc, gen string) *localDB {
}
}
if gap && on("restore-gap-closed") {
- w.logf("box %d restore refused: a gap after TXID %d under %s", b.ID, cur, prefix)
- w.stats["restore refused: gap"]++
- return nil
+ return nil // a gap after cur: refuse (litestream: "non-contiguous ltx files")
}
if len(applied) == 0 && gen != "" {
return nil
@@ -275,22 +258,69 @@ func (w *world) restore(b *box, inc int, loc, gen string) *localDB {
// own later snapshots and anchors carry forward
db.Log = txsOf(applied...)
db.TX = w.lineageTX(applied...)
+ db.Pos = cur
+ return db
+}
+
+// restoreInit is the activator's cold restore: the calculation above, then
+// the restore-to-replication initialization (§5.1 step 7, R5-1, R6-1).
+// Litestream's open takes a fresh box's position from the newest remote
+// level-0 file, or 0. When the restored position is above that (a
+// snapshot-only install), the activator writes the anchor, every page as
+// the level-0 file [cur, cur], and opens replication only once that PUT
+// is acknowledged (rule anchor-acked); the position is then read again
+// from the remote listing, never assumed. A PUT the client has waited
+// uploadTimeout steps for is retried with the same bytes. It returns nil
+// while the anchor is outstanding: the wake tries again. The mutation of
+// restore-anchor writes no anchor; the mutation of anchor-acked opens at
+// once with whatever the listing shows.
+func (w *world) restoreInit(b *box, inc int, loc, gen string) *localDB {
+ db := w.restoreCalc(b.Region, inc, loc, gen)
+ if db == nil {
+ w.logf("box %d restore refused under %s", b.ID, dataKey(loc, gen, ""))
+ w.stats["restore refused"]++
+ return nil
+ }
db.Stamp = b.stampOf(inc)
- // restore-to-replication initialization (R5-1, litestreamfacts
- // TestFact_R5_1_*): litestream's open takes a fresh box's position from
- // the newest remote level-0 file, or 0. When that is below the restored
- // position (a snapshot-only install), the activator writes the anchor,
- // every page as the level-0 file [cur, cur], before replication starts
- db.Pos = w.maxL0(bk, prefix)
- if cur > 0 && db.Pos < cur && on("restore-anchor") {
- db.Pos = cur
- w.issue(b.ID, &request{kind: rPut, region: b.Region, key: ltxKey(loc, gen, 0, cur, cur), b: anchorOf(db, inc)})
- w.stats["restore anchors"]++
+ bk := w.buckets[b.Region]
+ prefix := dataKey(loc, gen, "")
+ cur := db.Pos
+ remote := w.maxL0(bk, prefix)
+ if cur > remote && on("restore-anchor") {
+ key := ltxKey(loc, gen, 0, cur, cur)
+ acked, inflight := false, false
+ for _, r := range b.anchors[key] {
+ if r.done {
+ acked = true
+ } else if w.now-r.at < uploadTimeout {
+ inflight = true
+ }
+ }
+ if !acked && !inflight {
+ r := &request{kind: rPut, region: b.Region, key: key, b: anchorOf(db, inc)}
+ if v := w.issue(b.ID, r); v > 0 {
+ acked = true
+ } else {
+ if b.anchors == nil {
+ b.anchors = map[string][]*request{}
+ }
+ b.anchors[key] = append(b.anchors[key], r)
+ }
+ w.stats["restore anchors"]++
+ }
+ if !acked && on("anchor-acked") {
+ w.logf("box %d waits for its anchor %s to be acknowledged before opening replication", b.ID, key)
+ w.stats["anchor waits"]++
+ return nil
+ }
+ remote = w.maxL0(bk, prefix) // durable evidence: what the listing shows now
}
+ db.Pos = remote
+ w.logf("box %d restored %s: TXID %d at position %d (key %d, stamp %d)", b.ID, prefix, db.TX, db.Pos, db.Key, db.Stamp)
return db
}
-// stampOK is admission's local check (claim rev 6.4 §6.4): the worker's
+// stampOK is admission's local check (claim rev 6.5 §6.4): the worker's
// read of the claim carries the installation stamp active on this box at
// that read; it is admitted only if that is still the active stamp. A
// landing probe refused here by its own installation is the fault R3-3
@@ -359,13 +389,11 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool {
// a warm database from an earlier stay is parked, and the box
// restores cold (§5.1): retire-artifacts of its stamp
if b.DB != nil && (b.DB.Gen != bg || b.DB.Loc != loc) {
- b.retireArtifacts(h.Inc, b.DB.Stamp)
- b.Parked++
- b.DB = nil
+ w.retireDatabase(b, h.Inc, b.DB.Stamp)
}
}
if b.DB == nil {
- b.DB = w.restore(b, h.Inc, loc, want)
+ b.DB = w.restoreInit(b, h.Inc, loc, want)
if b.DB == nil {
return false
}
@@ -444,7 +472,7 @@ func (w *world) admits(b *box, c *claim, probe string) bool {
return false
}
if !w.stampOK(b, c, probe) {
- return false // a retired installation's worker (claim rev 6.4 §6.4)
+ return false // a retired installation's worker (claim rev 6.5 §6.4)
}
if w.isParticipant(c, b) && b.ExecUntil > 0 && w.localNow(b) > b.ExecUntil {
return false // self-fenced until the lease is renewed
@@ -591,13 +619,13 @@ func (w *world) parkDepth(b *box, prefix, dest string, quiet int, keep func(stri
// guard: a retired marker first, then each artifact renamed aside, one per
// call, so a crash can fall between any two (claim §6.3). It reports
// whether nothing is left.
-// localPark is claim rev 6.4's retire-installation (§6.3): the active
+// localPark is claim rev 6.5's retire-installation (§6.3): the active
// stamp moves into retired_stamps and becomes none, then every artifact is
// parked. It serves a delete, a move away and the quarantine; a landing
// parks its predecessor's leftovers with retire-artifacts instead.
func (w *world) localPark(b *box, inc int) bool {
if on("hostguard") && b.stampOf(inc) != 0 {
- b.retireStamp(inc) // retire-installation: active moves into retired_stamps (claim rev 6.4 §6.4)
+ b.retireStamp(inc) // retire-installation: active moves into retired_stamps (claim rev 6.5 §6.4)
return false
}
switch {
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 384b6772f..9ba303251 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -54,8 +54,8 @@ var allRules = []string{
"park-skip-lock", // §6.2 step 2/J-N6
"retirement-ids", // §6.2/J-D5/J-N7
"hostguard", // §6.4/J-N8
- "fence-by-installation", // claim rev 6.4 §6.4 (R3-3): a new installation of a retired incarnation sets its own active stamp; the mutation is rev 5.2's marker, retired for good
- "fence-stamp", // claim rev 6.4 §6.4 (R4-2): a writer is admitted only if its stamp equals the active stamp; the mutation admits any writer for the incarnation while one is active
+ "fence-by-installation", // claim rev 6.5 §6.4 (R3-3): a new installation of a retired incarnation sets its own active stamp; the mutation is rev 5.2's marker, retired for good
+ "fence-stamp", // claim rev 6.5 §6.4 (R4-2): a writer is admitted only if its stamp equals the active stamp; the mutation admits any writer for the incarnation while one is active
"purge-reserve-first", // §5.3/J-N9
"purge-adopts", // this model's finding: purge claims unclaimed legacy records first
"purge-journal", // this model's finding: the reservation is the purge's journal
@@ -84,11 +84,13 @@ var allRules = []string{
"restore-gap-closed", // rev 7.5 §5.1 (R4-1): a current file that starts beyond current+1 once nothing extends the range is a gap, and the restore refuses; the mutation returns what it has
"restore-anchor", // rev 7.6 §5.1 (R5-1): a cold restore with no level-0 file at its position writes the anchor [cur,cur] before replication starts; the mutation leaves the position to litestream's open
"root-advance", // rev 7.6 §5.1 (R5-3): the restore roots at the newest current successor snapshot at or past the pinned one; the mutation roots at the pinned snapshot only
+ "anchor-acked", // rev 7.7 §5.1 step 7 (R6-1): replication opens only once the anchor PUT is acknowledged, and the position is read from the listing; the mutation opens at once with whatever the listing shows
+ "return-stamp", // claim rev 6.5 (R6-4): the CAS that returns execution to the source writes holder.stamp = the source installation's stamp from the journal; the mutation leaves the target's
"quiet-before-ack", // this model's finding (late writes after a park)
"straggler-sweep", // claim rev 5 §6.2a (CC15): the at-rest sweep
"sweep-staging", // CC20: the sweep also covers moves/<host>/
"sweep-namespace", // claim rev 6 §6.2a (R3-4): the sweep discovers locations from the namespace; the mutation reads the capped retired_incarnations
- "live-set-region", // claim rev 6.4 §6.2a (R4-3): the live set is {authoritative region, location, generation}; the mutation exempts matching keys in every region
+ "live-set-region", // claim rev 6.5 §6.2a (R4-3): the live set is {authoritative region, location, generation}; the mutation exempts matching keys in every region
// moves spec
"seal-by-version", // J-N2: landing copies sealed versions
"staging-quiet", // J-N2: staging retired after its writers' horizon
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
index bf9b191ac..7dc286030 100644
--- a/internal/sim/hostlife/sim_test.go
+++ b/internal/sim/hostlife/sim_test.go
@@ -15,7 +15,7 @@ const (
)
func newWorld(seed int64, verbose bool) *world {
- w := &world{seed: seed, rng: rand.New(rand.NewSource(seed)), verbose: verbose,
+ w := &world{seed: seed, rng: &counting{r: rand.New(rand.NewSource(seed))}, verbose: verbose,
stores: map[string]bool{app0: true, app1: true}, cfgVer: map[string]int{app0: 1, app1: 1}, purgeRes: map[string]bool{}, purgeStep: map[string]int{},
control: newBucket(), delivered: map[int]bool{}, durable: map[string]map[int]bool{}, writeInc: map[int]int{}, txs: map[int]tx{}, legacyIncs: map[int]bool{}, purgeOp: map[string]string{}, genParent: map[string]string{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}
for r := 0; r < nRegions; r++ {
@@ -48,7 +48,7 @@ func newWorld(seed int64, verbose bool) *world {
}
// retentionStart: the host has been recreated more times than
-// retired_incarnations remembers (claim rev 6.4 §2 caps it at 32), and a
+// retired_incarnations remembers (claim rev 6.5 §2 caps it at 32), and a
// replication object of an incarnation the list forgot is still in a
// bucket (rev 7.5, R4 §3: the retention-boundary fixture). Only a sweep
// that discovers locations from the namespace parks it.
@@ -390,8 +390,23 @@ func hasNonMarker(vs []*version) bool {
// anything: the final oracle never writes.
func (w *world) canStart(e *box, c *claim) string {
c = c.clone()
- c.readStamp = e.stampOf(c.Holder.Inc) // as a fresh read by e would carry it
- if !w.admits(e, c, "") {
+ // the wake's first step is the record's initialization from this fresh
+ // read (claim rev 6.5 §6.4): a box with no record for the incarnation
+ // that the claim names as op.exec takes holder.stamp. On a copy of the
+ // box: the oracle never writes (R6-1)
+ eb := *e
+ eb.Stamps = map[int]*stamps{}
+ for k, v := range e.Stamps {
+ cp := *v
+ cp.Retired = append([]int(nil), v.Retired...)
+ eb.Stamps[k] = &cp
+ }
+ inc := c.Holder.Inc
+ if eb.stampOf(inc) == 0 && c.Holder.Stamp != 0 && c.Op.Exec == eb.ID && !(eb.Stamps[inc] != nil && contains(eb.Stamps[inc].Retired, c.Holder.Stamp)) {
+ eb.install(inc, c.Holder.Stamp)
+ }
+ c.readStamp = eb.stampOf(inc) // as a fresh read by e would carry it
+ if !w.admits(&eb, c, "") {
return "not admitted"
}
h := c.Holder
@@ -443,9 +458,11 @@ func (w *world) final() {
}
// the serving box's database as it stands, or, if it has none, the
// cold restore it would do: computed, never written
+ before := w.fingerprint()
+ defer w.pure("final oracle", before)
local := e.DB
if local == nil {
- local = w.restore(e, c.Holder.Inc, c.Holder.Location, c.Holder.Gen)
+ local = w.restoreCalc(e.Region, c.Holder.Inc, c.Holder.Location, c.Holder.Gen)
}
if local == nil {
w.violate("final: the serving box %d has no database and nothing to restore", e.ID)
@@ -469,7 +486,9 @@ func (w *world) checkDurable(c *claim, when string) {
if e == nil {
return
}
- db := w.restore(e, c.Holder.Inc, c.Holder.Location, c.Holder.Gen)
+ before := w.fingerprint()
+ defer w.pure("INV-2 oracle", before)
+ db := w.restoreCalc(e.Region, c.Holder.Inc, c.Holder.Location, c.Holder.Gen)
need := map[int]bool{}
seen := map[string]bool{}
for p := dataKey(c.Holder.Location, c.Holder.Gen, ""); p != "" && !seen[p]; p = w.genParent[p] {
@@ -496,6 +515,54 @@ func (w *world) checkDurable(c *claim, when string) {
}
}
+// counting is the sweep's random source, counting its draws so the oracle
+// purity check can show an oracle consumed none (R6-1).
+type counting struct {
+ r *rand.Rand
+ n int
+}
+
+func (c *counting) Intn(n int) int {
+ c.n++
+ return c.r.Intn(n)
+}
+
+// fingerprint is everything an oracle must leave alone: the buckets (the
+// version counter and every version), the pending requests, the boxes'
+// upload queues and anchors, the console's plans and the random source's
+// position (R6-1). An oracle that changes any of it is repairing or
+// disturbing the system it checks.
+func (w *world) fingerprint() string {
+ objs := 0
+ for _, bk := range w.buckets {
+ for _, vs := range bk.objs {
+ objs += len(vs)
+ }
+ }
+ queue, anchors := 0, 0
+ for _, b := range w.boxes {
+ if b.DB != nil {
+ queue += len(b.DB.Queue)
+ }
+ for _, rs := range b.anchors {
+ anchors += len(rs)
+ }
+ }
+ draws := -1
+ if c, ok := w.rng.(*counting); ok {
+ draws = c.n
+ }
+ return fmt.Sprintf("ver=%d objs=%d pending=%d queue=%d anchors=%d console=%d draws=%d", w.ver, objs, len(w.pending), queue, anchors, len(w.console), draws)
+}
+
+// pure records a violation if an oracle changed the system (R6-1): the
+// fingerprint taken before it must equal the one after.
+func (w *world) pure(what, before string) {
+ if after := w.fingerprint(); after != before {
+ w.violate("oracle purity: the %s changed the system: before %s, after %s", what, before, after)
+ }
+}
+
// ltxShape describes the current LTX files under prefix, for diagnosis.
func (w *world) ltxShape(r int, prefix string) string {
var parts []string
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go
index 279702341..7ac881efa 100644
--- a/internal/sim/hostlife/witness_test.go
+++ b/internal/sim/hostlife/witness_test.go
@@ -109,6 +109,11 @@ var witnesses = []witness{
"a snapshot-only install (a push), then writes and replication, then the disk is lost: without the level-0 anchor litestream's position restarts at 1, the new files sit below the snapshot, and the cold restore loses the writes (R5-1; litestreamfacts TestFact_R5_1_*)", wSnapshotOnlyInstall},
{"root-advance", "root-advance", "INV-3 (witness): woken cold",
"after a push, four compaction-and-snapshot rotations with retention; the disk is lost; a restore rooted at the pinned snapshot finds its continuation expired and refuses, while one rooted at the newest current successor snapshot succeeds (R5-3; litestreamfacts TestFact_R5_3_SnapshotRetention)", wRootAdvance},
+ // rev 7.7
+ {"anchor-acked", "anchor-acked", "before its anchor",
+ "a push installs a snapshot alone and its anchor PUT is slow; litestream reads its position from the remote level-0 listing, so the host must not open replication until the anchor is acknowledged; opened at once it runs from TXID 1 below the snapshot and a cold restore loses the writes (R6-1)", wAnchorHeld},
+ {"return-stamp", "return-stamp", "issued for box",
+ "a dirty rollback whose source lost its local stamp record; the return CAS writes the source installation's stamp back and the source re-initializes from it; left as the target's stamp, the source activates an installation that was never its own (claim rev 6.5, R6-4)", wReturnLostRecord},
}
// TestWitnesses is the deterministic half of the mutation evidence.
@@ -1010,7 +1015,7 @@ func (w *world) roundTrip(t *testing.T, uk, us *box) {
}, w.act(uk, us), w.recoveryPass, w.operator)
}
-// wStaleWriter (claim rev 6.4 §6.4, R4-2): a config-sync pass selects the
+// wStaleWriter (claim rev 6.5 §6.4, R4-2): a config-sync pass selects the
// row under the first installation and pauses; the host moves away and
// back; a new bundle is published; the pass takes the guard.
func wStaleWriter(t *testing.T, w *world) {
@@ -1032,7 +1037,7 @@ func wStaleWriter(t *testing.T, w *world) {
w.finish(t)
}
-// wLiveSetRegion (claim rev 6.4 §6.2a, R4-3): a legacy host serves in UK
+// wLiveSetRegion (claim rev 6.5 §6.2a, R4-3): a legacy host serves in UK
// (box 0) with a pre-release replica in US (box 1). Adoption's discovery
// parks US. A replication PUT the old US executor issued before the
// retirement completes after it.
@@ -1136,7 +1141,7 @@ func wRestoreGap(t *testing.T, w *world) {
f := w.compactedPending(b, n+2, n+2) // [n+2, n+2] is current
w.buckets[b.Region].objs[ltxKey(loc, gen, 0, n+2, n+2)] = []*version{{ID: w.newVer(), B: f}}
w.idleStop(b)
- db := w.restore(b, 1, loc, gen)
+ db := w.restoreCalc(b.Region, 1, loc, gen)
if db != nil {
w.violate("INV-2 (cold restore): a restore across the gap after TXID %d returned a database at position %d", n, db.Pos)
}
@@ -1198,3 +1203,94 @@ func wRootAdvance(t *testing.T, w *world) {
w.reach(t, 20, "woken cold", func() bool { return hasMain(b) }, func() { w.wake(b) })
w.finish(t)
}
+
+// ---------- rev 7.7 ----------
+
+// wAnchorHeld (R6-1): the push's install writes its anchor and the PUT is
+// slow. Until it is acknowledged the host must not open replication: the
+// position litestream would read from the listing is 0.
+func wAnchorHeld(t *testing.T, w *world) {
+ b := w.boxes[0]
+ w.serve(b, 1, app0)
+ w.wake(b)
+ for i := 0; i < 3; i++ {
+ w.appWrite(b)
+ }
+ w.replicate(b)
+ w.userPush()
+ gen := w.claim.Op.ID
+ loc := w.claim.Holder.Location
+ w.reach(t, 400, "push published", func() bool {
+ return w.claim.Op.Kind == "pushing" && w.claim.Op.Phase == "restore"
+ }, w.act(b))
+ m := w.buckets[b.Region].current(genMarkerKey(loc))
+ if m == nil || m.B.Gen != gen {
+ t.Fatalf("witness: the push did not publish its generation: %s", w.state())
+ }
+ n := m.B.TX
+ anchor := ltxKey(loc, gen, 0, n, n)
+ w.holdKey(anchor)
+ prefix := dataKey(loc, gen, "")
+ for i := 0; i < 40; i++ {
+ w.tick(w.act(b))
+ for _, f := range w.currentLTX(w.buckets[b.Region], prefix, 0) {
+ if f.B.Min != n {
+ w.violate("INV-2 (witness): box %d replicated [%d,%d] before its anchor [%d,%d] was acknowledged", b.ID, f.B.Min, f.B.Max, n, n)
+ return
+ }
+ }
+ if hasMain(b) {
+ w.violate("INV-2 (witness): box %d opened replication before its anchor [%d,%d] was acknowledged; litestream's position would be %d", b.ID, n, n, w.maxL0(w.buckets[b.Region], prefix))
+ return
+ }
+ }
+ w.hold = nil
+ if w.completeHeld(anchor) == 0 {
+ t.Fatalf("witness: no anchor PUT was held: %s", w.state())
+ }
+ w.reach(t, 400, "push released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(b))
+ w.idleStop(b)
+ w.reach(t, 20, "woken after the push", func() bool { return hasMain(b) }, func() { w.wake(b) })
+ for i := 0; i < 2; i++ {
+ w.appWrite(b)
+ w.replicate(b)
+ }
+ w.idleStop(b)
+ b.DB = nil // the disk is lost
+ w.reach(t, 20, "woken cold", func() bool { return hasMain(b) }, func() { w.wake(b) })
+ w.finish(t)
+}
+
+// wReturnLostRecord (claim rev 6.5, R6-4): a dirty rollback; the source's
+// local stamp record is lost before the return. The return CAS writes the
+// source installation's stamp back into holder.stamp, the source
+// re-initializes from it, installs the return generation under it, and its
+// probe CAS issues the new stamp, which retires it.
+func wReturnLostRecord(t *testing.T, w *world) {
+ src, tgt := w.boxes[0], w.boxes[1]
+ w.serve(src, 1, app0)
+ s := src.stampOf(1)
+ w.landProbed(t, src, tgt)
+ w.appWrite(tgt)
+ w.rollback(w.claim, "settle check failed")
+ w.reach(t, 400, "target returned", func() bool { return w.claim.Op.Phase == "returned" }, w.act(tgt))
+ src.Stamps = nil
+ w.logf("witness: box %d lost its local stamp record", src.ID)
+ w.finish(t)
+ if len(w.violations) > 0 {
+ return
+ }
+ c := w.claim
+ if c == nil || c.Holder == nil || c.Op.Exec != src.ID {
+ t.Fatalf("witness: the source does not serve after the rollback: %s", w.state())
+ }
+ act := src.stampOf(1)
+ switch {
+ case act != c.Holder.Stamp:
+ w.violate("INV-6 (witness): box %d active stamp %d, holder.stamp %d", src.ID, act, c.Holder.Stamp)
+ case src.DB == nil || src.DB.Stamp != act:
+ w.violate("INV-6 (witness): box %d database tagged %d, active %d", src.ID, dbStamp(src.DB), act)
+ case act == s || !contains(src.Stamps[1].Retired, s):
+ w.violate("INV-6 (witness): the pre-move stamp %d did not retire when %d activated on box %d", s, act, src.ID)
+ }
+}
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index ea559bddd..d28294236 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -1,7 +1,7 @@
// Package hostlife is a deterministic, randomized model of the host
// lifecycle claim (docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md,
-// rev 6.4, 697f0f9f) and Phase 1 of move-any-app
-// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 7.6).
+// rev 6.5, d36adcfa) and Phase 1 of move-any-app
+// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 7.7).
//
// Since joint round 2 the model encodes what the specs say and nothing
// stronger: restore reads the holder's location and the generation the
@@ -226,6 +226,7 @@ type request struct {
hold bool // the biased schedule holds it until its worst moment (rev 7.5: a generation marker)
by string
done bool // completed (or refused) on the server; the client may have given up long before
+ at int // when the client issued it
// result, for an immediate completion
resultVer int
}
@@ -238,7 +239,7 @@ type filesDir struct {
Gen string // .files-gen marker
Env int // admin token identity in <host>.env
Done bool // markers written last
- Stamp int // the installation stamp that produced it (claim rev 6.4 §6.3)
+ Stamp int // the installation stamp that produced it (claim rev 6.5 §6.3)
}
func (f *filesDir) clone() *filesDir {
@@ -265,7 +266,7 @@ type localDB struct {
InFlight *request // the head's upload, as the client sees it
InFlightAt int
Log []int // every write applied here, for the oracle
- Stamp int // the installation stamp that produced this artifact (claim rev 6.4 §6.3)
+ Stamp int // the installation stamp that produced this artifact (claim rev 6.5 §6.3)
Seq int
}
@@ -325,12 +326,17 @@ type box struct {
History []int // delivered history (disposable)
Attempt int // runner bookkeeping
Procs []*proc
- // Stamps is the local record per host incarnation (claim rev 6.4 §6.4,
+ // Stamps is the local record per host incarnation (claim rev 6.5 §6.4,
// R4-2): {active_stamp | none, retired_stamps}. A stamp is the claim
// gen captured at the CAS that made an installation current here. A
// writer is admitted only if its stamp equals the active one.
Stamps map[int]*stamps
Parked int // count of locally parked artifacts
+ // anchors are the level-0 anchor PUTs this box's activator has issued
+ // and not yet seen acknowledged, by key (rev 7.7, R6-1): replication
+ // opens only once one of them is done, and a request the client has
+ // waited uploadTimeout steps for is retried with the same bytes.
+ anchors map[string][]*request
ExecUntil int // local exec-lease file (watchdog input); 0 none
// in-memory, lost on crash
@@ -357,7 +363,7 @@ type plan struct {
Ver int // the config bundle version it selected
At int // it takes the guard no earlier than this
// Stamp is the installation stamp the pass read when it selected the
- // row (claim rev 6.4 §6.4, R2-3): the host guard admits the write only
+ // row (claim rev 6.5 §6.4, R2-3): the host guard admits the write only
// if it is still the active stamp.
Stamp int
}
@@ -377,7 +383,7 @@ func (b *box) stampOf(inc int) int {
return 0
}
-// install is activation (claim rev 6.4 §6.4): the box's record for inc
+// install is activation (claim rev 6.5 §6.4): the box's record for inc
// takes holder.stamp as the installing CAS wrote it (a create's serving
// CAS, a landing's flip, an adoption, a reinstall, a dirty rollback's
// probe CAS, a push's commit), or as initRecord read it fresh under the
@@ -398,20 +404,35 @@ func (b *box) install(inc, gen int) {
s.Active = gen
}
-// retireArtifacts is claim rev 6.4's retire-artifacts(S): the artifacts
-// tagged S are parked (the caller does that) and the record is untouched:
-// neither active_stamp nor retired_stamps moves. Only activation and
-// retire-installation move stamps. A landing uses it on its predecessor's
-// leftovers; a dirty rollback parks its pre-move database with S still
-// active, and S retires when the probe CAS's new stamp activates. The
-// helper exists so that every call names which retirement it is (claim
-// rev 6.4 §6.4: nothing calls retire-installation on a predecessor).
-func (b *box) retireArtifacts(inc, stamp int) {
- _ = inc
- _ = stamp
+// retireArtifacts is claim rev 6.5's retire-artifacts(S): the local
+// artifacts tagged S (the database, the files directory) are parked, and
+// the record is untouched: neither active_stamp nor retired_stamps moves.
+// Only activation and retire-installation move stamps. A landing uses it
+// on its predecessor's leftovers; a dirty rollback parks its pre-move
+// database with S still active, and S retires when the probe CAS's new
+// stamp activates. It parks by tag, as the real inventory does (R6-4): an
+// artifact of incarnation inc that carries another stamp stays, and the
+// callers assert what they expect the tags to be (INV-6).
+func (w *world) retireArtifacts(b *box, inc, stamp int) {
+ w.retireDatabase(b, inc, stamp)
+ if b.Files != nil && b.Files.Inc == inc && b.Files.Stamp == stamp {
+ b.Files = nil
+ b.Parked++
+ }
+}
+
+// retireDatabase is retire-artifacts(S) for the database alone: the files
+// directory is carried into the new generation (a push, F7 on §5.1; a
+// landing's restore phase after its files were installed; the activator's
+// park of a warm database from an earlier stay before a cold restore).
+func (w *world) retireDatabase(b *box, inc, stamp int) {
+ if b.DB != nil && b.DB.Inc == inc && b.DB.Stamp == stamp {
+ b.DB = nil
+ b.Parked++
+ }
}
-// retireStamp is claim rev 6.4's retire-installation: the active stamp
+// retireStamp is claim rev 6.5's retire-installation: the active stamp
// moves into retired_stamps and becomes none; the caller parks every
// artifact. Used at a delete, a move away, and the quarantine.
func (b *box) retireStamp(inc int) {
@@ -427,7 +448,7 @@ func (b *box) retireStamp(inc int) {
b.Stamps[inc].Active = 0
}
-// admitsStamp is the local record's admission (claim rev 6.4 §6.4): the
+// admitsStamp is the local record's admission (claim rev 6.5 §6.4): the
// writer's stamp must equal the active stamp; none active refuses all,
// and so does no record at all (R5-4: a writer is never admitted before
// initialization). The mutation of fence-stamp admits any writer for the
@@ -461,6 +482,7 @@ func (b *box) forget() {
if b.DB != nil {
b.DB.InFlight = nil // the upload's client is gone; the restarted replica uploads the same file again
}
+ b.anchors = nil // the activator issues the anchor again, the same bytes
}
// ---------- control plane ----------
@@ -478,7 +500,7 @@ type holder struct {
// current (moves rev 6 §5.1): "" is origin; a move, a push and a dirty
// rollback each install a generation named by their op id.
Gen string
- // Stamp is holder.stamp (claim rev 6.4 §2, R5-4): the gen produced by
+ // Stamp is holder.stamp (claim rev 6.5 §2, R5-4): the gen produced by
// the CAS that made the current installation current, written by that
// same CAS: a create's serving CAS, adoption, a flip, a reinstall, a
// dirty rollback's install, a push's commit. The claim is where a box
@@ -541,7 +563,8 @@ type opState struct {
BaseKey string
BaseTX int
RecVer int // a delete's or purge's intent: the record version it will DeleteIfMatch (claim §5.2 step 1, §5.3 step 4)
- FlipGen int // the holder.stamp the flip CAS wrote: the landing's installation stamp (claim rev 6.4 §6.4)
+ FlipGen int // the holder.stamp the flip CAS wrote: the landing's installation stamp (claim rev 6.5 §6.4)
+ SrcStamp int // the source installation's stamp before the flip, for the return to source (claim rev 6.5)
Committed bool
Opened bool
ParkLocalNow bool
@@ -592,7 +615,7 @@ type claim struct {
Cancelled []cancelledCreate
// readStamp is model bookkeeping on a box's read of the claim: the
// installation stamp active on that box at the read, which a worker
- // carries with the claim it validated under (claim rev 6.4 §6.4)
+ // carries with the claim it validated under (claim rev 6.5 §6.4)
readStamp int
}
@@ -669,10 +692,15 @@ type world struct {
// hold, when set, is a witness's hand on S3: a request it answers true
// for is accepted and completes only when the witness says so
// (witness_test.go). The random sweep never sets it.
- hold func(r *request) bool
- now int
- ver int
- verbose bool
+ hold func(r *request) bool
+ // stampBox records, for every installation stamp the claim issued, the
+ // box whose installation it names (claim rev 6.5: holder.stamp always
+ // names the installation op.exec should run). The oracle refuses an
+ // activation of another box's stamp (INV-6, R6-4).
+ stampBox map[int]int
+ now int
+ ver int
+ verbose bool
claim *claim // nil = absent
rec *record
@@ -748,7 +776,7 @@ func (w *world) newVer() int {
}
// nextGen is the gen the claim CAS in progress will carry: what a writer
-// captures as its installation stamp (claim rev 6.4 §6.4).
+// captures as its installation stamp (claim rev 6.5 §6.4).
func (w *world) nextGen() int {
if w.claim == nil {
return 1
@@ -850,6 +878,7 @@ func (w *world) iamCheck(actorBox int, r *request) bool {
// immediately and the client saw the answer; 0 when the client timed out
// (the request may still complete later).
func (w *world) issue(actorBox int, r *request) int {
+ r.at = w.now
if !w.iamCheck(actorBox, r) {
w.violate("IAM: box %d may not %v %s in region %d", actorBox, r.kind, r.key, r.region)
return 0