amadan

carlos / platform Public

zdd plan 3 final fix: the sim's process death is one transition (F2)

die marks the process dead and removes it from the model's running set
in one critical section (w.mu, then p.mu), so a reaper that sees
Exited() never finds it still listed and a concurrent die waits for the
first. TestSimDeathIsOneTransition drives the death/release interleaving
through a dying hook, with and without a concurrent die.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 29119d3d8262ea09c22e04f9c969c3699ef938ba parent 31bf28b
1 file changed, +55 −6
  • internal/activator/swap_sim_test.go +55 −6
diff --git a/internal/activator/swap_sim_test.go b/internal/activator/swap_sim_test.go
index 9bb36cf59..55add7e38 100644
--- a/internal/activator/swap_sim_test.go
+++ b/internal/activator/swap_sim_test.go
@@ -150,7 +150,8 @@ func (s *simLogSink) Write(p []byte) (int, error) {
// simWorld is the model: which simulated processes run on each host, the
// live link, the staged builds, and the violations seen. Lock order: a
// caller may hold a.mu when it takes w.mu (the backend is called under the
-// entry lock), never the reverse.
+// entry lock), never the reverse; a process's own p.mu nests inside w.mu
+// (die), never the reverse.
type simWorld struct {
mu sync.Mutex
rng *rand.Rand
@@ -177,6 +178,10 @@ type simWorld struct {
// outcomes counts the seed's settings and its Swap results by mode,
// outcome and reason, so a sweep shows what it reached.
outcomes map[string]int
+ // dying, when set, runs once a death is published, with no model lock
+ // held: the moment a reaper that saw Exited() could act. The model's
+ // own interleaving test sets it; the sweep never does.
+ dying func(p *simProc)
}
func (w *simWorld) logf(format string, args ...any) {
@@ -420,18 +425,24 @@ func (p *simProc) Exited() bool {
return p.dead
}
+// die is one transition of the model: the process is marked dead and
+// leaves running in the same critical section (w.mu, then p.mu, the
+// model's lock order), so no observer can see it Exited() and still
+// running. A concurrent die waits on w.mu and finds it already dead.
func (p *simProc) die(why string) {
+ p.w.mu.Lock()
p.mu.Lock()
was := p.dead
p.dead = true
p.mu.Unlock()
- if was {
- return
+ if !was {
+ delete(p.w.running[p.host], p)
+ p.w.events = append(p.w.events, fmt.Sprintf("exit p%d (%s)", p.id, why))
}
- p.w.mu.Lock()
- delete(p.w.running[p.host], p)
- p.w.events = append(p.w.events, fmt.Sprintf("exit p%d (%s)", p.id, why))
p.w.mu.Unlock()
+ if !was && p.w.dying != nil {
+ p.w.dying(p)
+ }
}
type simRep struct {
@@ -905,3 +916,41 @@ func simulateSwapOnce(seed int, staged map[string]simArtifact, sockDir string, s
<-checked
return w.snapshot()
}
+
+// The model's death is one transition (final review F2): a reaper that
+// sees a process Exited() and releases its lease never finds the same
+// process still listed as running, so the sweep cannot report a false I2.
+// The dying hook runs at the one point a reaper could act during a death;
+// a second, concurrent die of the same process returns there too.
+func TestSimDeathIsOneTransition(t *testing.T) {
+ for _, concurrent := range []bool{false, true} {
+ w := &simWorld{rng: rand.New(rand.NewSource(1)), running: map[string]map[*simProc]bool{},
+ live: map[string]string{}, staged: map[string]string{}, seen: map[string]bool{}, outcomes: map[string]int{},
+ killFails: map[string]int{}}
+ p := w.spawn("h.example.com", "v1", 1, true)
+ fired := false
+ w.dying = func(q *simProc) {
+ if fired {
+ return
+ }
+ fired = true
+ if concurrent {
+ q.die("concurrent")
+ }
+ // A reaper: the process reads as exited, so it gives the lease back.
+ if q.Exited() {
+ w.leaseFreed(q.host, "reaper")
+ }
+ }
+ p.die("first")
+ if !fired {
+ t.Fatalf("concurrent %v: the dying hook never ran", concurrent)
+ }
+ if v, ev, _ := w.snapshot(); len(v) != 0 {
+ t.Fatalf("concurrent %v: the model reported %v\n%s", concurrent, v, strings.Join(ev, "\n"))
+ }
+ if n := w.runningOn("h.example.com"); n != 0 {
+ t.Fatalf("concurrent %v: %d process(es) still listed after the death", concurrent, n)
+ }
+ }
+}