diff --git a/lib/system/yrc.nim b/lib/system/yrc.nim index 410d74acdb..a3c29d4d2c 100644 --- a/lib/system/yrc.nim +++ b/lib/system/yrc.nim @@ -1,23 +1,42 @@ # # YRC: Thread-safe ORC (concurrent cycle collector). -# Same API as orc.nim but with the global mutator/collector RWLock for safety. -# Destructors for refs run at collection time, not immediately on last decRef. -# See yrc_proof.lean for a Lean 4 proof of safety and deadlock freedom. +# Same API as orc.nim. Destructors for refs run at collection time, not +# immediately on the last decRef. +# See yrc_proof.lean for a machine-checked (Lean 4) proof of the core +# invariants — garbage stability, validation soundness, capture partition +# disjointness, grace periods, fence mutual exclusion, deadlock freedom — +# and yrc_tarjan_proof.lean for soundness AND completeness of the SCC +# deadness algorithm. # -# ## Locking Protocol +# ## Synchronization at a Glance # # Ref-field writes (`nimAsgnYrc`, `nimSinkYrc`) are LOCK-FREE: an atomic -# incRef of the new value, an atomic exchange of the slot, and a deferred -# decRef of the old value through the `toDec` stripe queues. Collection runs -# concurrently with them (see "The Write Barrier" below). +# incRef of the new value, an atomic exchange of the slot, a deferred +# decRef of the old value enqueued into a stripe queue. The stripe queues +# have LOCK-FREE PRODUCERS — reserve a slot by fetch-add, then publish it +# (see the Stripe declaration for the inc/dec publication asymmetry); the +# per-stripe consumerLock only serializes drains against each other. # -# Seq mutations that change the container structure (add/grow/shrink/setLen) -# still hold the mutator read lock, and the collector still acquires all -# write locks for the duration of a collection. Since ref assignments no -# longer contend on that lock, its only remaining jobs are: freezing seq -# len/payload pairs against the collector's traversal (so no deferred buffer -# frees and no torn len/pointer reads are possible), and collector-vs- -# collector exclusion. +# Candidate roots are THREAD-LOCAL (gLocalRoots): draining a thread's +# stripe registers candidates locally, and the thread's own collections +# steal that buffer as their root slice — the common path from +# "suspicious dec" to "freed" never crosses a thread. Exiting threads +# spill their buffer to a global orphan list, adopted by the next +# collection anywhere. A cell sits in at most one buffer, guarded by an +# atomic test-and-set of inRootsFlag; buffered cells are forced live. +# +# Up to MaxPar collections run CONCURRENTLY — with the mutators and with +# each other — each capturing a disjoint partition of the heap by CAS-ing +# a claim tag into the rootIdx header word. gMergeLock covers only the +# tag-slot claim and orphan adoption. All waiting (for a free slot, for a +# solo capture, for a grace period) is a bounded spin, then parking on +# gWaitCond. +# +# Seq mutations that change container structure (add/grow/setLen/shrink) +# announce themselves in the striped gSeqActive counters (seqs_v2.nim); a +# starting collection waits for those to drain (yrcGcFenceEnter) so its +# traversal never sees a torn len/payload pair or a freed payload. This +# fence is the only point where mutators delay a collector. # # ## The Write Barrier # @@ -31,7 +50,9 @@ # the *next* collection's merge: deletions can only make the captured # graph look MORE alive, never less. # * Stack copies enqueue into `toInc` (buffered incs). -# * Only `nimAsgnYrc`'s incRef mutates rc words directly (atomically). +# * Direct rc mutations (`nimAsgnYrc`'s incRef, queue drains, overflow +# incs) are atomic RMWs — globally visible when they retire, which the +# commit-time rc validation relies on. # # So the commit-time validation is: # 1. Any cell sitting in a `toInc`/`toDec` queue had its reference set @@ -54,9 +75,10 @@ # # 1. Capture: one Tarjan SCC traversal over everything reachable from the # candidate roots. Node -> dense index lookup is O(1) without hashing: -# the spare `rootIdx` header word (unused by YRC otherwise) is stamped -# with an epoch-tagged discovery index, so stale stamps never need -# clearing. Everything else lives in side arrays (SoA layout). +# the spare `rootIdx` header word is CAS-claimed with the collection's +# tag packed with the discovery index; stale tags of retired +# collections never need clearing. Everything else lives in side +# arrays (SoA layout). # # 2. Deadness: pure array work on the captured SCC condensation, no heap # access. An SCC is garbage iff it has no references beyond its internal @@ -66,20 +88,36 @@ # Tarjan emits SCCs sinks-first, so one linear scan in reverse emission # order settles every SCC (sources before their targets). # -# 3. Commit: only members of dead SCCs are touched. Every slot of a dead -# member is nil'ed; slots pointing at survivors decrement the survivor's -# rc for real (edges inside the dead group die with the group). Then the -# members are destroyed and freed. Because the slots are nil by the time -# destructors run, destructors cannot re-enter the decRef machinery for -# the already-processed edges. +# 3. Validate & commit: after validation (dirty peek + rc recheck, with +# demotions propagated to captured cross targets) and a grace period +# (foreign captures may still hold stale slot snapshots), only members +# of dead SCCs are touched. Every slot of a dead member is nil'ed; +# slots pointing at survivors decrement the survivor's rc for real +# (edges inside the dead group die with the group). Then the members +# are destroyed and freed — the slots are nil by the time destructors +# run, so destructors cannot re-enter the decRef machinery for the +# already-processed edges. When everything captured died and no +# cross-collection or pruned edge was seen, nil+free fuse into a +# single pass. # # This structure visits each edge at most twice (capture + commit of the # dead subset) instead of up to three times, and — because the outcome is -# decided on captured data and the heap is only written in commit — it is -# the stepping stone towards optimistic, lock-free collection: replace the -# frozen-heap invariant with a SATB write barrier plus commit-time -# validation (rc word unchanged since capture, no barrier hit on a member) -# and the same three phases run concurrently with mutators. +# decided on captured data and the heap is only written in commit — +# capture runs OPTIMISTICALLY, concurrent with mutators and with other +# collections, with the validation above as the safety net. +# +# ## Generational Epoch Stamps +# +# Commit re-stamps the cells it PROVED live with the current epoch and +# their survival age (same rootIdx word, in a namespace disjoint from the +# claim tags). Within that epoch, captures treat a stamped DESCENDANT of +# promoted age as an opaque live external and do not descend: long-lived +# structures are traced once per epoch instead of once per collection, +# while die-young data — never promoted — is never deferred. Roots always +# bypass stamps (every death has a dec-witness that gets registered, and +# registered cells are always scanned as roots), and explicit full +# collects advance the epoch first, staying exhaustive. The price is +# floating garbage bounded by ~2 epochs. # # ## Why No Lost Objects # @@ -101,11 +139,9 @@ import std/locks const NumStripes = 64 QueueSize {.intdefine.} = 128 # override with -d:QueueSize=N - RootsThreshold = 10 - colBlack = 0b000 - colGray = 0b001 - colWhite = 0b010 + # rc-word flag bits, layout shared with ORC. YRC does no tricolor + # marking; colorMask survives only for the debug printout. maybeCycle = 0b100 inRootsFlag = 0b1000 colorMask = 0b011 @@ -113,7 +149,6 @@ const type TraceProc = proc (p, env: pointer) {.nimcall, gcsafe, raises: [].} - DisposeProc = proc (p: pointer) {.nimcall, gcsafe, raises: [].} # With lock-free ref assignments, rc words are mutated concurrently with the # collector (direct atomic incRefs), so all collector-side rc accesses must @@ -135,14 +170,6 @@ when useAtomicRc: if atomicCompareExchangeN(addr c.rc, addr expected, desired, true, ATOMIC_ACQ_REL, ATOMIC_RELAXED): break - template rcSetFlag(c, flag) = - block: - var expected = atomicLoadN(addr c.rc, ATOMIC_RELAXED) - while true: - let desired = expected or flag - if atomicCompareExchangeN(addr c.rc, addr expected, desired, true, - ATOMIC_ACQ_REL, ATOMIC_RELAXED): - break template rcTestSetFlag(c, flag): bool = ## Atomically set `flag`; evaluates to true iff THIS call set it (it ## was clear). Candidate registration must win this race so that a @@ -162,7 +189,6 @@ else: template trialDec(c) = c.rc = c.rc -% rcIncrement template trialInc(c) = c.rc = c.rc +% rcIncrement template rcClearFlag(c, flag) = c.rc = c.rc and not flag - template rcSetFlag(c, flag) = c.rc = c.rc or flag template rcTestSetFlag(c, flag): bool = block: let won = (c.rc and flag) == 0 @@ -247,9 +273,9 @@ type sccOf: int32 # -1 while the cell is on the Tarjan stack CaptureBufs = object - ## side structure of a collection; persistent across collections (only - ## the collector, under the global write lock, ever touches it) so that - ## frequent small collections don't pay per-collection allocations + ## side structure of a collection; per collector thread (gCap is a + ## threadvar) and persistent across collections, so that frequent + ## small collections don't pay per-collection allocations recs: RawSeq[CaptureRec] tstack: RawSeq[int32] frames: RawSeq[TarjanFrame] @@ -403,19 +429,32 @@ else: type Stripe = object - when not defined(yrcAtomics): - lockInc: Lock - toIncLen: int + consumerLock: Lock + ## consumers (drains) exclude each other; producers and the + ## validation peek are lock-free + toIncLen: int # reservation counters; may exceed QueueSize under + toDecLen: int # overflow — reservations past QueueSize never write toInc: array[QueueSize, Cell] - lockDec: Lock - toDecLen: int + ## produced lock-free: reserve via fetch-add, publish the cell with + ## an atomic EXCHANGE (non-nil = ready; globals start zeroed and the + ## consumer nils consumed slots). The publish must be an RMW, not a + ## release store: a queued inc means the rc word UNDER-counts a live + ## reference, so the validation peek must reliably observe every + ## entry of a completed barrier — an RMW is globally ordered when it + ## retires, a release store could still sit in a store buffer. toDec: array[QueueSize, (Cell, PNimTypeV2)] + ## produced lock-free: reserve via fetch-add, store the cell, then + ## publish by storing the desc with release order (desc != nil = + ## ready). A plain release suffices here: a pending dec leaves the + ## target's rc with an unexplained surplus that forces it live even + ## if a peek misses the entry. type PreventThreadFromCollectProc* = proc(): bool {.nimcall, gcsafe, raises: [].} ## Callback run before this thread runs the cycle collector. ## Return `true` to allow collection, `false` to skip (e.g. real-time thread). - ## Invoked while holding the global lock; must not call back into YRC. + ## Invoked lock-free before this thread would start a collection; + ## must not call back into YRC. var roots: CellSeq[Cell] # ORPHANED candidates only: spilled by exiting @@ -471,39 +510,18 @@ proc nimIncRefCyclic(p: pointer; cyclic: bool) {.compilerRtl, inl.} = if cyclic: h.rc = h.rc or maybeCycle when defined(nimYrcAtomicIncs): discard atomicFetchAdd(addr h.rc, rcIncrement, ATOMIC_ACQ_REL) - elif defined(yrcAtomics): - let s = getStripeIdx() - let slot = atomicFetchAdd(addr stripes[s].toIncLen, 1, ATOMIC_ACQ_REL) - if slot < QueueSize: - atomicStoreN(addr stripes[s].toInc[slot], h, ATOMIC_RELEASE) - else: - trialInc(h) - for i in 0..= QueueSize: + discard atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQ_REL) + break + else: + var cur = reserved + if atomicCompareExchangeN(addr stripes[i].toIncLen, addr cur, 0, + false, ATOMIC_ACQ_REL, ATOMIC_RELAXED): + break + var consumed = 0 + while true: + let reserved = atomicLoadN(addr stripes[i].toDecLen, ATOMIC_ACQUIRE) + let n = min(reserved, QueueSize) + for j in consumed ..< n: + var desc = atomicLoadN(addr stripes[i].toDec[j][1], ATOMIC_ACQUIRE) + while desc == nil: + desc = atomicLoadN(addr stripes[i].toDec[j][1], ATOMIC_ACQUIRE) + let c = stripes[i].toDec[j][0] + trialDec(c) + registerLocal(c, desc) + atomicStoreN(addr stripes[i].toDec[j][1], cast[PNimTypeV2](nil), + ATOMIC_RELAXED) + consumed = n + if reserved >= QueueSize: + discard atomicExchangeN(addr stripes[i].toDecLen, 0, ATOMIC_ACQ_REL) + break + else: + var cur = reserved + if atomicCompareExchangeN(addr stripes[i].toDecLen, addr cur, 0, false, + ATOMIC_ACQ_REL, ATOMIC_RELAXED): + break + # new reservations arrived during processing: consume them too proc drainAllStripes() = ## Full-collect path: apply every pending RC operation; every resulting @@ -863,32 +916,36 @@ proc markDirtyFromQueues(j: var GcEnv; cap: ptr CaptureBufs) = cap.sccFlags.d[s] = cap.sccFlags.d[s] or flagDirty for i in 0.. s`. This induction principle is the + well-definedness of the whole scheme. -/ + +theorem descending_induction {n : Nat} (P : Fin n → Prop) + (step : ∀ s : Fin n, (∀ u : Fin n, s < u → P u) → P s) : + ∀ s, P s := by + have key : ∀ k, ∀ s : Fin n, n - s.val ≤ k → P s := by + intro k + induction k with + | zero => + intro s hs + have := s.isLt + omega + | succ k ih => + intro s _ + apply step + intro u hu + apply ih + have h1 := u.isLt + have h2 : s.val < u.val := hu + omega + intro s + exact key n s (by omega) + +/-! ## §2 The condensation and the liveness spec + + `edges` are the captured condensation cross edges (with multiplicity: + one entry per traversed slot, exactly like cap.edges bucketed into + crossTgt). `extRefs s` counts references into SCC `s` from OUTSIDE + the capture: stack refs, uncaptured heap cells, other collections' + partitions — everything in Σrc not explained by captured edges. + `seed s` is the inRootsFlag forcedLive seeding. -/ + +section Condensation + +variable {n : Nat} +variable (edges : List (Fin n × Fin n)) +variable (extRefs : Fin n → Nat) +variable (seed : Fin n → Bool) + +/-- The SPEC: an SCC is live iff something external anchors it — + directly or through a chain of captured cross edges. -/ +inductive LiveScc : Fin n → Prop where + | ext (s : Fin n) : 0 < extRefs s → LiveScc s + | root (s : Fin n) : seed s = true → LiveScc s + | pred (u s : Fin n) : (u, s) ∈ edges → LiveScc u → LiveScc s + +/-- The per-SCC equation the reverse scan establishes: dead iff no + external refs, no seed, and ALL cross predecessors dead. (The + sinks-first order makes this a valid definition: every predecessor + has a higher id and is decided first — see `descending_induction`; + without that order the "definition" would be circular.) -/ +def ScanEq (dead : Fin n → Bool) : Prop := + ∀ s, dead s = true ↔ + (extRefs s = 0 ∧ seed s = false ∧ + ∀ e ∈ edges, e.2 = s → dead e.1 = true) + +/-- Live SCCs are never marked dead (soundness direction). -/ +theorem live_not_dead (dead : Fin n → Bool) + (hfix : ScanEq edges extRefs seed dead) : + ∀ s, LiveScc edges extRefs seed s → dead s ≠ true := by + intro s hl + induction hl with + | ext s h => + intro hd + have := ((hfix s).mp hd).1 + omega + | root s h => + intro hd + have := ((hfix s).mp hd).2.1 + rw [h] at this + cases this + | pred u s hmem _ ih => + intro hd + exact ih (((hfix s).mp hd).2.2 (u, s) hmem rfl) + +/-- Non-live SCCs are always marked dead (completeness direction) — + by descending induction along the scan order. -/ +theorem not_live_dead + (horder : ∀ e ∈ edges, e.2 < e.1) + (dead : Fin n → Bool) + (hfix : ScanEq edges extRefs seed dead) : + ∀ s, ¬ LiveScc edges extRefs seed s → dead s = true := by + refine descending_induction + (fun s => ¬ LiveScc edges extRefs seed s → dead s = true) ?_ + intro s ihs hnl + rw [hfix] + refine ⟨?_, ?_, ?_⟩ + · cases Nat.eq_zero_or_pos (extRefs s) with + | inl h => exact h + | inr h => exact absurd (LiveScc.ext s h) hnl + · cases hsd : seed s with + | false => rfl + | true => exact absurd (LiveScc.root s hsd) hnl + · intro e he hes + have hlt : s < e.1 := by + have := horder e he + rw [hes] at this + exact this + apply ihs e.1 hlt + intro hlu + have hmem : (e.1, s) ∈ edges := by + rw [← hes] + simpa using he + exact hnl (LiveScc.pred e.1 s hmem hlu) + +/-- **Main condensation theorem**: the single reverse scan computes + EXACTLY the non-live SCCs. One Tarjan DFS + one linear scan replace + Bacon's three graph traversals, with no loss of precision on the + snapshot. -/ +theorem scan_dead_iff_not_live + (horder : ∀ e ∈ edges, e.2 < e.1) + (dead : Fin n → Bool) + (hfix : ScanEq edges extRefs seed dead) : + ∀ s, dead s = true ↔ ¬ LiveScc edges extRefs seed s := by + intro s + constructor + · intro hd hl + exact live_not_dead edges extRefs seed dead hfix s hl hd + · exact not_live_dead edges extRefs seed horder dead hfix s + +/-! ## §3 The implementation's arithmetic form + + computeDeadness does not test "all predecessors dead" directly; it + maintains ext(s) = sumRefs(s) − internal(s) − deadIn(s) and a + forcedLive flag pushed along cross edges of live SCCs. We show this + is the same equation, given rc-exactness: + + sumRefs s = extRefs s + internal s + (# cross edges into s). + + ext(s) = 0 then says extRefs s = 0 AND every cross in-edge came from + a dead predecessor; ¬forcedLive says no seed and no LIVE predecessor + pushed the flag — together exactly `ScanEq`. -/ + +def inCount (s : Fin n) : Nat := + edges.countP (fun e => e.2 == s) + +def deadInCount (dead : Fin n → Bool) (s : Fin n) : Nat := + edges.countP (fun e => e.2 == s && dead e.1) + +/-- countP is monotone under pointwise implication. -/ +theorem countP_le_of_imp {α : Type} (l : List α) (p q : α → Bool) + (himp : ∀ x ∈ l, p x = true → q x = true) : + l.countP p ≤ l.countP q := by + induction l with + | nil => simp + | cons a l ih => + have iht := ih (fun x hx => himp x (List.mem_cons_of_mem a hx)) + by_cases hpa : p a = true + · have hqa := himp a (by simp) hpa + simp [hpa, hqa] + omega + · simp only [List.countP_cons] + have : p a = false := by + cases h : p a + · rfl + · exact absurd h hpa + simp [this] + omega + +/-- If a stronger predicate matches as often as a weaker one, they + agree on every element. -/ +theorem countP_eq_forces_all {α : Type} (l : List α) (p q : α → Bool) + (himp : ∀ x ∈ l, q x = true → p x = true) + (heq : l.countP p = l.countP q) : + ∀ x ∈ l, p x = true → q x = true := by + induction l with + | nil => intro x hx; cases hx + | cons a l ih => + have himpt : ∀ x ∈ l, q x = true → p x = true := + fun x hx => himp x (List.mem_cons_of_mem a hx) + have hmono := countP_le_of_imp l q p himpt + intro x hx hpx + simp only [List.countP_cons] at heq + cases List.mem_cons.mp hx with + | inl hxa => + subst hxa + cases hqx : q x with + | true => rfl + | false => + exfalso + simp [hpx, hqx] at heq + omega + | inr hxl => + have hqa_pa : (if q a = true then 1 else 0) ≤ (if p a = true then 1 else 0) := by + by_cases hq : q a = true + · simp [hq, himp a (by simp) hq] + · simp [hq] + have heqt : l.countP p = l.countP q := by + by_cases hq : q a = true + · simp [hq, himp a (by simp) hq] at heq + omega + · have hqf : q a = false := by + cases h : q a + · rfl + · exact absurd h hq + by_cases hp : p a = true + · simp [hp, hqf] at heq + omega + · have hpf : p a = false := by + cases h : p a + · rfl + · exact absurd h hp + simp [hpf, hqf] at heq + omega + exact ih himpt heqt x hxl hpx + +/-- If all cross predecessors of `s` are dead, deadIn equals the full + in-count (and vice versa). -/ +theorem deadIn_eq_inCount_iff (dead : Fin n → Bool) (s : Fin n) : + deadInCount edges dead s = inCount edges s ↔ + (∀ e ∈ edges, e.2 = s → dead e.1 = true) := by + constructor + · intro heq e he hes + have himp : ∀ x ∈ edges, (fun e => e.2 == s && dead e.1) x = true → + (fun e => e.2 == s) x = true := by + intro x _ hx + simp only [Bool.and_eq_true] at hx + exact hx.1 + have := countP_eq_forces_all edges + (fun e => e.2 == s) (fun e => e.2 == s && dead e.1) + himp heq.symm e he + have hbeq : (e.2 == s) = true := by + simp [hes] + have := this hbeq + simp only [Bool.and_eq_true] at this + exact this.2 + · intro hall + unfold deadInCount inCount + apply List.countP_congr + intro e he + by_cases hes : e.2 = s + · simp [hes, hall e he hes] + · have : (e.2 == s) = false := by + simp [hes] + simp [this] + +/-- The implementation's per-SCC decision, verbatim from + computeDeadness: NOT forced (no seed, no live predecessor pushed + the flag) and ext = sumRefs − internal − deadIn = 0 (stated + subtraction-free). -/ +def ImplEq (sumRefs internal : Fin n → Nat) (dead : Fin n → Bool) : Prop := + ∀ s, dead s = true ↔ + (¬ (seed s = true ∨ ∃ e ∈ edges, e.2 = s ∧ dead e.1 = false) ∧ + sumRefs s = internal s + deadInCount edges dead s) + +/-- **The arithmetic is the spec**: under rc-exactness, the + implementation's equation is `ScanEq`, so `scan_dead_iff_not_live` + applies to computeDeadness as written. -/ +theorem impl_fixpoint_is_spec + (sumRefs internal : Fin n → Nat) (dead : Fin n → Bool) + (hcount : ∀ s, sumRefs s = extRefs s + internal s + inCount edges s) + (himpl : ImplEq edges seed sumRefs internal dead) : + ScanEq edges extRefs seed dead := by + intro s + rw [himpl s] + constructor + · rintro ⟨hnf, harith⟩ + have hor := hnf + rw [not_or] at hor + obtain ⟨hseed, hnopred⟩ := hor + have hseedf : seed s = false := by + cases h : seed s + · rfl + · exact absurd h hseed + have hall : ∀ e ∈ edges, e.2 = s → dead e.1 = true := by + intro e he hes + cases h : dead e.1 with + | true => rfl + | false => exact absurd ⟨e, he, hes, h⟩ hnopred + have hdc := (deadIn_eq_inCount_iff edges dead s).mpr hall + have hc := hcount s + refine ⟨by omega, hseedf, hall⟩ + · rintro ⟨hext, hseedf, hall⟩ + have hdc := (deadIn_eq_inCount_iff edges dead s).mpr hall + refine ⟨?_, ?_⟩ + · rw [not_or] + refine ⟨by simp [hseedf], ?_⟩ + rintro ⟨e, he, hes, hdf⟩ + rw [hall e he hes] at hdf + cases hdf + · have hc := hcount s + omega + +end Condensation + +/-! ## §4 Cell-level correctness + + Bridge from the condensation to the actual heap snapshot. `extRef` + covers every reference source outside the capture: mutator stacks, + the roots buffer, uncaptured heap cells' slots that the arithmetic + cannot explain, and other collections' partitions (cross-collection + edges — this is the SCC-side view of `cross_target_live` in + yrc_proof.lean §5). -/ + +structure CellGraph where + edge : Obj → Obj → Prop + extRef : Obj → Prop + +/-- A cell is live iff an external reference anchors it through heap + edges (the cell-level ground truth; `anchored` of yrc_proof.lean). -/ +inductive CellLive (g : CellGraph) : Obj → Prop where + | ext (x : Obj) : g.extRef x → CellLive g x + | step (x y : Obj) : CellLive g x → g.edge x y → CellLive g y + +/-- Paths through heap edges, used to move liveness around inside an + SCC (Tarjan guarantees SCC members are mutually reachable). -/ +inductive EdgePath (g : CellGraph) : Obj → Obj → Prop where + | refl (x : Obj) : EdgePath g x x + | step (x y z : Obj) : EdgePath g x y → g.edge y z → EdgePath g x z + +theorem cellLive_along_path (g : CellGraph) (u v : Obj) + (hl : CellLive g u) (hp : EdgePath g u v) : CellLive g v := by + induction hp with + | refl => exact hl + | step _ _ _ hedge ih => exact CellLive.step _ _ ih hedge + +section CellBridge + +variable {n : Nat} +variable (g : CellGraph) +variable (edges : List (Fin n × Fin n)) +variable (extRefs : Fin n → Nat) +variable (seed : Fin n → Bool) +variable (captured : Obj → Prop) +variable (scc : Obj → Fin n) + +/-- Any live captured cell sits in a live SCC. + Premises are properties of `capture`: + * `h_edge_resp` — every heap edge between captured cells was + recorded (same SCC → internal; different → cross edge); + * `h_closed` — an edge from an UNCAPTURED cell is unexplained by + the captured arithmetic, so it lands in extRefs; + * `h_ext` — direct external refs (stacks, roots buffer, foreign + partitions) are counted in extRefs. -/ +theorem captured_live_scc + (h_edge_resp : ∀ u v, captured u → captured v → g.edge u v → + scc u = scc v ∨ (scc u, scc v) ∈ edges) + (h_closed : ∀ u v, captured v → g.edge u v → ¬ captured u → + 0 < extRefs (scc v)) + (h_ext : ∀ v, captured v → g.extRef v → 0 < extRefs (scc v)) : + ∀ x, CellLive g x → captured x → + LiveScc edges extRefs seed (scc x) := by + intro x hl + induction hl with + | ext x h => + intro hc + exact LiveScc.ext _ (h_ext x hc h) + | step u v hu hedge ih => + intro hcv + by_cases hcu : captured u + · cases h_edge_resp u v hcu hcv hedge with + | inl heq => rw [← heq]; exact ih hcu + | inr hmem => exact LiveScc.pred _ _ hmem (ih hcu) + · exact LiveScc.ext _ (h_closed u v hcv hedge hcu) + +/-- **Soundness**: every cell of a dead SCC is unanchored in the + snapshot — freeing it is justified by yrc_proof.lean §1 + (`yrc_safety`) + §3 (stability through the commit window). -/ +theorem tarjan_sound + (dead : Fin n → Bool) + (hfix : ScanEq edges extRefs seed dead) + (h_edge_resp : ∀ u v, captured u → captured v → g.edge u v → + scc u = scc v ∨ (scc u, scc v) ∈ edges) + (h_closed : ∀ u v, captured v → g.edge u v → ¬ captured u → + 0 < extRefs (scc v)) + (h_ext : ∀ v, captured v → g.extRef v → 0 < extRefs (scc v)) : + ∀ x, captured x → dead (scc x) = true → ¬ CellLive g x := by + intro x hc hd hl + exact live_not_dead edges extRefs seed dead hfix (scc x) + (captured_live_scc g edges extRefs seed captured scc + h_edge_resp h_closed h_ext x hl hc) hd + +/-- Every cell of a live SCC is genuinely live. Needs the converse + premises: external counts are EXACT (no phantom refs — deferred + decs inflate rc, so in the running system this holds only after + the merge; overcounts delay collection by a round, they never + cause a wrong free), cross edges are real edges, and SCC members + are mutually reachable (Tarjan). -/ +theorem live_scc_cells_live + (h_ext_exact : ∀ s : Fin n, 0 < extRefs s → + ∃ v, captured v ∧ scc v = s ∧ g.extRef v) + (h_seed_exact : ∀ s : Fin n, seed s = true → + ∃ v, captured v ∧ scc v = s ∧ g.extRef v) + (h_cross_real : ∀ (u s : Fin n), (u, s) ∈ edges → + ∃ cu cv, captured cu ∧ captured cv ∧ scc cu = u ∧ scc cv = s ∧ + g.edge cu cv) + (h_conn : ∀ u v, captured u → captured v → scc u = scc v → + EdgePath g u v) : + ∀ s, LiveScc edges extRefs seed s → + ∀ x, captured x → scc x = s → CellLive g x := by + intro s hl + induction hl with + | ext s h => + intro x hc hs + obtain ⟨v, hcv, hsv, hev⟩ := h_ext_exact s h + exact cellLive_along_path g v x (CellLive.ext v hev) + (h_conn v x hcv hc (by rw [hsv, hs])) + | root s h => + intro x hc hs + obtain ⟨v, hcv, hsv, hev⟩ := h_seed_exact s h + exact cellLive_along_path g v x (CellLive.ext v hev) + (h_conn v x hcv hc (by rw [hsv, hs])) + | pred u s hmem _ ih => + intro x hc hs + obtain ⟨cu, cv, hccu, hccv, hscu, hscv, he⟩ := h_cross_real u s hmem + have hculive : CellLive g cu := ih cu hccu hscu + exact cellLive_along_path g cv x (CellLive.step cu cv hculive he) + (h_conn cv x hccv hc (by rw [hscv, hs])) + +/-- **Completeness**: every captured garbage cell is marked dead — the + scan collects ALL cycles reachable from the candidate set in one + round (on the snapshot; concurrent inflation only defers). -/ +theorem tarjan_complete + (horder : ∀ e ∈ edges, e.2 < e.1) + (dead : Fin n → Bool) + (hfix : ScanEq edges extRefs seed dead) + (h_ext_exact : ∀ s : Fin n, 0 < extRefs s → + ∃ v, captured v ∧ scc v = s ∧ g.extRef v) + (h_seed_exact : ∀ s : Fin n, seed s = true → + ∃ v, captured v ∧ scc v = s ∧ g.extRef v) + (h_cross_real : ∀ (u s : Fin n), (u, s) ∈ edges → + ∃ cu cv, captured cu ∧ captured cv ∧ scc cu = u ∧ scc cv = s ∧ + g.edge cu cv) + (h_conn : ∀ u v, captured u → captured v → scc u = scc v → + EdgePath g u v) : + ∀ x, captured x → ¬ CellLive g x → dead (scc x) = true := by + intro x hc hnl + apply not_live_dead edges extRefs seed horder dead hfix + intro hl + exact hnl (live_scc_cells_live g edges extRefs seed captured scc + h_ext_exact h_seed_exact h_cross_real h_conn (scc x) hl x hc rfl) + +end CellBridge + +/-! ## §5 Validate-time demotion must propagate + + validateDead demotes a dead SCC when a mutator dirtied it (queue + entry or changed rc word). A demoted SCC becomes a survivor: its + slots are NOT nil'd at commit, so its captured out-edges remain in + the heap. If a cross target of a demoted SCC stayed in the dead set, + the commit would free a cell that a surviving cell still points to — + deadIn had explained that edge away under the assumption that the + predecessor dies too. + + Minimal instance of the hazard: two SCCs, one edge 1 → 0, both + computed dead (ext = 0 for both; SCC 0's only reference comes from + SCC 1, subtracted as deadIn). Demote SCC 1 alone, and the freed set + {0} has a live in-edge from the surviving SCC 1. + + The theorem below states the repair: if the demoted set `K` is + successor-closed within the dead set (demoting s also demotes every + dead t with a captured edge s → t, transitively — one countdown pass + suffices because edges go from higher to lower ids), then the freed + set F = dead ∖ K is predecessor-closed: every captured edge into F + comes from F. Combined with extRefs = 0 and no seed (ScanEq) this + makes F closed in the sense of yrc_proof.lean §3, so freeing F is + covered by `commit_free_safe` there. -/ + +theorem demotion_closure_sound {n : Nat} + (edges : List (Fin n × Fin n)) + (extRefs : Fin n → Nat) (seed : Fin n → Bool) + (dead : Fin n → Bool) + (hfix : ScanEq edges extRefs seed dead) + (K : Fin n → Prop) -- the demoted SCCs + (hK_closed : ∀ e ∈ edges, K e.1 → dead e.2 = true → K e.2) : + -- every captured edge into the freed set comes from the freed set + ∀ e ∈ edges, (dead e.2 = true ∧ ¬ K e.2) → + (dead e.1 = true ∧ ¬ K e.1) := by + intro e he ⟨hd2, hk2⟩ + have hd1 : dead e.1 = true := + ((hfix e.2).mp hd2).2.2 e he rfl + refine ⟨hd1, ?_⟩ + intro hk1 + exact hk2 (hK_closed e he hk1 hd2) + +/-- Without successor-closure the guarantee genuinely fails: in the + two-SCC instance above, demoting only SCC 1 leaves the freed set + {0} with an in-edge from a survivor. (Concrete witness, checked by + `decide`-style evaluation.) -/ +example : + let edges : List (Fin 2 × Fin 2) := [(1, 0)] + let dead : Fin 2 → Bool := fun _ => true + let K : Fin 2 → Prop := fun s => s = 1 -- demote only SCC 1 + -- ScanEq holds for `dead` (both SCCs legitimately computed dead) … + ScanEq edges (fun _ => 0) (fun _ => false) dead ∧ + -- … yet the freed set {0} has an in-edge from surviving SCC 1: + ((1, 0) ∈ edges ∧ dead 0 = true ∧ ¬ K 0 ∧ K 1) := by + refine ⟨?_, ?_⟩ + · intro s + simp + · refine ⟨by simp, rfl, by simp, rfl⟩ + +/-! ## Summary (all QED, no sorry) + + * `descending_induction` — the sinks-first SCC numbering makes the + reverse scan a well-founded definition. + * `scan_dead_iff_not_live` — the scan marks an SCC dead iff it is + not externally anchored: exact garbage identification in ONE + linear pass over the condensation. + * `impl_fixpoint_is_spec` — the implementation's arithmetic + (ext = sumRefs − internal − deadIn, forcedLive propagation) is + that same equation under rc-exactness. + * `tarjan_sound` / `tarjan_complete` — at the cell level: dead cells + are unanchored (frees are safe) and unanchored captured cells are + freed (nothing is missed on the snapshot). + * `demotion_closure_sound` + counterexample — demotion is sound iff + it propagates along captured cross edges to still-dead targets; + a lone demotion can leave the freed set with a surviving + predecessor. + + Not modeled: the Tarjan DFS itself (its two classical invariants — + SCC partition and sinks-first emission — enter as premises), the + iterative traceStack encoding, crossPend (cross-collection edges are + folded into `extRefs`, justified by yrc_proof.lean §5), and the + temporal validity of rc-exactness (yrc_proof.lean §4). +-/