snapshot of https://github.com/seaweedfs/seaweedfs.git (master, 2026-09-16; blobs > 131072B omitted)

weed/ec/ec_lifecycle_model_test.go

@@ -0,0 +1,520 @@
+package ec
+
+import (
+	"fmt"
+	"sort"
+	"strings"
+	"testing"
+)
+
+// Bounded-exhaustive model check of the EC volume lifecycle.
+//
+// The randomized chaos harness samples the state space; this test enumerates
+// it. The lifecycle of one volume is modeled as a state machine whose
+// transitions mirror, step by step, the real pipelines in this package, and
+// the checker explores EVERY schedule within the bound: every operation, a
+// crash (kill, no cleanup) at every step boundary, an error return (which
+// runs the rollback, itself crashable at every step) at every step boundary,
+// a volume-server restart (running the startup reconciliation rules) in every
+// quiescent state, and every recovery re-run from every crashed state.
+//
+// Two safety invariants are asserted in every reachable state, including
+// mid-operation and post-crash:
+//
+//	I1 durability: the volume's data is always recoverable — the regular
+//	   replica exists, or some single generation holds at least dataShards
+//	   shard files.
+//	I2 single serving generation: at most one generation is ever mounted.
+//	I3 single generation on disk: the sweep-before-generate discipline keeps
+//	   at most one generation's files on disk through every schedule. (An
+//	   externally planted file breaks this by construction; that path is the
+//	   chaos harness's, not the orchestration's.)
+//
+// And one convergence property: from every quiescent state, the prescribed
+// recovery — re-running the interrupted operation, per the restart-not-resume
+// model — terminates in a clean state (a writable regular volume with no EC
+// leftovers, or exactly one complete mounted generation with no source
+// replica and no surplus copies).
+//
+// The model's fidelity contract: each step below names the code it stands
+// for. When the pipeline order changes, this file must change with it.
+//
+//	encode      = ProcessEcEncodeBatch/doEcEncode: markReadonly
+//	              (markVolumeReplicaWritable false) → sweep
+//	              (clearPreexistingEcShards, removes every prior generation) →
+//	              generate (VolumeEcShardsGenerate, a new generation's files) →
+//	              mount (VolumeEcShardsMount, registers it) → balance
+//	              (EcBalance; a crash mid-move leaves a surplus copy, never a
+//	              loss, because moves copy before they delete) → verify
+//	              (verifyEcShardsBeforeDelete) → deleteSource
+//	              (doDeleteVolumesWithLocations, the commit point).
+//	rollback    = rollbackFailedEcEncode, run only on an error return before
+//	              the commit: rollbackSweep (clearPreexistingEcShards again) →
+//	              restoreWritable. A kill runs nothing.
+//	decode      = DoEcDecode: collect (collectEcShards) → generateVolume
+//	              (VolumeEcShardsToVolume) → mountVolume (VolumeMount) →
+//	              verifyDecoded (verifyDecodedVolumeBeforeDelete) → three
+//	              per-location shard deletions (unmountAndDeleteEcShards).
+//	              Forward-only: no rollback.
+//	reconcile   = the volume server startup rules (weed/storage
+//	              disk_location_ec.go): with the source .dat present, a
+//	              partial generation fails validation and is deleted
+//	              (handleFoundEcxFile/validateEcVolume); surviving shard files
+//	              with their sidecars re-register (the #9212 adoption).
+//	dedup       = the balance's dedup phase removing surplus copies
+//	              (ecbalancer "dedup" moves + verifyEcShardOnKeepNode).
+//
+// Deliberately outside the model: multi-replica sources (the pipeline syncs
+// and reduces to one best replica before encoding), per-node shard placement
+// (I1/I2 do not depend on it), and externally planted files (the chaos
+// harness covers adoption of foreign shards).
+
+const (
+	modelDataShards  = 10
+	modelTotalShards = 14
+)
+
+type modelGen struct {
+	files   int  // shard files on disk, whether or not registered
+	mounted bool // registered and serving
+	surplus int  // duplicate copies left by an interrupted balance move
+}
+
+type modelState struct {
+	replica         bool
+	replicaReadonly bool
+	gens            []modelGen // oldest first; a new encode appends
+}
+
+func (s modelState) clone() modelState {
+	c := s
+	c.gens = append([]modelGen(nil), s.gens...)
+	return c
+}
+
+func (s modelState) key() string {
+	var b strings.Builder
+	fmt.Fprintf(&b, "r%v,ro%v", s.replica, s.replicaReadonly)
+	for _, g := range s.gens {
+		fmt.Fprintf(&b, "|f%d,m%v,s%d", g.files, g.mounted, g.surplus)
+	}
+	return b.String()
+}
+
+// dropEmptyGens removes generations with no files left.
+func (s *modelState) dropEmptyGens() {
+	kept := s.gens[:0]
+	for _, g := range s.gens {
+		if g.files > 0 {
+			kept = append(kept, g)
+		}
+	}
+	s.gens = kept
+}
+
+// ── invariants ──────────────────────────────────────────────────────────────
+
+func checkInvariants(s modelState) error {
+	// I1: durability.
+	recoverable := s.replica
+	for _, g := range s.gens {
+		if g.files >= modelDataShards {
+			recoverable = true
+		}
+	}
+	if !recoverable {
+		return fmt.Errorf("I1 violated: no replica and no generation with >= %d shard files", modelDataShards)
+	}
+	// I2: at most one mounted generation.
+	mounted := 0
+	for _, g := range s.gens {
+		if g.mounted {
+			mounted++
+		}
+	}
+	if mounted > 1 {
+		return fmt.Errorf("I2 violated: %d generations mounted", mounted)
+	}
+	// I3: at most one generation's files on disk.
+	withFiles := 0
+	for _, g := range s.gens {
+		if g.files > 0 {
+			withFiles++
+		}
+	}
+	if withFiles > 1 {
+		return fmt.Errorf("I3 violated: %d generations have files on disk", withFiles)
+	}
+	return nil
+}
+
+func isCleanEc(s modelState) bool {
+	if s.replica || len(s.gens) != 1 {
+		return false
+	}
+	g := s.gens[0]
+	return g.files == modelTotalShards && g.mounted && g.surplus == 0
+}
+
+// ── operations as step lists ────────────────────────────────────────────────
+
+// A step mutates the state; ok=false means the step's precondition failed
+// (the real command would return an error at this point).
+type modelStep struct {
+	name  string
+	apply func(*modelState) (ok bool)
+}
+
+func encodeSteps() []modelStep {
+	return []modelStep{
+		{"markReadonly", func(s *modelState) bool {
+			if !s.replica {
+				return false
+			}
+			s.replicaReadonly = true
+			return true
+		}},
+		// The orphan sweep tears down per (node, volume); a crash can land
+		// between nodes, leaving a partially removed generation.
+		{"sweepLoc0", func(s *modelState) bool { sweepLocation(s, 0); return true }},
+		{"sweepLoc1", func(s *modelState) bool { sweepLocation(s, 1); return true }},
+		{"sweepLoc2", func(s *modelState) bool { sweepLocation(s, 2); return true }},
+		// Generation writes the shard files on the generation host; a crash
+		// mid-write leaves a partial, unregistered set beside the .dat, which
+		// the startup validation removes and the next sweep also covers.
+		{"generateHalf", func(s *modelState) bool {
+			if !s.replica {
+				return false
+			}
+			s.gens = append(s.gens, modelGen{files: modelTotalShards / 2})
+			return true
+		}},
+		{"generateRest", func(s *modelState) bool {
+			s.gens[len(s.gens)-1].files = modelTotalShards
+			return true
+		}},
+		{"mount", func(s *modelState) bool {
+			s.gens[len(s.gens)-1].mounted = true
+			return true
+		}},
+		// balance: a completed run changes placement only. Its crash variant
+		// is modeled by crashing between "balanceCopy" and "balanceDelete":
+		// the copy landed, the source deletion did not.
+		{"balanceCopy", func(s *modelState) bool {
+			s.gens[len(s.gens)-1].surplus++
+			return true
+		}},
+		{"balanceDelete", func(s *modelState) bool {
+			s.gens[len(s.gens)-1].surplus--
+			return true
+		}},
+		{"verify", func(s *modelState) bool {
+			return s.gens[len(s.gens)-1].files >= modelDataShards
+		}},
+		{"deleteSource", func(s *modelState) bool {
+			s.replica = false
+			s.replicaReadonly = false
+			return true
+		}},
+	}
+}
+
+// encodeCommitIndex is the index of deleteSource: an error return at or after
+// it must not roll back (the shards are the only copy once it runs).
+func encodeCommitIndex() int { return len(encodeSteps()) - 1 }
+
+// sweepLocation removes one location's share of every generation's files —
+// the per-(node, volume) teardown of clearPreexistingEcShards. The last
+// location clears the remainder, sidecars included.
+func sweepLocation(s *modelState, loc int) {
+	for gi := range s.gens {
+		g := &s.gens[gi]
+		chunk := modelTotalShards / 3
+		if loc == 2 {
+			g.files, g.mounted, g.surplus = 0, false, 0
+		} else if g.files > chunk {
+			g.files -= chunk
+		} else {
+			g.files = 0
+		}
+	}
+	s.dropEmptyGens()
+}
+
+func rollbackSteps() []modelStep {
+	return []modelStep{
+		{"rollbackSweep", func(s *modelState) bool {
+			s.gens = nil
+			return true
+		}},
+		{"restoreWritable", func(s *modelState) bool {
+			if s.replica {
+				s.replicaReadonly = false
+			}
+			return true
+		}},
+	}
+}
+
+func decodeSteps() []modelStep {
+	steps := []modelStep{
+		{"collect", func(s *modelState) bool {
+			for _, g := range s.gens {
+				if g.mounted && g.files >= modelDataShards {
+					return true
+				}
+			}
+			return false
+		}},
+		{"generateVolume", func(s *modelState) bool {
+			s.replica = true
+			return true
+		}},
+		{"mountVolume", func(s *modelState) bool { return true }},
+		{"verifyDecoded", func(s *modelState) bool { return s.replica }},
+	}
+	// Shard deletion is per holder location; three locations model a spread
+	// volume, so a crash can land between any two of them.
+	for i := 0; i < 3; i++ {
+		i := i
+		steps = append(steps, modelStep{fmt.Sprintf("deleteShardsLoc%d", i), func(s *modelState) bool {
+			for gi := range s.gens {
+				g := &s.gens[gi]
+				if !g.mounted && g.files == 0 {
+					continue
+				}
+				// Each location holds roughly a third of the shards; the last
+				// pass clears the remainder and the generation with it.
+				chunk := modelTotalShards / 3
+				if i == 2 {
+					g.files, g.surplus, g.mounted = 0, 0, false
+				} else if g.files > chunk {
+					g.files -= chunk
+				}
+			}
+			s.dropEmptyGens()
+			return true
+		}})
+	}
+	return steps
+}
+
+// reconcile applies the volume-server startup rules after a crash-restart.
+func reconcile(s *modelState) {
+	for gi := range s.gens {
+		g := &s.gens[gi]
+		if s.replica && g.files < modelTotalShards {
+			// .dat present and the local generation is partial: validation
+			// fails and the files are removed (disk_location_ec.go).
+			g.files, g.mounted, g.surplus = 0, false, 0
+			continue
+		}
+		if g.files > 0 {
+			// Surviving files re-register through their sidecars (#9212).
+			g.mounted = true
+		}
+	}
+	s.dropEmptyGens()
+}
+
+// dedupSurplus is the balance dedup phase.
+func dedupSurplus(s *modelState) {
+	for gi := range s.gens {
+		s.gens[gi].surplus = 0
+	}
+}
+
+// ── recovery convergence ────────────────────────────────────────────────────
+
+// runToCompletion applies steps without interruption; false when a
+// precondition fails (the real re-run would error out).
+func runToCompletion(s *modelState, steps []modelStep) bool {
+	for _, st := range steps {
+		if !st.apply(s) {
+			return false
+		}
+	}
+	return true
+}
+
+// recover applies the prescribed recovery for a quiescent state and reports
+// whether it converges to a clean state. Per the restart-not-resume model:
+// a surviving replica means the encode restarts from scratch; no replica
+// means the encode had committed and only surplus cleanup can remain; a
+// mounted generation beside a replica can also be decoded away.
+func recoverModel(s modelState) (modelState, error) {
+	// A crash-restart happens before any operator action; its reconciliation
+	// must itself keep the invariants.
+	reconcile(&s)
+	if err := checkInvariants(s); err != nil {
+		return s, fmt.Errorf("after reconcile: %w", err)
+	}
+
+	if !s.replica {
+		// The encode committed: shards are the volume. Dedup cleans surplus.
+		dedupSurplus(&s)
+		if !isCleanEc(s) {
+			return s, fmt.Errorf("no replica and not clean EC")
+		}
+		return s, nil
+	}
+
+	// Replica survives: re-run the encode from scratch (sweep + regenerate),
+	// then the volume is EC; this is the restart path every interrupted
+	// encode and every leftover-orphan state takes.
+	if !runToCompletion(&s, encodeSteps()) {
+		return s, fmt.Errorf("recovery encode did not complete")
+	}
+	dedupSurplus(&s)
+	if err := checkInvariants(s); err != nil {
+		return s, fmt.Errorf("after recovery encode: %w", err)
+	}
+	if !isCleanEc(s) {
+		return s, fmt.Errorf("recovery encode did not converge to clean EC")
+	}
+	// And a decode must be able to bring it back to a regular volume.
+	if !runToCompletion(&s, decodeSteps()) {
+		return s, fmt.Errorf("decode after recovery did not complete")
+	}
+	if err := checkInvariants(s); err != nil {
+		return s, fmt.Errorf("after decode: %w", err)
+	}
+	if !s.replica || len(s.gens) != 0 {
+		return s, fmt.Errorf("decode after recovery did not converge to a bare regular volume")
+	}
+	return s, nil
+}
+
+// ── exhaustive exploration ──────────────────────────────────────────────────
+
+type trace []string
+
+// explore runs every schedule of one operation from state s: after every
+// step, the schedule may continue, crash (kill: stop, nothing else runs), or
+// error out (rollback runs, itself crashable at every step). Every resulting
+// quiescent state is handed to onQuiescent together with the trace that
+// produced it.
+func exploreOp(t *testing.T, s modelState, opName string, steps []modelStep, commitIndex int, withRollback bool, tr trace, onQuiescent func(modelState, trace)) {
+	t.Helper()
+	// Crash before the first step is the same as never starting.
+	for prefix := 1; prefix <= len(steps); prefix++ {
+		run := s.clone()
+		ok := true
+		for i := 0; i < prefix; i++ {
+			if !steps[i].apply(&run) {
+				ok = false
+				break
+			}
+			if err := checkInvariants(run); err != nil {
+				t.Fatalf("%s after %s: %v\ntrace: %v", opName, steps[i].name, err, append(tr, opName+"/"+steps[i].name))
+			}
+		}
+		if !ok {
+			continue // precondition stopped the op; same as an early error
+		}
+		stepTrace := append(append(trace{}, tr...), fmt.Sprintf("%s..%s", opName, steps[prefix-1].name))
+
+		// Kill here: nothing else runs.
+		onQuiescent(run.clone(), append(append(trace{}, stepTrace...), "KILL"))
+
+		// Error return here: the rollback runs, unless the op has committed;
+		// the rollback itself can be killed at each of its step boundaries.
+		if withRollback && prefix <= commitIndex {
+			rb := rollbackSteps()
+			for rbPrefix := 0; rbPrefix <= len(rb); rbPrefix++ {
+				rbRun := run.clone()
+				for i := 0; i < rbPrefix; i++ {
+					rb[i].apply(&rbRun)
+					if err := checkInvariants(rbRun); err != nil {
+						t.Fatalf("%s rollback after %s: %v\ntrace: %v", opName, rb[i].name, err, stepTrace)
+					}
+				}
+				suffix := "FAIL+rollback-killed"
+				if rbPrefix == len(rb) {
+					suffix = "FAIL+rollback-complete"
+				}
+				onQuiescent(rbRun.clone(), append(append(trace{}, stepTrace...), fmt.Sprintf("%s@%d", suffix, rbPrefix)))
+			}
+		}
+	}
+}
+
+// TestECLifecycleModelExhaustive enumerates every crash and failure schedule
+// of encode and decode up to two chained interrupted operations, checks the
+// safety invariants in every intermediate state, and requires the prescribed
+// recovery to converge from every quiescent state.
+func TestECLifecycleModelExhaustive(t *testing.T) {
+	start := modelState{replica: true}
+
+	visited := map[string]trace{}
+	quiescent := 0
+	schedules := 0
+	var enqueue func(s modelState, depth int, tr trace)
+
+	checkRecovery := func(s modelState, tr trace) {
+		schedules++
+		if _, seen := visited["Q"+s.key()]; seen {
+			return
+		}
+		visited["Q"+s.key()] = tr
+		quiescent++
+		if _, err := recoverModel(s.clone()); err != nil {
+			t.Fatalf("recovery does not converge: %v\nstate: %s\ntrace: %v", err, s.key(), tr)
+		}
+	}
+
+	enqueue = func(s modelState, depth int, tr trace) {
+		checkRecovery(s, tr)
+		if depth == 0 {
+			return
+		}
+		// A crash-restart may happen in any quiescent state before the next
+		// operation; explore both with and without it.
+		restarted := s.clone()
+		reconcile(&restarted)
+		if err := checkInvariants(restarted); err != nil {
+			t.Fatalf("reconcile violated invariants: %v\nstate: %s\ntrace: %v", err, s.key(), tr)
+		}
+		for _, variant := range []struct {
+			st  modelState
+			tag string
+		}{{s, ""}, {restarted, "+restart"}} {
+			st, tag := variant.st, variant.tag
+			if st.replica {
+				exploreOp(t, st, "encode"+tag, encodeSteps(), encodeCommitIndex(), true, tr, func(q modelState, qtr trace) {
+					enqueue(q, depth-1, qtr)
+				})
+			}
+			canDecode := false
+			for _, g := range st.gens {
+				if g.mounted && g.files >= modelDataShards {
+					canDecode = true
+				}
+			}
+			if canDecode {
+				exploreOp(t, st, "decode"+tag, decodeSteps(), len(decodeSteps()), false, tr, func(q modelState, qtr trace) {
+					enqueue(q, depth-1, qtr)
+				})
+			}
+		}
+	}
+
+	// Depth 2: an interrupted operation followed by another interrupted
+	// operation, recovery checked at every quiescent point in between and
+	// after. Deeper chains only revisit already-explored states (the state
+	// space is finite and memoized), which the visited count makes apparent.
+	enqueue(start, 2, trace{"start"})
+
+	// Not spec constants — collapse guards: if a refactor of the model or the
+	// explorer accidentally prunes schedules, these counts crater and this
+	// catches it. Update deliberately when the model changes fidelity.
+	if quiescent < 15 || schedules < 500 {
+		t.Fatalf("suspiciously small exploration: %d distinct quiescent states from %d schedules", quiescent, schedules)
+	}
+	keys := make([]string, 0, len(visited))
+	for k := range visited {
+		keys = append(keys, k)
+	}
+	sort.Strings(keys)
+	t.Logf("explored %d schedules reaching %d distinct quiescent states, all recoverable", schedules, quiescent)
+}