amadan

carlos / platform Public

sim: hostlife encodes exactly what the specs say (joint round 2, claim rev 4)

Joint round 2 found the model stronger than the specs. This rebuilds it on
claim rev 4 (a3c86fa5) and the moves rev 6 draft:

- restore reads holder.location and the generation the claim names, and
  replays every object of it; the start check compares markers, with the
  claim's generation as a separate rule (R2-8, R2-1)
- record-first flip, commit and rollback, with the claim half a separate
  step any actor or the recovery pass completes; exec none at stopped
- creates, purges and deletes as concurrent console plans over two
  hostnames, with app admission registration (R2-2) and cancelled creates
  (R2-7); late record PUTs
- host-guard writers as independent processes that pause before the lock
  (R2-3); door listings with O1 and O2 (R2-4); park manifests with archive
  and deletion sets (R2-6); adoption discovery of local state (N5)
- config bundle versions, pinned at admission (R2-5)
- requests that complete after H, and a straggler sweep at rest
- per-artifact local parks; the return lane under the staging lease
- a read-only final oracle: cold-restore checks of durable writes at every
  release and at the end, INV-10 at every operation's end; a disk-loss fault
- mutate.sh counts only a parsed invariant violation with a seed as CAUGHT;
  anything else is ERROR, and the sweep fails on ERROR, MISSED or STALE

