amadan

carlos / platform Public

sim: hostlife: claim rev 6.9, no local database reuse, warm and cold only, writer_box and writes_lost, admission bound to the operation, close evidence by client outcome (rev 7.10)

Joint round 9. Every admitted writer purges its local database (an
error-returning purge; a transient fault) and restores from the certified
remote: warm up to the certificate's max_txid, cold from the predecessor
generation (a prepared install generation is opened by its probe's cold
admission and never re-entered; a fresh one starts empty and roots at the
writer's full first upload, before its marker). holder.writer_box names
the current writer; a cold admission of an uncertified session records
writes_lost {box, generation, session, remote_max_txid} and alerts, and
the acknowledged unuploaded writes are declared lost, never silently.
Only warm and cold survive: open, fresh, the installation generation and
the recovery journal are gone; holder.generation is the only authoritative
generation; a clean rollback's return names the source's generation again.
The admission CAS is bound to the observed op.id, phase and kind (INV-13).
Close evidence is client-observed success for every request class, with
a sticky uncertainty for a timeout or a lost response. The pre-cut source
certifies; the idle stop kills the cgroup. Rules remote-baseline,
writes-lost, admit-bind-op replace warm-provenance; witnesses for the
stale local database after a clean close, the silent loss, the stale
closure during a delete, a maintenance retry and a lost response; the
empty install witnessed through a move; the whole-start-check witness
retired (subsumed by regional restores). 92 rules, 52 witnesses.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
claude 7a7568c3b158f379288b2a94a8df3f8b2e741838 parent 831a2ea
10 files changed, +904 −539
  • internal/sim/hostlife/background_test.go +15 −5
  • internal/sim/hostlife/console_test.go +5 −4
  • internal/sim/hostlife/expected-outcomes.txt +2 −1
  • internal/sim/hostlife/ltx_test.go +35 −12
  • internal/sim/hostlife/moves_test.go +61 −94
  • internal/sim/hostlife/protocol_test.go +493 −304
  • internal/sim/hostlife/rules_test.go +3 −1
  • internal/sim/hostlife/sim_test.go +2 −5
  • internal/sim/hostlife/witness_test.go +205 −42
  • internal/sim/hostlife/world_test.go +83 −71
diff --git a/internal/sim/hostlife/background_test.go b/internal/sim/hostlife/background_test.go
index 047da526d..a12609c38 100644
--- a/internal/sim/hostlife/background_test.go
+++ b/internal/sim/hostlife/background_test.go
@@ -38,14 +38,17 @@ func (w *world) idleStop(b *box) {
return
}
w.replicate(b)
+ // the unit stop kills the cgroup: the main process and every descendant
+ // placed in it; an escaped descendant survives, and while it lives the
+ // session cannot certify (rev 7.10)
var keep []*proc
for _, p := range b.Procs {
- if !p.Main {
+ if !p.Main && !p.Strict {
keep = append(keep, p)
}
}
b.Procs = keep
- // the clean close (claim rev 6.6 §6.4a): drain, then closed.json
+ // the clean close (claim rev 6.9 §6.4a): drain, then the certificate
if b.DB != nil {
b.DB.Closing = true
w.closeStep(b)
@@ -358,8 +361,7 @@ func (w *world) fault() {
}
}
b.DB = nil
- b.lineage = nil // the lineage file goes with the disk
- b.Procs = nil // nothing survives the disk: a descendant with no database would acknowledge writes into nowhere
+ b.Procs = nil // nothing survives the disk: a descendant with no database would acknowledge writes into nowhere
w.stats["disk-lost with the crash"]++
w.logf("box %d lost its disk with the crash", b.ID)
}
@@ -371,6 +373,15 @@ func (w *world) fault() {
b.plans = nil // a reboot ends every process
b.AgentDown, b.Frozen, b.AgentPaused = false, false, false
b.forget()
+ if w.rng.Intn(6) == 0 {
+ // the purge of the local database the next admitted writer must
+ // make returns an error for a while (claim rev 6.9): the writer
+ // does not start
+ b.PurgeFails = !b.PurgeFails
+ if b.PurgeFails {
+ w.stats["purge failures injected"]++
+ }
+ }
if w.rng.Intn(8) == 0 && len(b.Stamps) > 0 {
// the local stamp record is lost with the reboot: the box
// refuses every writer until it re-initializes from a fresh
@@ -438,7 +449,6 @@ func (w *world) fault() {
}
}
b.DB = nil
- b.lineage = nil
w.stats["disk-lost"]++
w.logf("box %d lost its database file", b.ID)
}
diff --git a/internal/sim/hostlife/console_test.go b/internal/sim/hostlife/console_test.go
index be458ceb8..61ab14485 100644
--- a/internal/sim/hostlife/console_test.go
+++ b/internal/sim/hostlife/console_test.go
@@ -330,7 +330,7 @@ func (w *world) userDelete() {
if c == nil || c.Holder == nil {
return
}
- if on("claim-op-exclusive") && c.Op.Kind != "serving" || c.Op.Rec != nil {
+ if on("claim-op-exclusive") && c.Op.Kind != "serving" {
return
}
id := w.newID("del")
@@ -363,7 +363,7 @@ func (w *world) userDelete() {
func (w *world) userMove() {
c := w.claim
- if c == nil || c.Holder == nil || c.Op.Kind != "serving" || c.Op.Rec != nil {
+ if c == nil || c.Holder == nil || c.Op.Kind != "serving" {
return
}
if src := w.execBox(c); src == nil || src.Destroyed {
@@ -403,7 +403,8 @@ func (w *world) moveTo(r int) {
return false
}
n.Op = opState{Kind: "moving", ID: id, Phase: "leases", Exec: src.ID, Parts: []int{src.ID, tgt.ID},
- Src: src.ID, Tgt: tgt.ID, SrcRegion: src.Region, TgtRegion: r, ReqAt: w.now, Auto: true, App: c.Holder.App}
+ Src: src.ID, Tgt: tgt.ID, SrcRegion: src.Region, TgtRegion: r, ReqAt: w.now, Auto: true, App: c.Holder.App,
+ SrcGen: c.Holder.Gen} // the source's generation, which a clean rollback's return names again (rev 7.10)
return true
}) {
w.logf("move %s inc %d from box %d to box %d", id, c.Holder.Inc, src.ID, tgt.ID)
@@ -412,7 +413,7 @@ func (w *world) moveTo(r int) {
func (w *world) userPush() {
c := w.claim
- if c == nil || c.Holder == nil || c.Op.Kind != "serving" || c.Op.Rec != nil {
+ if c == nil || c.Holder == nil || c.Op.Kind != "serving" {
return
}
b := w.execBox(c)
diff --git a/internal/sim/hostlife/expected-outcomes.txt b/internal/sim/hostlife/expected-outcomes.txt
index bd5afdee9..cfb23c5e5 100644
--- a/internal/sim/hostlife/expected-outcomes.txt
+++ b/internal/sim/hostlife/expected-outcomes.txt
@@ -11,11 +11,12 @@ watchdog-independent missed caught with declare-lost-compute (witness; sweep 3 /
exec-admission missed one of four admission fences (claim rev 6.8.1 adds exec-writer); caught with hold-op-open, start-check-claim-gen and exec-writer
hold-op-open missed one of four admission fences; caught with exec-admission, start-check-claim-gen and exec-writer
start-check-claim-gen missed one of four admission fences; caught with exec-admission, hold-op-open and exec-writer
-start-check missed caught with exec-admission, hold-op-open and exec-writer
+start-check missed subsumed since rev 7.10: a box restores only its own region's remote of holder.generation, so with the whole start check gone the stale source of a cross-region move finds nothing to restore and cannot start beside the target; the witness is retired, the generation clause (start-check-claim-gen) keeps its witness
strict-spawn missed caught with evidence-whole-tree
touched-incomplete missed caught with legacy-discovery
door-reread missed subsumed by C3a and, since rev 7.8, by writer epochs (claim rev 6.6): a recreated incarnation writes into a fresh generation the listing never selects; its witness is retired
door-by-version missed subsumed by C3a and, since rev 7.8, by writer epochs (claim rev 6.6): a recreated incarnation writes into a fresh generation the listing never selects; its witness is retired
registration-check missed a cheap extra: subsumed by purge-claim-fence and fence-etag together
exec-writer missed one of four admission fences (claim rev 6.8.1): the AdmitWriter CAS refuses a box that is not op.exec; caught with exec-admission, hold-op-open and start-check-claim-gen (witness)
+admit-bind-op missed caught with claim-cas-opid: the model's general CAS condition on op.id (C2) already refuses a closure whose operation changed; the binding adds the phase and the kinds in which no writer opens, and its witness needs both gone
exec-admission,hold-op-open,start-check-claim-gen missed the three box-side fences alone (rev 7.5's admission triple): under writer sessions the old source's wake has no certificate for the current session, and the AdmitWriter CAS alone refuses a box that is not op.exec (claim rev 6.8.1, exec-writer); the four-rule combination with exec-writer is the one that fails
diff --git a/internal/sim/hostlife/ltx_test.go b/internal/sim/hostlife/ltx_test.go
index 4bcd5f384..461a01d4b 100644
--- a/internal/sim/hostlife/ltx_test.go
+++ b/internal/sim/hostlife/ltx_test.go
@@ -306,18 +306,29 @@ func isClosedKey(k string) bool {
return i >= 0 && strings.HasSuffix(k, ".json")
}
-// track records a request the writer issued that did not return at once,
-// for the clean close's evidence (R8-5).
+// track records a request the writer issued whose success the client did
+// not see at once, for the clean close's evidence (R8-5, R9-5): every
+// class, level-0, compaction, snapshot and retention. A request the server
+// refused is a failure the client saw: the session is uncertain for good.
func (db *localDB) track(r *request, v int) {
- if v <= 0 && !r.done {
- db.Issued = append(db.Issued, r)
+ if v > 0 {
+ return // client-observed success
}
+ if r.done {
+ db.Uncertain = true // refused
+ return
+ }
+ db.Issued = append(db.Issued, r)
}
-// settled: every request the writer issued over its lifetime has returned
-// success and none was ever retried after a timeout (R8-5). The mutation
-// of close-evidence looks at the level-0 queue alone, as rev 7.8 did.
-func (db *localDB) settled() bool {
+// settled: every request the writer issued over its lifetime returned
+// success to the client, within the client's wait, and none was retried
+// after a timeout (R8-5, R9-5). A request still outstanding within the wait
+// is not yet settled; one the client gave up on, whether it later
+// completed on the server or not, makes the session uncertain for good,
+// since its outcome was never observed. The mutation of close-evidence
+// looks at the level-0 queue alone, as rev 7.8 did.
+func (db *localDB) settled(now int) bool {
queued := len(db.Queue) == 0 && (db.InFlight == nil || db.InFlight.done)
if !on("close-evidence") {
return queued
@@ -327,6 +338,14 @@ func (db *localDB) settled() bool {
}
for _, r := range db.Issued {
if !r.done {
+ if now-r.at >= uploadTimeout {
+ db.Uncertain = true // the client gave up: timeout
+ return false
+ }
+ return false // still waiting
+ }
+ if r.doneAt-r.at >= uploadTimeout {
+ db.Uncertain = true // completed after the client gave up: a lost response
return false
}
}
@@ -343,7 +362,11 @@ func (db *localDB) settled() bool {
// stops.
func (w *world) closeStep(b *box) {
db := b.DB
- if db == nil || !db.Closing || hasMain(b) {
+ if db == nil || !db.Closing || len(b.Procs) > 0 {
+ // nothing of the host may run when the session certifies: a
+ // descendant that outlived the main process can still acknowledge
+ // writes the certificate would not cover, which the next admission's
+ // purge would lose silently (rev 7.10; seed 17 / 300)
return
}
// the certificate is the live generation's: once an operation has
@@ -356,8 +379,8 @@ func (w *world) closeStep(b *box) {
// rollback's source was admitted cold at every wake and the rollback
// never released)
c := w.claim
- inside := c != nil && (c.Op.Kind == "serving" || c.Op.Kind == "landing" || c.Op.Kind == "restoring" || c.Op.Kind == "reverting")
- if c == nil || c.Holder == nil || !inside || c.Op.Exec != b.ID || c.Holder.Inc != db.Inc || (db.Gen != c.Holder.Gen && db.Gen != w.opGen(&c.Op)) {
+ inside := c != nil && (c.Op.Kind == "serving" || c.Op.Kind == "moving" || c.Op.Kind == "landing" || c.Op.Kind == "restoring" || c.Op.Kind == "reverting")
+ if c == nil || c.Holder == nil || !inside || c.Op.Exec != b.ID || c.Holder.Inc != db.Inc || db.Gen != c.Holder.Gen {
// a push, a move's cut, a delete or a purge is taking this writer
// over: its generation is being replaced or parked, and a
// certificate written into it now would outlive the park (seed
@@ -367,7 +390,7 @@ func (w *world) closeStep(b *box) {
return
}
w.ship(b)
- if !db.settled() && on("close-waits") {
+ if !db.settled(w.now) && on("close-waits") {
if db.Uncertain && on("close-evidence") {
// a request of this writer timed out and was retried: its outcome
// is unknown for good, so this session never certifies
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index e79640d55..93ca71fb7 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -172,32 +172,6 @@ func (w *world) role(b *box, c *claim) {
if c.Holder == nil {
return
}
- if r := c.Op.Rec; r != nil && r.Box != c.Op.Exec && (c.Op.Exec == b.ID || c.Op.Exec == -1 && w.isParticipant(c, b)) {
- // the admitting box lost op.exec before its build finished (a
- // rollback's release of the target, a declared loss): its cold
- // admission is abandoned by whoever holds op.exec next, and the
- // generation it was building is parked as a chore (seed 58795 /
- // 100,000: the source's rollback probe could not be admitted behind
- // the lost target's build)
- if w.cas(c, func(n *claim) bool {
- if n.Op.Rec == nil || n.Op.Rec.Gen != r.Gen || n.Op.Rec.Box == n.Op.Exec {
- return false
- }
- n.Obl = append(n.Obl, w.newObl(n, "park-generation", r.Region, -1, c.Holder.Location, r.Gen, w.now+horizonH))
- n.Op.Rec = nil
- return true
- }) {
- w.logf("box %d: cold admission %s of box %d abandoned, its exec is gone (op %s/%s exec %d)", b.ID, r.Gen, r.Box, c.Op.Kind, c.Op.ID, c.Op.Exec)
- w.stats["cold admissions abandoned"]++
- }
- return
- }
- if c.Op.Rec != nil && c.Op.Rec.Box == b.ID {
- // a cold admission's build runs under the operation, by the box it
- // admitted, before the operation's own step (claim rev 6.8 §6.4a, R8-2)
- w.recStep(b, c)
- return
- }
switch c.Op.Kind {
case "moving":
if b.ID == c.Op.Src {
@@ -719,6 +693,9 @@ func (w *world) revertSource(b *box, c *claim) {
w.cas(c, func(n *claim) bool { n.Op.RevPhase = "probed"; return sameOp(n.Op.ID, op.ID) })
return
}
+ if b.open != nil {
+ return // admitted, waiting for its PUT: not a failed try
+ }
w.cas(c, func(n *claim) bool {
n.Op.ProbeTries++
if n.Op.ProbeTries >= probeTries*3 {
@@ -776,6 +753,7 @@ func (w *world) followRecord(c *claim) bool {
}
n.Op.Kind, n.Op.Exec, n.Op.LandPhase, n.Op.FlipAt = "landing", op.Tgt, "checking", w.now
n.Op.SrcStamp = n.Holder.Stamp // the source installation's stamp, kept in the journal for the return (claim rev 6.5)
+ n.Op.SrcGen = n.Holder.Gen // the source's generation at the cut, which a clean rollback's return names again (rev 7.10)
n.Holder.Stamp = w.issueStamp(n, op.Tgt) // holder.stamp: the gen this CAS produces, the landing's installation stamp (claim rev 6.5 §2)
n.Op.FlipGen = n.Holder.Stamp
return true
@@ -785,9 +763,7 @@ func (w *world) followRecord(c *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, w.opGen(&op))
- n.Holder.Gen = w.opGen(&op) // the claim names the generation restore reads (C3a)
+ n.Op.Committed = true // holder.generation moved at the probe's cold admission (claim rev 6.9)
q := op.StopAt + horizonH
if !on("quiet-before-ack") {
q = 0
@@ -819,7 +795,7 @@ func (w *world) landTarget(b *box, c *claim) {
return
}
loc := c.Holder.Location
- g := w.opGen(&op) // the generation this landing installs (R8-2: a cold admission within it may have moved it)
+ g := installGen(&op) // the generation this landing prepares; the probe's cold admission makes it holder.generation (claim rev 6.9)
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
@@ -919,10 +895,10 @@ func (w *world) landTarget(b *box, c *claim) {
w.cas(c, func(n *claim) bool { n.Op.LandPhase = "published"; return sameOp(n.Op.ID, op.ID) })
}
case "published":
- v := w.publishGen(b, loc, g, c.Holder.Inc, op.BaseVer, op.BaseKey, op.BaseTX)
- if v > 0 {
- w.cas(c, func(n *claim) bool { n.Op.LandPhase, n.Op.Fresh = "local", true; return sameOp(n.Op.ID, op.ID) })
- }
+ // the build is complete; generation.json is published by the probe's
+ // cold admission, after readiness and before its first upload (claim
+ // rev 6.9 §6.4a)
+ w.cas(c, func(n *claim) bool { n.Op.LandPhase = "local"; return sameOp(n.Op.ID, op.ID) })
case "local":
w.installLocal(b, c, g, op.SealFiles, op.LandPhase, func(n *claim) { n.Op.LandPhase = "config" })
case "config":
@@ -941,24 +917,17 @@ func (w *world) landTarget(b *box, c *claim) {
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.Gen != g {
- if b.DB != nil {
- // an earlier stay's database: retire-artifacts of its stamp,
- // never of the installation checking activated
- if b.DB.Stamp == b.stampOf(c.Holder.Inc) {
- w.violate("INV-6: landing on box %d would park a database tagged with its own active stamp %d", b.ID, b.DB.Stamp)
- }
- w.retireDatabase(b, c.Holder.Inc, b.DB.Stamp)
- }
- if b.DB = w.restoreInit(b, c.Holder.Inc, loc, g); b.DB == nil && w.restoreCalc(b.Region, c.Holder.Inc, loc, g) != nil {
- return // the anchor is outstanding: try again
- }
- }
- if b.DB == nil {
+ // the installed digest, for the settle check's dirty verdict, from a
+ // restore of the prepared generation computed and not kept: the
+ // probe's admission restores the database it starts on (claim rev
+ // 6.9: a box never reuses a local database)
+ tmp := *b
+ tmp.DB = w.restorePinned(b.Region, c.Holder.Inc, loc, g, op.BaseKey, op.BaseVer, op.BaseTX)
+ if tmp.DB == nil {
w.rollback(c, "restore failed")
return
}
- d := w.digestOf(b)
+ d := w.digestOf(&tmp)
w.cas(c, func(n *claim) bool { n.Op.Installed, n.Op.LandPhase = d, "probing"; return sameOp(n.Op.ID, op.ID) })
case "probing":
if w.now > op.CutDeadline {
@@ -975,6 +944,9 @@ func (w *world) landTarget(b *box, c *claim) {
w.cas(c, func(n *claim) bool { n.Op.LandPhase, n.Op.ProbedAt = "probed", w.now; return sameOp(n.Op.ID, op.ID) })
return
}
+ if b.open != nil {
+ return // admitted, waiting for its PUT: not a failed try
+ }
tries := op.ProbeTries + 1
w.cas(c, func(n *claim) bool { n.Op.ProbeTries = tries; return sameOp(n.Op.ID, op.ID) })
if tries >= probeTries {
@@ -989,16 +961,16 @@ func (w *world) landTarget(b *box, c *claim) {
if !hasMain(b) {
// the probe died in its settle window (a crash, an agent
// restart): the landing restarts only the probe (§7.14), a
- // writer admitted like any other (claim rev 6.8 §6.4a, R8-2);
- // a cold admission's build runs first (recStep)
- if c.Op.Rec != nil {
- return
- }
- if w.spawn(b, c, g, true) {
+ // writer admitted like any other (claim rev 6.9 §6.4a, R8-2):
+ // cold, into a fresh generation restored from the dead probe's
+ if w.spawn(b, c, c.Holder.Gen, true) {
w.stats["probe restarted"]++
w.cas(c, func(n *claim) bool { n.Op.ProbedAt = w.now; return sameOp(n.Op.ID, op.ID) })
return
}
+ if b.open != nil {
+ return // admitted, waiting for its PUT: not a failed try
+ }
tries := op.ProbeTries + 1
w.cas(c, func(n *claim) bool { n.Op.ProbeTries = tries; return sameOp(n.Op.ID, op.ID) })
if tries >= probeTries {
@@ -1156,7 +1128,12 @@ func (w *world) releaseTarget(b *box, c *claim) {
return
}
dirty := false
- if op.LandPhase == "probing" || op.LandPhase == "probed" {
+ if (op.LandPhase == "probing" || op.LandPhase == "probed") && b.DB != nil {
+ // a target without a database never opened: nothing to return.
+ // Since rev 7.10 the probe's admission restores the database, so
+ // a target whose probe never started has none (seed 62 / 300:
+ // a spurious dirty return sealed an empty database and the
+ // source restored it)
dirty = w.digestOf(b) != op.Installed
}
if !on("dirty-return") {
@@ -1269,6 +1246,14 @@ func (w *world) recoverSource(b *box, c *claim) {
if on("return-stamp") {
n.Holder.Stamp = op.SrcStamp
}
+ // and, for a clean rollback, the source's generation (rev
+ // 7.10 §7.14): the target's probe moved holder.generation to
+ // its own; the target wrote nothing, and the source's probe
+ // restores from the predecessor generation's remote in its
+ // own region
+ if !op.Dirty && n.Holder.Gen != op.SrcGen {
+ n.Holder.Gen = op.SrcGen // "" is the origin generation
+ }
return true
})
}
@@ -1306,7 +1291,7 @@ func (w *world) recoverSource(b *box, c *claim) {
if sv == nil {
return // the lane is gone: wait (stuck, in time)
}
- g := w.opGen(&op)
+ g := installGen(&op)
if sv.B.Max == 0 && on("valid-ltx") {
w.cas(c, func(n *claim) bool {
n.Op.SrcPhase, n.Op.BaseVer, n.Op.BaseKey, n.Op.BaseTX = "published", 0, "", 0
@@ -1327,16 +1312,13 @@ func (w *world) recoverSource(b *box, c *claim) {
})
}
case "install-anchor":
- if w.anchorAcked(b, c.Holder.Location, w.opGen(&op), op.BaseKey, op.BaseVer, op.BaseTX) {
+ if w.anchorAcked(b, c.Holder.Location, installGen(&op), op.BaseKey, op.BaseVer, op.BaseTX) {
w.cas(c, func(n *claim) bool { n.Op.SrcPhase = "published"; return sameOp(n.Op.ID, op.ID) })
}
case "published":
- v := w.publishGen(b, c.Holder.Location, w.opGen(&op), c.Holder.Inc, op.BaseVer, op.BaseKey, op.BaseTX)
- if v > 0 {
- w.cas(c, func(n *claim) bool { n.Op.SrcPhase, n.Op.Fresh = "local", true; 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) }) // the marker is the probe's admission's (claim rev 6.9)
case "local":
- w.installLocal(b, c, w.opGen(&op), op.ReturnFiles, "", func(n *claim) { n.Op.SrcPhase = "config" })
+ w.installLocal(b, c, installGen(&op), op.ReturnFiles, "", func(n *claim) { n.Op.SrcPhase = "config" })
case "config":
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) })
@@ -1346,12 +1328,15 @@ func (w *world) recoverSource(b *box, c *claim) {
}
want := c.Holder.Gen
if op.Dirty {
- want = w.opGen(&op)
+ want = installGen(&op) // the return generation prepared from the target's sealed copy
}
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
}
+ if b.open != nil {
+ return // admitted, waiting for its PUT: not a failed try
+ }
w.logf("box %d: the rollback's probe did not start (try %d, generation %q, db=%v)", b.ID, op.ProbeTries+1, want, b.DB != nil)
w.cas(c, func(n *claim) bool {
n.Op.ProbeTries++
@@ -1361,11 +1346,11 @@ func (w *world) recoverSource(b *box, c *claim) {
return sameOp(n.Op.ID, op.ID)
})
case "probed":
- if op.Dirty && c.Holder.Gen != w.opGen(&op) {
+ if op.Dirty && !op.ReturnParked {
+ // holder.generation and holder.stamp moved at the probe's cold
+ // admission (claim rev 6.9); the return lane's park is owed
w.cas(c, func(n *claim) bool {
- w.newGen(n.Holder.Location, n.Holder.Gen, w.opGen(&n.Op))
- n.Holder.Gen = w.opGen(&n.Op)
- n.Holder.Stamp = w.issueStamp(n, op.Src) // a dirty rollback installs a new generation: a new stamp, never the predecessor's (claim rev 6.5 §6.4)
+ n.Op.ReturnParked = true
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)
})
@@ -1384,7 +1369,7 @@ func (w *world) recoverSource(b *box, c *claim) {
func (w *world) pushStep(b *box, c *claim) {
op := c.Op
loc := c.Holder.Location
- g := w.opGen(&op) // the generation this push installs (R8-2)
+ g := installGen(&op) // the generation this push prepares; its probe's cold admission makes it holder.generation (claim rev 6.9)
switch op.Phase {
case "stopping":
w.holdRow(b, "moving", op.ID, c)
@@ -1439,25 +1424,10 @@ func (w *world) pushStep(b *box, c *claim) {
w.cas(c, func(n *claim) bool { n.Op.Phase = "published"; return sameOp(n.Op.ID, op.ID) })
}
case "published":
- v := w.publishGen(b, loc, g, c.Holder.Inc, op.BaseVer, op.BaseKey, op.BaseTX)
- if v > 0 {
- w.cas(c, func(n *claim) bool { n.Op.Phase, n.Op.Fresh = "restore", true; 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) }) // the marker is the probe's admission's (claim rev 6.9)
case "restore":
- if b.DB != nil && b.DB.Gen != g {
- w.retireDatabase(b, c.Holder.Inc, b.DB.Stamp) // the files are carried (F7)
- }
- if b.DB == nil {
- b.DB = w.restoreInit(b, c.Holder.Inc, loc, g)
- }
- 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 = g
- }
+ // the probe's admission restores the database (claim rev 6.9); the
+ // files are unchanged and carried (F7)
// every probe renders config and materializes the release for the
// held row first (the passes skip held rows): RenderHeld, MaterializeHeld
if !b.HasKey {
@@ -1471,10 +1441,7 @@ func (w *world) pushStep(b *box, c *claim) {
}
if hasMain(b) || w.spawn(b, c, g, true) {
w.cas(c, func(n *claim) bool {
- n.Op.Phase = "probed"
- w.newGen(n.Holder.Location, n.Holder.Gen, w.opGen(&n.Op))
- n.Holder.Gen = w.opGen(&n.Op)
- n.Holder.Stamp = w.issueStamp(n, n.Op.Exec) // a push's commit installs a new generation: a new stamp (claim rev 6.5 §2)
+ n.Op.Phase = "probed" // holder.generation and holder.stamp moved at the probe's cold admission (claim rev 6.9)
q := op.StopAt + horizonH
if q > n.Quiet[b.Region] {
n.Quiet[b.Region] = q
@@ -1509,7 +1476,7 @@ func sameStep(a, b *claim) bool {
if a.Holder != nil && (a.Holder.Session != b.Holder.Session || a.Holder.Gen != b.Holder.Gen || a.Holder.Stamp != b.Holder.Stamp) {
return false
}
- if (x.Rec == nil) != (y.Rec == nil) || x.Rec != nil && (x.Rec.Gen != y.Rec.Gen || x.Rec.Phase != y.Rec.Phase) {
+ if a.Holder != nil && a.Holder.WriterBox != b.Holder.WriterBox {
return false
}
return len(x.Writers) == len(y.Writers)
@@ -1712,8 +1679,8 @@ func (w *world) publishGen(b *box, loc, gen string, inc int, base int, key strin
// mutation of restore-anchor writes none; the mutation of anchor-acked
// does not wait.
func (w *world) anchorAcked(b *box, loc, gen, snapKey string, snapVer, tx int) bool {
- if !on("restore-anchor") || tx == 0 {
- return true // no transactions yet: there is no position to anchor
+ if !on("restore-anchor") || tx == 0 && on("valid-ltx") {
+ return true // no transactions yet: there is no position to anchor (the mutation of valid-ltx writes [0,0], which the encoder refuses)
}
sv := w.buckets[b.Region].byID(snapKey, snapVer)
if sv == nil {
diff --git a/internal/sim/hostlife/protocol_test.go b/internal/sim/hostlife/protocol_test.go
index 49f0a1294..6d18fb387 100644
--- a/internal/sim/hostlife/protocol_test.go
+++ b/internal/sim/hostlife/protocol_test.go
@@ -171,6 +171,18 @@ func (w *world) evidence(b *box, opID string) bool {
// contract refuses. With restore-by-generation off it is the mutation: the
// newest object under the location.
func (w *world) restoreCalc(r int, inc int, loc, gen string) *localDB {
+ return w.restoreWith(r, inc, loc, gen, "", 0, -1)
+}
+
+// restorePinned is the restore of an operation's prepared generation before
+// its marker is published (rev 7.10 §7.14): the snapshot identity comes
+// from the operation's build journal instead of generation.json; tx 0 is
+// an empty generation.
+func (w *world) restorePinned(r int, inc int, loc, gen, snapKey string, snapVer, tx int) *localDB {
+ return w.restoreWith(r, inc, loc, gen, snapKey, snapVer, tx)
+}
+
+func (w *world) restoreWith(r int, inc int, loc, gen, pinKey string, pinVer, pinTX int) *localDB {
bk := w.buckets[r]
db := &localDB{Inc: inc, Loc: loc, Gen: gen, State: map[string]int{}}
if !on("restore-by-generation") {
@@ -200,7 +212,9 @@ func (w *world) restoreCalc(r int, inc int, loc, gen string) *localDB {
cur := 0
var applied []*blob
pinnedTX := 0
- if gen != "" {
+ if pinTX >= 0 {
+ pinnedTX = pinTX // the operation's build journal pins the root
+ } else if gen != "" {
m := bk.current(genMarkerKey(loc))
if m == nil || m.B.Gen != gen {
return nil // the marker does not name this generation: refuse
@@ -220,10 +234,14 @@ func (w *world) restoreCalc(r int, inc int, loc, gen string) *localDB {
}
}
if root == nil && gen != "" && pinnedTX > 0 {
- m := bk.current(genMarkerKey(loc))
- snap := bk.byID(m.B.SnapKey, m.B.Base)
- if snap == nil || snap.Marker || snap.B.Max != m.B.TX {
- return nil // the snapshot version is missing or not at the marker's TXID
+ key, ver := pinKey, pinVer
+ if pinTX < 0 {
+ m := bk.current(genMarkerKey(loc))
+ key, ver = m.B.SnapKey, m.B.Base
+ }
+ snap := bk.byID(key, ver)
+ if snap == nil || snap.Marker || snap.B.Max != pinnedTX {
+ return nil // the snapshot version is missing or not at the pinned TXID
}
root = snap.B
}
@@ -336,7 +354,7 @@ func (w *world) bucketGen(b *box, loc string) (string, int) {
func (w *world) spawn(b *box, c *claim, want string, probe bool) bool {
h := c.Holder
loc := h.Location
- admitted := "" // the admission mode this call decided (claim rev 6.8 §6.4a)
+ var adm admitInput // the admission this call decided (claim rev 6.9 §6.4a)
if b.Old {
// an old executable: no claim, no markers, no locations; it
// restores whatever is newest at the legacy root
@@ -360,28 +378,28 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool {
}
} 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): retire-artifacts of its stamp
- if b.DB != nil && (b.DB.Gen != bg || b.DB.Loc != loc) {
- w.retireDatabase(b, h.Inc, b.DB.Stamp)
- }
+ if on("start-check") && bg != "" && binc != h.Inc {
+ w.logf("box %d start check refused: generation.json %q inc %d, claim inc %d", b.ID, bg, binc, h.Inc)
+ return false
}
- // every path that opens replication is admitted here (claim rev 6.8
+ // every path that opens replication is admitted here (claim rev 6.9
// §6.4a, R8-2): an ordinary wake, a committed landing's serving, a
// probe and a restarted probe, a reverted source, an opened rollback
// recovery, a push's writer. A writer still closing holds the lease:
// the wake waits for it
+ if o := b.open; o != nil {
+ // an admitted writer whose start is in progress: it waits for the
+ // PUT it needs acknowledged and starts without another CAS; an
+ // admission that moved on (its session or generation changed)
+ // abandons it
+ if o.Gen != h.Gen || o.Session != h.Session {
+ b.open = nil
+ } else if !w.resumeOpen(b, c, o) {
+ return false
+ } else {
+ return w.startProc(b, c, want, probe, o.Mode)
+ }
+ }
if b.DB != nil && b.DB.Closing {
w.closeStep(b)
if b.DB.Closing {
@@ -390,22 +408,126 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool {
return false
}
}
- if admitted = w.admitWriter(b, c, want, probe); admitted == "" {
+ var ok bool
+ if adm, ok = w.admitWriter(b, c, want, probe); !ok {
return false
}
- if b.DB == nil {
- b.DB = w.restoreInit(b, h.Inc, loc, want)
- if b.DB == nil {
+ // the generation to restore from is holder.generation. generation.json
+ // may lag it: an admitted writer that never published (it died between
+ // its CAS and its marker, or the marker PUT was not acknowledged, rev
+ // 7.10 §7.14). A lagging marker for an operation's prepared generation
+ // is published again by op.exec before anything else, from the
+ // operation's pinned snapshot; a generation with no file at all is an
+ // abandoned fresh one, left to the sweep, and the baseline is the
+ // generation the marker names, its parent, which holds the data
+ source := h.Gen
+ prepared := adm.Mode == "cold" && adm.NewGeneration == want && want != h.Gen
+ if prepared {
+ // a cold admission into the operation's prepared generation: the
+ // marker names the predecessor and the admission publishes the
+ // new one; the generation clause has nothing to compare
+ bg = h.Gen
+ }
+ if !on("start-check-claim-gen") {
+ // rev 5's start check: the box's own marker decides, so the
+ // generation it restores is the one its region's generation.json
+ // names, whatever the claim says
+ source = bg
+ bg = h.Gen
+ }
+ if bg != h.Gen && on("start-check") {
+ switch {
+ case h.WriterBox == b.ID && w.ancestorGen(loc, h.Gen, bg):
+ // the marker lags behind this box's own admission: handled below.
+ // Another box's lagging marker is the start check's refusal
+ // (the generation clause, J2-R2-8): a stale box whose region
+ // holds none of holder.generation's files is not the admitted
+ // writer that died between its CAS and its marker
+ case w.ancestorGen(loc, bg, h.Gen):
+ // the marker names a descendant: a clean rollback returned the
+ // claim to the source's generation and abandoned the target's;
+ // the marker names the source's generation again, as it did
+ // before, so the restore contract reads it (rev 7.10 §7.14)
+ if !w.republishMarker(b, loc, h.Gen) {
+ return false
+ }
+ bg = h.Gen
+ default:
+ w.logf("box %d start check refused: generation.json %q, claim %q", b.ID, bg, h.Gen)
+ return false
+ }
+ }
+ if bg != h.Gen && on("start-check") {
+ if len(w.buckets[b.Region].keys(dataKey(loc, h.Gen, ""))) == 0 {
+ // the baseline is the nearest ancestor that holds a file
+ for source != bg && len(w.buckets[b.Region].keys(dataKey(loc, source, ""))) == 0 {
+ source, _ = w.parentGen(loc, source)
+ }
+ w.stats["abandoned empty generation skipped"]++
+ } else {
+ ver, key, tx := 0, "", 0
+ if h.Gen == installGen(&c.Op) && c.Op.BaseKey != "" {
+ ver, key, tx = c.Op.BaseVer, c.Op.BaseKey, c.Op.BaseTX
+ }
+ if w.publishGen(b, loc, h.Gen, h.Inc, ver, key, tx) <= 0 {
+ w.logf("box %d: generation.json for %q not acknowledged", b.ID, h.Gen)
+ return false
+ }
+ w.stats["marker republished"]++
+ w.logf("box %d: generation.json published again for %q, which the admitted writer never published", b.ID, h.Gen)
+ }
+ }
+ // a box never reuses its local database (claim rev 6.9, R9-1): the
+ // admitted writer purges it, and if the purge fails it does not
+ // start; then it restores from the certified remote baseline. The
+ // mutation of remote-baseline keeps a local database of the
+ // generation it opens, as rev 7.9 and today's activator do
+ if b.DB != nil && (on("remote-baseline") || b.DB.Inc != h.Inc || b.DB.Gen != adm.NewGeneration) {
+ if b.PurgeFails {
+ b.PurgeFails = false // a transient error: the next attempt's purge succeeds
+ w.stats["purge failed: writer not started"]++
+ w.logf("box %d: the purge of its local database failed; the writer does not start", b.ID)
return false
}
+ b.DB = nil
+ b.Parked++
+ w.stats["local database purged"]++
}
+ db := b.DB
+ if db == nil {
+ switch {
+ case prepared:
+ // the operation's prepared generation: its pinned snapshot and anchor
+ db = w.restorePinned(b.Region, h.Inc, loc, want, c.Op.BaseKey, c.Op.BaseVer, c.Op.BaseTX)
+ default:
+ db = w.restoreCalc(b.Region, h.Inc, loc, source)
+ if db != nil && adm.Mode == "warm" && db.Pos < adm.RemoteMaxTXID {
+ w.logf("box %d: the restore of %q reached position %d, the certificate says %d", b.ID, source, db.Pos, adm.RemoteMaxTXID)
+ db = nil
+ }
+ }
+ if db == nil {
+ w.stats["restore refused"]++
+ w.logf("box %d: nothing to restore for a %s admission from %q (generation.json %q)", b.ID, adm.Mode, source, bg)
+ return false
+ }
+ db.Stamp = b.stampOf(h.Inc)
+ w.logf("box %d restored %s: TXID %d at position %d (%s admission into %q)", b.ID, dataKey(loc, source, ""), db.TX, db.Pos, adm.Mode, adm.NewGeneration)
+ }
+ b.DB = db
if on("start-check") {
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 != 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)
+ // .files-gen names the generation the files were installed or
+ // carried into (F7): the one the marker names, holder.generation,
+ // or the one this admission opens (the admission retags them)
+ // .files-gen (F7) is retagged by every admission with the
+ // generation it opens; a stale tag from an earlier stay is not a
+ // refusal, the incarnation is
+ if b.Files != nil && b.Files.Inc != h.Inc {
+ w.logf("box %d start check refused: files inc %d, claim inc %d", b.ID, b.Files.Inc, h.Inc)
return false
}
}
@@ -451,27 +573,69 @@ func (w *world) spawn(b *box, c *claim, want string, probe bool) bool {
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
}
- if admitted != "" && !b.Old {
- // the admitting CAS, as the process starts; the writer opens under
- // the session it produced and writes its lineage file (claim rev 6.8
- // §6.4a). The replica reads its remote position at its first sync
- // (litestream's Replica.Sync initializes it lazily), RemotePos -1
- if !w.admitCommit(b, c, want, admitted) {
+ if !b.Old {
+ // the admitting CAS, after readiness and before any upload (claim rev
+ // 6.9 §6.4a); the writer then opens under the session and generation
+ // it produced. The replica reads its remote position at its first
+ // sync (litestream's Replica.Sync initializes it lazily), RemotePos -1
+ if !w.admitCommit(b, c, adm) {
return false
}
- b.DB.Session = w.claim.Holder.Session
- b.DB.RemotePos = -1
- if b.lineage == nil {
- b.lineage = map[int]lineageRec{}
+ db := b.DB
+ nh := w.claim.Holder
+ db.Gen, db.Session, db.Stamp = nh.Gen, nh.Session, nh.Stamp
+ if b.Files != nil {
+ // the carried files are tagged with the installing CAS's stamp
+ // at the CAS (§6.4), whether or not the start completes: the
+ // record activates that stamp from its next read (seed 62 / 300)
+ b.Files.Gen, b.Files.Stamp = nh.Gen, nh.Stamp
+ }
+ db.Pending, db.Queue, db.InFlight, db.Issued, db.Uncertain, db.Closing, db.CloseReq = nil, nil, nil, nil, false, false, nil
+ db.RemotePos, db.FirstFull = -1, true // litestream's first sync after a cold initialization is a full upload (fact R5-1c)
+ o := &openState{Gen: nh.Gen, Want: want, Session: nh.Session, Mode: adm.Mode, Prepared: adm.Mode == "cold" && adm.NewGeneration == want && want != h.Gen, DB: db}
+ switch {
+ case adm.Mode == "cold" && o.Prepared:
+ db.Pos = w.maxL0(w.buckets[b.Region], dataKey(loc, db.Gen, "")) // the prepared generation's anchor
+ o.stage = "marker"
+ case adm.Mode == "cold":
+ // a fresh generation is empty until the writer's first upload,
+ // the full file [1, 1] of the restored baseline (fact R5-1c),
+ // made after the CAS and before the marker: generation.json
+ // never names a generation without a root (INV-11), so a writer
+ // that dies before its first upload leaves an empty, unpublished
+ // generation whose parent stays the restore's baseline (§7.14)
+ db.Pos = 0
+ o.stage = "marker"
+ if len(db.Log) > 0 || len(db.State) > 0 {
+ o.stage = "first"
+ }
+ case db.Pos > w.maxL0(w.buckets[b.Region], dataKey(loc, db.Gen, "")) && on("restore-anchor"):
+ o.stage = "anchor" // the restored position is above the level-0 maximum: the anchor [N, N], after the CAS (§5.1 step 7)
+ default:
+ o.stage = "start"
+ }
+ b.DB = nil
+ b.open = o
+ if !w.resumeOpen(b, c, o) {
+ return false
}
- b.lineage[h.Inc] = lineageRec{Gen: b.DB.Gen, Session: b.DB.Session}
}
+ return w.startProc(b, c, want, probe, adm.Mode)
+}
+
+// startProc starts the host's processes on b for the admitted writer.
+func (w *world) startProc(b *box, c *claim, want string, probe bool, mode string) bool {
+ h := c.Holder
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: want, Box: b.ID})
+ gen := want
+ if b.DB != nil {
+ gen = b.DB.Gen
+ }
+ b.Procs = append(b.Procs, &proc{Main: true, Strict: strict, Inc: h.Inc, Gen: gen, Box: b.ID})
if w.rng.Intn(2) == 0 {
- b.Procs = append(b.Procs, &proc{Main: false, Strict: strict, Inc: h.Inc, Gen: want, Box: b.ID})
+ b.Procs = append(b.Procs, &proc{Main: false, Strict: strict, Inc: h.Inc, Gen: gen, 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, want, probe, strict, c.Op.Kind, c.Op.ID, c.Op.Exec)
+ w.logf("box %d spawned inc %d gen %q (%s, probe=%v strict=%v) claim=%s/%s exec=%d", b.ID, h.Inc, gen, mode, probe, strict, c.Op.Kind, c.Op.ID, c.Op.Exec)
return true
}
@@ -527,19 +691,21 @@ func (w *world) admits(b *box, c *claim, probe string) bool {
return false
}
-// warmCertificate is the clean-close certificate that permits a warm
-// admission (claim rev 6.8 §6.4a): closed/<holder.session>.json exists for
-// the generation, its max_txid is the generation's remote maximum TXID over
-// every level, and its box is this box. The mutation of writer-session
-// takes the newest certificate of any session (rev 7.8's single marker);
-// the mutation of closed-marker ignores max_txid.
-func (w *world) warmCertificate(b *box, c *claim, gen string) *version {
+// certificate is the clean-close certificate of the observed session
+// (claim rev 6.9 §6.4a): closed/<holder.session>.json exists for
+// holder.generation and its max_txid is the generation's remote maximum
+// TXID over every level. Any op.exec box may continue on it (claim rev
+// 6.8.2: the certificate proves every upload of the session completed,
+// whichever box made them). The mutation of writer-session takes the
+// newest certificate of any session (rev 7.8's single marker); the
+// mutation of closed-marker ignores max_txid.
+func (w *world) certificate(b *box, c *claim) *version {
h := c.Holder
bk := w.buckets[b.Region]
- prefix := dataKey(h.Location, gen, "")
+ prefix := dataKey(h.Location, h.Gen, "")
var m *version
if on("writer-session") {
- m = bk.current(closedKey(h.Location, gen, h.Session))
+ m = bk.current(closedKey(h.Location, h.Gen, h.Session))
} else {
for _, k := range bk.keys(prefix) {
if isClosedKey(k) {
@@ -554,9 +720,7 @@ func (w *world) warmCertificate(b *box, c *claim, gen string) *version {
return nil
}
if m.B.Seq != b.ID {
- w.stats["certificate of another box"]++
- w.logf("box %d: certificate %d for %s is box %d's", b.ID, m.B.Session, prefix, m.B.Seq)
- return nil
+ w.stats["certificate of another box"]++ // continued all the same (claim rev 6.8.2)
}
if on("closed-marker") && m.B.TX != w.remoteMax(bk, prefix) {
w.logf("box %d: certificate %d for %s is stale (max_txid %d, remote %d)", b.ID, m.B.Session, prefix, m.B.TX, w.remoteMax(bk, prefix))
@@ -566,297 +730,322 @@ func (w *world) warmCertificate(b *box, c *claim, gen string) *version {
return m
}
-// lastWriter is the newest writers journal entry, or nil.
-func lastWriter(op *opState) *writerEntry {
- if len(op.Writers) == 0 {
- return nil
+// installGen is the generation an operation has prepared for its writer: a
+// landing's or a push's g-<op id>/, a dirty rollback's return generation.
+// Its probe's cold admission makes it holder.generation (claim rev 6.9:
+// holder.generation is the only authoritative generation, in every kind
+// and phase).
+func installGen(op *opState) string {
+ if op.Kind == "restoring" {
+ return op.RollbackID
}
- return &op.Writers[len(op.Writers)-1]
+ return op.ID
}
-// admitWriter is AdmitWriter (claim rev 6.8 §6.4a, R8-1, R8-2): the one
-// claim CAS every path that opens replication makes before any upload. It
-// requires the observed holder.session and holder.generation, and op.exec
-// to be this box (claim rev 6.8.1, rule exec-writer); it writes
-// holder.session = its resulting gen and a writers journal entry. Three
-// modes, decided here and committed by admitCommit as the process starts
-// (so a start that fails after the decision leaves nothing admitted):
-//
-// - "open": the box's own cold admission has finished its build (the
-// newest entry is this box's, unopened, for gen): the writer opens it,
-// the CAS marking the entry opened;
-// - "warm": a certificate for the observed session permits a warm
-// admission; the CAS moves the session forward, so the certificate
-// names a dead session from then on;
-// - "fresh": the operation's freshly built generation has had no writer
-// (op.Fresh, an install's first probe): a cold admission whose build
-// was the install;
-// - otherwise lost replication state: a cold admission's CAS is made now
-// (op.Rec), its build runs under the operation (recStep), and this call
-// returns "" until the writer may open.
-func (w *world) admitWriter(b *box, c *claim, gen string, probe bool) string {
- h := c.Holder
- if on("exec-writer") && c.Op.Exec != b.ID {
- w.stats["admission refused: not op.exec"]++
- w.logf("box %d: admission refused, op.exec is %d (%s/%s)", b.ID, c.Op.Exec, c.Op.Kind, c.Op.ID)
- return ""
- }
- if !on("admit-everywhere") && c.Op.Kind != "serving" {
- return "unguarded" // the mutation: writer epochs for ordinary wakes only (rev 7.8)
- }
- if c.Op.Rec != nil {
- return "" // a cold admission's build is in progress
+// republishMarker writes generation.json for gen again, with the content
+// its last marker had: a clean rollback's return to the source generation.
+func (w *world) republishMarker(b *box, loc, gen string) bool {
+ bk := w.buckets[b.Region]
+ var last *version
+ for _, v := range bk.objs[genMarkerKey(loc)] {
+ if !v.Marker && v.B != nil && v.B.Gen == gen && (last == nil || v.ID > last.ID) {
+ last = v
+ }
}
- if e := lastWriter(&c.Op); e != nil && e.Box == b.ID && e.Session == h.Session && e.Gen == gen && !e.Opened {
- return "open"
+ if last == nil && gen != "" {
+ w.logf("box %d: no earlier marker names %q", b.ID, gen)
+ return false
}
- if !on("recovery-generation") {
- return "unguarded" // rev 7.7: a same-generation restart, no session
+ inc, base, key, tx := w.claim.Holder.Inc, 0, "", 0
+ if last != nil {
+ inc, base, key, tx = last.B.Inc, last.B.Base, last.B.SnapKey, last.B.TX
}
- if m := w.warmCertificate(b, c, gen); m != nil {
- return "warm"
+ if w.publishGen(b, loc, gen, inc, base, key, tx) <= 0 {
+ w.logf("box %d: generation.json for %q not acknowledged", b.ID, gen)
+ return false
}
- if c.Op.Fresh && w.opGen(&c.Op) == gen {
- return "fresh" // the operation's install was this writer's build
+ w.stats["marker republished after a clean rollback"]++
+ w.logf("box %d: generation.json names %q again after the rollback", b.ID, gen)
+ return true
+}
+
+// parentGen is the generation gen was admitted from within loc, as newGen
+// recorded it; ok is false at the origin.
+func (w *world) parentGen(loc, gen string) (string, bool) {
+ p, ok := w.genParent[dataKey(loc, gen, "")]
+ if !ok {
+ return "", false
}
- // cold: a fresh generation, built under this operation
- id := w.newID("rec")
- if w.cas(c, func(n *claim) bool {
- if n.Holder.Session != h.Session || n.Op.Rec != nil || n.Op.Exec != b.ID && on("exec-writer") {
- return false
- }
- n.Holder.Session = w.nextGen()
- p := pred{Session: h.Session, Box: w.predBox(c), Gen: gen, Stamp: h.Stamp}
- n.Op.Writers = append(n.Op.Writers, writerEntry{Session: n.Holder.Session, Box: b.ID, Gen: id, Mode: "cold", Pred: p})
- n.Op.Rec = &recState{Gen: id, Base: gen, Session: n.Holder.Session, Box: b.ID, Region: b.Region, Phase: "build", Pred: p}
- w.newGen(n.Holder.Location, gen, id)
- if gen == n.Holder.Gen {
- n.Holder.Gen = id // the claim's generation moves with the writer it admits
- } else {
- n.Op.InstGen = id // an operation's install generation, not yet the claim's
- }
- n.Holder.Stamp = w.issueStamp(n, b.ID) // an installing CAS (claim rev 6.8 §6.4a)
- n.Op.Writers[len(n.Op.Writers)-1].Stamp = n.Holder.Stamp
- n.Op.Fresh = false
- return true
- }) {
- w.logf("box %d: cold admission %s from generation %q (lost replication state, op %s/%s)", b.ID, id, gen, c.Op.Kind, c.Op.ID)
- w.stats["admissions: cold"]++
+ if p == loc {
+ return "", true
}
- return ""
+ return strings.TrimSuffix(strings.TrimPrefix(p, loc+"g-"), "/"), true
}
-// admitCommit is the admitting CAS for the open, warm and fresh modes, made
-// as the process starts; false means the claim moved and the start is
-// abandoned.
-func (w *world) admitCommit(b *box, c *claim, gen, mode string) bool {
- h := c.Holder
- if mode == "unguarded" {
- return true
- }
- ok := w.cas(c, func(n *claim) bool {
- if n.Holder.Session != h.Session || n.Op.Rec != nil || n.Op.Exec != b.ID && on("exec-writer") {
- return false
- }
- if mode == "open" {
- le := lastWriter(&n.Op)
- if le == nil || le.Session != h.Session || le.Opened {
- return false
- }
- le.Opened = true
+// ancestorGen: anc is gen or one of its ancestors within loc.
+func (w *world) ancestorGen(loc, gen, anc string) bool {
+ for {
+ if gen == anc {
return true
}
- n.Holder.Session = w.nextGen()
- n.Op.Fresh = false
- n.Op.Writers = append(n.Op.Writers, writerEntry{Session: n.Holder.Session, Box: b.ID, Gen: gen, Stamp: n.Holder.Stamp, Mode: mode, Opened: true,
- Pred: pred{Session: h.Session, Box: w.predBox(c), Gen: gen, Stamp: h.Stamp}})
- return true
- })
- if ok {
- w.stats["admissions: "+mode]++
- } else {
- w.logf("box %d: %s admission CAS refused (session %d, op %s/%s exec %d)", b.ID, mode, h.Session, c.Op.Kind, c.Op.ID, c.Op.Exec)
+ p, ok := w.parentGen(loc, gen)
+ if !ok {
+ return false
+ }
+ gen = p
}
- return ok
}
-// predBox is the box of the newest writer session the claim records, or
-// op.exec when it records none.
-func (w *world) predBox(c *claim) int {
- if e := lastWriter(&c.Op); e != nil {
- return e.Box
- }
- return c.Op.Exec
+// phaseOf is the operation phase an admission observes and binds to (R9-4).
+func phaseOf(op *opState) string {
+ return op.Phase + "/" + op.LandPhase + "/" + op.SrcPhase + "/" + op.RevPhase
}
-// opGen is the generation an operation installs: its install generation
-// when a cold admission within it moved it (R8-2), else its id, or the
-// rollback id for a rollback.
-func (w *world) opGen(op *opState) string {
- if op.InstGen != "" {
- return op.InstGen
+// admitInput is claim rev 6.9's AdmitWriter input (Admission in the claim library): what the box observed,
+// the mode it decided and the generation it opens.
+type admitInput struct {
+ ObservedOpID string
+ ObservedPhase string
+ ObservedSession int
+ ObservedGeneration string
+ Box int
+ Mode string // warm or cold; "unguarded" is the rev 7.7 mutation
+ NewGeneration string
+ PredecessorCertified bool
+ RemoteMaxTXID int
+}
+
+// admitWriter decides the admission for a start on b under the claim it
+// read (claim rev 6.9 §6.4a, R8-2, R9-3): it makes no CAS and issues
+// nothing. It requires op.exec to be this box (rule exec-writer) and
+// refuses every kind in which no writer may open (deleting, parking,
+// purging, creating; R9-4). The mode is warm when the certificate of the
+// observed session is intact and the generation to open is
+// holder.generation; else cold, into the operation's prepared generation
+// (want, when it is not holder.generation) or a fresh one.
+func (w *world) admitWriter(b *box, c *claim, want string, probe bool) (admitInput, bool) {
+ h := c.Holder
+ a := admitInput{ObservedOpID: c.Op.ID, ObservedPhase: phaseOf(&c.Op), ObservedSession: h.Session, ObservedGeneration: h.Gen, Box: b.ID}
+ if on("exec-writer") && c.Op.Exec != b.ID {
+ w.stats["admission refused: not op.exec"]++
+ w.logf("box %d: admission refused, op.exec is %d (%s/%s)", b.ID, c.Op.Exec, c.Op.Kind, c.Op.ID)
+ return a, false
}
- if op.Kind == "restoring" {
- return op.RollbackID
+ switch c.Op.Kind {
+ case "deleting", "parking", "purging", "creating":
+ w.stats["admission refused: op kind"]++
+ return a, false
}
- return op.ID
+ if !on("admit-everywhere") && c.Op.Kind != "serving" {
+ a.Mode, a.NewGeneration = "unguarded", want // the mutation: writer sessions for ordinary wakes only (rev 7.8)
+ if want == "" {
+ a.NewGeneration = h.Gen
+ }
+ return a, true
+ }
+ bk := w.buckets[b.Region]
+ a.RemoteMaxTXID = w.remoteMax(bk, dataKey(h.Location, h.Gen, ""))
+ a.PredecessorCertified = w.certificate(b, c) != nil
+ if want == "" || want == h.Gen || w.ancestorGen(h.Location, h.Gen, want) {
+ // holder.generation, or an operation's prepared generation that a
+ // writer already opened (it is holder.generation or an ancestor of
+ // it): never re-entered, since a dead writer's uploads may still
+ // land in it (seeds 43 and 87 / 300)
+ if a.PredecessorCertified || !on("recovery-generation") {
+ a.Mode, a.NewGeneration = "warm", h.Gen
+ return a, true
+ }
+ a.Mode, a.NewGeneration = "cold", w.newID("rec")
+ return a, true
+ }
+ a.Mode, a.NewGeneration = "cold", want // the operation's prepared generation, opened for the first time
+ return a, true
}
-// recStep is a cold admission's build (claim rev 6.8 §6.4a; moves rev 7.9
-// §7.14), run under whichever operation admitted the writer, by the box it
-// admitted, before that operation's own step:
-//
-// - build: stop evidence first. The baseline is the warm database only
-// with provenance (R8-4): its lineage file names the predecessor's
-// {generation, session}, the predecessor's box is this box, and it
-// passes its integrity check (the model's database is always
-// consistent, WAL included); else the predecessor generation restored
-// by the pure calculation, and the warm database's unreplicated writes
-// are declared lost. A snapshot [1, N] and an anchor [N, N] go into the
-// new generation and are acknowledged when N > 0; an empty generation
-// gets no LTX file (R8-3). A replay reuses a snapshot already current.
-// - publish: generation.json names the new generation; the predecessor
-// generation is parked as a chore after the dead writer's horizon; the
-// build is done, and the writer opens at its next admission.
-func (w *world) recStep(b *box, c *claim) {
- rec := c.Op.Rec
+// resumeOpen advances an admitted writer's start (rev 7.10 §7.14): each
+// stage issues one PUT and waits for its acknowledgement, retrying the
+// same bytes after the client's timeout; a stage whose effect is visible
+// (the file current, the marker naming the generation) is done whatever
+// became of the request. It returns true once the process may start, with
+// the database installed on the box.
+func (w *world) resumeOpen(b *box, c *claim, o *openState) bool {
h := c.Holder
loc := h.Location
bk := w.buckets[b.Region]
- switch rec.Phase {
- case "build":
- if !w.evidence(b, rec.Gen) {
- return
- }
- var base *localDB
- reused := false
- if snaps := w.currentLTX(bk, dataKey(loc, rec.Gen, ""), 9); len(snaps) > 0 {
- sv := snaps[len(snaps)-1].B
- base = &localDB{Inc: h.Inc, Loc: loc, Gen: rec.Gen, Key: sv.SealKey, Pos: sv.Max, State: cloneState(sv.Pages), Log: txsOf(sv), TX: w.lineageTX(sv)}
- reused = true
- w.stats["cold admission: snapshot reused on replay"]++
- } else if b.DB != nil && b.DB.Inc == h.Inc && b.DB.Gen == rec.Base && w.warmProvenance(b, h.Inc, rec) {
- base = b.DB
- w.stats["cold admission: warm baseline"]++
- } else {
- switch {
- case b.DB == nil:
- w.logf("box %d: cold admission %s has no local database; baseline from the remote of %q", b.ID, rec.Gen, rec.Base)
- case b.DB.Inc != h.Inc || b.DB.Gen != rec.Base:
- w.logf("box %d: cold admission %s finds a database of inc %d generation %q, not %q; baseline from the remote", b.ID, rec.Gen, b.DB.Inc, b.DB.Gen, rec.Base)
- }
- if b.DB != nil && b.DB.Inc == h.Inc && b.DB.Gen == rec.Base {
- // a warm database without provenance: the remote wins, and
- // its writes that never replicated are declared lost
- n := 0
- for i := range w.acks {
- a := &w.acks[i]
- if a.Box == b.ID && a.Inc == h.Inc && !a.Exempt && !w.isDurable(a.W) {
- a.Exempt = true
- n++
+ db := o.DB
+ for {
+ var key string
+ var mk func() *request
+ visible := func() bool { return false }
+ switch o.stage {
+ case "first":
+ key = ltxKey(loc, db.Gen, 0, 1, 1)
+ mk = func() *request { return &request{kind: rPut, region: b.Region, key: key, b: w.deltaOf(db, h.Inc)} }
+ visible = func() bool { return bk.current(key) != nil }
+ case "marker":
+ bg, _ := w.bucketGen(b, loc)
+ visible = func() bool { bg, _ = w.bucketGen(b, loc); return bg == db.Gen }
+ if bg != db.Gen {
+ ver, k, tx := 0, "", 0
+ if o.Prepared {
+ ver, k, tx = c.Op.BaseVer, c.Op.BaseKey, c.Op.BaseTX
+ }
+ if o.req == nil || o.req.done || w.now-o.req.at >= uploadTimeout {
+ if o.req != nil && !o.req.done {
+ w.stats["open: marker PUT retried"]++
+ }
+ v := w.publishGen(b, loc, db.Gen, h.Inc, ver, k, tx)
+ o.req = w.lastIssued
+ if v > 0 {
+ o.req = nil
}
}
- w.stats["cold admission: warm baseline refused, writes declared lost"] += n
- w.logf("box %d: warm database of %q has no provenance; %d unreplicated writes declared lost", b.ID, rec.Base, n)
- }
- base = w.restoreCalc(b.Region, h.Inc, loc, rec.Base)
- if base == nil {
- w.stats["cold admission: baseline unrestorable"]++
- w.logf("box %d: cold admission %s cannot restore %q yet: %s", b.ID, rec.Gen, rec.Base, w.ltxShape(b.Region, dataKey(loc, rec.Base, "")))
- return
- }
- w.stats["cold admission: remote baseline"]++
- }
- snap := snapshotOf(base, h.Inc)
- n := snap.Max // the baseline's position; 1 for a database with transactions that never replicated; 0 only when empty (R8-3)
- if !on("valid-ltx") {
- n = base.Pos // the mutation: the position as is, a zero-TXID file for a never-replicated database
- snap.Max = n
- }
- w.logf("box %d: cold admission %s baseline: position %d, TXID %d, %d writes (reused snapshot %v, warm %v)", b.ID, rec.Gen, n, base.TX, len(base.Log), reused, base == b.DB && !reused)
- key := ""
- ver := 0
- if n > 0 || !on("valid-ltx") {
- snap.Gen = rec.Gen
- if b.Files != nil {
- snap.SealKey = b.Files.Key
+ if !visible() {
+ w.stats["open: waits for the marker"]++
+ return false
+ }
}
- key = snapKey(loc, rec.Gen, n)
- if !reused && !w.ackedPut(b, key, snap, false) {
- return
+ o.stage, o.req = "start", nil
+ continue
+ case "anchor":
+ key = ltxKey(loc, db.Gen, 0, db.Pos, db.Pos)
+ mk = func() *request { return &request{kind: rPut, region: b.Region, key: key, b: anchorOf(db, h.Inc)} }
+ visible = func() bool { return bk.current(key) != nil }
+ case "start":
+ if o.stage == "start" {
+ b.DB = db
+ b.open = nil
+ if o.Mode == "cold" && !o.Prepared && (len(db.Log) > 0 || len(db.State) > 0) {
+ db.Pos, db.FirstFull, db.Pending = 1, false, nil
+ }
+ return true
}
- sv := bk.current(key)
- if sv == nil {
- return
+ }
+ // first and anchor: one PUT, acknowledged before the next stage
+ if !visible() {
+ if o.req == nil || (!o.req.done && w.now-o.req.at >= uploadTimeout) {
+ if o.req != nil {
+ w.stats["open: PUT retried"]++
+ }
+ r := mk()
+ if o.stage == "anchor" {
+ w.stats["restore anchors"]++
+ } else {
+ w.stats["first uploads"]++
+ }
+ v := w.issue(b.ID, r)
+ o.req = r
+ if v > 0 {
+ o.req = nil
+ }
}
- ver = sv.ID
- if !w.anchorAcked(b, loc, rec.Gen, key, ver, n) {
- return
+ if !visible() {
+ if o.stage == "anchor" && !on("anchor-acked") {
+ // the mutation opens before the anchor is acknowledged
+ } else {
+ w.stats["open: waits for its "+o.stage]++
+ return false
+ }
}
- base.Key = snap.SealKey
}
- db := base
- if db != b.DB {
- b.DB = db
+ if o.stage == "first" {
+ w.markDurable(key, bk.current(key).B)
+ o.stage = "marker"
+ } else {
+ o.stage = "start"
}
- db.Gen, db.Pending, db.Queue, db.InFlight, db.FirstFull, db.Closing, db.CloseReq = rec.Gen, nil, nil, nil, true, false, nil
- db.Issued, db.Uncertain = nil, false
- db.Pos = w.maxL0(bk, dataKey(loc, rec.Gen, ""))
- db.RemotePos = db.Pos
- db.Stamp = h.Stamp
- if b.Files != nil {
- // the files are unchanged; .files-gen names the new generation (F7)
- // and the carried files are tagged with the installing CAS's
- // stamp, like the database (§6.4; seed 453 / 30,000)
- b.Files.Gen, b.Files.Stamp = rec.Gen, h.Stamp
+ o.req = nil
+ }
+}
+
+// admitCommit is the AdmitWriter CAS (claim rev 6.9 §6.4a), made after
+// readiness and before any upload. It is bound to the observed op.id and
+// phase (R9-4; rule admit-bind-op), the observed session and generation,
+// and op.exec. It writes holder.session, holder.writer_box and the journal
+// entry; in cold mode also holder.generation, holder.stamp (the installing
+// CAS), a writes_lost record when the observed session had no certificate
+// (R9-2), and a park-generation chore for a fresh generation's predecessor.
+func (w *world) admitCommit(b *box, c *claim, a admitInput) bool {
+ if a.Mode == "unguarded" {
+ return true
+ }
+ h := c.Holder
+ var lost *writesLost
+ ok := w.cas(c, func(n *claim) bool {
+ if n.Holder == nil || n.Holder.Session != a.ObservedSession || n.Holder.Gen != a.ObservedGeneration {
+ return false
}
- w.cas(c, func(nc *claim) bool {
- if nc.Op.Rec == nil || nc.Op.Rec.Gen != rec.Gen {
+ if on("admit-bind-op") {
+ // bound to the observed op.id and phase (serving's "" compared
+ // literally) and to the kinds in which a writer may open: a
+ // closure computed under serving fails once any operation
+ // started, a delete included (R9-4)
+ if n.Op.ID != a.ObservedOpID || phaseOf(&n.Op) != a.ObservedPhase {
return false
}
- nc.Op.Rec.Phase, nc.Op.Rec.BaseVer, nc.Op.Rec.BaseKey, nc.Op.Rec.BaseTX = "publish", ver, key, n
- return true
- })
- case "publish":
- cur := bk.current(genMarkerKey(loc))
- if cur == nil || cur.B.Gen != rec.Gen {
- if v := w.publishGen(b, loc, rec.Gen, h.Inc, rec.BaseVer, rec.BaseKey, rec.BaseTX); v <= 0 {
- return
+ switch n.Op.Kind {
+ case "deleting", "parking", "purging", "creating":
+ return false
}
}
- w.cas(c, func(nc *claim) bool {
- if nc.Op.Rec == nil || nc.Op.Rec.Gen != rec.Gen {
- return false
+ if on("exec-writer") && n.Op.Exec != b.ID {
+ return false
+ }
+ n.Holder.Session = w.nextGen()
+ n.Holder.WriterBox = b.ID
+ e := writerEntry{Session: n.Holder.Session, Box: b.ID, Gen: a.NewGeneration, Stamp: n.Holder.Stamp, Mode: a.Mode,
+ Pred: pred{Session: a.ObservedSession, Box: h.WriterBox, Gen: h.Gen, Stamp: h.Stamp}}
+ if a.Mode == "cold" {
+ w.newGen(n.Holder.Location, h.Gen, a.NewGeneration)
+ n.Holder.Gen = a.NewGeneration
+ n.Holder.Stamp = w.issueStamp(n, b.ID) // the installing CAS (claim rev 6.8 §6.4a, §6.4)
+ e.Stamp = n.Holder.Stamp
+ if !a.PredecessorCertified && on("writes-lost") {
+ lost = &writesLost{Box: h.WriterBox, Gen: h.Gen, Session: h.Session, RemoteMaxTXID: a.RemoteMaxTXID}
+ e.Lost = lost
}
- nc.Op.Rec = nil
- nc.Obl = append(nc.Obl, w.newObl(nc, "park-generation", b.Region, -1, loc, rec.Base, w.now+horizonH))
- return true
- })
- w.stats["cold admissions done"]++
- }
-}
-
-// warmProvenance is claim rev 6.8 §6.4a's three conditions for taking the
-// warm database as a cold admission's baseline (R8-4): the local lineage
-// file, written by the writer that opened the database, names the
-// journalled predecessor's {generation, session}; the predecessor's box is
-// this box; and the database passes its integrity check with its WAL in
-// place, which here is that it stands at or beyond its own generation's
-// remote position (its uploads came from it; a shorter file is a truncated
-// one). The mutation of warm-provenance takes any database of the
-// predecessor generation.
-func (w *world) warmProvenance(b *box, inc int, rec *recState) bool {
- if !on("warm-provenance") {
+ if a.NewGeneration != installGen(&n.Op) || n.Op.Kind == "serving" {
+ // a recovery into a fresh generation: the predecessor is
+ // dead and parked as a chore after the dead writer's horizon;
+ // an operation's prepared generation leaves its predecessor
+ // to the operation's own finalization or rollback
+ // in this box's region: the predecessor's files are where this
+ // box restored them from
+ n.Obl = append(n.Obl, w.newObl(n, "park-generation", b.Region, -1, n.Holder.Location, h.Gen, w.now+horizonH))
+ }
+ }
+ n.Op.Writers = append(n.Op.Writers, e)
return true
- }
- l, ok := b.lineage[inc]
- if !ok || l.Gen != rec.Pred.Gen || l.Session != rec.Pred.Session || rec.Pred.Box != b.ID {
+ })
+ if !ok {
+ w.logf("box %d: %s admission CAS refused (session %d, op %s/%s exec %d)", b.ID, a.Mode, h.Session, c.Op.Kind, c.Op.ID, c.Op.Exec)
+ w.stats["admission CAS refused"]++
return false
}
- if remote := w.maxL0(w.buckets[b.Region], dataKey(b.DB.Loc, rec.Base, "")); b.DB.Pos < remote {
- w.logf("box %d: warm database of %q fails its integrity check: position %d behind its remote %d", b.ID, rec.Base, b.DB.Pos, remote)
- w.stats["cold admission: warm baseline failed integrity"]++
- return false
+ w.stats["admissions: "+a.Mode]++
+ switch w.claim.Op.Kind {
+ case "deleting", "parking", "purging", "creating":
+ // INV-13 (R9-4): no writer is admitted while the host is being
+ // deleted, parked, purged or created
+ w.violate("INV-13: box %d was admitted as a writer while the host is %s (%s)", b.ID, w.claim.Op.Kind, w.claim.Op.ID)
+ }
+ if a.Mode == "cold" {
+ w.logf("box %d: cold admission %s from generation %q (session %d %scertified, op %s/%s)", b.ID, a.NewGeneration, h.Gen, h.Session, map[bool]string{true: "", false: "un"}[a.PredecessorCertified], c.Op.Kind, c.Op.ID)
+ }
+ if lost != nil {
+ // the writes the predecessor acknowledged and never uploaded are
+ // lost, declared and alerted (claim rev 6.9), never silently
+ n := 0
+ for i := range w.acks {
+ x := &w.acks[i]
+ if x.Box == lost.Box && x.Inc == h.Inc && x.Kind == "write" && !x.Exempt && !w.isDurable(x.W) {
+ x.Exempt = true
+ n++
+ }
+ }
+ w.stats["writes_lost declared"]++
+ w.stats["writes declared lost"] += n
+ w.logf("box %d: alert writes_lost {box %d, generation %q, session %d, remote_max_txid %d}: %d acknowledged writes", b.ID, lost.Box, lost.Gen, lost.Session, lost.RemoteMaxTXID, n)
}
return true
}
diff --git a/internal/sim/hostlife/rules_test.go b/internal/sim/hostlife/rules_test.go
index 623c09a4b..234d091d3 100644
--- a/internal/sim/hostlife/rules_test.go
+++ b/internal/sim/hostlife/rules_test.go
@@ -94,7 +94,9 @@ var allRules = []string{
"writer-session", // claim rev 6.8 §6.4a (R8-1): a warm admission needs the certificate of the observed holder.session and moves the session forward, so a certificate is one-use; the mutation takes the newest certificate of any session and moves nothing
"admit-everywhere", // claim rev 6.8 §6.4a (R8-2): every path that opens replication is an AdmitWriter, a committed landing's serving, a probe restart, a reverted source, an opened rollback included; the mutation gates ordinary wakes only
"exec-writer", // claim rev 6.8.1 (D1): the AdmitWriter CAS requires op.exec to be this box, in every operation; the mutation admits any box the phase table reaches
- "warm-provenance", // claim rev 6.8 §6.4a (R8-4): the warm database is a cold admission's baseline only with its lineage file naming the journalled predecessor's generation and session and the predecessor's box this box; the mutation takes any database of the predecessor generation
+ "remote-baseline", // claim rev 6.9 §6.4a (R9-1): a box never reuses its local database; every admitted writer purges it and restores from the certified remote baseline; the mutation keeps a local database of the generation it opens, as today's activator does
+ "writes-lost", // claim rev 6.9 §6.4a (R9-2): a cold admission whose observed session had no certificate records writes_lost {box: holder.writer_box, generation, session, remote_max_txid} and alerts; the mutation loses the writes silently
+ "admit-bind-op", // claim rev 6.9 §6.4a (R9-4): the AdmitWriter CAS is bound to the observed op.id and phase, serving's "" compared literally; the mutation compares session and generation alone
"valid-ltx", // rev 7.9 §5.1 step 9 (R8-3): an empty generation gets no LTX file, never a zero-TXID snapshot or anchor; the mutation writes [1,0] and [0,0]
"close-evidence", // claim rev 6.8 §6.4a (R8-5): a certificate needs every request of the writer's lifetime returned with success and no retry after a timeout; the mutation looks at the level-0 queue alone
"quiet-before-ack", // this model's finding (late writes after a park)
diff --git a/internal/sim/hostlife/sim_test.go b/internal/sim/hostlife/sim_test.go
index ab4254c60..79e42919f 100644
--- a/internal/sim/hostlife/sim_test.go
+++ b/internal/sim/hostlife/sim_test.go
@@ -211,7 +211,7 @@ func (w *world) heal(final bool) {
if linger {
continue
}
- b.Partitioned, b.Frozen, b.AgentPaused, b.AgentDown = false, false, false, false
+ b.Partitioned, b.Frozen, b.AgentPaused, b.AgentDown, b.PurgeFails = false, false, false, false, false
}
if final {
for _, b := range w.boxes {
@@ -264,9 +264,6 @@ func (w *world) whyNotQuiescent() string {
}
}
if c := w.claim; c != nil && c.Holder != nil {
- if c.Op.Rec != nil {
- out = append(out, fmt.Sprintf("cold admission %s in phase %s", c.Op.Rec.Gen, c.Op.Rec.Phase))
- }
if c.Op.Kind != "serving" {
out = append(out, "op "+c.Op.Kind)
}
@@ -313,7 +310,7 @@ func (w *world) atRest() bool {
if c.Holder == nil {
return c.Op.Kind == "" && w.rec == nil && len(c.Obl) == 0
}
- if c.Op.Kind != "serving" || c.Op.Rec != nil || len(c.Obl) > 0 || w.rec == nil || w.rec.Inc != c.Holder.Inc || w.rec.MoveID != "" {
+ if c.Op.Kind != "serving" || len(c.Obl) > 0 || w.rec == nil || w.rec.Inc != c.Holder.Inc || w.rec.MoveID != "" {
return false
}
e := w.execBox(c)
diff --git a/internal/sim/hostlife/witness_test.go b/internal/sim/hostlife/witness_test.go
index 14b4bb733..c6d558ee5 100644
--- a/internal/sim/hostlife/witness_test.go
+++ b/internal/sim/hostlife/witness_test.go
@@ -69,13 +69,12 @@ var witnesses = []witness{
"a target that wrote during its probe is rolled back; without the return its writes are lost (INV-2)", wDirtyReturn},
{"commit-before-open", "commit-before-open", "INV-5",
"a public request reaches the target's edge while its probe runs; a row opened at the probe routes it before the commit (INV-5, R3-5)", wCommitBeforeOpen},
- {"exec-admission", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-6",
- "one of four admission fences (J2-R2-8, claim rev 6.8.1): a paused open from an earlier operation makes the old source ready after the commit; hold_op refuses the open, the exec check refuses the wake, the generation check refuses the start, AdmitWriter refuses a box that is not op.exec; with all four gone the source's wake is a cold admission by a non-exec box, whose installing CAS moves holder.stamp under the target (INV-6), and the source would then serve beside the target (INV-1)", wAdmissionTriple},
- {"hold-op-open", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-6", "one of four admission fences (see exec-admission)", wAdmissionTriple},
- {"start-check-claim-gen", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-6", "one of four admission fences (see exec-admission)", wAdmissionTriple},
- {"exec-writer", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-6",
- "a paused open from an earlier operation lands after the commit while the source's row is still held; the source's AdmitWriter CAS requires op.exec to be the source, which it no longer is, and refuses (claim rev 6.8.1); with the three box-side fences gone as well, the non-exec source is admitted: its cold admission moves holder.stamp under the target (INV-6) on the way to two boxes running the host (INV-1)", wAdmissionTriple},
- {"start-check", "exec-admission,hold-op-open,start-check,exec-writer", "INV-6", "the whole start check in place of its generation clause (see exec-admission)", wAdmissionTriple},
+ {"exec-admission", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1",
+ "one of four admission fences (J2-R2-8, claim rev 6.8.1): a paused open from an earlier operation makes the old source ready after the commit; hold_op refuses the open, the exec check refuses the wake, the generation check refuses the start, AdmitWriter refuses a box that is not op.exec; with all four gone the source's wake is a cold admission by a non-exec box into a fresh generation restored from its own region's old files, and it serves beside the target (INV-1; its installing CAS also moves holder.stamp under the target, INV-6 a step later)", wAdmissionTriple},
+ {"hold-op-open", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1", "one of four admission fences (see exec-admission)", wAdmissionTriple},
+ {"start-check-claim-gen", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1", "one of four admission fences (see exec-admission)", wAdmissionTriple},
+ {"exec-writer", "exec-admission,hold-op-open,start-check-claim-gen,exec-writer", "INV-1",
+ "a paused open from an earlier operation lands after the commit while the source's row is still held; the source's AdmitWriter CAS requires op.exec to be the source, which it no longer is, and refuses (claim rev 6.8.1); with the three box-side fences gone as well, the non-exec source is admitted cold and two boxes run the host (INV-1)", wAdmissionTriple},
{"strict-spawn", "strict-spawn,evidence-whole-tree", "INV-1",
"redundant alone: an escaped descendant is killed by the whole-tree cleanup; with evidence blind to escapees, a non-strict descendant survives the cut and writes beside the target (INV-1)", wStrictSpawn},
{"touched-incomplete", "touched-incomplete,legacy-discovery", "freed with residue",
@@ -98,8 +97,8 @@ var witnesses = []witness{
"a config pass selected under the first installation pauses across a retire-and-reinstall (UK→US→UK) and a bundle change; the host guard's fresh check refuses its stale bundle, the stamp refuses its retired installation; with both gone it writes host state for a retired installation (R4-2)", wStaleWriter},
{"live-set-region", "live-set-region", "residue never retired",
"a legacy host serving in UK with an earlier replica in US; discovery parks US; an old US replication PUT lands after; the live set is region-qualified, so the US sweep parks it; exempted by key alone it stays for good (R4-3)", wLiveSetRegion},
- {"restore-overlap", "restore-overlap", "INV-2",
- "a generation's snapshot ends at TXID 11 and the only continuation is a compacted file [10,15]; litestream's planner takes it and restores through 15; rev 7.4's rule (min == current+1) discards it and the wake loses four acknowledged writes (R4-1)", wRestoreOverlap},
+ {"restore-overlap", "restore-overlap", "INV-3",
+ "a generation's snapshot ends at TXID 11 and the only continuation is a compacted file [10,15]; litestream's planner takes it and restores through 15; rev 7.4's rule (min == current+1) discards it, the restore stops short of the certificate's max_txid, and the box never starts again (R4-1; since rev 7.10 the certified position is checked before the start, where rev 7.4's rule lost four acknowledged writes)", wRestoreOverlap},
{"restore-gap-closed", "restore-gap-closed", "INV-2 (cold restore)",
"a generation's snapshot ends at TXID n, the file [n+1,n+1] is missing and [n+2,n+2] is current: a genuine gap; the restore refuses; returning what it has would wake the host without durable transactions (R4-1)", wRestoreGap},
// rev 7.6
@@ -138,10 +137,19 @@ var witnesses = []witness{
"a committed move's target serves while the claim is still landing; it dies with its disk and an upload in flight; the next wake must be an AdmitWriter within the landing, a cold one into a fresh generation; gated for ordinary wakes only, the target continues the generation and the late upload replaces its file (claim rev 6.8 §6.4a, R8-2)", wCommittedLandingCrash},
{"admit-everywhere", "admit-everywhere", "INV-2",
"a landing's probe dies with its disk and an upload in flight; the restarted probe must be a cold AdmitWriter within the landing, into a fresh install generation; gated for ordinary wakes only, the restarted probe reuses the generation and the late upload replaces its file (R8-2)", wProbeRestart},
- {"warm-provenance", "warm-provenance", "INV-2",
- "a cold admission finds a warm database of the predecessor generation whose lineage file names another session: a cached copy, behind the remote; without provenance it must restore from the remote; taken as the baseline, the new generation's snapshot lacks a durable write (claim rev 6.8 §6.4a, R8-4)", wWarmLineageMismatch},
{"valid-ltx", "valid-ltx", "INV-12",
- "a created incarnation's first wake: an empty generation, position 0; the cold admission writes no LTX file and the app's first transaction is the first upload; a snapshot [1,0] or an anchor [0,0] is a file the pinned encoder refuses (R8-3)", wEmptyBootstrap},
+ "a created incarnation's first wake is a cold admission into an empty generation with no LTX file, and a move of the still-empty incarnation installs nothing at position 0; the mutation installs a snapshot [1,0] and an anchor [0,0], files the pinned encoder refuses (R8-3)", wEmptyBootstrap},
+ // rev 7.10
+ {"remote-baseline", "remote-baseline", "INV-2",
+ "a session closes cleanly through N+1 and its certificate stands; the box's local database is a cached copy through N (R9-1's clean-close variant); the next wake must purge it and restore the certified remote; keeping it serves a database without an acknowledged write, and its own upload for N+1 is skipped at the remote position (claim rev 6.9)", wStaleLocalAfterClose},
+ {"writes-lost", "writes-lost", "INV-2",
+ "a writer acknowledges a write and crashes before uploading it; the next wake is cold and restores the remote, which lacks the write: the admission must record writes_lost {box, generation, session, remote_max_txid} and alert; silently, the serving database differs from the acknowledged writes (claim rev 6.9, R9-2)", wSilentLoss},
+ {"admit-bind-op", "admit-bind-op,claim-cas-opid", "INV-13",
+ "a wake's admission closure is computed under serving (op.id \"\"); a delete begins, preserving session, generation and executor; the stale closure resumes: bound to the observed op.id, phase and kind it is refused; the model's general CAS condition on op.id (C2, claim-cas-opid) refuses it too, so the two must go together for a writer to be admitted into a host being deleted (claim rev 6.9, R9-4)", wStaleClosureDelete},
+ {"close-evidence", "close-evidence", "certificate while",
+ "a compaction's level-1 PUT is held past the client's timeout; the next compaction pass retries and lands; the original completes afterwards; the session's clean stop must write no certificate, since a request of its lifetime was retried after a timeout; looking at the level-0 queue alone it certifies (R9-5)", wMaintenanceRetry},
+ {"close-evidence", "close-evidence", "certificate while",
+ "a snapshot PUT completes on the server after the client gave up on it, a lost response; the client never observed success, so the session must stay uncertain and certify nothing; counting server completion it certifies (R9-5)", wLostResponse},
{"close-evidence", "close-evidence", "certificate while",
"an upload times out and its retry succeeds while the original stays unresolved; the writer's clean close must write no certificate, because a request of its lifetime is unaccounted for; looking at the level-0 queue alone it certifies (claim rev 6.8 §6.4a, R8-5)", wRetryUnresolved},
{"build-completion", "build-completion", "before its snapshot",
@@ -327,7 +335,7 @@ func (w *world) serve(b *box, inc int, app string) {
n = w.claim.clone()
n.Ver++
}
- n.Holder = &holder{Inc: inc, App: app, Serial: w.serial, Location: loc, Stamp: n.Ver, Session: n.Ver} // the serving CAS wrote holder.stamp; one writer session so far
+ n.Holder = &holder{Inc: inc, App: app, Serial: w.serial, Location: loc, Stamp: n.Ver, Session: n.Ver, WriterBox: b.ID} // the serving CAS wrote holder.stamp; one writer session so far
n.Op = opState{Kind: "serving", Exec: b.ID, Parts: []int{b.ID}}
n.Regions, n.Boxes, n.Complete, n.Obl = []int{b.Region}, []int{b.ID}, true, nil
w.claim = n
@@ -535,6 +543,7 @@ func (w *world) completeHeld(key string) int {
var keep []*request
for _, r := range w.pending {
if (r.key == key || strings.HasSuffix(key, "/") && strings.HasPrefix(r.key, key)) && r.doneAt == 1<<30 {
+ r.doneAt = w.now // the response arrives now (the close's evidence reads the completion time, R9-5)
w.complete(r)
w.logf("witness: held %v %s r%d completes now", r.kind, r.key, r.region)
n++
@@ -586,12 +595,15 @@ func wGenerationConditional(t *testing.T, w *world) {
push := func(holdMarker bool) {
w.userPush()
id := w.claim.Op.ID
- if !w.reach(t, 400, "push "+id+" published", func() bool { return w.claim.Op.ID == id && w.claim.Op.Phase == "published" }, w.act(e)) {
+ if !w.reach(t, 400, "push "+id+" probing", func() bool { return w.claim.Op.ID == id && w.claim.Op.Phase == "probing" }, w.act(e)) {
return
}
if holdMarker {
+ // the probe's cold admission publishes generation.json for the
+ // prepared generation (rev 7.10): accepted, response lost; the
+ // writer does not start, and the next attempt publishes again
w.holdKey(genMarkerKey(loc))
- w.tick(w.act(e)) // the first publication: accepted, response lost
+ w.tick(w.act(e))
w.hold = nil
}
w.reach(t, 400, "push "+id+" released", func() bool { return w.claim.Op.Kind == "serving" }, w.act(e))
@@ -710,6 +722,10 @@ func wRollbackJournal(t *testing.T, w *world) {
c := w.claim
return c.Op.Kind == "restoring" && c.Op.SrcPhase == "probed" && hasMain(src)
}, w.act(src, tgt), w.recoveryPass)
+ if !hasMain(src) {
+ w.violate("INV-3 (witness): the source's probe did not run on the return: %s%s", w.state(), w.boxesState())
+ return
+ }
w.appWrite(src)
w.replicate(src) // into the return generation: durable there
src.Procs = nil
@@ -794,6 +810,7 @@ func wDirtyReturn(t *testing.T, w *world) {
w.serve(src, 1, app0)
w.landProbed(t, src, tgt)
w.appWrite(tgt)
+ w.replicate(tgt) // durable in the target's generation: no writes_lost declaration can cover it (rev 7.10)
w.rollback(w.claim, "settle check failed")
w.finish(t)
}
@@ -1814,8 +1831,9 @@ func wProbeRestart(t *testing.T, w *world) {
if w.completeHeld(key) == 0 {
t.Fatalf("witness: the dead probe's upload was not held")
}
- // the landing's install generation, as its planner would restore it now
- gen := w.opGen(&w.claim.Op)
+ // the landing's generation, holder.generation since the probe's cold
+ // admission (claim rev 6.9), as its planner would restore it now
+ gen := w.claim.Holder.Gen
db := w.restoreCalc(tgt.Region, 1, loc, gen)
if db == nil || !contains(db.Log, wr) {
w.violate("INV-2 (witness): the landing's generation %q lost the restarted probe's write %d after the dead probe's upload landed", gen, wr)
@@ -1824,25 +1842,6 @@ func wProbeRestart(t *testing.T, w *world) {
w.finish(t)
}
-// wWarmLineageMismatch (claim rev 6.8 §6.4a, R8-4): a warm database of the
-// predecessor generation whose lineage names another session.
-func wWarmLineageMismatch(t *testing.T, w *world) {
- b := w.boxes[0]
- w.serve(b, 1, app0)
- w.wake(b)
- w.appWrite(b)
- w.replicate(b)
- stale := b.DB.clone() // a cached copy at this position
- w.appWrite(b)
- w.replicate(b) // one more durable write the copy lacks
- w.crash(b)
- b.DB = stale
- b.lineage[1] = lineageRec{Gen: stale.Gen, Session: 999} // a lineage no session of this claim wrote
- w.logf("witness: box %d's database is a stale copy with a foreign lineage", b.ID)
- w.recovered(t, b, "running after the crash")
- w.finish(t)
-}
-
// wEmptyBootstrap (R8-3): a created incarnation's first wake.
func wEmptyBootstrap(t *testing.T, w *world) {
w.console = append(w.console, &consolePlan{Kind: "create", Host: "h", App: app0, OpID: w.newID("cr"), Inc: 1, Region: 0})
@@ -1852,8 +1851,8 @@ func wEmptyBootstrap(t *testing.T, w *world) {
return c != nil && c.Holder != nil && c.Holder.Inc == 1 && c.Op.Kind == "serving" && b.Row != nil
}, w.runConsole, w.actAll(), w.recoveryPass)
b.Config, b.CfgVer, b.Live, b.LiveInc = 1, w.cfgVer[app0], app0, 1
- // the first wake: a cold admission into an empty generation, which the
- // mutation builds with files the encoder refuses (INV-12 at the PUT)
+ // the first wake: a cold admission into an empty generation (claim rev
+ // 6.9), no LTX file at all
w.reach(t, 120, "first wake", func() bool { return hasMain(b) }, w.act(b), w.recoveryPass, func() { w.wake(b) })
if len(w.violations) > 0 {
return
@@ -1866,11 +1865,28 @@ func wEmptyBootstrap(t *testing.T, w *world) {
if n := len(w.currentLTX(w.buckets[b.Region], dataKey(loc, gen, ""), 0)) + len(w.currentLTX(w.buckets[b.Region], dataKey(loc, gen, ""), 9)); n != 0 {
t.Fatalf("witness: an empty generation has %d LTX files before the first transaction", n)
}
- w.appWrite(b)
- w.replicate(b) // the first transaction is the first upload, [1,1]
+ // a move of the empty incarnation: its seal at the cut is at position 0
+ // with no transaction, and the landing installs nothing; the mutation
+ // installs a snapshot [1,0] and an anchor [0,0], which the encoder
+ // refuses (INV-12 at the PUT). A push cannot be empty: its seal carries
+ // the push's own mark
w.idleStop(b)
- w.loseDisk(b)
- w.recovered(t, b, "woken cold")
+ w.reach(t, 400, "the first wake's chores done", func() bool { return len(w.claim.Obl) == 0 }, w.act(b), w.recoveryPass)
+ tgt := w.regionBox(1)
+ w.moveTo(tgt.Region)
+ if w.claim.Op.Kind != "moving" {
+ t.Fatalf("witness: the move of the empty incarnation did not start: %s", w.state())
+ }
+ w.reach(t, 800, "move of the empty incarnation finalized", func() bool { return w.claim.Op.Kind == "serving" && w.claim.Op.Exec == tgt.ID }, w.act(b, tgt), w.recoveryPass)
+ if len(w.violations) > 0 {
+ return
+ }
+ w.recovered(t, tgt, "woken after the move")
+ w.appWrite(tgt)
+ w.replicate(tgt) // the first transaction is the first upload, [1,1]
+ w.idleStop(tgt)
+ w.loseDisk(tgt)
+ w.recovered(t, tgt, "woken cold")
w.finish(t)
}
@@ -1911,3 +1927,150 @@ func wRetryUnresolved(t *testing.T, w *world) {
w.completeHeld(key)
w.finish(t)
}
+
+// ---------- rev 7.10 ----------
+
+// wStaleLocalAfterClose (claim rev 6.9, R9-1): a valid certificate and a
+// stale local database.
+func wStaleLocalAfterClose(t *testing.T, w *world) {
+ b := w.boxes[0]
+ w.serve(b, 1, app0)
+ w.wake(b)
+ stale := b.DB.clone() // a cached copy through N
+ w.appWrite(b)
+ w.replicate(b) // N+1, durable
+ w.idleStop(b) // the certificate names N+1 as the remote maximum
+ loc := w.claim.Holder.Location
+ if w.buckets[b.Region].current(closedKey(loc, w.claim.Holder.Gen, b.DB.Session)) == nil {
+ t.Fatalf("witness: no certificate after the clean close")
+ }
+ b.DB = stale
+ w.logf("witness: box %d's local database is a cached copy without the last acknowledged write", b.ID)
+ w.recovered(t, b, "woken on the certificate")
+ w.appWrite(b)
+ w.replicate(b) // the next upload: skipped at the remote position if the stale copy was kept
+ w.checkLocal(w.claim, b, b.DB)
+ w.checkDurable(w.claim, "after the wake on the stale copy")
+ w.finish(t)
+}
+
+// wSilentLoss (claim rev 6.9, R9-2): an acknowledged, unuploaded write and
+// a crash; the next admission declares the loss.
+func wSilentLoss(t *testing.T, w *world) {
+ b := w.boxes[0]
+ w.serve(b, 1, app0)
+ w.wake(b)
+ w.appWrite(b) // acknowledged, never uploaded
+ w.crash(b)
+ w.recovered(t, b, "woken after the crash")
+ if w.stats["writes_lost declared"] == 0 && on("writes-lost") {
+ t.Fatalf("witness: no writes_lost record after the crash")
+ }
+ w.checkLocal(w.claim, b, b.DB)
+ w.finish(t)
+}
+
+// wStaleClosureDelete (claim rev 6.9, R9-4): an admission closure computed
+// under serving resumes after a delete began.
+func wStaleClosureDelete(t *testing.T, w *world) {
+ b := w.boxes[0]
+ w.serve(b, 1, app0)
+ w.wake(b)
+ w.idleStop(b)
+ stale := w.claim.clone() // the wake's read, under serving
+ w.userDelete()
+ if w.claim.Op.Kind != "deleting" {
+ t.Fatalf("witness: the delete did not begin: %s", w.state())
+ }
+ // the claim library's BeginDelete preserves session, generation and the
+ // executor (R9-4); this model's delete names no executor, so the
+ // witness keeps the serving box as op.exec, as the library does
+ w.cas(w.claim, func(n *claim) bool { n.Op.Exec = b.ID; return true })
+ w.logf("witness: a stalled wake resumes with its serving-time read of the claim")
+ if w.spawn(b, stale, stale.Holder.Gen, false) {
+ w.logf("witness: the stale closure admitted a writer during the delete")
+ }
+ w.finish(t)
+}
+
+// wMaintenanceRetry (R9-5): a compaction PUT retried after a timeout.
+func wMaintenanceRetry(t *testing.T, w *world) {
+ b := w.boxes[0]
+ w.serve(b, 1, app0)
+ w.wake(b)
+ loc := w.claim.Holder.Location
+ gen := w.claim.Holder.Gen
+ var original *request
+ w.hold = func(r *request) bool {
+ if r.kind == rPut && r.b != nil && r.b.Level == 1 && original == nil {
+ original = r
+ return true // the first compaction attempt alone is held
+ }
+ return r == original
+ }
+ for i := 0; i < 3; i++ {
+ w.appWrite(b)
+ w.replicate(b) // three level-0 files: compaction issues its level-1 PUT, held
+ }
+ if original == nil {
+ t.Fatalf("witness: no compaction PUT was issued: %s", w.ltxShape(b.Region, dataKey(loc, gen, "")))
+ }
+ for i := 0; i <= uploadTimeout; i++ {
+ w.tick(func() { w.replicate(b) }) // the client times out; the next compaction pass retries and lands
+ }
+ if len(w.currentLTX(w.buckets[b.Region], dataKey(loc, gen, ""), 1)) == 0 {
+ // the retry may compact a wider range than the original, under its own key
+ t.Fatalf("witness: the compaction retry did not land: %s", w.ltxShape(b.Region, dataKey(loc, gen, "")))
+ }
+ w.idleStop(b)
+ sk := closedKey(loc, gen, b.DB.Session)
+ for i := 0; i < 10; i++ {
+ w.tick(func() { w.replicate(b) })
+ if w.buckets[b.Region].current(sk) != nil {
+ w.violate("INV-2 (witness): box %d wrote its certificate while its original compaction PUT %s was unresolved (R9-5)", b.ID, original.key)
+ return
+ }
+ }
+ w.hold = nil
+ w.completeHeld(original.key)
+ w.finish(t)
+}
+
+// wLostResponse (R9-5): a snapshot PUT whose response is lost.
+func wLostResponse(t *testing.T, w *world) {
+ b := w.boxes[0]
+ w.serve(b, 1, app0)
+ w.wake(b)
+ loc := w.claim.Holder.Location
+ gen := w.claim.Holder.Gen
+ var original *request
+ w.hold = func(r *request) bool {
+ if r.kind == rPut && r.b != nil && r.b.Level == 9 && original == nil {
+ original = r
+ return true // the snapshot PUT alone is held
+ }
+ return r == original
+ }
+ for i := 0; i < 3; i++ {
+ w.appWrite(b)
+ w.replicate(b) // compaction rotates a snapshot, whose PUT is held
+ }
+ if original == nil {
+ t.Fatalf("witness: no snapshot PUT was issued: %s", w.ltxShape(b.Region, dataKey(loc, gen, "")))
+ }
+ for i := 0; i <= uploadTimeout; i++ {
+ w.tick(func() { w.replicate(b) }) // the client gives up on it
+ }
+ w.hold = nil
+ w.completeHeld(original.key) // the server completes it after the client gave up: a lost response
+ w.idleStop(b)
+ sk := closedKey(loc, gen, b.DB.Session)
+ for i := 0; i < 10; i++ {
+ w.tick(func() { w.replicate(b) })
+ if w.buckets[b.Region].current(sk) != nil {
+ w.violate("INV-2 (witness): box %d wrote its certificate while the response to its snapshot PUT %s was lost (R9-5)", b.ID, original.key)
+ return
+ }
+ }
+ w.finish(t)
+}
diff --git a/internal/sim/hostlife/world_test.go b/internal/sim/hostlife/world_test.go
index d321f3ad9..18028fcb0 100644
--- a/internal/sim/hostlife/world_test.go
+++ b/internal/sim/hostlife/world_test.go
@@ -359,11 +359,14 @@ type box struct {
// writer is admitted only if its stamp equals the active one.
Stamps map[int]*stamps
Parked int // count of locally parked artifacts
- // lineage is the local lineage file per incarnation: the generation and
- // session the writer that opened this database was admitted to (claim
- // rev 6.8 §6.4a, R8-4). Lost with the disk; never written by a stamp
- // re-initialization.
- lineage map[int]lineageRec
+ // open is an admitted writer's start in progress (rev 7.10 §7.14): the
+ // claim CAS is done and the PUT it must have acknowledged before the
+ // process starts (its first upload, its marker, its anchor) is
+ // outstanding; local bookkeeping, not a claim transition
+ open *openState
+ // PurgeFails is the fault: the purge of the local database an admitted
+ // writer must make before it starts returns an error (claim rev 6.9)
+ PurgeFails bool
// anchors are the PUTs this box's activator must see acknowledged before
// it goes on (an anchor, a recovery's snapshot, a closed.json), by key
// (rev 7.7, R6-1): a request the client has waited uploadTimeout steps
@@ -564,6 +567,10 @@ type holder struct {
// current (moves rev 6 §5.1): "" is origin; a move, a push and a dirty
// rollback each install a generation named by their op id.
Gen string
+ // WriterBox is holder.writer_box (claim rev 6.9): the box every
+ // admission names as the current writer; it survives operation
+ // replacement, so a later cold admission's writes_lost names it (R9-2).
+ WriterBox int
// Session is holder.session (claim rev 6.8 §6.4a, R8-1): the gen of the
// AdmitWriter CAS that admitted the current writer session. Every path
// that opens replication goes through that CAS, which moves the
@@ -596,41 +603,42 @@ type writerEntry struct {
Session, Box int
Gen string
Stamp int
- Mode string
- Opened bool
+ Mode string // warm or cold (claim rev 6.9)
Pred pred
+ Lost *writesLost // a cold admission whose observed session had no certificate (claim rev 6.9, R9-2)
}
-// pred is the predecessor a cold admission journals before the recovery
-// stamp activates (claim rev 6.8 §6.4a, R8-4).
+// pred is the predecessor an admission journals: the session, writer box,
+// generation and stamp it observed.
type pred struct {
Session, Box int
Gen string
Stamp int
}
-// recState is a cold admission's build in progress (moves rev 7.9 §7.14):
-// the new generation, the predecessor generation it restores from, the
-// session and box admitted, the phase, the predecessor, and the snapshot
-// identity once written.
-type recState struct {
- Region int // the admitting box's region, where the generation under construction lives
-
- Gen, Base string
- Session, Box int
- Phase string
- Pred pred
- BaseVer int
- BaseKey string
- BaseTX int
+// openState is an admitted writer between its AdmitWriter CAS and its
+// process start (rev 7.10 §7.14): the generation and session it was
+// admitted to, the database it restored, and the stage whose PUT it waits
+// for: "first" (a fresh generation's full first upload), "marker"
+// (generation.json), "anchor" (a warm restore above the level-0 maximum).
+type openState struct {
+ Gen, Want string
+ Session int
+ Mode string
+ Prepared bool
+ DB *localDB
+ stage string
+ req *request
}
-// lineageRec is the local lineage file a writer writes as it opens (claim
-// rev 6.8 §6.4a): the generation and session it was admitted to. A stamp
-// re-initialization never writes it (R8-4).
-type lineageRec struct {
- Gen string
- Session int
+// writesLost is claim rev 6.9's writes_lost record: the writer whose
+// acknowledged, unuploaded writes a cold admission leaves behind, named by
+// holder.writer_box, never inferred from op.exec (R9-2). The box alerts.
+type writesLost struct {
+ Box int
+ Gen string
+ Session int
+ RemoteMaxTXID int
}
type opState struct {
@@ -649,46 +657,44 @@ type opState struct {
NewSerial int
// journal
- ReportAt int
- ReportOK bool
- CutAt int
- CutDeadline int
- StopAt int
- StopDigest digest
- StopFiles *filesDir
- SealDB ref
- SealFiles ref
- SealQuiet int
- LandPhase string
- Installed digest
- ProbeTries int
- ProbedAt int
- RevPhase string
- SrcPhase string
- Dirty bool
- DirtyKnown bool
- ReturnDB ref
- ReturnFiles ref
- ReturnQuiet int
- LostBox int
- LostAt int
- RollbackID string
- PushSnap *blob // a push's installed snapshot (the final checkpoint plus the push's mark)
- BaseKey string
- BaseTX int
- RecVer int // a delete's or purge's intent: the record version it will DeleteIfMatch (claim §5.2 step 1, §5.3 step 4)
- FlipGen int // the holder.stamp the flip CAS wrote: the landing's installation stamp (claim rev 6.5 §6.4)
- SrcStamp int // the source installation's stamp before the flip, for the return to source (claim rev 6.5)
- // Writers is op.journal.writers (claim rev 6.8 §6.4a): one entry per
- // AdmitWriter CAS. Rec is a cold admission whose build (the new
- // generation's snapshot and anchor, generation.json) is still in
- // progress; it never replaces the operation (R8-2). InstGen is the
- // generation an operation is installing when a cold admission within it
- // moved it off the op id; "" means the op id (or the rollback id).
+ ReportAt int
+ ReportOK bool
+ CutAt int
+ CutDeadline int
+ StopAt int
+ StopDigest digest
+ StopFiles *filesDir
+ SealDB ref
+ SealFiles ref
+ SealQuiet int
+ LandPhase string
+ Installed digest
+ ProbeTries int
+ ProbedAt int
+ RevPhase string
+ SrcPhase string
+ Dirty bool
+ DirtyKnown bool
+ ReturnDB ref
+ ReturnFiles ref
+ ReturnQuiet int
+ ReturnParked bool // the return lane's park-staging chore is owed (rev 7.10)
+ LostBox int
+ LostAt int
+ RollbackID string
+ PushSnap *blob // a push's installed snapshot (the final checkpoint plus the push's mark)
+ BaseKey string
+ BaseTX int
+ RecVer int // a delete's or purge's intent: the record version it will DeleteIfMatch (claim §5.2 step 1, §5.3 step 4)
+ FlipGen int // the holder.stamp the flip CAS wrote: the landing's installation stamp (claim rev 6.5 §6.4)
+ SrcStamp int // the source installation's stamp before the flip, for the return to source (claim rev 6.5)
+ // Writers is op.journal.writers (claim rev 6.9 §6.4a): one entry per
+ // AdmitWriter CAS. It is the operation's, dropped with it; the writer's
+ // box lives in holder.writer_box (R9-2). SrcGen is the source's
+ // generation at the move's start, which a clean rollback's return CAS
+ // names again (rev 7.10 §7.14).
Writers []writerEntry
- Rec *recState
- InstGen string
- Fresh bool // the operation's freshly built generation has had no writer yet: its first probe is admitted cold without another build
+ SrcGen string
Committed bool
Opened bool
ParkLocalNow bool
@@ -817,6 +823,9 @@ type world struct {
// for is accepted and completes only when the witness says so
// (witness_test.go). The random sweep never sets it.
hold func(r *request) bool
+ // lastIssued is the request issue saw last, for a caller that needs
+ // the request object behind a helper's return value (resumeOpen)
+ lastIssued *request
// stampBox records, for every installation stamp the claim issued, the
// box whose installation it names (claim rev 6.5: holder.stamp always
// names the installation op.exec should run). The oracle refuses an
@@ -961,9 +970,11 @@ func (c *claim) clone() *claim {
n.Op.Parts = append([]int(nil), c.Op.Parts...)
n.Op.StopFiles = c.Op.StopFiles.clone()
n.Op.Writers = append([]writerEntry(nil), c.Op.Writers...)
- if c.Op.Rec != nil {
- r := *c.Op.Rec
- n.Op.Rec = &r
+ for i := range n.Op.Writers {
+ if l := n.Op.Writers[i].Lost; l != nil {
+ cp := *l
+ n.Op.Writers[i].Lost = &cp
+ }
}
n.Regions = append([]int(nil), c.Regions...)
n.Boxes = append([]int(nil), c.Boxes...)
@@ -1008,6 +1019,7 @@ func (w *world) iamCheck(actorBox int, r *request) bool {
// (the request may still complete later).
func (w *world) issue(actorBox int, r *request) int {
r.at = w.now
+ w.lastIssued = r
if r.kind == rPut && r.b != nil && isDataKey(r.key) && (r.b.Min == 0 || r.b.Max == 0) {
// INV-12 (R8-3): the pinned LTX encoder refuses a zero TXID, so no
// such file can exist; a position-0 snapshot [1,0] or anchor [0,0]