amadan

carlos / platform Public

sim: relocReleasing and relocProbeFailed journal their release through relocJournalRelease, the one copy of the release-and-journal CAS (final review Important 3); two-box COUNTERS and traces unchanged

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Paul Campbell pushed by claude 04c9487da9026d425a5eb5d02b947db2f16c0633 parent 3f86896
2 files changed, +14 −32
  • internal/sim/hostlife/moves_test.go +1 −1
  • internal/sim/hostlife/regionha_test.go +13 −31
diff --git a/internal/sim/hostlife/moves_test.go b/internal/sim/hostlife/moves_test.go
index 5c25972ad..3b434c9d7 100644
--- a/internal/sim/hostlife/moves_test.go
+++ b/internal/sim/hostlife/moves_test.go
@@ -311,7 +311,7 @@ func (w *world) relocate(b *box, c *claim) {
// The mutation goes on into the phase switch, as rev 7 did
w.stats["relocation: phase held, a participant's fence is pending"]++
if (op.Phase == "releasing" || op.Phase == "probe-failed") && b.ID == op.Exec && (op.Release == nil || op.Release.Box != op.Exec) {
- w.relocJournalRelease(b, c)
+ w.relocJournalRelease(b, c, true)
}
return
}
diff --git a/internal/sim/hostlife/regionha_test.go b/internal/sim/hostlife/regionha_test.go
index a32a4705f..ee54ac62d 100644
--- a/internal/sim/hostlife/regionha_test.go
+++ b/internal/sim/hostlife/regionha_test.go
@@ -690,20 +690,7 @@ func (w *world) relocReleasing(b *box, c *claim) {
}
return
}
- r := w.relocRelease(b, c)
- if r == nil {
- return
- }
- if w.cas(c, func(n *claim) bool {
- ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "releasing" && n.Op.Exec == b.ID && n.Op.Release == nil
- if ok {
- n.Op.Release = r
- }
- return ok
- }) {
- w.stats["release journaled: source"]++
- w.logf("relocation %s: box %d released the host at TXID %d (flushed=%v)", op.ID, b.ID, r.FinalTX, r.Flushed)
- }
+ w.relocJournalRelease(b, c, false)
return
}
if on("reloc-ack-before-pinning") && !acked(c) {
@@ -1247,19 +1234,7 @@ func (w *world) relocProbeFailed(b *box, c *claim) {
if b.ID != op.Exec {
return
}
- r := w.relocRelease(b, c)
- if r == nil {
- return
- }
- if w.cas(c, func(n *claim) bool {
- ok := sameOp(n.Op.ID, op.ID) && n.Op.Kind == "relocating" && n.Op.Phase == "probe-failed" && n.Op.Exec == b.ID && (n.Op.Release == nil || n.Op.Release.Box != b.ID)
- if ok {
- n.Op.Release = r
- }
- return ok
- }) {
- w.stats["release journaled: failed target"]++
- }
+ w.relocJournalRelease(b, c, false)
return
}
if on("reloc-replacement-cap") && op.Replacements >= maxReplacements {
@@ -2367,9 +2342,12 @@ func (w *world) preparedManifestHere(b *box, c *claim, gen string) bool {
// relocJournalRelease is the participant's release (1b-next Task 7): the
// live executor runs its release sequence and journals it
// (JournalRelease), the source in releasing, a failed target in
-// probe-failed. It is the release branch of relocReleasing and
-// relocProbeFailed, run by itself while a fence is pending (rev 8).
-func (w *world) relocJournalRelease(b *box, c *claim) {
+// probe-failed. relocReleasing and relocProbeFailed call it for their
+// release branch, and relocate calls it by itself while a fence is
+// pending (rev 8; pending marks the trace line). The CAS is the union of
+// the two phases' conditions: in releasing no release is journaled yet;
+// in probe-failed the journaled release, if any, is another box's.
+func (w *world) relocJournalRelease(b *box, c *claim, pending bool) {
op := c.Op
phase := op.Phase
r := w.relocRelease(b, c)
@@ -2388,6 +2366,10 @@ func (w *world) relocJournalRelease(b *box, c *claim) {
} else {
w.stats["release journaled: failed target"]++
}
- w.logf("relocation %s: box %d released the host at TXID %d (flushed=%v), a fence pending", op.ID, b.ID, r.FinalTX, r.Flushed)
+ note := ""
+ if pending {
+ note = ", a fence pending"
+ }
+ w.logf("relocation %s: box %d released the host at TXID %d (flushed=%v)%s", op.ID, b.ID, r.FinalTX, r.Flushed, note)
}
}