State at this commit: 30,000 seeds clean; 100,000 seeds 1 failure
(seed 77725, staging residue), under investigation.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude eade8ef171ea33654fd014f820efe8f08474c53e parent df41156
9 files changed, +1288 −425
  • internal/sim/hostlife/background_test.go +52 −10
  • internal/sim/hostlife/console_test.go +317 −114
  • internal/sim/hostlife/expected-outcomes.txt +1 −0
  • internal/sim/hostlife/moves_test.go +301 −96
  • internal/sim/hostlife/mutate.sh +61 −18
  • internal/sim/hostlife/protocol_test.go +159 −98
  • internal/sim/hostlife/rules_test.go +28 −20
  • internal/sim/hostlife/sim_test.go +195 −34
  • internal/sim/hostlife/world_test.go +174 −35
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go
index 5781407ad..d8c7c0fe1 100644
--- a/internal/sim/hostlife/background_test.go
+++ b/internal/sim/hostlife/background_test.go
@@ -35,7 +35,8 @@ func (w *world) replicate(b *box) {
return
}
bl := &blob{Kind: "ltx", Inc: b.DB.Inc, Gen: b.DB.Gen, Writes: append([]int(nil), b.DB.Writes...), SealKey: b.DB.Key}
- w.issue(b.ID, &request{kind: rPut, region: b.Region, key: "instances/" + host + "/ltx", b: bl})
+ // into the location and generation the database was restored from
+ w.issue(b.ID, &request{kind: rPut, region: b.Region, key: dataKey(b.DB.Loc, b.DB.Gen, "ltx"), b: bl})
}
// idleStop: the activator's ordinary idle stop (main only; a descendant
@@ -64,7 +65,7 @@ func (w *world) wake(b *box) {
return
}
c := &claim{Holder: &holder{Inc: w.rec.Inc, App: w.rec.App, Legacy: true}}
- w.spawn(b, c, lin{}, false)
+ w.spawn(b, c, "", false)
return
}
c, ok := w.admissionClaim(b)
@@ -74,7 +75,7 @@ func (w *world) wake(b *box) {
if b.DB == nil && on("quiet-before-ack") && w.now < c.Quiet[b.Region] {
return // a first install into this region waits out quiet_after (claim §6.2a)
}
- w.spawn(b, c, holderLin(c.Holder), false)
+ w.spawn(b, c, c.Holder.Gen, false)
}
// ---------- reconcile ----------
@@ -147,7 +148,7 @@ 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},
+ n := &claim{Ver: 1, Holder: &holder{Inc: w.rec.Inc, App: w.rec.App, Legacy: true, Location: locationFor(w.rec.Inc, true)},
Op: opState{Kind: "serving", Exec: eb.ID, Parts: []int{eb.ID}}, Regions: []int{w.rec.Region}, Boxes: []int{eb.ID}, Complete: false}
if on("legacy-discovery") {
// every other region parks whatever it holds: it cannot be the
@@ -160,6 +161,13 @@ func (w *world) adopt() bool {
n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: "adopt", Kind: "park-replica", Region: r, Box: -1, Prefix: p, Ret: "legacy"})
}
}
+ // and local state on every box but the record region's serving box
+ // (claim rev 4 §9, the J2 N5 note): it cannot be the live instance's
+ for _, b := range w.liveBoxes() {
+ if b.ID != eb.ID {
+ n.Obl = append(n.Obl, obligation{ID: w.newID("ob"), Op: "adopt", Kind: "park-local", Box: b.ID, Region: -1, Ret: "legacy"})
+ }
+ }
}
w.claim = n
w.logf("adopted legacy host inc %d on box %d", w.rec.Inc, eb.ID)
@@ -216,25 +224,40 @@ func (w *world) passPlan(b *box, kind string) {
if kind == "config" && !b.HasKey {
return
}
- b.plans = append(b.plans, &plan{Kind: kind, Inc: b.Row.Inc, App: b.Row.App})
+ b.plans = append(b.plans, &plan{Kind: kind, Inc: b.Row.Inc, App: b.Row.App, Ver: w.cfgVer[b.Row.App], At: w.now + w.pauseLen()})
}
+// passExec runs one independent process's write. It needs the box running,
+// not the agent. Under the host guard (an exclusive flock shared by the
+// agent and every root command, claim rev 4 §6.4) it reads the claim
+// fresh and refuses if the incarnation, the operation or the config
+// identity it selected has moved on. The mutation keeps an in-process lock
+// only: the process acts on what it validated before it paused.
func (w *world) passExec(b *box) {
- if !w.agentUp(b) || len(b.plans) == 0 {
+ if b.Destroyed || b.Frozen || len(b.plans) == 0 {
return
}
i := w.rng.Intn(len(b.plans))
p := b.plans[i]
+ if p.At > w.now {
+ return
+ }
b.plans = append(b.plans[:i:i], b.plans[i+1:]...)
if on("hostguard") {
- c, ok := w.readClaim(b)
- if !ok || c == nil || c.Holder == nil || c.Holder.Inc != p.Inc || b.Row == nil || b.Row.Inc != p.Inc || b.Retired[p.Inc] {
+ if b.Partitioned {
+ return
+ }
+ c := w.claim
+ if c == nil || c.Holder == nil || c.Holder.Inc != p.Inc || b.Row == nil || b.Row.Inc != p.Inc || b.Retired[p.Inc] {
return
}
+ if p.Kind == "config" && p.Ver != w.cfgVer[p.App] {
+ return // the selected bundle is no longer the held one
+ }
}
switch p.Kind {
case "config":
- b.Config = p.Inc
+ b.Config, b.CfgVer = p.Inc, p.Ver
case "adopt":
b.Live, b.LiveInc = p.App, p.Inc
}
@@ -306,6 +329,7 @@ func (w *world) fault() {
}
case 1:
b.Procs = nil
+ b.plans = nil // a reboot ends every process
b.AgentDown, b.Frozen, b.AgentPaused = false, false, false
b.forget()
if !on("floor-boot-recovery") && w.rng.Intn(3) == 0 {
@@ -327,13 +351,31 @@ func (w *world) fault() {
}
case 5:
c := w.claim
- if w.fail["destroy"] && c != nil && (c.Op.Kind == "landing" || c.Op.Kind == "restoring") && !c.Op.Committed && b.ID == c.Op.Tgt {
+ committed := c != nil && (c.Op.Committed || w.rec != nil && w.rec.MoveID == c.Op.ID && w.rec.MoveState == "committed")
+ if w.fail["destroy"] && c != nil && (c.Op.Kind == "landing" || c.Op.Kind == "restoring") && !committed && b.ID == c.Op.Tgt {
b.Destroyed = true
b.Procs = nil
w.logf("box %d destroyed", b.ID)
}
case 6:
w.console = nil // console crash: plans dropped
+ case 7:
+ // the serving box loses its database file while the app is idle: the
+ // next wake restores cold. Writes after the last completed
+ // checkpoint are lost by design (the RPO), and declared so; every
+ // durable write must come back (§14.2.3).
+ c := w.claim
+ if w.fail["disk"] && c != nil && c.Holder != nil && c.Op.Kind == "serving" && c.Op.Exec == b.ID && b.DB != nil && !hasMain(b) && len(b.Procs) == 0 {
+ for i := range w.acks {
+ a := &w.acks[i]
+ if a.Box == b.ID && a.Inc == b.DB.Inc && !w.isDurable(a.W) {
+ a.Exempt = true
+ }
+ }
+ b.DB = nil
+ w.stats["disk-lost"]++
+ w.logf("box %d lost its database file", b.ID)
+ }
default:
w.completeDue(false)
}
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index f89eb43fe..1a403c781 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -6,18 +6,29 @@ import "fmt"
// every plan; the claim-recovery pass must then finish or undo the work
// from the claim alone (claim C2).
type consolePlan struct {
- Kind string // create, delete, purge
- Step int
- App string
- OpID string
+ Kind string // create, delete, purge
+ Step int
+ App string
+ OpID string
+ Host string // "h" or "h2" for a create
+ Inc int
+ Region int
}
+// doorPlan is one pull-door listing (claim rev 4 §6.5): O1 is the claim
+// read it authorized against; it selects versions under O1's location after
+// a pause, reads the claim again (O2), and only then signs handles, which a
+// file request opens after another pause.
type doorPlan struct {
Region int
+ Loc string
+ Gen string
+ Inc int // O1's holder incarnation
+ OpID string // O1's op
Key string
Ver int
- Inc int
- Until int // a stalled read may resume until then (one in four stall long)
+ Signed bool
+ Until int // a stalled step may resume until then (one in four stall long)
}
func (w *world) execBox(c *claim) *box {
@@ -27,8 +38,10 @@ func (w *world) execBox(c *claim) *box {
return w.boxByID(c.Op.Exec)
}
-// fixRecord converges the record's region and move id to the claim. It is
-// the record half of every flip, release and recovery (claim C2).
+// fixRecord is the recovery owner for the record halves of a move (claim
+// C2): the request's `move` field after the claim's intent; the claim half
+// of a record-first transition (followRecord); and, after a release, the
+// CAS that clears `move` and names the executor's region (§7.9 step 5).
func (w *world) fixRecord() {
c := w.claim
if c == nil || c.Holder == nil || w.rec == nil || w.rec.Inc != c.Holder.Inc {
@@ -36,17 +49,17 @@ func (w *world) fixRecord() {
}
switch c.Op.Kind {
case "serving":
- if b := w.execBox(c); b != nil {
- w.rec.Region = b.Region
+ if b := w.execBox(c); b != nil && (w.rec.MoveID != "" || w.rec.Region != b.Region) {
+ w.rec.Region, w.rec.MoveID, w.rec.MoveState, w.rec.RollbackID = b.Region, "", "", ""
+ w.rec.Ver++
+ }
+ case "moving":
+ if w.rec.MoveID == "" {
+ w.rec.MoveID, w.rec.MoveState = c.Op.ID, ""
+ w.rec.Ver++
}
- w.rec.MoveID = ""
- case "moving", "reverting":
- w.rec.Region, w.rec.MoveID = c.Op.SrcRegion, c.Op.ID
- case "landing":
- w.rec.Region, w.rec.MoveID = c.Op.TgtRegion, c.Op.ID
- case "restoring":
- w.rec.Region, w.rec.MoveID = c.Op.SrcRegion, c.Op.ID
}
+ w.followRecord(c)
}
func (w *world) liveBoxes() []*box {
@@ -61,26 +74,30 @@ func (w *world) liveBoxes() []*box {
// ---------- user operations ----------
+// userCreate starts a create as a console plan: registration, the claim
+// CAS, the record and serving are separate steps on separate objects, and
+// the console may pause or crash between any two (J2-R2-2, J2-R2-7).
func (w *world) userCreate() {
- c := w.claim
- if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) {
- return
- }
- if w.rec != nil {
- return
- }
app := app0
if w.rng.Intn(2) == 0 {
app = app1
}
- if w.purgeRes[app] {
+ if w.rng.Intn(3) == 0 {
+ if w.h2.Kind != "" {
+ return
+ }
+ w.nextInc++
+ w.console = append(w.console, &consolePlan{Kind: "create", Host: "h2", App: app, OpID: w.newID("cr"), Inc: w.nextInc})
return
}
- r := w.rng.Intn(nRegions)
- b := w.regionBox(r)
- if b == nil || (c != nil && contains(c.Lost, b.ID)) {
+ c := w.claim
+ if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) {
return
}
+ if w.rec != nil || w.recPend != nil {
+ return
+ }
+ r := w.rng.Intn(nRegions)
var inc int
if on("fresh-incarnation") || c == nil || len(c.Retired) == 0 {
w.nextInc++
@@ -88,20 +105,134 @@ func (w *world) userCreate() {
} else {
inc = c.Retired[len(c.Retired)-1] // a caller-supplied CreatedAt repeats an identity
}
- if on("fresh-incarnation") && c != nil && contains(c.Retired, inc) {
- return
- }
- w.serial++
- id := w.newID("cr")
- if w.cas(c, func(n *claim) bool {
- n.Holder = &holder{Inc: inc, App: app, Serial: w.serial}
- n.Op = opState{Kind: "creating", ID: id, Exec: -1, NewInc: inc, NewApp: app, NewRegion: r, ReqAt: w.now}
- n.Regions, n.Boxes, n.Complete, n.Obl = []int{r}, []int{b.ID}, true, nil
+ w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app, OpID: w.newID("cr"), Inc: inc, Region: r})
+}
+
+func (w *world) createSteps(p *consolePlan) bool {
+ ad := w.admit[p.App]
+ abandon := func() bool {
+ delete(ad.Reg, p.OpID)
return true
- }) {
- w.stores[app] = true
- w.console = append(w.console, &consolePlan{Kind: "create", OpID: id})
- w.logf("create %s inc %d app %s in region %d", id, inc, app, r)
+ }
+ switch p.Step {
+ case 0:
+ // app admission (claim rev 4 §5.1 step 0): register while open.
+ // The mutation is rev 3's check of the purge reservation, a read of
+ // another object than the claim the create then writes.
+ if on("admission-registration") {
+ if ad.Closed {
+ return true
+ }
+ ad.Reg[p.OpID] = regEntry{Host: p.Host, Until: w.now + 60}
+ w.logf("create %s registered for app %s (%s)", p.OpID, p.App, p.Host)
+ } else if w.purgeRes[p.App] {
+ return true
+ }
+ w.stores[p.App] = true // the app exists, or exists again after a purge
+ p.Step = 1
+ return false
+ case 1:
+ if e, ok := ad.Reg[p.OpID]; on("admission-registration") && on("registration-recovery") && (!ok || w.now > e.Until-maxPause) {
+ return abandon() // the registration lease ended before the claim CAS
+ }
+ if p.Host == "h2" {
+ if w.h2.Kind != "" {
+ return abandon()
+ }
+ w.h2 = liteHost{Inc: p.Inc, App: p.App, Kind: "creating", OpID: p.OpID, At: w.now}
+ w.logf("create %s: second host claimed for app %s", p.OpID, p.App)
+ p.Step = 2
+ return false
+ }
+ c := w.claim
+ if c != nil && (c.Holder != nil || (c.Op.Kind != "" && c.Op.Kind != "serving")) || w.rec != nil || w.recPend != nil {
+ return abandon()
+ }
+ b := w.regionBox(p.Region)
+ if b == nil || (c != nil && contains(c.Lost, b.ID)) {
+ return abandon()
+ }
+ if on("fresh-incarnation") && c != nil && contains(c.Retired, p.Inc) {
+ return abandon()
+ }
+ w.serial++
+ if !w.cas(c, func(n *claim) bool {
+ n.Holder = &holder{Inc: p.Inc, App: p.App, Serial: w.serial, Location: locationFor(p.Inc, false)}
+ n.Op = opState{Kind: "creating", ID: p.OpID, Exec: -1, NewInc: p.Inc, NewApp: p.App, NewRegion: p.Region, ReqAt: w.now}
+ n.Regions, n.Boxes, n.Complete, n.Obl = []int{p.Region}, []int{b.ID}, true, nil
+ return true
+ }) {
+ return abandon()
+ }
+ w.logf("create %s inc %d app %s in region %d", p.OpID, p.Inc, p.App, p.Region)
+ p.Step = 2
+ return false
+ case 2:
+ if p.Host == "h2" {
+ if w.h2.OpID != p.OpID || w.h2.Kind != "creating" {
+ return abandon()
+ }
+ w.h2.Rec = true
+ p.Step = 3
+ return false
+ }
+ c := w.claim
+ if c == nil || c.Op.ID != p.OpID || c.Op.Kind != "creating" {
+ return abandon()
+ }
+ if w.rec == nil && w.recPend == nil {
+ rec := &record{Inc: c.Holder.Inc, App: c.Holder.App, Region: c.Op.NewRegion}
+ switch n := w.rng.Intn(10); {
+ case n < 7:
+ w.rec = rec
+ case n < 9:
+ // the response is lost and the PUT lands later, rarely after
+ // cancelled_creates' window
+ at := w.now + 1 + w.rng.Intn(2*horizonH)
+ if w.rng.Intn(beyondH) == 0 {
+ at = w.now + 4*horizonH + w.rng.Intn(10*horizonH)
+ }
+ w.recPend = &pendingRec{rec: rec, at: at}
+ }
+ // otherwise it failed outright; the next step retries
+ }
+ p.Step = 3
+ return false
+ default:
+ if p.Host == "h2" {
+ if w.h2.OpID != p.OpID || w.h2.Kind != "creating" {
+ return abandon()
+ }
+ w.h2.Kind = "serving" // a CAS from creating, like the main host's
+ w.logf("create %s: second host serving", p.OpID)
+ delete(ad.Reg, p.OpID)
+ return true
+ }
+ c := w.claim
+ if c == nil || c.Op.ID != p.OpID || c.Op.Kind != "creating" {
+ return abandon()
+ }
+ if w.rec == nil || w.rec.Inc != c.Holder.Inc {
+ if w.rec == nil && w.recPend == nil {
+ p.Step = 2 // publish again
+ }
+ return false
+ }
+ b := w.regionBox(c.Op.NewRegion)
+ if b == nil {
+ return false
+ }
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, p.OpID) {
+ return false
+ }
+ n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}}
+ return true
+ }) {
+ delete(ad.Reg, p.OpID)
+ return true
+ }
+ return false
}
}
@@ -156,7 +287,6 @@ func (w *world) userMove() {
Src: src.ID, Tgt: tgt.ID, SrcRegion: src.Region, TgtRegion: r, ReqAt: w.now, Auto: true, App: c.Holder.App}
return true
}) {
- w.fixRecord()
w.logf("move %s inc %d from box %d to box %d", id, c.Holder.Inc, src.ID, tgt.ID)
}
}
@@ -230,15 +360,15 @@ func (w *world) parkingObligations(n *claim, inc int) {
n.Retired = addUniq(n.Retired, inc)
}
-// consoleStep runs the next step of the oldest console plan.
+// consoleStep runs the next step of one console plan, chosen at random:
+// the console's requests run concurrently.
func (w *world) consoleStep() {
if len(w.console) == 0 {
return
}
- p := w.console[0]
- done := w.runPlan(p)
- if done {
- w.console = w.console[1:]
+ i := w.rng.Intn(len(w.console))
+ if w.runPlan(w.console[i]) {
+ w.console = append(w.console[:i:i], w.console[i+1:]...)
}
}
@@ -246,28 +376,7 @@ func (w *world) runPlan(p *consolePlan) bool {
c := w.claim
switch p.Kind {
case "create":
- if c == nil || c.Op.ID != p.OpID || c.Op.Kind != "creating" {
- return true
- }
- if p.Step == 0 {
- if w.rec == nil {
- w.rec = &record{Inc: c.Holder.Inc, App: c.Holder.App, Region: c.Op.NewRegion}
- }
- p.Step = 1
- return false
- }
- b := w.regionBox(c.Op.NewRegion)
- if b == nil {
- return false
- }
- w.cas(c, func(n *claim) bool {
- if !sameOp(n.Op.ID, p.OpID) {
- return false
- }
- n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}}
- return true
- })
- return true
+ return w.createSteps(p)
case "delete":
if c == nil || c.Op.ID != p.OpID {
return true
@@ -325,6 +434,9 @@ func (w *world) free(c *claim) {
}) {
w.logf("host freed")
w.opsDone++
+ if r := w.residueAtEnd(); len(r) > 0 {
+ w.violate("INV-10: the host was freed with residue %v", r)
+ }
w.stats["freed"]++
if w.purgeRes[app] && !on("purge-journal") {
w.purgeRes[app] = false // freeing the host drops the reservation
@@ -372,36 +484,78 @@ func (w *world) purgeSteps(p *consolePlan) bool {
}
}()
}
+ ad := w.admit[p.App]
switch p.Step {
case 0:
if on("purge-reserve-first") {
reserve()
- p.Step = 1
} else {
w.stores[p.App] = false // tear down first
- p.Step = 1
}
+ p.Step = 1
return false
case 1:
- if !claimIt() {
- return false
+ // close admission (claim rev 4 §5.3 step 1b), so no new create can
+ // register
+ if on("admission-registration") {
+ ad.Closed = true
+ w.logf("purge %s: admission closed", p.App)
}
p.Step = 2
return false
case 2:
+ // drain: every registered create reaches serving or is cancelled
+ // before the host set is fixed; an expired registration is dead
+ if on("admission-registration") {
+ for id, e := range ad.Reg {
+ // an expired registration whose host's claim does not name
+ // its create is dead: the create checks the expiry right
+ // before its claim CAS, so it can no longer claim (CC16)
+ claimed := e.Host == "h2" && w.h2.OpID == id && w.h2.Kind == "creating" ||
+ e.Host == "h" && w.claim != nil && w.claim.Op.ID == id && w.claim.Op.Kind == "creating"
+ if on("registration-recovery") && w.now > e.Until && !claimed {
+ delete(ad.Reg, id)
+ continue
+ }
+ return false
+ }
+ }
+ p.Step = 3
+ return false
+ case 3:
+ // the host set: records, plus registered in-flight creates (drained
+ // above). A second host the purge cannot see is not in it.
+ if !claimIt() {
+ return false
+ }
+ if w.h2.App == p.App && w.h2.Rec {
+ switch w.h2.Kind {
+ case "serving":
+ w.h2.Kind = "purging"
+ case "purging":
+ default:
+ return false
+ }
+ }
+ p.Step = 4
+ return false
+ case 4:
if on("purge-reserve-first") {
+ w.logf("purge %s: store torn down", p.App)
w.stores[p.App] = false
} else {
reserve()
}
- p.Step = 3
+ p.Step = 5
return false
default:
+ if w.h2.App == p.App && w.h2.Kind == "purging" {
+ w.h2 = liteHost{} // record deleted, claim freed
+ }
if c == nil || c.Holder == nil || c.Holder.App != p.App {
- if c == nil || c.Holder == nil {
- w.purgeRes[p.App] = false
- delete(w.purgeStep, p.App)
- }
+ w.purgeRes[p.App] = false
+ delete(w.purgeStep, p.App)
+ ad.Closed = false // the purge's completion reopens admission
return true
}
w.deleteSteps(c)
@@ -434,7 +588,7 @@ func (w *world) resumePurges() {
// ---------- the door (claim §6.5) ----------
func (w *world) doorAuthorize() {
- c := w.claim
+ c := w.claim // O1
if c == nil || c.Holder == nil || c.Op.Kind != "serving" {
return
}
@@ -442,33 +596,21 @@ func (w *world) doorAuthorize() {
if b == nil {
return
}
- bk := w.buckets[b.Region]
- key := "instances/" + host + "/ltx"
- d := &doorPlan{Region: b.Region, Key: key, Inc: c.Holder.Inc, Until: w.now + 1 + w.pauseLen()}
- if on("door-by-version") {
- for _, v := range bk.objs[key] {
- if !v.Marker && v.B.Inc == c.Holder.Inc {
- d.Ver = v.ID
- }
- }
- if d.Ver == 0 {
- return
- }
- }
- w.doorReads = append(w.doorReads, d)
+ w.doorReads = append(w.doorReads, &doorPlan{Region: b.Region, Loc: c.Holder.Location, Gen: c.Holder.Gen, Inc: c.Holder.Inc, OpID: c.Op.ID,
+ Key: dataKey(c.Holder.Location, c.Holder.Gen, "ltx"), Until: w.now + 1 + w.pauseLen()})
}
+// doorOpen advances one stalled listing or file request. A stalled step
+// resumes at its worst moment if one comes before its stall ends: when the
+// claim's holder has changed since O1. Otherwise it waits out its stall.
func (w *world) doorOpen() {
if len(w.doorReads) == 0 {
return
}
i := w.rng.Intn(len(w.doorReads))
- // a stalled read resumes at its worst moment if one comes before its
- // stall ends: when its location's current object belongs to another
- // incarnation. Otherwise it waits out its stall.
worst := -1
for j, d := range w.doorReads {
- if cur := w.buckets[d.Region].current(d.Key); cur != nil && !cur.Marker && cur.B.Inc != 0 && cur.B.Inc != d.Inc {
+ if c := w.claim; c == nil || c.Holder == nil || c.Holder.Inc != d.Inc {
worst = j
break
}
@@ -480,8 +622,26 @@ func (w *world) doorOpen() {
return
}
d := w.doorReads[i]
- w.doorReads = append(w.doorReads[:i:i], w.doorReads[i+1:]...)
bk := w.buckets[d.Region]
+ if !d.Signed {
+ // select versions only under O1's location (step 3)
+ if on("door-by-version") {
+ v := bk.current(d.Key)
+ if v == nil {
+ w.doorReads = append(w.doorReads[:i:i], w.doorReads[i+1:]...)
+ return
+ }
+ d.Ver = v.ID
+ }
+ // O2: refuse if the holder or the op changed since O1 (step 5)
+ if c := w.claim; on("door-reread") && (c == nil || c.Holder == nil || c.Holder.Inc != d.Inc || c.Op.ID != d.OpID) {
+ w.doorReads = append(w.doorReads[:i:i], w.doorReads[i+1:]...)
+ return
+ }
+ d.Signed, d.Until = true, w.now+1+w.pauseLen()
+ return
+ }
+ w.doorReads = append(w.doorReads[:i:i], w.doorReads[i+1:]...)
var v *version
if d.Ver != 0 {
v = bk.byID(d.Key, d.Ver)
@@ -500,15 +660,41 @@ func (w *world) recoveryPass() {
return
}
w.resumePurges()
+ // the second host's create (control plane only)
+ if h := w.h2; h.Kind == "creating" && w.now-h.At >= 15 {
+ if h.Rec {
+ w.h2.Kind = "serving"
+ } else {
+ w.h2 = liteHost{}
+ }
+ w.logf("recovery: second host's create %s -> %q", h.OpID, w.h2.Kind)
+ delete(w.admit[h.App].Reg, h.OpID)
+ }
c := w.claim
if c == nil {
return
}
- // an orphan record: the claim is free or names someone else
- if w.rec != nil && (c.Holder == nil || c.Holder.Inc != w.rec.Inc) && c.Op.Kind != "creating" {
- w.logf("recovery: removing orphan record inc %d", w.rec.Inc)
- w.rec = nil
- return
+ // a late record PUT from a cancelled create: an orphan, never admitted
+ // (C1); DeleteIfMatch when cancelled_creates names its incarnation
+ // (claim rev 4 §5.1, J2-R2-7)
+ if w.rec != nil && (c.Holder == nil || c.Holder.Inc != w.rec.Inc) && c.Op.Kind != "creating" && on("cancelled-creates") {
+ orphan := false
+ for _, x := range c.Cancelled {
+ if x.Inc == w.rec.Inc && w.now <= x.Until {
+ orphan = true
+ }
+ }
+ // CC17: a record PUT has no completion bound either (C3a's
+ // lesson), so `until` cannot close the window. A record whose
+ // incarnation is retired is an orphan whenever it lands.
+ if on("orphan-no-deadline") && contains(c.Retired, w.rec.Inc) {
+ orphan = true
+ }
+ if orphan {
+ w.logf("recovery: removing a cancelled create's late record inc %d", w.rec.Inc)
+ w.rec = nil
+ return
+ }
}
switch c.Op.Kind {
case "creating":
@@ -520,22 +706,32 @@ func (w *world) recoveryPass() {
if b == nil {
return
}
- w.cas(c, func(n *claim) bool {
+ if w.cas(c, func(n *claim) bool {
if !sameOp(n.Op.ID, c.Op.ID) {
return false
}
n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}}
return true
- })
+ }) {
+ delete(w.admit[c.Holder.App].Reg, c.Op.ID)
+ }
} else if w.rec == nil {
- w.cas(c, func(n *claim) bool {
- if !sameOp(n.Op.ID, c.Op.ID) {
+ // authoritatively absent: cancel, retiring the incarnation and
+ // remembering it, so a late record PUT can be removed
+ inc, app, id := c.Holder.Inc, c.Holder.App, c.Op.ID
+ if w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, id) {
return false
}
n.Holder, n.Op = nil, opState{}
n.Regions, n.Boxes = nil, nil
+ n.Retired = addUniq(n.Retired, inc)
+ n.Cancelled = append(n.Cancelled, cancelledCreate{Inc: inc, Until: w.now + 4*horizonH})
return true
- })
+ }) {
+ delete(w.admit[app].Reg, id)
+ w.logf("recovery: cancelled create %s inc %d", id, inc)
+ }
}
case "deleting", "parking":
if w.now-c.Op.ReqAt < 15 {
@@ -633,14 +829,22 @@ func (w *world) operator() {
if !ok {
return
}
+ if op.Kind == "landing" {
+ // it proceeds as a rollback, record first (§7.8, §7.10); the
+ // claim follows, and the loss is applied to the restoring claim on
+ // the operator's next call
+ if w.rec != nil && w.rec.MoveID == op.ID && w.rec.MoveState == "landing" {
+ w.rollback(c, "declared lost")
+ } else {
+ w.followRecord(c)
+ }
+ return
+ }
if w.cas(c, func(n *claim) bool {
- if !sameOp(n.Op.ID, op.ID) || n.Op.Committed {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Committed || n.Op.Kind != "restoring" {
return false
}
n.Lost = addUniq(n.Lost, t.ID)
- if n.Op.Kind == "landing" {
- n.Op.Kind, n.Op.RollbackID, n.Op.SrcPhase = "restoring", w.newID("rb"), "waiting"
- }
n.Op.Exec, n.Op.DirtyKnown, n.Op.Dirty, n.Op.Phase, n.Op.LostBox, n.Op.LostAt = -1, true, false, "released", t.ID, w.now
var keep []obligation
for _, o := range n.Obl {
@@ -652,7 +856,7 @@ func (w *world) operator() {
n.Obl = keep
if owesEvidence { // a box that released already queued these
n.Obl = append(n.Obl,
- w.newObl(n, "park-superseded", op.TgtRegion, -1, "instances/"+host+"/", "", w.now+horizonH),
+ w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", w.now+horizonH),
w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))
}
return true
@@ -663,6 +867,5 @@ func (w *world) operator() {
}
}
w.logf("operator declared box %d lost for %s", t.ID, op.ID)
- w.fixRecord()
}
}
diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt
new file mode 100644
index 000000000..1cab9ebd4
--- /dev/null
+++ b/internal/sim/hostlife/expected-outcomes.txt
@@ -0,0 +1 @@
+# rule outcome reason (see mutate.sh)
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index c0ea5c7c1..e23df1460 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -1,6 +1,9 @@
package hostlife
-import "fmt"
+import (
+ "fmt"
+ "strings"
+)
// worker is one box agent's lifecycle worker: exec-lease renewal, the
// obligations it owns, then its role in the current operation. One call
@@ -30,6 +33,7 @@ func (w *world) workerMode(b *box, obl bool) {
return
}
}
+ w.sweep(b, c)
return
}
if b.stale != nil && w.rng.Intn(6) == 0 {
@@ -63,8 +67,9 @@ func (w *world) workerMode(b *box, obl bool) {
if b.DB != nil {
inc = b.DB.Inc
}
- w.localPark(b, inc)
- b.Row = nil
+ if w.localPark(b, inc) {
+ b.Row = nil
+ }
}
}
return
@@ -117,13 +122,19 @@ func (w *world) leasesSeen(c *claim) bool {
return true
}
-// stagingLease: the shared staging-work lease (claim C3), per target region.
+// stagingLease: the shared staging-work lease (claim C3), per destination
+// region: the target's for a move's staging, the source's for a dirty
+// rollback's return lane.
func (w *world) takeStaging(c *claim, b *box) bool {
- l := w.staging[c.Op.TgtRegion]
- if l.Op != "" && l.Op != c.Op.ID && l.Until >= w.now {
+ return w.takeStagingFor(c.Op.TgtRegion, c.Op.ID, b)
+}
+
+func (w *world) takeStagingFor(region int, opID string, b *box) bool {
+ l := w.staging[region]
+ if l.Op != "" && l.Op != opID && l.Until >= w.now {
return false
}
- w.staging[c.Op.TgtRegion] = stagingLease{Op: c.Op.ID, Box: b.ID, Until: w.now + stagingTTL}
+ w.staging[region] = stagingLease{Op: opID, Box: b.ID, Until: w.now + stagingTTL}
return true
}
@@ -133,11 +144,23 @@ type stagingLease struct {
Until int
}
+// snapshotBlob is a staging round: the source's final checkpoint over its
+// replica, which is what the mirror copies (§7.3). With no local database
+// (a lost disk, or never woken) it is the replica alone.
func (w *world) snapshotBlob(b *box, c *claim) (*blob, *blob) {
+ return w.snapshotBlobOf(b, c, c.Holder.Gen)
+}
+
+func (w *world) snapshotBlobOf(b *box, c *claim, gen string) (*blob, *blob) {
db := &blob{Kind: "snap", Inc: c.Holder.Inc}
+ if r := w.restore(b, c.Holder.Inc, c.Holder.Location, gen); r != nil {
+ db.Writes, db.SealKey = r.Writes, r.Key
+ }
if b.DB != nil {
- db.Writes = append([]int(nil), b.DB.Writes...)
- db.SealKey = b.DB.Key
+ db.Writes = unionInts(db.Writes, b.DB.Writes)
+ if b.DB.Key != 0 {
+ db.SealKey = b.DB.Key
+ }
db.Inc = b.DB.Inc
}
files := &blob{Kind: "files", Inc: c.Holder.Inc, Files: b.Files.clone(), Timers: append([]int(nil), b.Timers...)}
@@ -148,6 +171,12 @@ func (w *world) moveSource(b *box, c *claim) {
op := c.Op
switch op.Phase {
case "leases":
+ if w.rec != nil && w.rec.Inc == c.Holder.Inc && w.rec.MoveID == "" {
+ // the record half of the request, after the claim's intent (C2):
+ // a crash between is finished here or by the recovery pass
+ w.rec.MoveID, w.rec.MoveState = op.ID, ""
+ return
+ }
if w.leasesSeen(c) {
w.cas(c, func(n *claim) bool { n.Op.Phase = "preparing"; return sameOp(n.Op.ID, op.ID) })
}
@@ -159,15 +188,20 @@ func (w *world) moveSource(b *box, c *claim) {
srcReady := !on("source-readiness") || (b.Config == c.Holder.Inc && b.Live == c.Holder.App && b.LiveInc == c.Holder.Inc && b.HasKey)
if op.Phase == "ready" && op.ReportOK && w.now-op.ReportAt < 60 && op.Auto && srcReady {
// auto-cut: admission is atomic with abort eligibility
+ if w.rec == nil || w.rec.MoveID != op.ID {
+ return
+ }
+ deadline := w.now + cutBudget
+ if !on("cut-deadline") {
+ deadline = 1 << 30
+ }
w.cas(c, func(n *claim) bool {
if !sameOp(n.Op.ID, op.ID) || n.Op.CutAt != 0 || n.Op.Kind != "moving" {
return false
}
n.Op.CutAt = w.now
- n.Op.CutDeadline = w.now + cutBudget
- if !on("cut-deadline") {
- n.Op.CutDeadline = 1 << 30
- }
+ n.Op.CutDeadline = deadline
+ n.Op.PinVer = w.cfgVer[c.Holder.App] // move.inputs, pinned at admission
n.Op.Phase = "stopping"
return true
})
@@ -228,6 +262,7 @@ func (w *world) moveSource(b *box, c *claim) {
}
n.Op.Phase, n.Op.StopAt, n.Op.StopDigest, n.Op.StopFiles = "stopped", w.now, d, files
n.Op.Repl, n.Op.Next = repl, next
+ n.Op.Exec = -1 // K3: the source gives up execution, citing its evidence
return true
})
case "stopped":
@@ -269,15 +304,18 @@ func (w *world) moveSource(b *box, c *claim) {
})
}
case "sealed":
- // the flip: kind and exec move together, citing the source's evidence
- if w.cas(c, func(n *claim) bool {
- if !sameOp(n.Op.ID, op.ID) || n.Op.Phase != "sealed" || n.Op.StopAt == 0 {
- return false
- }
- n.Op.Kind, n.Op.Exec, n.Op.LandPhase, n.Op.FlipAt = "landing", op.Tgt, "checking", w.now
- return true
- }) {
- w.fixRecord()
+ // the flip, record first (§7.5): one CAS on the record, then the
+ // claim follows on a later step. A crash between leaves nobody
+ // with execution, which is safe; whoever next sees the record
+ // completes the claim (rev 6 §19 K4).
+ if w.rec != nil && w.rec.Inc == c.Holder.Inc && w.rec.MoveID == op.ID && w.rec.MoveState == "landing" {
+ w.followRecord(c)
+ return
+ }
+ if w.rec != nil && w.rec.Inc == c.Holder.Inc && w.rec.MoveID == op.ID && w.rec.MoveState == "" && op.StopAt != 0 {
+ w.rec.Region, w.rec.MoveState = op.TgtRegion, "landing"
+ w.rec.Ver++
+ w.logf("flip %s: record names region %d", op.ID, op.TgtRegion)
}
}
}
@@ -399,19 +437,24 @@ func (w *world) pauseSign() int { return w.rng.Intn(2*stagingTTL + horizonH + 1)
// staging round: the first attempt's goroutine paused before signing and
// the agent retried. The paused attempt may sign after the seal.
func (w *world) maybeStallDuplicate(b *box, op opState, r *request) {
+ w.maybeStallDuplicateFor(b, op.TgtRegion, r)
+}
+
+func (w *world) maybeStallDuplicateFor(b *box, region int, r *request) {
if w.rng.Intn(3) != 0 {
return
}
dup := *r
- w.stalled = append(w.stalled, &stalledSign{box: b.ID, epoch: b.Epoch, req: &dup, signAt: w.now + w.pauseSign(), until: w.staging[op.TgtRegion].Until})
+ w.stalled = append(w.stalled, &stalledSign{box: b.ID, epoch: b.Epoch, req: &dup, signAt: w.now + w.pauseSign(), until: w.staging[region].Until})
}
type stalledSign struct {
- box int
- epoch int
- req *request
- signAt int
- until int
+ box int
+ epoch int
+ req *request
+ signAt int
+ until int
+ checked bool // passed its SafeUntil check, not yet signed
}
// runStalled lets paused goroutines resume: deferred registry writes and
@@ -427,10 +470,18 @@ func (w *world) runStalled() {
keep = append(keep, s)
continue
}
- if on("sign-before-safeuntil") && w.localNow(b) > s.until-maxSkew {
+ if s.checked {
+ w.issue(b.ID, s.req) // signs, at most maxPause after the check
+ continue
+ }
+ if on("sign-before-safeuntil") && w.localNow(b) > s.until-maxSkew-maxPause {
continue // checked SafeUntil immediately before signing: too late
}
- w.issue(b.ID, s.req)
+ // the check passed; the goroutine may still pause before the
+ // signature, within the claim's §3.1 bound, which SafeUntil's
+ // margin covers
+ s.checked, s.signAt = true, w.now+w.rng.Intn(maxPause+1)
+ keep = append(keep, s)
}
w.stalled = keep
for _, b := range w.boxes {
@@ -495,9 +546,9 @@ func (w *world) revertSource(b *box, c *claim) {
return
}
if b.HasKey { // RenderHeld + MaterializeHeld before every probe
- b.Config, b.Live, b.LiveInc = c.Holder.Inc, c.Holder.App, c.Holder.Inc
+ b.Config, b.CfgVer, b.Live, b.LiveInc = c.Holder.Inc, w.cfgVer[c.Holder.App], c.Holder.App, c.Holder.Inc
}
- if hasMain(b) || w.spawn(b, c, holderLin(c.Holder), true) {
+ if hasMain(b) || w.spawn(b, c, c.Holder.Gen, true) {
w.cas(c, func(n *claim) bool { n.Op.RevPhase = "probed"; return sameOp(n.Op.ID, op.ID) })
return
}
@@ -525,20 +576,71 @@ func (w *world) holdSourceRow(b *box, c *claim) {
}
}
+// rollback is record first (§7.8): one CAS on the record, landing →
+// rolling_back, guarded by move id. The commit is a CAS on the same record
+// field, so exactly one of them wins. The claim follows on a later step.
func (w *world) rollback(c *claim, why string) {
op := c.Op
- if w.cas(c, func(n *claim) bool {
- if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "landing" || n.Op.Committed {
- return false
- }
- n.Op.Kind, n.Op.RollbackID, n.Op.SrcPhase, n.Op.Phase = "restoring", w.newID("rb"), "waiting", "releasing"
- n.Op.Reason = why
- return true
- }) {
- w.logf("rollback %s: %s", op.ID, why)
- w.stats["why: "+why+" @"+op.LandPhase]++
- w.fixRecord()
+ r := w.rec
+ if r == nil || r.Inc != c.Holder.Inc || r.MoveID != op.ID || r.MoveState != "landing" {
+ return
+ }
+ r.MoveState, r.Region, r.RollbackID, r.Reason = "rolling_back", op.SrcRegion, w.newID("rb"), why
+ r.Ver++
+ w.logf("rollback %s: %s", op.ID, why)
+ w.stats["why: "+why+" @"+op.LandPhase]++
+}
+
+// followRecord completes the claim half of a record transition the claim
+// has not caught up with: the flip, the commit, a rollback. Any actor that
+// reads both may do it (rev 6 §19 K4): the CAS is fully determined by the
+// record and is conditional on the op id and the claim's prior state.
+func (w *world) followRecord(c *claim) bool {
+ r := w.rec
+ if c == nil || c.Holder == nil || r == nil || r.Inc != c.Holder.Inc || r.MoveID == "" || r.MoveID != c.Op.ID {
+ return false
+ }
+ op := c.Op
+ switch {
+ case r.MoveState == "landing" && op.Kind == "moving" && op.Phase == "sealed":
+ return w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "moving" || n.Op.Phase != "sealed" {
+ return false
+ }
+ n.Op.Kind, n.Op.Exec, n.Op.LandPhase, n.Op.FlipAt = "landing", op.Tgt, "checking", w.now
+ return true
+ })
+ case r.MoveState == "committed" && op.Kind == "landing" && !op.Committed:
+ return w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "landing" || n.Op.Committed {
+ return false
+ }
+ n.Op.Committed = true
+ w.newGen(n.Holder.Location, n.Holder.Gen, op.ID)
+ n.Holder.Gen = op.ID // the claim names the generation restore reads (C3a)
+ q := op.StopAt + horizonH
+ if !on("quiet-before-ack") {
+ q = 0
+ }
+ n.Obl = append(n.Obl,
+ w.newObl(n, "park-superseded", op.SrcRegion, -1, c.Holder.Location, "", q),
+ w.newObl(n, "park-local", -1, op.Src, "", "", 0),
+ w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))
+ if q > n.Quiet[op.SrcRegion] {
+ n.Quiet[op.SrcRegion] = q
+ }
+ return true
+ })
+ case r.MoveState == "rolling_back" && op.Kind == "landing":
+ return w.cas(c, func(n *claim) bool {
+ if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "landing" || n.Op.Committed {
+ return false
+ }
+ n.Op.Kind, n.Op.RollbackID, n.Op.SrcPhase, n.Op.Phase, n.Op.Reason = "restoring", r.RollbackID, "waiting", "releasing", r.Reason
+ return true
+ })
}
+ return false
}
func (w *world) landTarget(b *box, c *claim) {
@@ -546,7 +648,12 @@ func (w *world) landTarget(b *box, c *claim) {
if c.Op.Exec != b.ID {
return
}
+ loc := c.Holder.Location
if !op.Committed {
+ if w.rec != nil && w.rec.MoveID == op.ID && w.rec.MoveState != "landing" {
+ w.followRecord(c) // a commit or rollback the claim has not caught up with
+ return
+ }
w.holdRow(b, "landing", op.ID, c)
if w.now > op.CutDeadline {
w.rollback(c, "cut deadline") // N15: every phase before the commit
@@ -570,7 +677,8 @@ func (w *world) landTarget(b *box, c *claim) {
b.mem[op.ID+"quietwait"] = true
w.violate("INV-9: the cut of %s waits on quiet_after[%d] until %d", op.ID, b.Region, c.Quiet[b.Region])
}
- if w.parkStep(b, "instances/"+host+"/", fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], "") {
+ // an earlier stay of this incarnation, in its location here
+ if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/install/", op.ID, host), c.Quiet[b.Region], nil) {
w.cas(c, func(n *claim) bool { n.Op.LandPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })
}
case "install-copy":
@@ -589,9 +697,16 @@ func (w *world) landTarget(b *box, c *claim) {
}
src.Ver = cur.ID
}
- v := w.issue(b.ID, &request{kind: rCopy, region: b.Region, key: "instances/" + host + "/base", srcRegion: b.Region, srcKey: src.Key, srcVer: src.Ver})
+ // into this move's own generation: a copy that completes late can
+ // only ever add an object to this generation
+ v := w.issue(b.ID, &request{kind: rCopy, region: b.Region, key: dataKey(loc, op.ID, "base"), srcRegion: b.Region, srcKey: src.Key, srcVer: src.Ver})
if v > 0 {
- w.cas(c, func(n *claim) bool { n.Op.BaseVer, n.Op.LandPhase = v, "local"; return sameOp(n.Op.ID, op.ID) })
+ w.cas(c, func(n *claim) bool { n.Op.LandPhase = "published"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "published":
+ v := w.issue(b.ID, &request{kind: rPut, region: b.Region, key: genMarkerKey(loc), b: &blob{Kind: "gen", Gen: op.ID, Inc: c.Holder.Inc}})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool { n.Op.LandPhase = "local"; return sameOp(n.Op.ID, op.ID) })
}
case "local":
w.installLocal(b, c, op.ID, op.SealFiles, op.LandPhase, func(n *claim) { n.Op.LandPhase = "config" })
@@ -601,13 +716,21 @@ func (w *world) landTarget(b *box, c *claim) {
return
}
if b.HasKey {
- b.Config = c.Holder.Inc
+ b.Config, b.CfgVer = c.Holder.Inc, w.cfgVer[c.Holder.App]
+ if b.CfgVer != op.PinVer {
+ // `configured`: the bundle changed after admission (§7.6)
+ w.rollback(c, "configuration changed during the move")
+ return
+ }
}
b.Live, b.LiveInc = c.Holder.App, c.Holder.Inc
w.cas(c, func(n *claim) bool { n.Op.LandPhase = "restore"; return sameOp(n.Op.ID, op.ID) })
case "restore":
- if b.DB == nil {
- b.DB = w.restore(b, c.Holder.Inc, c.Holder.Legacy, lin{Op: op.ID, FilesGen: op.ID, Region: b.Region, Ver: op.BaseVer})
+ if b.DB == nil || b.DB.Gen != op.ID {
+ if b.DB != nil {
+ b.Parked++
+ }
+ b.DB = w.restore(b, c.Holder.Inc, loc, op.ID)
}
if b.DB == nil {
w.rollback(c, "restore failed")
@@ -623,7 +746,7 @@ func (w *world) landTarget(b *box, c *claim) {
if !w.admits(b, c, op.ID) {
return
}
- if hasMain(b) || w.spawn(b, c, lin{Op: op.ID, FilesGen: op.ID, Region: b.Region, Ver: op.BaseVer}, true) {
+ if hasMain(b) || w.spawn(b, c, op.ID, true) {
if !on("commit-before-open") {
w.openRow(b, op.ID)
}
@@ -651,27 +774,16 @@ func (w *world) landTarget(b *box, c *claim) {
w.rollback(c, "settle check failed")
return
}
- if w.cas(c, func(n *claim) bool {
- if !sameOp(n.Op.ID, op.ID) || n.Op.Kind != "landing" || w.now > n.Op.CutDeadline {
- return false
- }
- n.Op.Committed = true
- n.Holder.Lineage = lineage{Op: op.ID, Region: b.Region, Ver: op.BaseVer}
- n.Holder.FilesGen = op.ID
- q := op.StopAt + horizonH
- if !on("quiet-before-ack") {
- q = 0
+ // the commit, record first (§7.9): a CAS on the same record
+ // field the rollback uses, conditional on the deadline
+ r := w.rec
+ if r != nil && r.MoveID == op.ID && r.MoveState == "landing" && w.now <= op.CutDeadline {
+ r.MoveState = "committed"
+ r.Ver++
+ w.logf("commit %s: record committed", op.ID)
+ if w.now > op.CutAt+cutBudget {
+ w.violate("INV-9: %s committed at %d, cut at %d (budget %d)", op.ID, w.now, op.CutAt, cutBudget)
}
- n.Obl = append(n.Obl,
- w.newObl(n, "park-superseded", op.SrcRegion, -1, "instances/"+host+"/", "", q),
- w.newObl(n, "park-local", -1, op.Src, "", "", 0),
- w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))
- if q > n.Quiet[op.SrcRegion] {
- n.Quiet[op.SrcRegion] = q
- }
- return true
- }) && w.now > op.CutAt+cutBudget {
- w.violate("INV-9: %s committed at %d, cut at %d (budget %d)", op.ID, w.now, op.CutAt, cutBudget)
}
return
}
@@ -750,8 +862,12 @@ func (w *world) release(c *claim, execBox int) {
return true
}) {
w.logf("released %s to serving on box %d", op.ID, execBox)
- w.fixRecord()
w.opsDone++
+ // the record half (CAS-clear move) follows on a later step (§7.9)
+ w.checkDurable(w.claim, "at the release of "+op.ID)
+ if r := w.residueAtEnd(); len(r) > 0 {
+ w.violate("INV-10: %s ended with residue %v", op.ID, r)
+ }
switch {
case op.Kind == "landing":
w.stats["move-done"]++
@@ -792,7 +908,7 @@ func (w *world) releaseTarget(b *box, c *claim) {
n.Op.Exec, n.Op.DirtyKnown, n.Op.Dirty, n.Op.Phase, n.Op.TgtStopAt = -1, true, dirty, "released", w.now
q := w.now + horizonH
if on("target-park") {
- n.Obl = append(n.Obl, w.newObl(n, "park-superseded", op.TgtRegion, -1, "instances/"+host+"/", "", q))
+ n.Obl = append(n.Obl, w.newObl(n, "park-superseded", op.TgtRegion, -1, c.Holder.Location, "", q))
}
n.Obl = append(n.Obl, w.newObl(n, "park-staging", op.TgtRegion, -1, fmt.Sprintf("moves/%s/%s/", host, op.ID), "", op.SealQuiet))
if !dirty {
@@ -806,10 +922,17 @@ func (w *world) releaseTarget(b *box, c *claim) {
return
}
if op.Dirty && op.Phase == "released" && op.Exec == -1 {
- // return the target's writes over the approved lane (M17)
- db, files := w.snapshotBlob(b, c)
+ // return the target's writes over the approved lane (M17), under
+ // the staging-work lease of the source's region, with the same
+ // paused signers and SafeUntil rule as the forward path
+ if !w.takeStagingFor(op.SrcRegion, op.RollbackID, b) {
+ return
+ }
+ db, files := w.snapshotBlobOf(b, c, op.ID)
if op.ReturnDB.Ver == 0 {
- v := w.issue(b.ID, &request{kind: rPut, region: op.SrcRegion, key: fmt.Sprintf("moves/%s/%s/db", host, op.RollbackID), b: db})
+ r := &request{kind: rPut, region: op.SrcRegion, key: fmt.Sprintf("moves/%s/%s/db", host, op.RollbackID), b: db}
+ w.maybeStallDuplicateFor(b, op.SrcRegion, r)
+ v := w.issue(b.ID, r)
if v > 0 {
w.cas(c, func(n *claim) bool {
n.Op.ReturnDB = ref{Region: op.SrcRegion, Key: fmt.Sprintf("moves/%s/%s/db", host, op.RollbackID), Ver: v}
@@ -818,14 +941,19 @@ func (w *world) releaseTarget(b *box, c *claim) {
}
return
}
- v := w.issue(b.ID, &request{kind: rPut, region: op.SrcRegion, key: fmt.Sprintf("moves/%s/%s/files", host, op.RollbackID), b: files})
+ r := &request{kind: rPut, region: op.SrcRegion, key: fmt.Sprintf("moves/%s/%s/files", host, op.RollbackID), b: files}
+ w.maybeStallDuplicateFor(b, op.SrcRegion, r)
+ v := w.issue(b.ID, r)
if v > 0 {
w.cas(c, func(n *claim) bool {
if !sameOp(n.Op.ID, op.ID) {
return false
}
n.Op.ReturnFiles = ref{Region: op.SrcRegion, Key: fmt.Sprintf("moves/%s/%s/files", host, op.RollbackID), Ver: v}
- n.Op.ReturnQuiet = w.now + horizonH
+ n.Op.ReturnQuiet = w.now + stagingTTL + horizonH // the forward path's staging horizon (§7.3)
+ if !on("staging-quiet") {
+ n.Op.ReturnQuiet = w.now
+ }
n.Op.Phase = "returned"
n.Obl = append(n.Obl, w.newObl(n, "park-local", -1, b.ID, "", "", 0))
return true
@@ -878,28 +1006,33 @@ func (w *world) recoverSource(b *box, c *claim) {
if !w.evidence(b, op.RollbackID) {
return
}
- if w.parkStep(b, "instances/"+host+"/", fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, "") {
+ if w.parkStep(b, c.Holder.Location, fmt.Sprintf("superseded/%s/%s/return/", op.ID, host), op.StopAt+horizonH, nil) {
w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "install-copy"; return sameOp(n.Op.ID, op.ID) })
}
case "install-copy":
- v := w.issue(b.ID, &request{kind: rCopy, region: b.Region, key: "instances/" + host + "/base", srcRegion: b.Region, srcKey: op.ReturnDB.Key, srcVer: op.ReturnDB.Ver})
+ v := w.issue(b.ID, &request{kind: rCopy, region: b.Region, key: dataKey(c.Holder.Location, op.RollbackID, "base"), srcRegion: b.Region, srcKey: op.ReturnDB.Key, srcVer: op.ReturnDB.Ver})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "published"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "published":
+ v := w.issue(b.ID, &request{kind: rPut, region: b.Region, key: genMarkerKey(c.Holder.Location), b: &blob{Kind: "gen", Gen: op.RollbackID, Inc: c.Holder.Inc}})
if v > 0 {
- w.cas(c, func(n *claim) bool { n.Op.BaseVer, n.Op.SrcPhase = v, "local"; return sameOp(n.Op.ID, op.ID) })
+ w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "local"; return sameOp(n.Op.ID, op.ID) })
}
case "local":
w.installLocal(b, c, op.RollbackID, op.ReturnFiles, "", func(n *claim) { n.Op.SrcPhase = "config" })
case "config":
- b.Config, b.Live, b.LiveInc = c.Holder.Inc, c.Holder.App, c.Holder.Inc
+ b.Config, b.CfgVer, b.Live, b.LiveInc = c.Holder.Inc, w.cfgVer[c.Holder.App], c.Holder.App, c.Holder.Inc
w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "probing"; return sameOp(n.Op.ID, op.ID) })
case "probing":
if !w.admits(b, c, op.RollbackID) {
return
}
- L := holderLin(c.Holder)
+ want := c.Holder.Gen
if op.Dirty {
- L = lin{Op: op.RollbackID, FilesGen: op.RollbackID, Region: b.Region, Ver: op.BaseVer}
+ want = op.RollbackID
}
- if hasMain(b) || w.spawn(b, c, L, true) {
+ if hasMain(b) || w.spawn(b, c, want, true) {
w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "probed"; return sameOp(n.Op.ID, op.ID) })
return
}
@@ -911,10 +1044,10 @@ func (w *world) recoverSource(b *box, c *claim) {
return sameOp(n.Op.ID, op.ID)
})
case "probed":
- if op.Dirty && c.Holder.Lineage.Op != op.RollbackID {
+ if op.Dirty && c.Holder.Gen != op.RollbackID {
w.cas(c, func(n *claim) bool {
- n.Holder.Lineage = lineage{Op: op.RollbackID, Region: b.Region, Ver: op.BaseVer}
- n.Holder.FilesGen = op.RollbackID
+ w.newGen(n.Holder.Location, n.Holder.Gen, op.RollbackID)
+ n.Holder.Gen = op.RollbackID
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)
})
@@ -932,6 +1065,7 @@ func (w *world) recoverSource(b *box, c *claim) {
func (w *world) pushStep(b *box, c *claim) {
op := c.Op
+ loc := c.Holder.Location
switch op.Phase {
case "stopping":
w.holdRow(b, "moving", op.ID, c)
@@ -939,8 +1073,11 @@ func (w *world) pushStep(b *box, c *claim) {
return
}
var writes []int
+ if r := w.restore(b, c.Holder.Inc, loc, c.Holder.Gen); r != nil {
+ writes = r.Writes // the replica, under the final checkpoint
+ }
if b.DB != nil {
- writes = append(writes, b.DB.Writes...)
+ writes = unionInts(writes, b.DB.Writes)
}
w.nextW++
mark := w.nextW
@@ -954,7 +1091,7 @@ func (w *world) pushStep(b *box, c *claim) {
return true
})
case "park":
- if w.parkStep(b, "instances/"+host+"/", fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, "") {
+ if w.parkStep(b, loc, fmt.Sprintf("superseded/%s/%s/push/", op.ID, host), op.StopAt+horizonH, nil) {
w.cas(c, func(n *claim) bool { n.Op.Phase = "install"; return sameOp(n.Op.ID, op.ID) })
}
case "install":
@@ -965,34 +1102,47 @@ func (w *world) pushStep(b *box, c *claim) {
if b.Files != nil {
key = b.Files.Key
}
- v := w.issue(b.ID, &request{kind: rPut, region: b.Region, key: "instances/" + host + "/base", b: &blob{Kind: "base", Inc: c.Holder.Inc, Gen: op.ID, Writes: op.PushWrites, SealKey: key}})
+ v := w.issue(b.ID, &request{kind: rPut, region: b.Region, key: dataKey(loc, op.ID, "base"), b: &blob{Kind: "base", Inc: c.Holder.Inc, Gen: op.ID, Writes: op.PushWrites, SealKey: key}})
+ if v > 0 {
+ w.cas(c, func(n *claim) bool { n.Op.Phase = "published"; return sameOp(n.Op.ID, op.ID) })
+ }
+ case "published":
+ v := w.issue(b.ID, &request{kind: rPut, region: b.Region, key: genMarkerKey(loc), b: &blob{Kind: "gen", Gen: op.ID, Inc: c.Holder.Inc}})
if v > 0 {
- w.cas(c, func(n *claim) bool { n.Op.BaseVer, n.Op.Phase = v, "restore"; return sameOp(n.Op.ID, op.ID) })
+ w.cas(c, func(n *claim) bool { n.Op.Phase = "restore"; return sameOp(n.Op.ID, op.ID) })
}
case "restore":
- if b.DB != nil {
+ if b.DB != nil && b.DB.Gen != op.ID {
b.Parked++
b.DB = nil
}
- b.DB = w.restore(b, c.Holder.Inc, c.Holder.Legacy, lin{Op: op.ID, FilesGen: c.Holder.FilesGen, Region: b.Region, Ver: op.BaseVer})
+ if b.DB == nil {
+ b.DB = w.restore(b, c.Holder.Inc, loc, op.ID)
+ }
if b.DB == nil {
return
}
+ // .files-gen last: the files are unchanged, the marker names the
+ // new generation (F7 on §5.1)
+ if b.Files != nil {
+ b.Files.Gen = op.ID
+ }
// every probe renders config and materializes the release for the
// held row first (the passes skip held rows): RenderHeld, MaterializeHeld
if !b.HasKey {
return
}
- b.Config, b.Live, b.LiveInc = c.Holder.Inc, c.Holder.App, c.Holder.Inc
+ b.Config, b.CfgVer, b.Live, b.LiveInc = c.Holder.Inc, w.cfgVer[c.Holder.App], c.Holder.App, c.Holder.Inc
w.cas(c, func(n *claim) bool { n.Op.Phase = "probing"; return sameOp(n.Op.ID, op.ID) })
case "probing":
if !w.admits(b, c, op.ID) {
return
}
- if hasMain(b) || w.spawn(b, c, lin{Op: op.ID, FilesGen: c.Holder.FilesGen, Region: b.Region, Ver: op.BaseVer}, true) {
+ if hasMain(b) || w.spawn(b, c, op.ID, true) {
w.cas(c, func(n *claim) bool {
n.Op.Phase = "probed"
- n.Holder.Lineage = lineage{Op: op.ID, Region: b.Region, Ver: op.BaseVer}
+ w.newGen(n.Holder.Location, n.Holder.Gen, op.ID)
+ n.Holder.Gen = op.ID
q := op.StopAt + horizonH
if q > n.Quiet[b.Region] {
n.Quiet[b.Region] = q
@@ -1018,3 +1168,58 @@ func sameStep(a, b *claim) bool {
x.SrcPhase == y.SrcPhase && x.RevPhase == y.RevPhase && x.Exec == y.Exec && x.Committed == y.Committed &&
x.Opened == y.Opened && len(a.Obl) == len(b.Obl) && (a.Holder == nil) == (b.Holder == nil)
}
+
+// sweep is the straggler sweep (moves rev 6 §6.4, CC15): a request accepted
+// before S3's signature limit can complete after it (claim C3a), so a
+// retirement's horizon listing can miss it. While the host is at rest (the
+// claim free, or serving with no operation and no obligation), each region's
+// box lists the host namespace in its own bucket and parks, as a retirement
+// event of its own, everything outside the live set: the claim's location
+// and current generation in the executor's region, and the parkers' locks.
+// It re-reads the claim on every visit and abandons the event the moment
+// the host is no longer at rest; every delete names a snapshot version, so
+// nothing written later is touched.
+func (w *world) sweep(b *box, c *claim) {
+ if !on("straggler-sweep") {
+ return
+ }
+ rest := c == nil || c.Holder == nil && c.Op.Kind == "" && len(c.Obl) == 0 ||
+ c.Holder != nil && c.Op.Kind == "serving" && len(c.Obl) == 0
+ if !rest {
+ b.sweepID = ""
+ return
+ }
+ live := map[string]bool{}
+ if c != nil && c.Holder != nil && c.Op.Exec == b.ID {
+ loc, gen := c.Holder.Location, c.Holder.Gen
+ live[dataKey(loc, gen, "base")], live[dataKey(loc, gen, "ltx")], live[genMarkerKey(loc)] = true, true, true
+ }
+ keep := func(k string) bool { return live[k] }
+ bk := w.buckets[b.Region]
+ any := false
+ for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} {
+ for _, k := range bk.keys(p) {
+ if !strings.HasSuffix(k, "lock.json") && !live[k] && hasNonMarker(bk.objs[k]) {
+ any = true
+ }
+ }
+ }
+ if !any && b.sweepID == "" {
+ return
+ }
+ if b.sweepID == "" {
+ b.sweepID = w.newID("sw")
+ }
+ dest := fmt.Sprintf("parked/sweep/%s/%s/", host, b.sweepID)
+ done := true
+ for _, p := range []string{"instances/" + host + "/", "moves/" + host + "/"} {
+ if !w.parkStep(b, p, dest+strings.TrimSuffix(strings.TrimPrefix(p, ""), "/")+"/", 0, keep) {
+ done = false
+ }
+ }
+ if done {
+ w.logf("box %d swept stragglers (%s)", b.ID, b.sweepID)
+ w.stats["swept"]++
+ b.sweepID = ""
+ }
+}
diff --git a/internal/sim/hostlife/mutate.sh b/internal/sim/hostlife/mutate.sh
index 69331449a..51c731272 100755
--- a/internal/sim/hostlife/mutate.sh
+++ b/internal/sim/hostlife/mutate.sh
@@ -1,5 +1,5 @@
#!/bin/bash
-# Mutation checks for the hostlife model (move-any-app spec §14.2.5).
+# Mutation checks for the hostlife model (move-any-app spec §14.2).
#
# Each rule is dropped in its own scratch copy of the module, never in
# place: an interrupted in-place mutation once left a disabled guard in a
@@ -7,46 +7,89 @@
#
# internal/sim/hostlife/mutate.sh 3000 # every rule
# internal/sim/hostlife/mutate.sh 30000 rule-a rule-b # named rules
-# internal/sim/hostlife/mutate.sh 30000 rule-a,rule-b # a pair, dropped together
+# internal/sim/hostlife/mutate.sh 30000 rule-a,rule-b # a combination, dropped together
#
-# A rule is CAUGHT when at least one seed fails. Scratch copies live under
-# ${HOSTLIFE_SCRATCH:-$HOME/.cache/hostlife-sim} and are removed after use.
+# Classification (joint round 2, R2-10):
+#
+# CAUGHT the test ran to completion and reported at least one seed
+# that violated an invariant, with the seed number parsed from
+# its output (so it can be replayed with HOSTLIFE_SEED);
+# MISSED the test ran to completion and every seed passed;
+# ERROR anything else: a build failure, a timeout, a panic, a
+# read-only cache, or output the harness cannot parse. An
+# error is never a detection.
+#
+# Expected outcomes live in expected-outcomes.txt beside this script: a
+# rule listed there as `missed` (liveness-only, unreachable, or caught
+# only in a stated combination) is reported as EXPECTED-MISS. The sweep
+# exits nonzero on any ERROR, on any unexpected MISSED, and on any rule
+# listed as `missed` that is CAUGHT (the expectation is stale).
+#
+# Every run's full output is kept in $SCRATCH/logs/<rule>.log.
set -u
SEEDS=${1:?seeds}
shift
ROOT=$(git -C "$(dirname "$0")" rev-parse --show-toplevel)
+PKG="$ROOT/internal/sim/hostlife"
SCRATCH=${HOSTLIFE_SCRATCH:-$HOME/.cache/hostlife-sim}
-mkdir -p "$SCRATCH/gotmp"
+mkdir -p "$SCRATCH/gotmp" "$SCRATCH/logs" "$SCRATCH/verdicts"
RULES="$*"
if [ -z "$RULES" ]; then
- RULES=$(sed -n '/^var allRules/,/^}/p' "$ROOT/internal/sim/hostlife/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t')
+ RULES=$(sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -o '^\s*"[a-z0-9-]*"' | tr -d ' "\t')
fi
+rm -f "$SCRATCH"/verdicts/*
one() {
r=$1
- d="$SCRATCH/mut-$(echo "$r" | tr ',' '+')"
+ tag=$(echo "$r" | tr ',' '+')
+ d="$SCRATCH/mut-$tag"
+ log="$SCRATCH/logs/$tag.log"
+ verdict="$SCRATCH/verdicts/$tag"
+ for x in $(echo "$r" | tr ',' ' '); do
+ if ! sed -n '/^var allRules/,/^}/p' "$PKG/rules_test.go" | grep -q "^\s*\"$x\","; then
+ echo "ERROR $r: no rule named $x" | tee "$verdict"
+ return
+ fi
+ done
rm -rf "$d"
mkdir -p "$d/internal/sim"
cp "$ROOT/go.mod" "$ROOT/go.sum" "$d/"
- cp -a "$ROOT/internal/sim/hostlife" "$d/internal/sim/"
+ cp -a "$PKG" "$d/internal/sim/"
sed -i "s/^var mutated = \"\"/var mutated = \"$r\"/" "$d/internal/sim/hostlife/rules_test.go"
if ! grep -q "^var mutated = \"$r\"" "$d/internal/sim/hostlife/rules_test.go"; then
- echo "SEDFAIL $r"
+ echo "ERROR $r: could not set the mutation" | tee "$verdict"
+ rm -rf "$d"
return
fi
- out=$(cd "$d" && GOTMPDIR="$SCRATCH/gotmp" TMPDIR="$SCRATCH/gotmp" HOSTLIFE_SEEDS=$SEEDS \
- go test ./internal/sim/hostlife/ -run TestHostLifecycle -count=1 -timeout 120m -v 2>&1)
+ (cd "$d" && GOTMPDIR="$SCRATCH/gotmp" TMPDIR="$SCRATCH/gotmp" HOSTLIFE_SEEDS=$SEEDS \
+ go test ./internal/sim/hostlife/ -run TestHostLifecycle -count=1 -timeout 180m -v) >"$log" 2>&1
rc=$?
- if echo "$out" | grep -q "violated an invariant"; then
- n=$(echo "$out" | grep -o "[0-9]* of $SEEDS seeds violated" | head -1)
- echo "CAUGHT $r: $n"
- elif [ $rc -ne 0 ]; then
- echo "CAUGHT $r: test failed rc=$rc"
+ expect=$(awk -v r="$r" '$1==r {print $2}' "$PKG/expected-outcomes.txt" 2>/dev/null)
+ nviol=$(grep -o "[0-9]* of $SEEDS seeds violated an invariant" "$log" | head -1 | awk '{print $1}')
+ seed=$(grep -o "first seed [0-9]*" "$log" | head -1 | awk '{print $3}')
+ clean=$(grep -c "^ sim_test.go:[0-9]*: $SEEDS seeds, 0 failed" "$log")
+ if [ $rc -ne 0 ] && [ -n "$nviol" ] && [ -n "$seed" ] && ! grep -q "^panic:\|build failed\|test timed out" "$log"; then
+ if [ "$expect" = "missed" ]; then
+ echo "STALE $r: $nviol of $SEEDS seeds violated (first seed $seed), but expected-outcomes.txt says missed" | tee "$verdict"
+ else
+ echo "CAUGHT $r: $nviol of $SEEDS seeds violated (first seed $seed)" | tee "$verdict"
+ fi
+ elif [ $rc -eq 0 ] && [ "$clean" -eq 1 ]; then
+ if [ "$expect" = "missed" ]; then
+ echo "EXPECTED-MISS $r ($SEEDS seeds)" | tee "$verdict"
+ else
+ echo "MISSED $r ($SEEDS seeds)" | tee "$verdict"
+ fi
else
- echo "MISSED $r ($SEEDS seeds)"
+ echo "ERROR $r: rc=$rc, no parsable verdict; see $log" | tee "$verdict"
fi
rm -rf "$d"
}
export -f one
-export SEEDS ROOT SCRATCH
+export SEEDS ROOT PKG SCRATCH
printf '%s\n' $RULES | xargs -P "${HOSTLIFE_PAR:-8}" -I{} bash -c 'one "$@"' _ {}
+bad=$(cat "$SCRATCH"/verdicts/* 2>/dev/null | grep -c "^ERROR\|^MISSED\|^STALE")
+if [ "$bad" -gt 0 ]; then
+ echo "sweep: $bad rule(s) ERROR, MISSED or STALE" >&2
+ exit 1
+fi
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index a5bb6df57..675a9dc5e 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -161,50 +161,55 @@ func (w *world) evidence(b *box, opID string) bool {
// ---------- restore and spawn ----------
-type lin struct {
- Op string
- FilesGen string
- Region int
- Ver int
-}
-
-func (w *world) restore(b *box, inc int, legacy bool, L lin) *localDB {
+// restore rebuilds a database from location loc, generation gen, in b's own
+// bucket (claim C3a; moves rev 6 §5.1). It replays every replica object of
+// that generation, as litestream replays every LTX file of a generation:
+// base snapshots and later LTX alike, current and noncurrent. It never
+// looks at another location or generation. The mutation restores the
+// newest single object anywhere under the location instead, 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]
- db := &localDB{Inc: inc, Gen: L.Op}
- if L.Op != "" {
- if L.Region != b.Region {
- return nil
+ db := &localDB{Inc: inc, Loc: loc, Gen: gen}
+ if !on("restore-by-generation") {
+ var best *version
+ for _, k := range bk.keys(loc) {
+ if !isDataKey(k) {
+ continue
+ }
+ for _, v := range bk.objs[k] {
+ if !v.Marker && (best == nil || v.ID > best.ID) {
+ best = v
+ }
+ }
}
- v := bk.byID("instances/"+host+"/base", L.Ver)
- if v == nil {
- return nil
+ if best != nil {
+ db.Writes = append([]int(nil), best.B.Writes...)
+ db.Key = best.B.SealKey
+ if best.B.Inc != 0 {
+ db.Inc = best.B.Inc
+ }
}
- db.Writes = append(db.Writes, v.B.Writes...)
- db.Key = v.B.SealKey
- db.Inc = v.B.Inc
+ return db
}
- var best *version
- if on("restore-lineage-filter") {
- for _, v := range bk.objs["instances/"+host+"/ltx"] {
+ found := false
+ for _, k := range []string{dataKey(loc, gen, "base"), dataKey(loc, gen, "ltx")} {
+ for _, v := range bk.objs[k] {
if v.Marker {
continue
}
- okInc := v.B.Inc == inc || (legacy && v.B.Inc == 0)
- if okInc && v.B.Gen == L.Op && (best == nil || len(v.B.Writes) >= len(best.B.Writes)) {
- best = v
+ found = true
+ db.Writes = unionInts(db.Writes, v.B.Writes)
+ if db.Key == 0 {
+ db.Key = v.B.SealKey
+ }
+ if v.B.Inc != 0 {
+ db.Inc = v.B.Inc
}
}
- } else {
- best = bk.current("instances/" + host + "/ltx")
}
- if best != nil {
- if best.B.Inc != 0 {
- db.Inc = best.B.Inc
- }
- db.Writes = unionInts(db.Writes, best.B.Writes)
- if db.Key == 0 {
- db.Key = best.B.SealKey
- }
+ if !found && gen != "" {
+ return nil // an installed generation with nothing in it: refuse
}
return db
}
@@ -221,33 +226,68 @@ func unionInts(a, b []int) []int {
return out
}
-// spawn starts the app on b for the holder incarnation, with the given
-// expected lineage. It returns true if the app answered its readiness path.
-func (w *world) spawn(b *box, c *claim, L lin, probe bool) bool {
+// bucketGen reads generation.json at loc in b's own bucket: the generation
+// and incarnation it names, or origin when absent.
+func (w *world) bucketGen(b *box, loc string) (string, int) {
+ v := w.buckets[b.Region].current(genMarkerKey(loc))
+ if v == nil {
+ return "", 0
+ }
+ return v.B.Gen, v.B.Inc
+}
+
+// spawn starts the app on b for the holder incarnation. want is the
+// generation the claim expects: the holder's current generation for an
+// ordinary wake, or the generation an operation is installing for its
+// probe. It returns true if the app answered its readiness path.
+func (w *world) spawn(b *box, c *claim, want string, probe bool) bool {
h := c.Holder
+ loc := h.Location
if b.Old {
- // an old executable: no claim, no markers, best-effort placement
+ // an old executable: no claim, no markers, no locations; it
+ // restores whatever is newest at the legacy root
if b.DB == nil {
- b.DB = w.restore(b, h.Inc, true, lin{})
+ b.DB = &localDB{Inc: h.Inc, Loc: "instances/" + host + "/"}
+ if v := w.buckets[b.Region].current("instances/" + host + "/ltx"); v != nil {
+ b.DB.Writes, b.DB.Key = append([]int(nil), v.B.Writes...), v.B.SealKey
+ if v.B.Inc != 0 {
+ b.DB.Inc = v.B.Inc
+ }
+ }
}
} else {
+ bg, binc := w.bucketGen(b, loc)
+ if !on("start-check-claim-gen") {
+ // rev 5's start check: the box's own markers decide, so the
+ // generation to restore is the one its region's generation.json
+ // names
+ want = bg
+ }
+ if on("start-check") {
+ if bg != want || (bg != "" && binc != h.Inc) {
+ w.logf("box %d start check refused: generation.json %q inc %d, claim wants %q", b.ID, bg, binc, want)
+ return false
+ }
+ // a warm database from an earlier stay is parked, and the box
+ // restores cold (§5.1)
+ if b.DB != nil && (b.DB.Gen != bg || b.DB.Loc != loc) {
+ b.Parked++
+ b.DB = nil
+ }
+ }
if b.DB == nil {
- b.DB = w.restore(b, h.Inc, h.Legacy, L)
+ b.DB = w.restore(b, h.Inc, loc, want)
if b.DB == nil {
return false
}
}
if on("start-check") {
- if b.DB.Gen != L.Op || b.DB.Inc != h.Inc && !(h.Legacy && b.DB.Inc == 0) {
- w.logf("box %d start check refused: db gen %q inc %d want %q %d", b.ID, b.DB.Gen, b.DB.Inc, L.Op, h.Inc)
+ if b.DB.Inc != h.Inc && !(h.Legacy && b.DB.Inc == 0) {
+ w.logf("box %d start check refused: db inc %d", b.ID, b.DB.Inc)
return false
}
- if b.Files != nil && (b.Files.Gen != L.FilesGen || b.Files.Inc != h.Inc) {
- w.logf("box %d start check refused: files gen %q inc %d", b.ID, b.Files.Gen, b.Files.Inc)
- return false
- }
- if b.Files == nil && L.FilesGen != "" {
- w.logf("box %d start check refused: files missing for gen %q", b.ID, L.FilesGen)
+ if b.Files != nil && (b.Files.Gen != bg || b.Files.Inc != h.Inc) {
+ w.logf("box %d start check refused: files gen %q inc %d, generation.json %q", b.ID, b.Files.Gen, b.Files.Inc, bg)
return false
}
}
@@ -264,7 +304,7 @@ func (w *world) spawn(b *box, c *claim, L lin, probe bool) bool {
}
if b.Files == nil {
w.nextID++
- b.Files = &filesDir{Inc: h.Inc, Key: w.nextID, Gen: L.FilesGen, Env: w.nextID, Done: true}
+ b.Files = &filesDir{Inc: h.Inc, Key: w.nextID, Gen: want, Env: w.nextID, Done: true}
}
if b.DB.Key == 0 {
b.DB.Key = b.Files.Key // unsealed data (never booted) adopts the key
@@ -275,28 +315,32 @@ func (w *world) spawn(b *box, c *claim, L lin, probe bool) bool {
}
// FailApp is the injected "the target cannot run it" fault: landing probes only
healthy := b.Config == h.Inc && b.Live == h.App && b.LiveInc == h.Inc && !(probe && b.FailApp && c.Op.Kind == "landing")
+ // §7.7: the probe checks the launch environment at spawn. The forward
+ // path requires the inputs pinned at admission. A recovery probe (the
+ // source's revert or rollback) runs on the inputs it rendered now and
+ // records them (rev 6, J2-R2-5); the mutation keeps rev 5's rule, which
+ // pins recoveries too.
+ if probe && c.Op.PinVer != 0 && b.CfgVer != c.Op.PinVer {
+ switch {
+ case c.Op.Kind == "landing":
+ healthy = false
+ case (c.Op.Kind == "reverting" || c.Op.Kind == "restoring") && !on("recovery-current-inputs"):
+ healthy = false
+ }
+ }
if !healthy {
w.logf("box %d unhealthy start inc %d: cfg=%d live=%s/%d fail=%v kind=%s", b.ID, h.Inc, b.Config, b.Live, b.LiveInc, b.FailApp, c.Op.Kind)
return false
}
strict := !b.Old && (on("strict-spawn") || w.rng.Intn(2) == 0)
- b.Procs = append(b.Procs, &proc{Main: true, Strict: strict, Inc: h.Inc, Gen: L.Op, Box: b.ID})
+ b.Procs = append(b.Procs, &proc{Main: true, Strict: strict, Inc: h.Inc, Gen: want, Box: b.ID})
if w.rng.Intn(2) == 0 {
- b.Procs = append(b.Procs, &proc{Main: false, Strict: strict, Inc: h.Inc, Gen: L.Op, Box: b.ID})
+ b.Procs = append(b.Procs, &proc{Main: false, Strict: strict, Inc: h.Inc, Gen: want, Box: b.ID})
}
- w.logf("box %d spawned inc %d gen %q (probe=%v strict=%v) claim=%s/%s exec=%d", b.ID, h.Inc, L.Op, probe, strict, c.Op.Kind, c.Op.ID, c.Op.Exec)
+ w.logf("box %d spawned inc %d gen %q (probe=%v strict=%v) claim=%s/%s exec=%d", b.ID, h.Inc, want, probe, strict, c.Op.Kind, c.Op.ID, c.Op.Exec)
return true
}
-func holderLin(h *holder) lin {
- return lin{Op: h.Lineage.Op, FilesGen: h.LinFiles(), Region: h.Lineage.Region, Ver: h.Lineage.Ver}
-}
-
-// LinFiles: the files generation compatible with the lineage. Moves set it
-// to the move id; a push (not modelled as a separate generation of files)
-// keeps it.
-func (h *holder) LinFiles() string { return h.FilesGen }
-
// ---------- admission (C4, §19.1 of the moves spec) ----------
func (w *world) admits(b *box, c *claim, probe string) bool {
@@ -353,16 +397,19 @@ func (w *world) admits(b *box, c *claim, probe string) bool {
// parkStep advances one park of `prefix` in b's own bucket into dest. It
// returns true when the location is verified empty after the quiet time.
-// excludeGen keeps the current lineage's objects (push).
-func (w *world) parkStep(b *box, prefix, dest string, quiet int, excludeGen string) bool {
- return w.parkDepth(b, prefix, dest, quiet, excludeGen, 0)
+// keep, when set, names keys the park must leave alone.
+func (w *world) parkStep(b *box, prefix, dest string, quiet int, keep func(string) bool) bool {
+ return w.parkDepth(b, prefix, dest, quiet, keep, 0)
}
-func (w *world) parkDepth(b *box, prefix, dest string, quiet int, excludeGen string, depth int) bool {
+func (w *world) parkDepth(b *box, prefix, dest string, quiet int, keep func(string) bool, depth int) bool {
if depth > 8 {
return false // a park that cannot finish: reported as non-convergence
}
bk := w.buckets[b.Region]
+ skip := func(k string) bool {
+ return (strings.HasSuffix(k, "lock.json") && on("park-skip-lock")) || (keep != nil && keep(k))
+ }
// the parker takes the location's replica lease first (claim §6.2 step 1):
// its own lock.json, renewed on every visit
w.issue(b.ID, &request{kind: rPut, region: b.Region, key: prefix + "lock.json", b: &blob{Kind: "lock", Text: fmt.Sprintf("box%d@%d", b.ID, w.now)}})
@@ -376,31 +423,32 @@ func (w *world) parkDepth(b *box, prefix, dest string, quiet int, excludeGen str
}
man := bk.current(manKey)
if man == nil {
- // snapshot every data version except the live lock
- var snap []ref
+ // the snapshot (claim rev 4 §6.2 step 2): the archive set is every
+ // non-marker version, current and noncurrent; the deletion set is
+ // every version, delete markers included. The mutation archives
+ // and deletes only current versions, so older ones resurface.
+ var archive, dels []ref
for _, k := range bk.keys(prefix) {
- if strings.HasSuffix(k, "lock.json") && on("park-skip-lock") {
+ if skip(k) {
continue
}
vs := bk.objs[k]
for i, v := range vs {
- if v.Marker {
+ current := i == len(vs)-1
+ if !on("park-all-versions") && !current {
continue
}
- if excludeGen != "" && v.B != nil && v.B.Gen == excludeGen {
- continue
- }
- if !on("park-all-versions") && i != len(vs)-1 {
- continue
+ dels = append(dels, ref{Region: b.Region, Key: k, Ver: v.ID})
+ if !v.Marker {
+ archive = append(archive, ref{Region: b.Region, Key: k, Ver: v.ID})
}
- snap = append(snap, ref{Region: b.Region, Key: k, Ver: v.ID})
}
}
- // copy each version by id; a destination keyed by the source
- // version is idempotent, so progress accumulates across attempts
+ // copy each archive-set version by id; a destination keyed by the
+ // source version is idempotent, so progress accumulates
all := true
- for _, r := range snap {
- dk := dest + strings.TrimPrefix(r.Key, "instances/"+host+"/") + fmt.Sprintf(".v%d", r.Ver)
+ for _, r := range archive {
+ dk := dest + strings.TrimPrefix(r.Key, "instances/"+host+"/") + fmt.Sprintf("@%d", r.Ver)
if bk.current(dk) != nil {
continue
}
@@ -410,13 +458,13 @@ func (w *world) parkDepth(b *box, prefix, dest string, quiet int, excludeGen str
if !all {
return false
}
- // the manifest last, once every copy exists
- w.issue(b.ID, &request{kind: rPut, region: b.Region, key: manKey, b: &blob{Kind: "manifest", Refs: snap}})
+ // the manifest last, once every copy exists, with both sets
+ w.issue(b.ID, &request{kind: rPut, region: b.Region, key: manKey, b: &blob{Kind: "manifest", Refs: archive, Dels: dels}})
return false
}
- // delete the manifest's versions, in one batch per visit
+ // replay the manifest's deletion set, by version id, in one batch per visit
issued := false
- for _, r := range man.B.Refs {
+ for _, r := range man.B.Dels {
if bk.byID(r.Key, r.Ver) == nil {
continue
}
@@ -436,13 +484,12 @@ func (w *world) parkDepth(b *box, prefix, dest string, quiet int, excludeGen str
}
// a straggler written after the snapshot: park it as a new event
for _, k := range bk.keys(prefix) {
- if strings.HasSuffix(k, "lock.json") && on("park-skip-lock") {
+ if skip(k) {
continue
}
for _, v := range bk.objs[k] {
- if !v.Marker && !(excludeGen != "" && v.B.Gen == excludeGen) {
- // start a further retirement event under a fresh id
- return w.parkDepth(b, prefix, dest+"s/", quiet, excludeGen, depth+1)
+ if !v.Marker {
+ return w.parkDepth(b, prefix, dest+"s/", quiet, keep, depth+1)
}
}
}
@@ -451,19 +498,33 @@ func (w *world) parkDepth(b *box, prefix, dest string, quiet int, excludeGen str
}
// localPark retires b's local state for incarnation inc under the host
-// guard: a retired marker first, then rename everything aside.
-func (w *world) localPark(b *box, inc int) {
- if on("hostguard") {
+// 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.
+func (w *world) localPark(b *box, inc int) bool {
+ if on("hostguard") && !b.Retired[inc] {
if b.Retired == nil {
b.Retired = map[int]bool{}
}
b.Retired[inc] = true
+ return false
}
- if b.DB != nil || b.Files != nil || b.Config != 0 || b.Live != "" {
- b.Parked++
+ switch {
+ case b.DB != nil:
+ b.DB = nil
+ case b.Files != nil:
+ b.Files = nil
+ case b.Config != 0:
+ b.Config = 0
+ case b.Live != "":
+ b.Live, b.LiveInc = "", 0
+ case len(b.Timers) > 0 || len(b.History) > 0 || b.Attempt != 0:
+ b.Timers, b.History, b.Attempt = nil, nil, 0
+ default:
+ return true
}
- b.DB, b.Files, b.Config, b.Live, b.LiveInc = nil, nil, 0, "", 0
- b.Timers, b.History, b.Attempt = nil, nil, 0
+ b.Parked++
+ return false
}
// ---------- obligations ----------
@@ -493,7 +554,9 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {
if b.DB != nil && b.DB.Inc != 0 {
inc = b.DB.Inc
}
- w.localPark(b, inc)
+ if !w.localPark(b, inc) {
+ return // the next artifact on a later step
+ }
if b.Row != nil && b.Row.HoldOp == o.Op || b.Row != nil && (c.Holder == nil || b.ID != c.Op.Exec) {
b.Row = nil
}
@@ -519,7 +582,7 @@ func (w *world) doObligation(b *box, c *claim, o obligation) {
quiet = b.evidAt[o.ID] + horizonH
}
}
- if !w.parkStep(b, o.Prefix, o.Dest(), quiet, o.excludeGen(c)) {
+ if !w.parkStep(b, o.Prefix, o.Dest(), quiet, nil) {
return
}
}
@@ -552,8 +615,6 @@ func (o obligation) Dest() string {
return fmt.Sprintf("superseded/%s/%s/%s/", o.Op, host, o.ID)
}
-func (o obligation) excludeGen(c *claim) string { return o.Exclude }
-
func (w *world) newObl(c *claim, kind string, region, boxID int, prefix, ret string, quiet int) obligation {
return obligation{ID: w.newID("ob"), Op: c.Op.ID, Kind: kind, Region: region, Box: boxID, Prefix: prefix, Ret: ret, Quiet: quiet}
}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index ba2431bf4..58b8fd7c5 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -43,7 +43,12 @@ var allRules = []string{
"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
+ "admission-registration", // claim rev 4 §5.1 step 0, §5.3 step 1b (J2-R2-2)
+ "registration-recovery", // CC16: a registration is a lease, so a dead create cannot block purge
+ "cancelled-creates", // claim rev 4 §5.1 (J2-R2-7): a late record PUT is removed
+ "orphan-no-deadline", // CC17: ... whenever it lands, not only before `until`
"door-by-version", // §6.5/J-N10
+ "door-reread", // claim rev 4 §6.5 (J2-R2-4): O2 refuses if the holder or op changed
"strict-spawn", // §6.1/J-D3
"evidence-whole-tree", // §6.1: stray and non-strict processes
"evidence-from-state", // §6.1/R2-2
@@ -53,26 +58,29 @@ var allRules = []string{
"floor-boot-recovery", // §10/J-N12
"participant-rows", // claim §2/R2-4
"stale-hold-release", // this model's finding: release a hold whose op ended
- "restore-lineage-filter", // this model's finding (replication exception)
+ "restore-by-generation", // C3a + moves rev 6 §5.1: restore replays the claim's generation only
"quiet-before-ack", // this model's finding (late writes after a park)
+ "straggler-sweep", // CC15 + moves rev 6 §6.4: stragglers past H are parked at rest
// moves spec
- "seal-by-version", // J-N2: landing copies sealed versions
- "staging-quiet", // J-N2: staging retired after its writers' horizon
- "commit-before-open", // INV-5
- "hold-op-open", // §5.2 conditional open
- "start-check", // INV-4
- "markers-last", // R2-6
- "revert-journal", // J-N11
- "rollback-journal", // R2-3
- "dirty-return", // INV-2
- "target-park", // R2-5/INV-10
- "abort-target-owner", // J-N13
- "timer-freeze", // J-N14 runner bookkeeping
- "timer-canonical", // J-N14 prune path
- "cut-deadline", // J-N15
- "readiness-key", // T2
- "source-readiness", // S1: the source can run the instance before the cut
- "readiness-quiet", // T12: the target region's quiet_after has passed
- "files-carried", // §8 (the kpmg outage)
- "config-before-probe", // L3 (the kpmg outage)
+ "seal-by-version", // J-N2: landing copies sealed versions
+ "staging-quiet", // J-N2: staging retired after its writers' horizon
+ "commit-before-open", // INV-5
+ "hold-op-open", // §5.2 conditional open
+ "start-check", // INV-4: markers agree
+ "start-check-claim-gen", // rev 6 §5.1 (R2-8): and name the generation the claim expects
+ "markers-last", // R2-6
+ "revert-journal", // J-N11
+ "rollback-journal", // R2-3
+ "dirty-return", // INV-2
+ "target-park", // R2-5/INV-10
+ "abort-target-owner", // J-N13
+ "timer-freeze", // J-N14 runner bookkeeping
+ "timer-canonical", // J-N14 prune path
+ "cut-deadline", // J-N15
+ "readiness-key", // T2
+ "source-readiness", // S1: the source can run the instance before the cut
+ "readiness-quiet", // T12: the target region's quiet_after has passed
+ "files-carried", // §8 (the kpmg outage)
+ "config-before-probe", // L3 (the kpmg outage)
+ "recovery-current-inputs", // rev 6 §7.7 (J2-R2-5): a recovery probe is not bound to the move's pinned inputs
}
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
index ad04fe588..406b0116a 100644
--- a/internal/sim/hostlife/sim_test.go
+++ b/internal/sim/hostlife/sim_test.go
@@ -16,12 +16,13 @@ const (
func newWorld(seed int64, verbose bool) *world {
w := &world{seed: seed, rng: rand.New(rand.NewSource(seed)), verbose: verbose,
- stores: map[string]bool{app0: true, app1: true}, purgeRes: map[string]bool{}, purgeStep: map[string]int{},
- control: newBucket(), delivered: map[int]bool{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}
+ 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{}, genParent: map[string]string{}, execLease: map[int]execLease{}, fail: map[string]bool{}, stats: map[string]int{}}
for r := 0; r < nRegions; r++ {
w.buckets[r] = newBucket()
}
- for _, f := range []string{"partition", "freeze", "pause", "destroy"} {
+ w.admit = map[string]*admission{app0: {Reg: map[string]regEntry{}}, app1: {Reg: map[string]regEntry{}}}
+ for _, f := range []string{"partition", "freeze", "pause", "destroy", "disk"} {
w.fail[f] = w.rng.Intn(2) == 0
}
for r := 0; r < nRegions; r++ {
@@ -61,15 +62,23 @@ func (w *world) legacyStart() {
w.acks = append(w.acks, ack{W: w.nextW, Inc: inc, Box: b.ID, At: 0, Kind: "write"})
}
b.Row = &row{Inc: inc, App: app0, Status: "ready"}
- b.DB = &localDB{Inc: inc, Key: key, Writes: writes}
+ b.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, Writes: writes}
b.Files = &filesDir{Inc: inc, Key: key, Env: 1, Done: true}
- b.Config, b.Live, b.LiveInc = inc, app0, inc
+ b.Config, b.CfgVer, b.Live, b.LiveInc = inc, 1, app0, inc
w.buckets[r].objs["instances/"+host+"/ltx"] = []*version{{ID: w.newVer(), B: &blob{Kind: "ltx", Inc: 0, Writes: writes, SealKey: key}}}
+ w.markDurable("instances/"+host+"/ltx", &blob{Writes: writes})
other := (r + 1 + w.rng.Intn(nRegions-1)) % nRegions
w.buckets[other].objs["instances/"+host+"/ltx"] = []*version{{ID: w.newVer(), B: &blob{Kind: "ltx", Inc: 0, Writes: writes[:1], SealKey: key}}}
if w.rng.Intn(2) == 0 {
b.Procs = []*proc{{Main: true, Strict: false, Inc: inc, Box: b.ID}, {Main: false, Strict: false, Inc: inc, Box: b.ID}}
}
+ if w.rng.Intn(2) == 0 {
+ // that earlier move also left the old box's local state behind:
+ // a database, a files directory and env files, and no row
+ ob := w.regionBox(other)
+ ob.DB = &localDB{Inc: inc, Loc: locationFor(inc, true), Key: key, Writes: writes[:1]}
+ ob.Files = &filesDir{Inc: inc, Key: key, Env: 1, Done: true}
+ }
}
// ---------- the scheduler ----------
@@ -77,13 +86,25 @@ func (w *world) legacyStart() {
func (w *world) step() {
w.now++
w.completeDue(false)
+ if p := w.recPend; p != nil && p.at <= w.now {
+ w.recPend = nil
+ if w.rec == nil { // create-only: it lands only where no record is
+ w.rec = p.rec
+ w.logf("a late record PUT for inc %d landed", p.rec.Inc)
+ }
+ }
w.runStalled()
bs := w.liveBoxes()
b := bs[w.rng.Intn(len(bs))]
n := w.rng.Intn(100)
switch {
case !w.calm && n < 6:
- switch w.rng.Intn(9) {
+ switch w.rng.Intn(10) {
+ case 9:
+ // a config or secrets update publishes a new bundle version
+ app := []string{app0, app1}[w.rng.Intn(2)]
+ w.cfgVer[app]++
+ w.logf("config bundle %s v%d published", app, w.cfgVer[app])
case 0, 1:
w.userCreate()
case 2, 7, 8:
@@ -174,9 +195,27 @@ func (w *world) heal(final bool) {
}
func (w *world) quiescent() bool {
- if len(w.pending) > 0 || len(w.console) > 0 {
+ if len(w.pending) > 0 || len(w.console) > 0 || w.recPend != nil || !w.atRest() {
return false
}
+ return len(w.residue()) == 0
+}
+
+// atRest: the claim, record and boxes have converged.
+func (w *world) atRest() bool {
+ if w.h2.Kind == "creating" || w.h2.Kind == "purging" {
+ return false
+ }
+ for _, ad := range w.admit {
+ if ad.Closed {
+ return false
+ }
+ for _, e := range ad.Reg {
+ if w.now <= e.Until || !on("registration-recovery") {
+ return false // a live registration: its create is still in flight
+ }
+ }
+ }
c := w.claim
if c == nil {
return w.rec == nil
@@ -217,6 +256,9 @@ func (w *world) checkStep() {
w.violate("INV-1: boxes %v run the host at once", writers)
}
// an app store exists while any instance of the app is held for serving
+ if w.h2.Kind == "serving" && !w.stores[w.h2.App] {
+ w.violate("purge: store of app %s destroyed while its second host serves", w.h2.App)
+ }
if c := w.claim; c != nil && c.Holder != nil && !w.stores[c.Holder.App] {
switch c.Op.Kind {
case "purging", "deleting", "parking":
@@ -240,8 +282,98 @@ func (w *world) boxesState() string {
return s
}
+// residue lists live-namespace data that should not exist: everything
+// under the host's namespace in a region the host does not serve from, and
+// in the serving region anything but the claim's location and generation
+// (and the parkers' own locks). Nothing here writes.
+func (w *world) residue() []string { return w.residueOf(false) }
+
+// residueAtEnd is INV-10 as the spec states it, checked when an operation
+// ends (a release to serving, a free): no copy outside the live set, except
+// a straggler that completed after H, which only the sweep can retire.
+func (w *world) residueAtEnd() []string { return w.residueOf(true) }
+
+func (w *world) residueOf(exceptStragglers bool) []string {
+ var out []string
+ c := w.claim
+ live := map[string]bool{}
+ serving := -1
+ if c != nil && c.Holder != nil {
+ if e := w.execBox(c); e != nil {
+ serving = e.Region
+ loc, gen := c.Holder.Location, c.Holder.Gen
+ live[dataKey(loc, gen, "base")] = true
+ live[dataKey(loc, gen, "ltx")] = true
+ live[genMarkerKey(loc)] = true
+ }
+ }
+ for r := 0; r < nRegions; r++ {
+ 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]) {
+ continue
+ }
+ if exceptStragglers && w.owed(r, k) {
+ continue // a pending chore of another operation covers it
+ }
+ for _, v := range bk.objs[k] {
+ if !v.Marker && !(exceptStragglers && v.Straggler) {
+ out = append(out, fmt.Sprintf("r%d:%s", r, k))
+ break
+ }
+ }
+ }
+ }
+ }
+ return out
+}
+
+// owed: an open park obligation names this region and a prefix of k.
+func (w *world) owed(r int, k string) bool {
+ if w.claim == nil {
+ return false
+ }
+ for _, o := range w.claim.Obl {
+ if o.Region == r && o.Prefix != "" && strings.HasPrefix(k, o.Prefix) {
+ return true
+ }
+ }
+ return false
+}
+
+func hasNonMarker(vs []*version) bool {
+ for _, v := range vs {
+ if !v.Marker {
+ return true
+ }
+ }
+ return false
+}
+
+// canStart is the start check and admission, computed without starting
+// anything: the final oracle never writes.
+func (w *world) canStart(e *box, c *claim) string {
+ if !w.admits(e, c, "") {
+ return "not admitted"
+ }
+ h := c.Holder
+ bg, binc := w.bucketGen(e, h.Location)
+ if bg != h.Gen || (bg != "" && binc != h.Inc) {
+ return fmt.Sprintf("generation.json %q, claim %q", bg, h.Gen)
+ }
+ if e.Files != nil && (e.Files.Gen != bg || e.Files.Inc != h.Inc) {
+ return fmt.Sprintf(".files-gen %q inc %d", e.Files.Gen, e.Files.Inc)
+ }
+ return ""
+}
+
func (w *world) final() {
if !w.quiescent() {
+ if len(w.pending) == 0 && len(w.console) == 0 && w.atRest() {
+ w.violate("INV-10: residue never retired: %v", w.residue())
+ return
+ }
w.violate("INV-3: no convergence after %d calm steps: %s%s", calmSteps, w.state(), w.boxesState())
return
}
@@ -250,11 +382,6 @@ func (w *world) final() {
if w.rec != nil {
w.violate("claim/record: claim free but record inc %d exists", w.rec.Inc)
}
- for r := 0; r < nRegions; r++ {
- if w.buckets[r].hasData("instances/"+host+"/", true) || w.buckets[r].hasData("moves/"+host+"/", true) {
- w.violate("INV-10: region %d still holds data for a freed host", r)
- }
- }
for _, b := range w.liveBoxes() {
if b.DB != nil || b.Files != nil {
w.violate("INV-10: box %d still holds local state for a freed host", b.ID)
@@ -266,37 +393,67 @@ func (w *world) final() {
if w.rec.Region != e.Region {
w.violate("claim/record: record region %d, claim serves from box %d in region %d", w.rec.Region, e.ID, e.Region)
}
- for r := 0; r < nRegions; r++ {
- if r != e.Region && (w.buckets[r].hasData("instances/"+host+"/", true) || w.buckets[r].hasData("moves/"+host+"/", true)) {
- w.violate("INV-10: region %d holds live-namespace data; the host serves from region %d", r, e.Region)
- }
- }
- if w.buckets[e.Region].hasData("moves/"+host+"/", true) {
- w.violate("INV-10: staging left in the serving region %d", e.Region)
- }
for _, b := range w.liveBoxes() {
if b != e && (b.DB != nil || b.Files != nil) {
w.violate("INV-10: box %d holds local state; the host serves from box %d", b.ID, e.ID)
}
}
- // make the serving box start, then check every acknowledged write
if !hasMain(e) {
- if !w.admits(e, c, "") || !w.spawn(e, c, holderLin(c.Holder), false) {
- w.violate("final: the serving box %d cannot start the host (%s) box: row=%+v db=%+v files=%+v cfg=%d live=%s/%d retired=%v fail=%v until=%d",
- e.ID, w.state(), e.Row, e.DB, e.Files, e.Config, e.Live, e.LiveInc, e.Retired, e.FailApp, e.ExecUntil)
+ if why := w.canStart(e, c); why != "" {
+ w.violate("final: the serving box %d cannot start the host: %s (%s)", e.ID, why, w.state())
return
}
}
- w.checkAcks(c, e, e.DB.Writes, "local")
- // and the replica path: replicate now, cold-restore, check again
- bl := &blob{Kind: "ltx", Inc: e.DB.Inc, Gen: e.DB.Gen, Writes: append([]int(nil), e.DB.Writes...), SealKey: e.DB.Key}
- w.complete(&request{kind: rPut, region: e.Region, key: "instances/" + host + "/ltx", b: bl})
- db := w.restore(e, c.Holder.Inc, c.Holder.Legacy, holderLin(c.Holder))
- if db == nil {
- w.violate("final: cold restore failed on box %d", e.ID)
+ // the serving box's database as it stands, or, if it has none, the
+ // cold restore it would do: computed, never written
+ local := e.DB
+ if local == nil {
+ local = w.restore(e, 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)
+ return
+ }
+ w.checkAcks(c, e, local.Writes, "local")
+ w.checkDurable(c, "final")
+}
+
+// checkDurable is the cold-restore promise, checked at every release to
+// serving and at the end: a restore of the claim's location and generation
+// in the serving region holds every acknowledged write that a completed
+// replica object ever held. It reads the bucket and writes nothing.
+func (w *world) checkDurable(c *claim, when string) {
+ if c == nil || c.Holder == nil {
+ return
+ }
+ e := w.execBox(c)
+ if e == nil {
return
}
- w.checkAcks(c, e, db.Writes, "cold restore")
+ db := w.restore(e, 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] {
+ seen[p] = true
+ for x := range w.durable[p] {
+ need[x] = true
+ }
+ }
+ have := map[int]bool{}
+ if db != nil {
+ for _, x := range db.Writes {
+ have[x] = true
+ }
+ }
+ for _, a := range w.acks {
+ if a.Inc != c.Holder.Inc || a.Exempt || a.Kind != "write" || !need[a.W] {
+ continue
+ }
+ if !have[a.W] {
+ w.violate("INV-2 (cold restore, %s): durable write %d (box %d, t=%d) lost", when, a.W, a.Box, a.At)
+ return
+ }
+ }
}
func (w *world) checkAcks(c *claim, e *box, writes []int, how string) {
@@ -332,8 +489,12 @@ func (w *world) state() string {
for _, o := range c.Obl {
obl += fmt.Sprintf(" %s:%s/r%d/b%d/%s", o.ID, o.Kind, o.Region, o.Box, o.Prefix)
}
- return fmt.Sprintf("op=%s/%s phase=%s land=%s src=%s rev=%s exec=%d obl=%d holder=%+v rec=%+v pending=%d console=%d obls=[%s] quiet=%v",
- c.Op.Kind, c.Op.ID, c.Op.Phase, c.Op.LandPhase, c.Op.SrcPhase, c.Op.RevPhase, c.Op.Exec, len(c.Obl), c.Holder, w.rec, len(w.pending), len(w.console), obl, c.Quiet)
+ adm := ""
+ for app, ad := range w.admit {
+ adm += fmt.Sprintf(" %s:closed=%v/reg=%d", app, ad.Closed, len(ad.Reg))
+ }
+ return fmt.Sprintf("op=%s/%s phase=%s land=%s src=%s rev=%s exec=%d obl=%d holder=%+v rec=%+v pending=%d console=%d obls=[%s] quiet=%v h2=%+v admission=[%s] residue=%v",
+ c.Op.Kind, c.Op.ID, c.Op.Phase, c.Op.LandPhase, c.Op.SrcPhase, c.Op.RevPhase, c.Op.Exec, len(c.Obl), c.Holder, w.rec, len(w.pending), len(w.console), obl, c.Quiet, w.h2, adm, w.residue())
}
// ---------- running ----------
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index d225b382c..e61d079b8 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -1,7 +1,12 @@
// Package hostlife is a deterministic, randomized model of the host
// lifecycle claim (docs/superpowers/specs/2026-10-02-host-lifecycle-claim-design.md,
-// rev 2) and Phase 1 of move-any-app
-// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 4).
+// rev 4, a3c86fa5) and Phase 1 of move-any-app
+// (docs/superpowers/specs/2026-10-02-move-any-app-design.md, rev 6).
+//
+// Since joint round 2 the model encodes what the specs say and nothing
+// stronger: restore reads the holder's location and the generation the
+// claim names, the start check compares markers, every multi-object step
+// is split at its real write boundaries, and the final oracle only reads.
//
// It is test-only. Nothing here is product code: every file is a _test.go
// file, so `go build ./...` never sees it. It exists to find interleavings
@@ -44,7 +49,9 @@ const (
stagingTTL = 400 // staging-work lease TTL: longer than the cut budget, as in production
probeTries = 3
readyWait = 800 // abort a move whose readiness never comes
- maxSkew = 1 // a box clock is within this of true time (SafeUntil's margin)
+ maxSkew = 1 // a box clock is within this of true time
+ maxPause = 3 // the claim's §3.1 bound on a pause between a check and the act
+ beyondH = 20 // one long-tail request in this many completes after H (R2-1)
)
// ---------- storage ----------
@@ -58,7 +65,8 @@ type blob struct {
Writes []int
Files *filesDir
Timers []int
- Refs []ref
+ Refs []ref // a park manifest's archive set
+ Dels []ref // a park manifest's deletion set, delete markers included
Text string
}
@@ -69,9 +77,10 @@ type ref struct {
}
type version struct {
- ID int
- B *blob
- Marker bool
+ ID int
+ B *blob
+ Marker bool
+ Straggler bool // created by a request that completed after H
}
type bucket struct {
@@ -139,6 +148,33 @@ func (b *bucket) hasData(prefix string, skipLock bool) bool {
return false
}
+// ---------- locations and generations (claim C3a, moves rev 6 §5.1) ----------
+
+// locationFor is holder.location for an incarnation.
+func locationFor(inc int, legacy bool) string {
+ if legacy {
+ return "instances/" + host + "/"
+ }
+ return fmt.Sprintf("instances/%s/%d/", host, inc)
+}
+
+// dataKey is a replica object of generation gen within location loc. The
+// origin generation keeps the bare layout; every later generation has its
+// own operation-scoped prefix, so a request from one generation that lands
+// late can only ever add an object to that generation.
+func dataKey(loc, gen, kind string) string {
+ if gen == "" {
+ return loc + kind
+ }
+ return loc + "g-" + gen + "/" + kind
+}
+
+func genMarkerKey(loc string) string { return loc + "generation.json" }
+
+func isDataKey(k string) bool {
+ return strings.HasPrefix(k, "instances/") && (strings.HasSuffix(k, "/base") || strings.HasSuffix(k, "/ltx"))
+}
+
// ---------- requests (late completion) ----------
type reqKind int
@@ -160,6 +196,7 @@ type request struct {
srcKey string
srcVer int
doneAt int
+ beyond bool // completes after H
by string
// result, for an immediate completion
resultVer int
@@ -185,6 +222,7 @@ func (f *filesDir) clone() *filesDir {
type localDB struct {
Inc int
+ Loc string // the holder location it was restored from (claim C3a)
Gen string // <dbPath>.gen
Key int // the key it was sealed with
Writes []int
@@ -237,6 +275,7 @@ type box struct {
DB *localDB
Files *filesDir
Config int // incarnation the config.env was rendered for; 0 none
+ CfgVer int // the bundle version it was rendered from
Live string // app the live symlink points at
LiveInc int
Timers []int // active once-timers (registration ids)
@@ -256,53 +295,59 @@ type box struct {
stopped map[string]bool
mem map[string]bool
evidAt map[string]int
+ sweepID string
pendingTimers []int
}
-// plan is a background pass's decision, taken now and acted on later: the
-// shape of every stale-writer race (J-N8).
+// plan is a host-specific write by a separate OS process
+// (carlos-config-sync, carlos-adopt), decided now and acted on later: the
+// shape of every stale-writer race (J-N8, J2-R2-3). It survives an agent
+// crash, because it is not the agent; a reboot ends it. It may pause
+// before it takes the host guard.
type plan struct {
Kind string // "config", "adopt"
Inc int
App string
+ Ver int // the config bundle version it selected
+ At int // it takes the guard no earlier than this
}
func (b *box) forget() {
b.Epoch++ // every goroutine of the old agent is gone
b.deferred = nil
- b.snap, b.plans, b.stopped, b.stale = nil, nil, nil, nil
+ b.snap, b.stopped, b.stale = nil, nil, nil
b.mem = map[string]bool{}
b.evidAt = map[string]int{}
+ b.sweepID = ""
b.pendingTimers = nil
}
// ---------- control plane ----------
type holder struct {
- Inc int
- App string
- Serial int // ground-truth creation event (model only)
- Legacy bool
- Lineage lineage
- FilesGen string // the files generation compatible with the lineage
-}
-
-type lineage struct {
- Op string // "" = origin
- Region int
- Ver int // version of instances/<host>/base in Region
+ Inc int
+ App string
+ Serial int // ground-truth creation event (model only)
+ Legacy bool
+ // Location is holder.location (claim C3a): instances/<host>/<inc>/ for a
+ // new incarnation, instances/<host>/ for an adopted legacy host. It never
+ // changes while this holder holds the host.
+ Location string
+ // Gen is the generation within the location that the claim names as
+ // 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
}
type obligation struct {
- ID string
- Op string
- Kind string // park-replica, park-local, park-superseded, park-staging
- Region int
- Box int
- Prefix string
- Ret string
- Quiet int // not before
- Exclude string // lineage to leave in place (a push parks only the old one)
+ ID string
+ Op string
+ Kind string // park-replica, park-local, park-superseded, park-staging
+ Region int
+ Box int
+ Prefix string
+ Ret string
+ Quiet int // not before
}
type opState struct {
@@ -333,7 +378,6 @@ type opState struct {
SealQuiet int
LandPhase string
Installed digest
- BaseVer int
ProbeTries int
ProbedAt int
RevPhase string
@@ -350,6 +394,7 @@ type opState struct {
Committed bool
Opened bool
ParkLocalNow bool
+ PinVer int // move.inputs: the bundle version pinned at admission
Auto bool
ReqAt int
Repl string
@@ -379,6 +424,41 @@ type claim struct {
Retired []int
Quiet [nRegions]int
PurgeRes bool
+ // Cancelled is cancelled_creates (claim rev 4 §5.1, J2-R2-7): creates
+ // recovery cancelled, so a late record PUT can be removed. It survives free.
+ Cancelled []cancelledCreate
+}
+
+type cancelledCreate struct {
+ Inc int
+ Until int
+}
+
+// liteHost is a second hostname of the same apps, modelled for the
+// control plane only: create, app admission and purge (J2-R2-2).
+type liteHost struct {
+ Inc int
+ App string
+ Kind string // "", "creating", "serving", "purging"
+ OpID string
+ Rec bool // its record is published
+ At int
+}
+
+// admission is apps/<acct>/<app>/admission.json (claim rev 4 §5.1 step 0).
+type admission struct {
+ Closed bool
+ Reg map[string]regEntry // create id -> registration
+}
+
+type regEntry struct {
+ Host string
+ Until int // a registration is a lease: a create claims before it ends (CC16)
+}
+
+type pendingRec struct {
+ rec *record
+ at int
}
type record struct {
@@ -387,6 +467,12 @@ type record struct {
App string
Region int
MoveID string
+ // MoveState is the record's move journal state for the four transitions
+ // the moves spec makes record-first (§7.5, §7.8, §7.9): "landing" after
+ // the flip, "committed", "rolling_back". The claim follows each.
+ MoveState string
+ RollbackID string
+ Reason string
}
// ---------- the world ----------
@@ -397,7 +483,7 @@ type ack struct {
Box int
At int
Kind string // "write" or "timer"
- Exempt bool // lost under a declared loss (M16)
+ Exempt bool // lost under a declared loss (M16) or past the last checkpoint of a lost disk
}
type world struct {
@@ -411,14 +497,20 @@ type world struct {
claim *claim // nil = absent
rec *record
stores map[string]bool
+ cfgVer map[string]int // each app's current config bundle version
purgeRes map[string]bool
purgeStep map[string]int // the reservation's durable phase (purge journal)
+ admit map[string]*admission
+ h2 liteHost
+ recPend *pendingRec // a record PUT whose response was lost
floor bool
buckets [nRegions]*bucket
control *bucket
boxes []*box
pending []*request
acks []ack
+ durable map[string]map[int]bool // per generation prefix: writes a completed replica object holds
+ genParent map[string]string // generation prefix -> the one it superseded
nextW int
nextInc int
serial int
@@ -527,6 +619,7 @@ func (c *claim) clone() *claim {
n.Obl = append([]obligation(nil), c.Obl...)
n.Lost = append([]int(nil), c.Lost...)
n.Retired = append([]int(nil), c.Retired...)
+ n.Cancelled = append([]cancelledCreate(nil), c.Cancelled...)
return &n
}
@@ -580,6 +673,12 @@ func (w *world) issue(actorBox int, r *request) int {
if w.rng.Intn(4) == 0 {
r.doneAt = w.now + horizonH // as late as the signature-age limit allows
}
+ if w.rng.Intn(beyondH) == 0 {
+ // accepted before the signature limit, completed after it: S3
+ // bounds acceptance, not completion (claim C3a, J2-R2-1)
+ r.doneAt = w.now + horizonH + 1 + w.rng.Intn(10*horizonH)
+ r.beyond = true
+ }
}
r.by = fmt.Sprintf("box:%d", actorBox)
w.pending = append(w.pending, r)
@@ -591,8 +690,9 @@ func (w *world) complete(r *request) int {
bk := w.buckets[r.region]
switch r.kind {
case rPut:
- v := &version{ID: w.newVer(), B: r.b}
+ v := &version{ID: w.newVer(), B: r.b, Straggler: r.beyond}
bk.objs[r.key] = append(bk.objs[r.key], v)
+ w.markDurable(r.key, r.b)
return v.ID
case rDelVer:
vs := bk.objs[r.key]
@@ -612,18 +712,57 @@ func (w *world) complete(r *request) int {
if src == nil || src.Marker {
return 0
}
- v := &version{ID: w.newVer(), B: src.B}
+ v := &version{ID: w.newVer(), B: src.B, Straggler: r.beyond}
bk.objs[r.key] = append(bk.objs[r.key], v)
+ w.markDurable(r.key, src.B)
return v.ID
}
return 0
}
+// markDurable: a write is durable in a generation once a completed replica
+// object of that generation holds it. The cold-restore checks (§14.2.3)
+// require every write durable in the claim's generation or in any
+// generation it superseded.
+func (w *world) markDurable(key string, b *blob) {
+ if b == nil || !isDataKey(key) {
+ return
+ }
+ p := key[:strings.LastIndex(key, "/")+1]
+ if w.durable[p] == nil {
+ w.durable[p] = map[int]bool{}
+ }
+ for _, x := range b.Writes {
+ w.durable[p][x] = true
+ }
+}
+
+// isDurable: W is durable anywhere (the disk-loss fault's RPO line).
+func (w *world) isDurable(x int) bool {
+ for _, m := range w.durable {
+ if m[x] {
+ return true
+ }
+ }
+ return false
+}
+
+// newGen records that the claim's generation moved from old to gen within
+// loc, so the durability promise carries over.
+func (w *world) newGen(loc, old, gen string) {
+ if old != gen {
+ w.genParent[dataKey(loc, gen, "")] = dataKey(loc, old, "")
+ }
+}
+
func (w *world) completeDue(force bool) {
var keep []*request
for _, r := range w.pending {
if force || r.doneAt <= w.now {
w.complete(r)
+ if r.beyond {
+ w.stats["completed beyond H"]++
+ }
w.logf("late completion %v %s r%d (%s)", r.kind, r.key, r.region, r.by)
} else {
keep = append(keep, r)