diff --git a/compiler/liftdestructors.nim b/compiler/liftdestructors.nim index aa8a20bc2a..032a4623f2 100644 --- a/compiler/liftdestructors.nim +++ b/compiler/liftdestructors.nim @@ -806,8 +806,22 @@ proc atomicRefOp(c: var TLiftCtx; t: PType; body, x, y: PNode) = createTypeBoundOps(c.g, c.c, elemType, c.info, c.idgen) - # YRC uses dedicated runtime procs for the entire write barrier: - if c.g.config.selectedGC == gcYrc: + # YRC uses dedicated runtime procs for the entire write barrier -- but ONLY + # for refs that can actually form cycles. Routing an acyclic ref through + # `nimAsgnYrc` defeats the entire purpose of `.acyclic`: the barrier defers + # the dec into a stripe queue, `drainStripe` then hands the cell to + # `registerLocal`, and it enters the collector as a capture ROOT -- so a + # type annotated precisely to stay out of the cycle collector gets traced + # by it anyway. (The collector never reaches such a cell by TRAVERSAL: the + # attachedTrace hook below only emits `nimTraceRef` when `isCyclic`. The + # queued dec was the only way in.) + # + # Falling through instead gives acyclic refs the same prompt arc-style + # reclamation they get under --mm:arc/orc, which is also what lets a thread + # that avoids cycles at compile time avoid the collector entirely at run + # time. `canFormAcycle` is the same predicate ccgtypes.nim:1903 uses to set + # the descriptor's acyclic flag, so codegen and runtime cannot disagree. + if c.g.config.selectedGC == gcYrc and types.canFormAcycle(c.g, elemType): let desc = if isFinal(elemType): let ti = genBuiltin(c, mGetTypeInfoV2, "getTypeInfoV2", newNodeIT(nkType, x.info, elemType)) diff --git a/lib/core/locks.nim b/lib/core/locks.nim index 5237274792..d219771b76 100644 --- a/lib/core/locks.nim +++ b/lib/core/locks.nim @@ -25,7 +25,15 @@ type ## or not is unspecified! Cond* = SysCond ## Nim condition variable -{.push stackTrace: off.} +# `enforceNoRaises`: these are thin wrappers over the OS primitives and +# cannot raise. Without the flag `canRaiseDisp` falls into its conservative +# branch (they are not in the system module), so the codegen emits an +# `if (*nimErr_) goto BeforeRet_` right after every `acquire` -- which sits +# BETWEEN the acquire and the `try` that `withLock` generates, so the +# `finally` cannot cover it. A caller entered with the error flag already +# set then acquires the lock and jumps straight past the `release`, +# leaking it. See lib/system/yrc.nim's drainStripe. +{.push stackTrace: off, enforceNoRaises.} proc `$`*(lock: Lock): string = diff --git a/lib/system/yrc.nim b/lib/system/yrc.nim index 681fb1db94..0a73fd72ea 100644 --- a/lib/system/yrc.nim +++ b/lib/system/yrc.nim @@ -5,8 +5,10 @@ # 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. +# yrc_tarjan_proof.lean for soundness AND completeness of the SCC +# deadness algorithm, and yrc_opt_proof.lean for the three optimizations +# that changed those invariants: SCC-uniform epoch ages, the demand-grown +# `gParSlots` pool, and deferred reclamation (gPendingCells). # # ## Synchronization at a Glance # @@ -25,7 +27,7 @@ # 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 +# Up to one collection PER THREAD runs 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 @@ -255,10 +257,6 @@ proc setLenZeroed[T](s: var RawSeq[T]; n: int) = s.len = n zeroMem(s.d, n *% sizeof(T)) -proc setLenUninit[T](s: var RawSeq[T]; n: int) = - if s.cap < n: resize(s, n) - s.len = n - type TraceEntry = object ## (slot, value) snapshot taken at trace time. The value is read exactly @@ -270,6 +268,7 @@ type TarjanFrame = object u: int32 # dense index of the cell this frame belongs to + ebase: int32 # edges.len when this cell's frame was pushed base: int # traceStack.len before this cell's trace ran CaptureRec = object @@ -281,7 +280,7 @@ type desc: PNimTypeV2 rcWord: int # rc word as captured lowlink: int32 - sccOf: int32 # -1 while the cell is on the Tarjan stack + selfRefs: int32 # self edges, folded out of the edge array SccRec = object ## per SCC of the condensation; the deadness pass reads all of these @@ -293,7 +292,6 @@ type deadIn: int # number of edges from dead SCCs memStart: int32 # offset into sccMembers crossOff: int32 # offset into crossTgt (cross edges by source) - crossCursor: int32 flags: uint8 CaptureBufs = object @@ -301,9 +299,19 @@ type ## threadvar) and persistent across collections, so that frequent ## small collections don't pay per-collection allocations recs: RawSeq[CaptureRec] + sccIdx: RawSeq[int32] # per captured cell: its SCC, -1 while the cell + # is on the Tarjan stack. Deliberately NOT a + # CaptureRec field: it is read once per captured + # EDGE, and a 4-byte stride keeps that array + # L1-resident where a 32-byte record stride would + # miss on almost every edge. tstack: RawSeq[int32] frames: RawSeq[TarjanFrame] - edges: RawSeq[int64] # (u shl 32) or v, dense indices + edges: RawSeq[int32] # PENDING out-edge targets (dense indices) of the + # SCCs still being built. An SCC's edges are + # classified and dropped the moment it is emitted + # (see `capture`), so this stays proportional to + # the DFS frontier, not to the captured graph. sccs: RawSeq[SccRec] sccMembers: RawSeq[int32] crossTgt: RawSeq[int32] @@ -336,10 +344,11 @@ proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} = # The spare rootIdx header word (unused by YRC's root registration, which # relies on inRootsFlag) doubles as the capture claim: it packs the owning -# collection's tag with the cell's dense discovery index. Up to MaxPar -# collections run CONCURRENTLY, each capturing a disjoint partition of the -# heap: the first collection to CAS its tag into a cell owns it; everyone -# else treats the cell as an opaque survivor. Stale tags (from retired +# collection's tag with the cell's dense discovery index. Collections run +# CONCURRENTLY — one slot per collecting thread, see gParSlots — each +# capturing a disjoint partition of the heap: the first collection to CAS +# its tag into a cell owns it; everyone else treats the cell as an opaque +# survivor. Stale tags (from retired # collections) never need clearing, they are simply reclaimable. # # The word does double duty a second time: commit re-stamps proven-live @@ -350,13 +359,29 @@ proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} = # collection. Roots always bypass the stamp: every death has a dec-witness # that gets registered, and registered cells are always scanned as roots. const - MaxPar {.intdefine.} = 8 # max concurrent collections + MaxPar {.intdefine.} = 256 + ## CAPACITY of the slot table, not a tuning knob: a hard ceiling on + ## concurrent collections, sized to stay out of the way (16 bytes of BSS + ## per entry, and scans only ever run over `gParSlots`, below). Raise it + ## only for programs with more than this many threads collecting AT ONCE. ParSlots = MaxPar var gMergeLock: Lock # protects the tag slots + orphaned roots gActiveTags: array[ParSlots, int64] # 0 = free slot gSlotPhase: array[ParSlots, int] # 0 idle, 1 capturing, 2 committing + gParSlots: int = 1 + ## How many slots are IN PLAY. Every scan below runs over this prefix + ## rather than over the whole table, and it is raised (under gMergeLock, + ## never lowered) exactly when a thread wants to collect and every slot + ## already in play is busy. It therefore converges on the number of + ## threads that actually collect CONCURRENTLY — one slot each — and then + ## stops: the parallelism is auto-tuned to the workload instead of being + ## a compile-time guess. A fixed bound throttled hard whenever the thread + ## count exceeded it, because the surplus threads did not just collect + ## later, they PARKED in `parkUntil(anySlotFree())` waiting for a slot + ## (32 threads against 8 slots: 6.3s vs 2.6s with a slot each). + ## Starting at 1 also means single-threaded programs scan one entry. gSoloCapture: int # a solo collection is in its capture phase gTagCounter: int64 gMyTag {.threadvar.}: int64 @@ -399,9 +424,19 @@ const epochBase = 0x40000000 # stamp namespace: tags stay below this epochMask = 0x3FFFFFFF -# stamp layout: high word = epochBase|epoch, low word = survival age +# Every packed word in this file squeezes two 32-bit fields into one int64 as +# `(hi shl 32) or lo`. The claim word (a cell's `rootIdx`, see above) is either +# hi = owning collection's tag, lo = the cell's dense capture index +# hi = epochBase|epoch (a stamp), lo = the cell's survival age +# and a `gPendingWatch` entry is hi = slot, lo = tag. The high half is read +# with a plain `shr 32` — every value stored there is below 2^31, so the shift +# keeps it positive and needs no mask. The low half is the one that needs +# masking: `shl 32` left the high half sitting above it, and `and 0xFFFFFFFF` +# is what clears those bits back out. +template loWord(w: int64): int64 = w and 0xFFFFFFFF + template epochStamp(e: int): int64 = int64(epochBase or (e and epochMask)) shl 32 -template stampAge(w: int64): int = int(w and 0xFFFFFFFF) +template stampAge(w: int64): int = int(loWord(w)) template isEpochStamp(w: int64): bool = (w shr 32) >= epochBase template parkUntil(cond: untyped) = @@ -426,9 +461,17 @@ proc collectorEvent() {.inline.} = broadcast gWaitCond release gWaitLock +proc slotsInPlay(): int {.inline.} = + ## Must be loaded AFTER whatever claim word the caller is validating: a + ## slot is put in play before the collection owning it can tag any cell, + ## so a load ordered after reading a tagged word is guaranteed to cover + ## the slot that wrote the tag. `gParSlots` only ever grows, so a scan + ## over this prefix can never shrink under a reader. + atomicLoadN(addr gParSlots, ATOMIC_ACQUIRE) + proc anySlotFree(): bool {.inline.} = result = false - for sl in 0 ..< ParSlots: + for sl in 0 ..< slotsInPlay(): if atomicLoadN(addr gActiveTags[sl], ATOMIC_ACQUIRE) == 0: return true @@ -438,12 +481,12 @@ template isStamped(c: Cell): bool = # value routes into claimCell which re-validates with acquire + CAS. (atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) shr 32) == gMyTag template denseIdx(c: Cell): int32 = - int32(atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) and 0xFFFFFFFF) + int32(loWord(atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED))) proc isActiveTag(t: int64): bool {.inline.} = result = false if t != 0: - for s in 0 ..< ParSlots: + for s in 0 ..< slotsInPlay(): if atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) == t: return true @@ -485,6 +528,25 @@ var ## draining this thread's stripe queue registers candidates here, and ## this thread's collections steal it as their slice — no lock, and ## collections keep the cache locality of thread-local data. + gPendingCells {.threadvar.}: CellSeq[Cell] + ## Cells this thread committed dead — slots nil'ed, references already + ## decremented — but has not handed back to the allocator yet, because a + ## capture that was in flight at commit time may still hold a stale + ## (slot, value) snapshot pointing at them. Released at the start of this + ## thread's next collection; see `releasePending`. + gPendingWatch {.threadvar.}: RawSeq[int64] + ## The captures that batch must outlive, packed as (slot shl 32) or tag. + gPendingSlot {.threadvar.}: int + gPendingActive {.threadvar.}: bool + gSpareRoots {.threadvar.}: CellSeq[Cell] + ## The buffer a finished collection hands back, so that stealing + ## `gLocalRoots` costs no allocation in steady state. + gTraceBuf {.threadvar.}: CellSeq[TraceEntry] + gFreeBuf {.threadvar.}: CellSeq[Cell] + ## Storage for `GcEnv.traceStack` / `GcEnv.toFree`, kept across + ## collections like the `gCap` arrays: both grow to the size of the + ## captured graph, so re-allocating and re-growing them per collection + ## was a memcpy of the whole trace frontier every time. stripes: array[NumStripes, Stripe] rootsThreshold: int = 128 # shared adaptive heuristic; races are benign defaultThreshold = when defined(nimFixedOrc): 10_000 else: 128 @@ -677,6 +739,62 @@ template orcAssert(cond, msg) = cfprintf(cstderr, "[Bug!] %s\n", msg) rawQuit 1 +proc graceSatisfied(): bool = + ## Has every capture recorded in `gPendingWatch` finished? A capture that + ## started later cannot hold a stale snapshot of the batch: it reads every + ## slot fresh, and the batch's cells are unreachable by then. + result = true + for i in 0 ..< gPendingWatch.len: + let w = gPendingWatch.d[i] + let s = int(w shr 32) + let tg = loWord(w) + if atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) == tg and + atomicLoadN(addr gSlotPhase[s], ATOMIC_ACQUIRE) == 1: + return false + +proc buildPendingWatch(): bool = + ## Record the collections that are in their CAPTURE phase right now: they + ## are the only ones that can hold a stale (slot, value) snapshot of the + ## cells we are about to release. `false` (nothing capturing) is the common + ## case below a handful of threads, and means the batch can be freed on the + ## spot with no deferral and no destructor-timing change at all. + if gPendingWatch.d == nil: init gPendingWatch + gPendingWatch.len = 0 + for s in 0 ..< slotsInPlay(): + if s != gMySlot: + let tg = atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) + if tg != 0 and atomicLoadN(addr gSlotPhase[s], ATOMIC_ACQUIRE) == 1: + gPendingWatch.add((int64(s) shl 32) or tg) + result = gPendingWatch.len > 0 + +proc releasePending() = + ## Hand this thread's parked batch back to the allocator and give its slot + ## up. Called at the start of every collection, so by the time it runs the + ## watched captures have had a whole collection's worth of time to finish + ## and the wait below is virtually always already satisfied — that is the + ## whole point: the wait moved off the commit path, where it blocked BOTH + ## the committing collector and (because commit runs inside the GC fence) + ## every mutator doing a seq operation. + if not gPendingActive: return + parkUntil(graceSatisfied()) + # Give the slot up FIRST: the batch is unreachable and no capture can hold + # a snapshot of it any more, so the tag has nothing left to protect. + gPendingActive = false + gPendingWatch.len = 0 + atomicStoreN(addr gActiveTags[gPendingSlot], 0, ATOMIC_SEQ_CST) + collectorEvent() + # Destructors run here. `Collecting` is the existing re-entrancy guard: a + # destructor-driven dec that overflows a stripe must drain it, not start a + # nested collection that would write into the batch we are walking. + let prev = lockState + lockState = Collecting + for i in 0 ..< gPendingCells.len: + when orcLeakDetector: + writeCell("CYCLIC OBJECT FREED", gPendingCells.d[i][0], gPendingCells.d[i][1]) + free(gPendingCells.d[i][0], gPendingCells.d[i][1]) + gPendingCells.len = 0 + lockState = prev + proc nimTraceRef(q: pointer; desc: PNimTypeV2; env: pointer) {.compilerRtl, inl.} = let p = cast[ptr pointer](q) # read the slot exactly once: mutators may exchange it concurrently. @@ -698,6 +816,7 @@ proc nimTraceRefDyn(q: pointer; env: pointer) {.compilerRtl, inl.} = proc prepareCapture() = if gCap.recs.d == nil: init gCap.recs + init gCap.sccIdx init gCap.tstack init gCap.frames init gCap.edges @@ -709,11 +828,13 @@ proc prepareCapture() = init gCap.ages else: gCap.recs.len = 0 + gCap.sccIdx.len = 0 gCap.tstack.len = 0 gCap.frames.len = 0 gCap.edges.len = 0 gCap.sccs.len = 0 gCap.sccMembers.len = 0 + gCap.crossTgt.len = 0 gCap.crossPend.len = 0 gCap.prunedSrc.len = 0 gCap.ages.len = 0 @@ -722,18 +843,22 @@ proc prepareCapture() = # inRootsFlag between capture and commit, which must not look like a # mutation to the commit-time rc validation. proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs; - pruneLive: bool): int32 = + pruneLive: bool; old0: int64): int32 = ## Dense index if this collection owns `c` (claiming and registering it ## if it was unclaimed), -1 if another ACTIVE collection owns it, or ## -2 if `pruneLive` and the cell was proven live in the current epoch ## (treat as an opaque live external, don't descend). + ## + ## `old0` is `c`'s claim word as the caller already read it (acquire): the + ## DFS reads it to test ownership, and re-reading it here would be a second + ## dependent load of the same cold header word on every traversed edge. if gAmSolo: # no other collection is (or can start) capturing: plain stores. # This recovers the sequential capture speed of the single-collector # design whenever collections do not actually overlap. - let old = c.rootIdx + let old = old0 if (old shr 32) == gMyTag: - return int32(old and 0xFFFFFFFF) + return int32(loWord(old)) if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and stampAge(old) >= YrcPromoteAge: return -2 @@ -744,18 +869,22 @@ proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs; if old != 0: bumpStat gStatCapRepeat cap.recs.add CaptureRec(cell: c, desc: desc, rcWord: loadRc(c) and not rcMask, - lowlink: int32(idx), sccOf: -1'i32) + lowlink: int32(idx), selfRefs: 0'i32) + cap.sccIdx.add -1'i32 cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0) cap.tstack.add int32(idx) return int32(idx) + var old = old0 while true: - var old = atomicLoadN(addr c.rootIdx, ATOMIC_ACQUIRE) if (old shr 32) == gMyTag: - return int32(old and 0xFFFFFFFF) + return int32(loWord(old)) if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and stampAge(old) >= YrcPromoteAge: return -2 - if isActiveTag(old shr 32): + # an epoch stamp is never a tag (tags are allocated below `epochBase`), + # so the scan over the active-tag slots is skipped for the common + # "cell survived an earlier collection" word + if not isEpochStamp(old) and isActiveTag(old shr 32): return -1 let idx = cap.recs.len if atomicCompareExchangeN(addr c.rootIdx, addr old, @@ -766,38 +895,69 @@ proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs; if old != 0: bumpStat gStatCapRepeat cap.recs.add CaptureRec(cell: c, desc: desc, rcWord: loadRc(c) and not rcMask, - lowlink: int32(idx), sccOf: -1'i32) + lowlink: int32(idx), selfRefs: 0'i32) + cap.sccIdx.add -1'i32 cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0) cap.tstack.add int32(idx) return int32(idx) + # a failed CAS leaves the fresh claim word in `old`; loop with it proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) = ## Iterative Tarjan SCC over everything reachable from `s`. A frame's ## pending out-edges are the traceStack entries above frame.base; a child ## pushes and drains its own segment above ours, so when the child's frame ## pops, the stack is back at our segment and we resume popping our edges. - if isStamped(s): return + ## + ## An SCC's out-edges are classified into internal/cross the moment the SCC + ## is emitted, not in a later pass over a whole-graph edge list. That works + ## because `cap.edges` is truncated back to a frame's `ebase` whenever that + ## frame's cell turns out to be an SCC root: edges of already-emitted + ## sub-SCCs are gone, so `edges[ebase(u) ..< len]` at u's emission holds + ## exactly the out-edges of u's SCC. Every one of them targets either a + ## member (u would not be an SCC root if a member pointed at a cell still + ## on the stack below u) or an SCC emitted earlier, so `sccIdx` is final + ## for all of them and the cross targets can be appended to `crossTgt` + ## contiguously — which makes `crossOff` a prefix offset for free. + let rootWord = atomicLoadN(addr s.rootIdx, ATOMIC_ACQUIRE) + if (rootWord shr 32) == gMyTag: return orcAssert(j.traceStack.len == 0, "capture: trace stack not empty") # roots never prune: a dec-witnessed suspicion overrides any epoch stamp - let root = claimCell(s, desc, cap, pruneLive = false) + let root = claimCell(s, desc, cap, pruneLive = false, old0 = rootWord) if root < 0: return # another active collection owns this candidate; it handles it trace(s, desc, j) - cap.frames.add TarjanFrame(u: root, base: 0) - while cap.frames.len > 0: - let u = cap.frames.d[cap.frames.len -% 1].u - let base = cap.frames.d[cap.frames.len -% 1].base + # The innermost frame is kept in `u`/`base` instead of being re-read from + # `cap.frames` on every iteration: the loop body runs once per captured + # EDGE, so reloading the frame there costs more than the frame stack itself. + # `cap.frames` therefore only holds the ANCESTORS of `u`. + var u = root + var base = 0 + var ebase = 0'i32 + while true: if j.traceStack.len > base: - let (entry, tdesc) = j.traceStack.pop() - let t = head(entry.val) - if isStamped(t): - let v = denseIdx(t) - cap.edges.add (int64(u) shl 32) or int64(v) - if cap.recs.d[v].sccOf < 0 and v < cap.recs.d[u].lowlink: - cap.recs.d[u].lowlink = v + # inlined pop: the stamped path never needs the entry's descriptor + let last = j.traceStack.len -% 1 + j.traceStack.len = last + let t = head(j.traceStack.d[last][0].val) + # one load of the target's claim word serves both the ownership test + # and the dense-index extraction + let cw = atomicLoadN(addr t.rootIdx, ATOMIC_ACQUIRE) + if (cw shr 32) == gMyTag: + let v = int32(loWord(cw)) + if v == u: + # A self edge is internal by construction and its reference is + # already in `rcWord`, so it cancels out of `sumRefs - internal` + # exactly. Counting it here keeps it out of the edge array and out + # of the classification pass below. + inc cap.recs.d[u].selfRefs + else: + cap.edges.add v + if cap.sccIdx.d[v] < 0 and v < cap.recs.d[u].lowlink: + cap.recs.d[u].lowlink = v else: + let tdesc = j.traceStack.d[last][1] let childBase = j.traceStack.len - let v = claimCell(t, tdesc, cap, pruneLive = true) + let v = claimCell(t, tdesc, cap, pruneLive = true, old0 = cw) if v == -1: # cross-collection edge: the owner sees our reference in the rc # word and classifies the target live; we re-register it as a @@ -810,75 +970,72 @@ proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) = when defined(nimOrcStats): bumpStat gStatCapPruned else: - cap.edges.add (int64(u) shl 32) or int64(v) + cap.edges.add v trace(t, tdesc, j) - cap.frames.add TarjanFrame(u: v, base: childBase) + cap.frames.add TarjanFrame(u: u, ebase: ebase, base: base) + u = v + ebase = int32(cap.edges.len) + base = childBase else: - cap.frames.len = cap.frames.len -% 1 - if cap.frames.len > 0: - let pu = cap.frames.d[cap.frames.len -% 1].u - if cap.recs.d[u].lowlink < cap.recs.d[pu].lowlink: - cap.recs.d[pu].lowlink = cap.recs.d[u].lowlink - if cap.recs.d[u].lowlink == u: + let lowU = cap.recs.d[u].lowlink + if lowU == u: # u is the root of an SCC: pop the members off the Tarjan stack + let sid = int32(j.nScc) let memStart = int32(cap.sccMembers.len) var sum = 0 while true: - let w = cap.tstack.pop() - cap.recs.d[w].sccOf = int32(j.nScc) - cap.sccMembers.add w - sum = sum +% (cap.recs.d[w].rcWord shr rcShift) +% 1 - if w == u: break - cap.sccs.add SccRec(sumRefs: sum, memStart: memStart) + let m = cap.tstack.pop() + cap.sccIdx.d[m] = sid + cap.sccMembers.add m + # `- selfRefs`: a self edge counts in both `sumRefs` and `internal` + # and was folded out of the edge array in the loop above + sum = sum +% (cap.recs.d[m].rcWord shr rcShift) +% 1 -% + cap.recs.d[m].selfRefs + if m == u: break + # classify this SCC's out-edges now that every target's SCC is final + let crossOff = int32(cap.crossTgt.len) + var internal = 0 + for i in ebase ..< int32(cap.edges.len): + let sv = cap.sccIdx.d[cap.edges.d[i]] + if sv == sid: inc internal + else: cap.crossTgt.add sv + cap.edges.len = ebase + cap.sccs.add SccRec(sumRefs: sum, internal: internal, + memStart: memStart, crossOff: crossOff) inc j.nScc + if cap.frames.len == 0: break + let pi = cap.frames.len -% 1 + cap.frames.len = pi + let pu = cap.frames.d[pi].u + if lowU < cap.recs.d[pu].lowlink: + cap.recs.d[pu].lowlink = lowU + u = pu + ebase = cap.frames.d[pi].ebase + base = cap.frames.d[pi].base # ---------------- phase 2: deadness, side arrays only ---------------- proc computeDeadness(j: var GcEnv; cap: ptr CaptureBufs) = let nScc = j.nScc - # append the sentinel record ([nScc]); capture left internal/deadIn/flags - # zero-initialized and memStart valid. crossOff is filled below as a prefix - # sum, so the sentinel closes the last SCC's member and cross-edge slices. - cap.sccs.add SccRec(memStart: int32(cap.sccMembers.len)) - # classify captured edges: internal to an SCC vs condensation cross edges - var nCross = 0 - for i in 0 ..< cap.edges.len: - let e = cap.edges.d[i] - let su = cap.recs.d[int32(e shr 32)].sccOf - let sv = cap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf - if su == sv: - inc cap.sccs.d[su].internal - else: - inc cap.sccs.d[su].crossOff - inc nCross - var total = 0'i32 - for s in 0 ..< nScc: - let c = cap.sccs.d[s].crossOff - cap.sccs.d[s].crossOff = total - cap.sccs.d[s].crossCursor = total - total = total +% c - cap.sccs.d[nScc].crossOff = total - setLenUninit cap.crossTgt, nCross - for i in 0 ..< cap.edges.len: - let e = cap.edges.d[i] - let su = cap.recs.d[int32(e shr 32)].sccOf - let sv = cap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf - if su != sv: - cap.crossTgt.d[cap.sccs.d[su].crossCursor] = sv - inc cap.sccs.d[su].crossCursor + # append the sentinel record ([nScc]) that closes the last SCC's member and + # cross-edge slices; capture left deadIn/flags zero-initialized and filled + # sumRefs/internal/memStart/crossOff in already, so the condensation is + # complete the moment the DFS ends. + cap.sccs.add SccRec(memStart: int32(cap.sccMembers.len), + crossOff: int32(cap.crossTgt.len)) # pruned out-edges taint the source SCC: pruning cannot cause a false # "dead" (an untraced target only ever ADDS unexplained external refs), # but a "live" verdict may lean on a stamp that went stale within the # epoch, so validate re-registers surviving pruned SCCs for i in 0 ..< cap.prunedSrc.len: - let s = cap.recs.d[cap.prunedSrc.d[i]].sccOf + let s = cap.sccIdx.d[cap.prunedSrc.d[i]] cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagPruned # cells that stay registered as roots (partial collection) count as # externally referenced: the roots buffer itself points at them for mi in 0 ..< cap.sccMembers.len: let m = cap.sccMembers.d[mi] if (loadRc(cap.recs.d[m].cell) and inRootsFlag) != 0: - let s = cap.recs.d[m].sccOf + let s = cap.sccIdx.d[m] cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagForcedLive # deadness over the condensation. Tarjan emits sinks first, so higher SCC # ids are sources and every cross edge goes from a higher id to a lower @@ -910,7 +1067,7 @@ proc markDirtyFromQueues(j: var GcEnv; cap: ptr CaptureBufs) = template taint(cp: Cell) = let c = cp if isStamped(c): - let s = cap.recs.d[denseIdx(c)].sccOf + let s = cap.sccIdx.d[denseIdx(c)] cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagDirty for i in 0.. 0: let (entry, _) = j.traceStack.pop() entry.slot[] = nil - when orcLeakDetector: - writeCell("CYCLIC OBJECT FREED", cell, desc) - free(cell, desc) + holdOrFree(cell, desc, deferred) j.freed = cap.recs.len + if deferred: + gPendingSlot = gMySlot + gPendingActive = true else: - init j.toFree + if gFreeBuf.d == nil: init gFreeBuf + gFreeBuf.len = 0 + j.toFree = gFreeBuf for s in 0 ..< j.nScc: if (cap.sccs.d[s].flags and flagDead) != 0: for mi in cap.sccs.d[s].memStart ..< cap.sccs.d[s+1].memStart: @@ -1067,32 +1239,60 @@ proc commitDead(j: var GcEnv; cap: ptr CaptureBufs) = let (entry, tdesc) = j.traceStack.pop() let t = head(entry.val) entry.slot[] = nil - if not deadCell(t): + let tw = atomicLoadN(addr t.rootIdx, ATOMIC_RELAXED) + if not deadCell(tw): trialDec(t) # a stamped target was not analyzed by THIS collection, so # this dec may be the death blow: keep the cell examinable - if isEpochStamp(atomicLoadN(addr t.rootIdx, ATOMIC_RELAXED)): + if isEpochStamp(tw): registerLocal(t, tdesc) - # epoch-stamp what this collection PROVED live, carrying the cell's - # survival age: only cells that keep surviving get promoted to ages - # where captures prune them, so die-young data is never deferred. - # Demoted (dirty) and pruned SCCs stay unproven — leave their stale - # tags claimable. Our tag is still active, so no foreign claim can - # race these stores. + # epoch-stamp what this collection PROVED live, carrying the survival + # age: only cells that keep surviving get promoted to ages where + # captures prune them, so die-young data is never deferred. Demoted + # (dirty) and pruned SCCs stay unproven — leave their stale tags + # claimable. Our tag is still active, so no foreign claim can race + # these stores. + # + # The age is the SCC's, not the cell's: the whole SCC gets the age of + # its YOUNGEST member, so promotion is all-or-nothing. A per-cell age + # lets one member of an SCC promote ahead of its own SCC-mates; the + # next capture then prunes that INTERNAL edge, which taints the SCC as + # flagPruned, which stops it from ever being stamped again — freezing + # every member's age at its current value and re-tracing the whole + # structure on every collection from then on. Members age at different + # rates whenever a structure is built incrementally (a list appended to + # across several collections), so this is the common case, not a corner + # one. Taking the minimum can only delay a promotion, never hasten one, + # so it cannot widen the floating-garbage bound. for s in 0 ..< j.nScc: if (cap.sccs.d[s].flags and (flagDead or flagDirty or flagPruned)) == 0: - for mi in cap.sccs.d[s].memStart ..< cap.sccs.d[s+1].memStart: - let m = cap.sccMembers.d[mi] - atomicStoreN(addr cap.recs.d[m].cell.rootIdx, - gMyEpochStamp or int64(cap.ages.d[m] +% 1), - ATOMIC_RELAXED) - graceWait() - for i in 0 ..< j.toFree.len: - when orcLeakDetector: - writeCell("CYCLIC OBJECT FREED", j.toFree.d[i][0], j.toFree.d[i][1]) - free(j.toFree.d[i][0], j.toFree.d[i][1]) + let memStart = cap.sccs.d[s].memStart + let memEnd = cap.sccs.d[s+1].memStart + var age = high(int32) + for mi in memStart ..< memEnd: + let a = cap.ages.d[cap.sccMembers.d[mi]] + if a < age: age = a + let stamp = gMyEpochStamp or int64(age +% 1) + for mi in memStart ..< memEnd: + atomicStoreN(addr cap.recs.d[cap.sccMembers.d[mi]].cell.rootIdx, + stamp, ATOMIC_RELAXED) j.freed = j.toFree.len - deinit j.toFree + if j.toFree.len > 0 and buildPendingWatch(): + # park the whole batch by swapping buffers: the collection keeps the + # (now empty) buffer the previous batch used, so neither side allocates + let spare = gPendingCells + gPendingCells = j.toFree + j.toFree = spare + j.toFree.len = 0 + gPendingSlot = gMySlot + gPendingActive = true + else: + for i in 0 ..< j.toFree.len: + when orcLeakDetector: + writeCell("CYCLIC OBJECT FREED", j.toFree.d[i][0], j.toFree.d[i][1]) + free(j.toFree.d[i][0], j.toFree.d[i][1]) + j.toFree.len = 0 + gFreeBuf = j.toFree proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; wait: bool; drainAll = false): bool = @@ -1100,11 +1300,12 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; ## collect) and try to become a collector over THIS THREAD's candidates: ## claim a tag slot — the only step still under gMergeLock — and steal ## the thread-local buffer as this collection's slice, lock-free. When - ## there is enough work but all ParSlots collections are running, `wait` - ## decides between parking until a slot frees (backpressure for - ## overflowing mutators) and giving up. Either way the drain happened, + ## there is enough work but the slot table is full (more than MaxPar + ## threads collecting at once), `wait` decides between parking until a + ## slot frees and giving up. Either way the drain happened, ## so the caller's overflowing queue has room again. result = false + releasePending() # last collection's batch: its watch list is long clear if drainAll: drainAllStripes() else: drainStripe(getStripeIdx()) adoptOrphans() @@ -1112,15 +1313,23 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; mayRunCycleCollect(): acquire gMergeLock var slot = -1 - for sl in 0 ..< ParSlots: + let inPlay = gParSlots + for sl in 0 ..< inPlay: if atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) == 0: slot = sl break + if slot < 0 and inPlay < ParSlots: + # Every slot in play is busy and the table has room: widen the pool + # instead of throttling this thread. Publishing the wider bound before + # the tag lands in the new slot is what makes `slotsInPlay` safe. + slot = inPlay + atomicStoreN(addr gParSlots, inPlay +% 1, ATOMIC_SEQ_CST) if slot < 0: release gMergeLock if not wait: break - # backpressure: all ParSlots collections are running; park until one - # finishes (finishCollection broadcasts) instead of burning a core + # the table itself is full (more than MaxPar threads collecting at + # once): park until one finishes (finishCollection broadcasts) + # instead of burning a core parkUntil(anySlotFree()) drainStripe(getStripeIdx()) # the world moved while we waited adoptOrphans() @@ -1131,7 +1340,7 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; gMySlot = slot gMyEpochStamp = epochStamp(atomicLoadN(addr gEpoch, ATOMIC_RELAXED)) var othersActive = false - for sl in 0 ..< ParSlots: + for sl in 0 ..< gParSlots: if sl != slot and atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) != 0: othersActive = true gAmSolo = not othersActive @@ -1143,7 +1352,12 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; # our buffer, our slice: no lock needed if keepBelow == 0: slice = gLocalRoots # steal the whole buffer - init(gLocalRoots) + if gSpareRoots.d != nil: + gLocalRoots = gSpareRoots + gLocalRoots.len = 0 + gSpareRoots = default(CellSeq[Cell]) + else: + init(gLocalRoots) else: init(slice, max(gLocalRoots.len - keepBelow, 8)) for i in keepBelow ..< gLocalRoots.len: @@ -1155,8 +1369,16 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; proc finishCollection() = if atomicAddFetch(addr gCollectionCounter, 1, ATOMIC_RELAXED) mod YrcEpochLen == 0: discard atomicAddFetch(addr gEpoch, 1, ATOMIC_RELAXED) - atomicStoreN(addr gActiveTags[gMySlot], 0, ATOMIC_SEQ_CST) - atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE) + if gPendingActive: + # A batch is parked under this collection's tag. Clear only the PHASE — + # so nobody's grace check waits on us — and leave the tag in + # `gActiveTags`: it is what stops a foreign capture from claiming, and + # then freeing, a cell that is sitting in the batch. `releasePending` + # gives the slot back. + atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE) + else: + atomicStoreN(addr gActiveTags[gMySlot], 0, ATOMIC_SEQ_CST) + atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE) gMyTag = 0 gAmSolo = false collectorEvent() # wake backpressure and grace waiters @@ -1170,7 +1392,9 @@ proc collectCyclesImpl(j: var GcEnv; slice: var CellSeq[Cell]) = for i in countdown(last, 0): writeCell("root", slice.d[i][0], slice.d[i][1]) - init j.traceStack + if gTraceBuf.d == nil: init gTraceBuf + gTraceBuf.len = 0 + j.traceStack = gTraceBuf prepareCapture() let cap = addr gCap # hoist the TLS lookup out of the hot loops j.nScc = 0 @@ -1194,11 +1418,11 @@ proc collectCyclesImpl(j: var GcEnv; slice: var CellSeq[Cell]) = commitDead(j, cap) j.keepThreshold = j.freed == j.touched and j.touched > 0 - deinit j.traceStack + gTraceBuf = j.traceStack # hand the (possibly grown) buffer back proc runCollection(j: var GcEnv; slice: var CellSeq[Cell]) = ## Runs one collection over the stolen slice, concurrently with mutators - ## AND with up to ParSlots-1 other collections over disjoint partitions. + ## AND with the other collecting threads over disjoint partitions. yrcGcFenceEnter() # freeze seq structure mutations, not ref writes if not gAmSolo: # a solo collection claims with plain stores; nobody else may claim @@ -1210,7 +1434,10 @@ proc runCollection(j: var GcEnv; slice: var CellSeq[Cell]) = lockState = prev yrcGcFenceExit() finishCollection() - deinit slice + if gSpareRoots.d == nil and slice.d != nil: + gSpareRoots = slice # recycle it as the next steal's replacement + else: + deinit slice when defined(nimOrcStats): var freedCyclicObjects {.threadvar.}: int @@ -1283,6 +1510,7 @@ proc GC_runOrc* = if startCollection(1, 0, slice, wait = true, drainAll = true): var j: GcEnv runCollection(j, slice) + releasePending() # GC_fullCollect must not leave a batch parked # note: aborted SCCs and cross-collection targets legitimately leave # re-registered roots behind; other RUNNING threads' local candidates # are theirs to collect (exiting threads spill to the orphan buffer) @@ -1315,6 +1543,7 @@ proc nimYrcThreadTeardown() = ## of ours is stranded in a queue no other thread hashes to, then spill ## our candidate buffer to the global orphan buffer, where the next ## collection on any thread adopts it. + releasePending() # nobody else can release this thread's parked batch drainStripe(getStripeIdx()) if gLocalRoots.len > 0: acquire gMergeLock @@ -1326,6 +1555,11 @@ proc nimYrcThreadTeardown() = deinit(gLocalRoots) gLocalRoots.d = nil gLocalRoots.len = 0 + deinit(gSpareRoots) + deinit(gTraceBuf) + deinit(gFreeBuf) + deinit(gPendingCells) + deinit(gPendingWatch) proc GC_enableMarkAndSweep*() = GC_enableOrc() proc GC_disableMarkAndSweep*() = GC_disableOrc() @@ -1362,7 +1596,27 @@ proc nimDecRefIsLastCyclicDyn(p: pointer): bool {.compilerRtl, inl.} = enqueueDec(head(p), cast[ptr PNimTypeV2](p)[]) proc nimDecRefIsLastDyn(p: pointer): bool {.compilerRtl, inl.} = - nimDecRefIsLastCyclicDyn(p) + ## ACYCLIC ref: prompt reclamation, exactly as under --mm:arc. This used to + ## forward to `nimDecRefIsLastCyclicDyn`, which enqueued the dec and so + ## dragged every `.acyclic` type through capture/deadness/commit -- the + ## precise opposite of what the annotation asks for. + ## + ## No grace period is needed here, and that is not an accident: the + ## collector has no way to be holding this cell. It cannot reach it by + ## traversal, because liftdestructors only emits `nimTraceRef` for fields + ## whose type is cyclic; and it cannot hold it as a capture root, because + ## roots come only from `registerLocal` on a drained dec, and an acyclic + ## dec is never queued now that `nimAsgnYrc` is gated on `canFormAcycle`. + ## Both halves must stay true together -- prompt reclamation here is only + ## sound while nothing else puts an acyclic cell into the collector. + result = false + if p != nil: + when hasThreadSupport: + result = atomicDec(head(p).rc, rcIncrement) == -rcIncrement + else: + let cell = head(p) + if (cell.rc and not rcMask) == 0: result = true + else: cell.rc = cell.rc -% rcIncrement proc nimDecRefIsLastCyclicStatic(p: pointer; desc: PNimTypeV2): bool {.compilerRtl, inl.} = result = false diff --git a/lib/system/yrc_opt_proof.lean b/lib/system/yrc_opt_proof.lean new file mode 100644 index 0000000000..79bec0d009 --- /dev/null +++ b/lib/system/yrc_opt_proof.lean @@ -0,0 +1,668 @@ +/- + YRC Optimization Proofs — SCC-uniform ages, demand-grown slots, deferred + reclamation + ======================================================================= + Self-contained, no Mathlib. Checked with Lean 4 (v4.32.0). + + Companion to yrc_proof.lean (core safety: garbage stability, validation + soundness, partitions, grace, fence, deadlock freedom) and to + yrc_tarjan_proof.lean (soundness AND completeness of the SCC deadness + scan). This file models the three changes of the "YRC: optimizations" + round, each of which touches an invariant the other two files rely on: + + §A SCC-UNIFORM EPOCH AGES (commitDead's re-stamp loop). + Before: every proven-live cell was stamped with its OWN survival + age + 1. One member of an SCC could then reach `YrcPromoteAge` + ahead of its SCC-mates; the next capture pruned that INTERNAL edge, + tainting the SCC `flagPruned`, which stops it from ever being + re-stamped — freezing every member's age and re-tracing the whole + structure on every collection from then on. Members age at + different rates whenever a structure is built incrementally, so + this was the common case. + After: the whole SCC is stamped with the age of its YOUNGEST + member + 1, so promotion is all-or-nothing. + + §B DEMAND-GROWN COLLECTOR SLOTS (`gParSlots`, startCollection). + Before: `MaxPar` was a fixed 8 and the 9th collecting thread PARKED + in `parkUntil(anySlotFree())` instead of collecting. After: + `gParSlots` counts the slots in play, starts at 1, and is raised + under gMergeLock exactly when a thread wants to collect and every + slot in play is busy; `MaxPar` (256) is only the table capacity. + Every scan (`isActiveTag`, `anySlotFree`, `buildPendingWatch`) now + runs over a prefix that GROWS under the reader, which is sound only + because of the ordering rule at `slotsInPlay`. + + §C DEFERRED RECLAMATION (`gPendingCells` / `releasePending`). + Before: commitDead BLOCKED until every concurrent capture ended + (the grace period), inside the GC fence — stalling both the + committing collector and every mutator doing a seq operation. + After: the dead batch is parked together with a watch list of the + captures it must outlive, and released at the start of this + thread's next collection. The parked collection's TAG STAYS in + `gActiveTags` (only the phase is cleared): that is what stops a + foreign capture from claiming — and then freeing — a parked cell. + + Nothing here weakens yrc_proof.lean: §A only changes which cells a + capture skips (pruning shrinks the captured set, the conservative + direction), §B only changes how many slots a scan covers, and §C only + moves the free of an already-validated, already-closed dead set later + in time, where garbage stability (yrc_proof.lean §3) keeps it dead. +-/ + +abbrev Obj := Nat +abbrev Tag := Nat +-- Slot indices and times are plain `Nat`: `omega` ignores atoms whose type +-- is an abbreviation, and both appear in arithmetic below. + +/-! ## §A SCC-uniform epoch ages + + The spare header word (`rootIdx`) is a three-way namespace: 0 for a + cell no collection ever touched, a claim tag while a collection owns + the cell, or an epoch stamp (`epochBase | epoch` in the high word, the + survival age in the low word). Tags are allocated strictly below + `epochBase`, so a stamp is never mistaken for a tag — modelled here by + keeping the three cases as separate constructors. -/ + +inductive Word where + | fresh -- 0: never claimed, never stamped + | tag (t : Tag) -- a collection's claim word + | stamp (e : Nat) (age : Nat) -- an epoch stamp written by commitDead + +/-- The age a capture reads out of a claim word (`cap.ages`): a stamp + contributes its recorded age, anything else contributes 0. -/ +def ageOf : Word → Nat + | .stamp _ a => a + | _ => 0 + +def capturedAge (w : Obj → Word) (x : Obj) : Nat := ageOf (w x) + +/-- `claimCell(pruneLive = true)` prunes at a target whose stamp is of the + CURRENT epoch and whose age reached `YrcPromoteAge`: the target is + treated as an opaque live external and is not descended into. Roots + are always claimed with `pruneLive = false`, so this never applies to + them. -/ +def prunable (curEpoch promoteAge : Nat) : Word → Prop + | .stamp e a => e = curEpoch ∧ promoteAge ≤ a + | _ => False + +/-- `high(int32)`, the seed of commitDead's per-SCC minimum. -/ +def bigAge : Nat := 2147483647 + +/-- Minimum of a list with a default (the `var age = high(int32)` fold). -/ +def listMin : List Nat → Nat → Nat + | [], d => d + | a :: l, d => Nat.min a (listMin l d) + +theorem listMin_le : ∀ (l : List Nat) (d a : Nat), a ∈ l → listMin l d ≤ a := by + intro l + induction l with + | nil => intro d a ha; cases ha + | cons b t ih => + intro d a ha + cases List.mem_cons.mp ha with + | inl h => + simp only [listMin, Nat.min_def] + split <;> omega + | inr h => + have := ih d a h + simp only [listMin, Nat.min_def] + split <;> omega + +theorem listMin_ge : ∀ (l : List Nat) (d b : Nat), b ≤ d → + (∀ x, x ∈ l → b ≤ x) → b ≤ listMin l d := by + intro l + induction l with + | nil => intro d b hd _; simpa [listMin] using hd + | cons a t ih => + intro d b hd hall + have h1 : b ≤ a := hall a (by simp) + have h2 := ih d b hd (fun x hx => hall x (List.mem_cons_of_mem a hx)) + simp only [listMin, Nat.min_def] + split <;> omega + +theorem listMin_const (l : List Nat) (d a : Nat) (hne : l ≠ []) + (hall : ∀ x, x ∈ l → x = a) (had : a ≤ d) : listMin l d = a := by + have hlo : a ≤ listMin l d := + listMin_ge l d a had (fun x hx => by have := hall x hx; omega) + cases l with + | nil => exact absurd rfl hne + | cons b t => + have hb : b ∈ b :: t := by simp + have hhi := listMin_le (b :: t) d b hb + have := hall b hb + omega + +/-- **The change.** commitDead stamps a proven-live SCC with ONE word: the + current epoch and 1 + the age of its YOUNGEST member. -/ +def sccAge (w : Obj → Word) (ms : List Obj) : Nat := + listMin (ms.map (fun m => capturedAge w m)) bigAge + 1 + +/-- The post-state of commitDead's re-stamp loop, as committed: every + member of the SCC gets the same word, nothing else is touched. -/ +structure StampedUniform (w w' : Obj → Word) (e : Nat) (ms : List Obj) : Prop where + members : ∀ m, m ∈ ms → w' m = .stamp e (sccAge w ms) + others : ∀ x, x ∉ ms → w' x = w x + +/-- The previous, per-cell scheme, for contrast. -/ +structure StampedPerCell (w w' : Obj → Word) (e : Nat) (ms : List Obj) : Prop where + members : ∀ m, m ∈ ms → w' m = .stamp e (capturedAge w m + 1) + others : ∀ x, x ∉ ms → w' x = w x + +/-- **A1 Uniformity**: after commit, all members of a stamped SCC carry + the identical claim word — same epoch AND same age. -/ +theorem stamped_uniform (w w' : Obj → Word) (e : Nat) (ms : List Obj) + (h : StampedUniform w w' e ms) : + ∀ x y, x ∈ ms → y ∈ ms → w' x = w' y := by + intro x y hx hy + rw [h.members x hx, h.members y hy] + +/-- **A2 No internal prune**: a capture descends into a member `u` of an + SCC only through an edge that was NOT pruned (or because `u` is a + root, which bypasses stamps entirely). With uniform words, every + other member `v` is then unprunable too — so no INTERNAL edge of the + SCC can be pruned, and the SCC is never tainted `flagPruned` by its + own topology. This is precisely the failure the per-cell age caused. -/ +theorem uniform_no_internal_prune + (w : Obj → Word) (curEpoch promoteAge : Nat) (ms : List Obj) + (huni : ∀ x y, x ∈ ms → y ∈ ms → w x = w y) + (u v : Obj) (hu : u ∈ ms) (hv : v ∈ ms) + (hdescended : ¬ prunable curEpoch promoteAge (w u)) : + ¬ prunable curEpoch promoteAge (w v) := by + rw [← huni u v hu hv] + exact hdescended + +/-- A2 applied to the state commitDead actually leaves behind. -/ +theorem committed_scc_no_internal_prune + (w w' : Obj → Word) (e curEpoch promoteAge : Nat) (ms : List Obj) + (hst : StampedUniform w w' e ms) + (u v : Obj) (hu : u ∈ ms) (hv : v ∈ ms) + (hdescended : ¬ prunable curEpoch promoteAge (w' u)) : + ¬ prunable curEpoch promoteAge (w' v) := + uniform_no_internal_prune w' curEpoch promoteAge ms + (stamped_uniform w w' e ms hst) u v hu hv hdescended + +/-- **A3 The per-cell scheme diverges**: two members of ONE SCC whose + captured ages differ (the normal case for a structure built + incrementally across collections) end up with different ages. -/ +theorem perCell_ages_diverge (w w'' : Obj → Word) (e : Nat) (ms : List Obj) + (hp : StampedPerCell w w'' e ms) (u v : Obj) (hu : u ∈ ms) (hv : v ∈ ms) + (hdiff : capturedAge w u ≠ capturedAge w v) : + ageOf (w'' u) ≠ ageOf (w'' v) := by + rw [hp.members u hu, hp.members v hv] + simp only [ageOf] + omega + +/-- ...and diverged ages inside one SCC mean exactly one prunable end of + an internal edge: the promoted member is pruned while its unpromoted + SCC-mate is still being traced. -/ +theorem diverged_ages_prune_internally (curEpoch promoteAge au av : Nat) + (hu : au < promoteAge) (hv : promoteAge ≤ av) : + ¬ prunable curEpoch promoteAge (.stamp curEpoch au) ∧ + prunable curEpoch promoteAge (.stamp curEpoch av) := by + constructor + · intro h + obtain ⟨-, h2⟩ := h + omega + · exact ⟨rfl, hv⟩ + +/-- **A4 The minimum can only delay a promotion, never hasten one**, so + taking it cannot widen the floating-garbage bound (~2 epochs). -/ +theorem uniform_age_le_perCell (w w' w'' : Obj → Word) (e : Nat) (ms : List Obj) + (hu : StampedUniform w w' e ms) (hp : StampedPerCell w w'' e ms) + (m : Obj) (hm : m ∈ ms) : + ageOf (w' m) ≤ ageOf (w'' m) := by + have hmem : capturedAge w m ∈ ms.map (fun x => capturedAge w x) := + List.mem_map_of_mem hm + have hle := listMin_le (ms.map (fun x => capturedAge w x)) bigAge + (capturedAge w m) hmem + rw [hu.members m hm, hp.members m hm] + simp only [ageOf, sccAge] + omega + +/-- Corollary: wherever the SCC-uniform stamp prunes, the per-cell stamp + would have pruned too. Pruning is the only thing a stamp does, so the + change cannot make any capture skip MORE than before. -/ +theorem uniform_never_hastens_promotion (w w' w'' : Obj → Word) (e : Nat) + (ms : List Obj) (promoteAge : Nat) + (hu : StampedUniform w w' e ms) (hp : StampedPerCell w w'' e ms) + (m : Obj) (hm : m ∈ ms) (h : promoteAge ≤ ageOf (w' m)) : + promoteAge ≤ ageOf (w'' m) := by + have := uniform_age_le_perCell w w' w'' e ms hu hp m hm + omega + +/-- **A5 The uniform age is exactly the common age + 1**, so a surviving + SCC's age advances by one per collection and stays uniform: the + invariant of A1/A2 is inductive. -/ +theorem uniform_age_succ (w w' : Obj → Word) (e a : Nat) (ms : List Obj) + (hne : ms ≠ []) (hcap : a ≤ bigAge) + (hall : ∀ m, m ∈ ms → capturedAge w m = a) + (h : StampedUniform w w' e ms) : + ∀ m, m ∈ ms → ageOf (w' m) = a + 1 := by + intro m hm + have hmin : listMin (ms.map (fun x => capturedAge w x)) bigAge = a := by + apply listMin_const + · cases ms with + | nil => exact absurd rfl hne + | cons b t => simp + · intro x hx + obtain ⟨y, hy, rfl⟩ := List.mem_map.mp hx + exact hall y hy + · exact hcap + rw [h.members m hm] + simp only [ageOf, sccAge, hmin] + +/-- **A6 The freeze**: an SCC that is never re-stamped (the `flagPruned` + taint excludes it from commitDead's stamp loop) keeps its age + forever. Below `YrcPromoteAge` that means it is fully re-traced by + every collection until the epoch turns — the regression A2 removes. -/ +theorem age_frozen_if_never_restamped (age : Nat → Nat) (a : Nat) + (h0 : age 0 = a) (hfreeze : ∀ n, age (n + 1) = age n) : + ∀ n, age n = a := by + intro n + induction n with + | zero => exact h0 + | succ n ih => rw [hfreeze n, ih] + +/-- **A7 Progress**: an SCC that IS re-stamped every round promotes after + `YrcPromoteAge` collections, and by A2 stays promoted uniformly — so + a long-lived structure is traced once per epoch, not once per + collection. -/ +theorem age_promotes_if_restamped (age : Nat → Nat) (a promoteAge : Nat) + (h0 : age 0 = a) (hstep : ∀ n, age (n + 1) = age n + 1) : + promoteAge ≤ age promoteAge := by + have h : ∀ n, age n = a + n := by + intro n + induction n with + | zero => simpa using h0 + | succ n ih => rw [hstep n, ih]; omega + rw [h promoteAge] + omega + +/-! ## §B Demand-grown collector slots + + `gParSlots` counts the slots IN PLAY. It starts at 1, is raised under + gMergeLock when a thread wants to collect and every slot in play is + busy, and is NEVER lowered. Two things must hold: + + (i) a scan over the prefix `0 ..< slotsInPlay()` must never MISS an + active tag — a missed tag would let a second collection claim a + cell another collection already owns, breaking partition + disjointness (yrc_proof.lean §5) and admitting a double free; + (ii) a thread must not park while the table still has room — that was + the throttle the fixed `MaxPar = 8` imposed. + + (i) rests on the publication order in startCollection: the wider bound + is stored BEFORE the tag lands in the new slot, and `gParSlots` only + grows. So a load of `slotsInPlay()` ordered AFTER the read of a tagged + claim word is guaranteed to cover the slot that wrote that tag. -/ + +/-- `gParSlots` never shrinks, so a prefix scan cannot shrink under a + reader either. -/ +theorem in_play_persists (parSlots : Nat → Nat) + (hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j) + (k : Nat) (t t' : Nat) (h : t ≤ t') (hk : k < parSlots t) : + k < parSlots t' := by + have := hmono t t' h + omega + +/-- **B1 The scan covers the slot that wrote the tag.** `tGrow` is when + the slot was put in play (under gMergeLock), `tTag` the tag store, + `tRead` the reader's load of the claim word, `tScan` its subsequent + load of `slotsInPlay()`. -/ +theorem scan_covers_tagged_slot (parSlots : Nat → Nat) + (hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j) + (k : Nat) (tGrow tTag tRead tScan : Nat) + (hgrow : k < parSlots tGrow) + (hpub : tGrow ≤ tTag) -- wider bound published before the tag store + (hread : tTag ≤ tRead) -- the reader observed the tag + (hafter : tRead ≤ tScan) :-- slotsInPlay() loaded AFTER the claim word + k < parSlots tScan := by + have := hmono tGrow tScan (by omega) + omega + +/-- **B2 `isActiveTag` is complete**: an active tag is always found by the + prefix scan, so `claimCell` never claims a cell another collection + owns. -/ +theorem active_tag_never_missed (parSlots : Nat → Nat) + (tagAt : Nat → Nat → Tag) + (hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j) + (k : Nat) (t : Tag) (tGrow tTag tRead tScan : Nat) + (hgrow : k < parSlots tGrow) (hpub : tGrow ≤ tTag) + (hread : tTag ≤ tRead) (hafter : tRead ≤ tScan) + (hheld : tagAt k tScan = t) : + ∃ j, j < parSlots tScan ∧ tagAt j tScan = t := + ⟨k, scan_covers_tagged_slot parSlots hmono k tGrow tTag tRead tScan + hgrow hpub hread hafter, hheld⟩ + +/-- **B3 The ordering rule is load-bearing**: a `slotsInPlay()` load + ordered BEFORE the read of the claim word can legitimately miss the + slot, because the pool may widen in between. -/ +theorem scan_before_read_may_miss : + ∃ (parSlots : Nat → Nat) (k : Nat) (tScan tGrow : Nat), + (∀ i j, i ≤ j → parSlots i ≤ parSlots j) ∧ tScan < tGrow ∧ + k < parSlots tGrow ∧ ¬ (k < parSlots tScan) := by + refine ⟨fun t => t + 1, 1, 0, 1, ?_, ?_, ?_, ?_⟩ + · intro i j h + show i + 1 ≤ j + 1 + omega + · decide + · decide + · decide + +/-- startCollection's slot decision. -/ +inductive SlotOutcome where + | reuse (k : Nat) -- a slot already in play was free + | grow (k : Nat) -- pool widened; the new slot is `k = inPlay` + | park -- table full: MaxPar collections already running + +inductive SlotClaim (busy : Nat → Prop) (inPlay maxPar : Nat) : SlotOutcome → Prop where + | reuse (k : Nat) (hk : k < inPlay) (hfree : ¬ busy k) : + SlotClaim busy inPlay maxPar (.reuse k) + | grow (hfull : ∀ k, k < inPlay → busy k) (hroom : inPlay < maxPar) : + SlotClaim busy inPlay maxPar (.grow inPlay) + | park (hfull : ∀ k, k < inPlay → busy k) (hno : maxPar ≤ inPlay) : + SlotClaim busy inPlay maxPar .park + +/-- **B4 Parking means saturation**, not throttling: a thread blocks in + `parkUntil(anySlotFree())` only when `MaxPar` collections are running + concurrently. Under the old fixed bound this triggered at the 9th + collecting thread (32 threads vs 8 slots: 6.3s against 2.6s). -/ +theorem park_only_when_saturated (busy : Nat → Prop) (inPlay maxPar : Nat) + (h : SlotClaim busy inPlay maxPar .park) : + maxPar ≤ inPlay ∧ ∀ k, k < inPlay → busy k := by + cases h with + | park hfull hno => exact ⟨hno, hfull⟩ + +/-- **B5 No parking below capacity.** -/ +theorem no_park_below_capacity (busy : Nat → Prop) (inPlay maxPar : Nat) + (hroom : inPlay < maxPar) : ¬ SlotClaim busy inPlay maxPar .park := by + intro h + cases h with + | park hfull hno => omega + +/-- **B6 A grown slot is fresh**: `k = inPlay` is distinct from every slot + already in play, so the widening thread cannot collide with a + collection that is already running. -/ +theorem grown_slot_not_in_play (inPlay k : Nat) (hk : k < inPlay) : + inPlay ≠ k := by omega + +/-! ## §C Deferred reclamation + + commitDead used to spin until every concurrent capture had ended before + freeing, INSIDE the GC fence. Now the batch is parked in + `gPendingCells` with a watch list `gPendingWatch` of the (slot, tag) + pairs that were in capture phase at commit time, and `releasePending` + — the FIRST thing startCollection does, outside the fence and holding + no lock — waits out that list and then frees. + + Three obligations: + (C1) the watch list is COMPLETE: every capture that could hold a stale + `(slot, value)` snapshot of the batch is on it; + (C2) the grace check is SOUND: `graceSatisfied` reports "finished" only + when the watched capture really has finished; + (C3) the batch is PROTECTED while parked: no foreign capture may claim + (and hence free) one of its cells. This is why finishCollection + clears only `gSlotPhase` and leaves the tag in `gActiveTags`. -/ + +/-- One slot's published state. -/ +structure SlotState where + tag : Tag + phase : Nat -- 0 idle, 1 capturing, 2 committing + +/-- finishCollection with a batch parked: phase → 0, tag RETAINED. -/ +def finishParked (st : SlotState) : SlotState := { st with phase := 0 } + +/-- releasePending, after the grace wait: the tag is given up first, then + the destructors and `nimRawDispose` run. -/ +def releaseSlot (st : SlotState) : SlotState := { st with tag := 0 } + +theorem finishParked_keeps_tag (st : SlotState) : + (finishParked st).tag = st.tag := rfl + +/-- A parked slot blocks nobody's grace period: its phase is 0, so every + other collector's `graceSatisfied` passes over it. -/ +theorem parked_slot_blocks_nobody (st : SlotState) (tg : Tag) : + ¬ ((finishParked st).tag = tg ∧ (finishParked st).phase = 1) := by + intro h + simp [finishParked] at h + +/-- ...yet the tag survives, which is what protects the parked cells. -/ +theorem parked_slot_still_tagged (st : SlotState) (t : Tag) (h : st.tag = t) : + (finishParked st).tag = t := h + +/-- `gPendingWatch`, as `(slot shl 32) or tag` pairs. -/ +abbrev WatchList := List (Nat × Tag) + +/-- `graceSatisfied()` evaluated at time `t`. -/ +def graceSatisfied (tagAt : Nat → Nat → Tag) (phaseAt : Nat → Nat → Nat) + (W : WatchList) (t : Nat) : Prop := + ∀ p, p ∈ W → ¬ (tagAt p.1 t = p.2 ∧ phaseAt p.1 t = 1) + +/-- **C1 The watch list is complete.** A capture that was in flight at + commit time is running on a slot that was in play when its tag was + stored; by B1 the `buildPendingWatch` scan — which loads + `slotsInPlay()` after reading the claim state — covers that slot, and + the capture's phase is 1, so it is recorded. -/ +theorem watch_covers_inflight_capture (parSlots : Nat → Nat) + (tagAt : Nat → Nat → Tag) (phaseAt : Nat → Nat → Nat) + (hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j) + (s : Nat) (tg : Tag) (tGrow tTag commitT : Nat) + (hgrow : s < parSlots tGrow) (hpub : tGrow ≤ tTag) (hread : tTag ≤ commitT) + (hcapturing : tagAt s commitT = tg ∧ phaseAt s commitT = 1) : + s < parSlots commitT ∧ tagAt s commitT = tg ∧ phaseAt s commitT = 1 := + ⟨scan_covers_tagged_slot parSlots hmono s tGrow tTag commitT commitT + hgrow hpub hread (Nat.le_refl commitT), hcapturing.1, hcapturing.2⟩ + +/-- **C2 The grace check is sound**: if `graceSatisfied` holds at `t` and + a watched capture was still running at `t`, we have a contradiction — + so every watched capture finished strictly before `t`. There is no + ABA on the (slot, tag) pair: tags come from a monotonic counter + (yrc_proof.lean §5 `tags_distinct`), so a later collection on the + same slot carries a different tag. -/ +theorem grace_check_sound (tagAt : Nat → Nat → Tag) (phaseAt : Nat → Nat → Nat) + (W : WatchList) (s : Nat) (tg : Tag) (start finish t : Nat) + (hw : (s, tg) ∈ W) + (hcap : ∀ u, start ≤ u → u ≤ finish → tagAt s u = tg ∧ phaseAt s u = 1) + (hstart : start ≤ t) + (hsat : graceSatisfied tagAt phaseAt W t) : + finish < t := by + cases Nat.lt_or_ge finish t with + | inl h => exact h + | inr h => exact absurd (hcap t hstart h) (hsat (s, tg) hw) + +/-- A capture's window and the values it ever snapshots (TraceEntry), as + in yrc_proof.lean §6. -/ +structure CaptureWindow where + start : Nat + finish : Nat + snap : Obj → Prop + derefs : Obj → Nat → Prop + +/-- **C3 Grace safety survives the deferral.** `commitT` is when the dead + set validated, `releaseT` when releasePending's wait succeeded (C2), + `freeT` when the batch is actually disposed. The only change from + yrc_proof.lean's `grace_no_use_after_free` is that `freeT` moved + LATER — the wait is unchanged in strength, it just happens off the + commit path. -/ +theorem deferred_grace_no_use_after_free + (C : CaptureWindow) (D : Obj → Prop) (commitT releaseT freeT : Nat) + (h_deref : ∀ x t, C.derefs x t → C.start ≤ t ∧ t ≤ C.finish ∧ C.snap x) + (h_watched : C.start < commitT → C.finish < releaseT) + (h_release : releaseT ≤ freeT) + (h_miss : commitT ≤ C.start → ∀ x, D x → ¬ C.snap x) : + ∀ x t, D x → C.derefs x t → t < freeT := by + intro x t hD hd + obtain ⟨h1, h2, h3⟩ := h_deref x t hd + cases Nat.lt_or_ge C.start commitT with + | inl h => have := h_watched h; omega + | inr h => exact absurd h3 (h_miss h x hD) + +/-- claimCell's decision on a cell, as a relation over its claim word. -/ +inductive ClaimResult where + | mine -- our own tag: already captured this round + | refuse -- owned by another ACTIVE collection (-1, crossPend) + | prune -- proven live this epoch (-2, opaque live external) + | claim -- CAS it into our partition + +inductive ClaimDecision (myTag curEpoch promoteAge : Nat) (active : Tag → Prop) : + Word → ClaimResult → Prop where + | mine (t : Tag) (h : t = myTag) : + ClaimDecision myTag curEpoch promoteAge active (.tag t) .mine + | refuse (t : Tag) (hne : t ≠ myTag) (ha : active t) : + ClaimDecision myTag curEpoch promoteAge active (.tag t) .refuse + | claimTag (t : Tag) (hne : t ≠ myTag) (ha : ¬ active t) : + ClaimDecision myTag curEpoch promoteAge active (.tag t) .claim + | prune (e a : Nat) (hp : prunable curEpoch promoteAge (.stamp e a)) : + ClaimDecision myTag curEpoch promoteAge active (.stamp e a) .prune + | claimStamp (e a : Nat) (hp : ¬ prunable curEpoch promoteAge (.stamp e a)) : + ClaimDecision myTag curEpoch promoteAge active (.stamp e a) .claim + | claimFresh : + ClaimDecision myTag curEpoch promoteAge active .fresh .claim + +/-- **C4 A cell carrying an active foreign tag is always refused.** -/ +theorem tagged_cell_refused (myTag curEpoch promoteAge : Nat) (active : Tag → Prop) + (ownerTag : Tag) (hne : ownerTag ≠ myTag) (ha : active ownerTag) + (r : ClaimResult) + (h : ClaimDecision myTag curEpoch promoteAge active (.tag ownerTag) r) : + r = .refuse := by + cases h with + | mine t ht => exact absurd ht hne + | refuse t hne' ha' => rfl + | claimTag t hne' ha' => exact absurd ha ha' + +/-- **C5 No double free while parked.** The parked cells still carry the + parking collection's tag, and finishCollection left that tag in + `gActiveTags` (only the phase was cleared, C-`finishParked`). So a + foreign capture that reaches a parked cell through a stale snapshot + refuses it: it can neither traverse it nor claim it, hence never + classifies it dead and never frees it. Without the tag retention this + is exactly a double free — the batch's owner will free it too. -/ +theorem no_foreign_claim_while_parked + (activeAt : Nat → Tag → Prop) (ownerTag myTag : Tag) + (curEpoch promoteAge : Nat) (commitT releaseT u : Nat) + (hretain : ∀ v, commitT ≤ v → v ≤ releaseT → activeAt v ownerTag) + (hne : ownerTag ≠ myTag) (h1 : commitT ≤ u) (h2 : u ≤ releaseT) + (r : ClaimResult) + (h : ClaimDecision myTag curEpoch promoteAge (activeAt u) (.tag ownerTag) r) : + r = .refuse := + tagged_cell_refused myTag curEpoch promoteAge (activeAt u) ownerTag hne + (hretain u h1 h2) r h + +/-- **C6 Deferring the free is safe.** The batch was closed (unreachable) + at commit time — that is what validation established (yrc_proof.lean + §4 `validated_closed`) — and `hstable` is exactly + yrc_proof.lean §3 `garbage_stability`: a closed set stays closed + under every mutator step, allocation and foreign free. Freeing one + collection later therefore satisfies the same §1 free condition as + freeing immediately. -/ +theorem deferred_free_safe (unreachable : Nat → Obj → Prop) (D : Obj → Prop) + (commitT freeT : Nat) + (hcommit : ∀ x, D x → unreachable commitT x) + (hstable : ∀ x t t', D x → t ≤ t' → unreachable t x → unreachable t' x) + (hlater : commitT ≤ freeT) : + ∀ x, D x → unreachable freeT x := + fun x hx => hstable x commitT freeT hx hlater (hcommit x hx) + +/-- **C7 The grace wait left the GC fence.** It now runs at the start of + startCollection, before `yrcGcFenceEnter`, so no mutator seq + operation can be stalled by it — the property the deferral was made + for. -/ +theorem grace_wait_outside_fence (waitStart waitEnd fenceEnter fenceExit t : Nat) + (horder : waitEnd < fenceEnter) (hw : waitStart ≤ t ∧ t ≤ waitEnd) : + ¬ (fenceEnter ≤ t ∧ t ≤ fenceExit) := by + intro hf + omega + +/-- `waits a b`: thread `a` is blocked in releasePending on thread `b`'s + capture. -/ +def waits (capturing releasing : Nat → Prop) (a b : Nat) : Prop := + releasing a ∧ capturing b + +/-- **C8 The new wait cannot deadlock.** releasePending runs BEFORE this + thread claims a slot, so a releasing thread is never itself + capturing; the wait-for graph therefore has depth one and cannot + contain a cycle of any length. (Captures never wait on anything: + claimCell returns -1 immediately on contention.) -/ +theorem release_wait_depth_one (capturing releasing : Nat → Prop) + (hexcl : ∀ t, releasing t → ¬ capturing t) + (a b c : Nat) (h1 : waits capturing releasing a b) : + ¬ waits capturing releasing b c := by + intro h2 + exact hexcl b h2.1 h1.2 + +/-- Corollary: no 2-cycle, hence no mutual wait between two parked + collectors. -/ +theorem release_wait_acyclic (capturing releasing : Nat → Prop) + (hexcl : ∀ t, releasing t → ¬ capturing t) (a b : Nat) + (h1 : waits capturing releasing a b) : + ¬ waits capturing releasing b a := + release_wait_depth_one capturing releasing hexcl a b a h1 + +/-! ## Summary of verified properties (all QED, no sorry) + + §A `stamped_uniform` — a committed SCC's members carry one identical + claim word. + `uniform_no_internal_prune`, `committed_scc_no_internal_prune` — a + capture that descends into a member cannot prune an internal edge, + so an SCC is never tainted `flagPruned` by its own topology. + `perCell_ages_diverge` + `diverged_ages_prune_internally` — the + pre-fix scheme admits exactly that taint. + `uniform_age_le_perCell`, `uniform_never_hastens_promotion` — the + minimum only delays promotions, so the float bound is unchanged. + `uniform_age_succ` — uniformity is inductive: age advances by one + and stays uniform. + `age_frozen_if_never_restamped` / `age_promotes_if_restamped` — the + frozen-age regression versus the intended once-per-epoch trace. + + §B `in_play_persists`, `scan_covers_tagged_slot`, + `active_tag_never_missed` — a growing `gParSlots` prefix scan never + misses an active tag, PROVIDED `slotsInPlay()` is loaded after the + claim word; `scan_before_read_may_miss` shows the order is + load-bearing. + `park_only_when_saturated`, `no_park_below_capacity`, + `grown_slot_not_in_play` — a collector parks only when `MaxPar` + collections run at once, and a widened slot collides with nobody. + + §C `watch_covers_inflight_capture` — the watch list records every + capture that could hold a stale snapshot of the batch (via §B). + `grace_check_sound` — `graceSatisfied` reports "finished" only when + the watched capture has finished. + `deferred_grace_no_use_after_free` — no capture dereferences a + parked cell at or after its free time. + `tagged_cell_refused`, `no_foreign_claim_while_parked` — retaining + the tag (finishCollection clears only the phase) is what prevents a + foreign collection from claiming and freeing a parked cell. + `parked_slot_blocks_nobody`, `parked_slot_still_tagged` — the two + halves of that split: protection without blocking. + `deferred_free_safe` — deferring the free preserves the §1 free + condition, by garbage stability. + `grace_wait_outside_fence` — the wait no longer overlaps the GC + fence, so it cannot stall a mutator's seq operation. + `release_wait_depth_one`, `release_wait_acyclic` — the new wait + adds no cycle to the wait-for structure of yrc_proof.lean §8. + + ## What is NOT proved + + • Slot-retention liveness. A parked batch holds its tag slot until the + owning thread's NEXT collection (or GC_runOrc / nimYrcThreadTeardown, + both of which call releasePending). A thread that parks a batch and + then never collects again keeps a slot occupied; with enough such + threads the table could saturate and other collectors would park + (§B4). Bounded in practice by `MaxPar = 256` and by teardown, not + formalized. + • That `buildPendingWatch` returning false (nothing capturing) really + is the common case — a performance claim, measured, not proved. + • Destructor timing. Deferral runs a dead batch's destructors one + collection later. Safety is C6; the observable-behaviour claim + ("nothing else observes the delay, the cells are unreachable and + their references already dropped") is an argument about the Nim + language semantics, not modelled here. + • Conservatism of tag retention. While a batch is parked, the tag also + protects SURVIVORS that kept a stale tag (dirty and pruned SCCs are + deliberately not re-stamped), so a foreign capture refuses them for + one extra collection. That delays their re-examination; it cannot + lose them, because §A's E1–E4 hooks keep a dec-witness registered. + • Everything already listed as unproved in yrc_proof.lean (rc-exactness + mechanics, the C11 memory model, liveness/completeness of the retry + loop, tag wrap-around). +-/ diff --git a/lib/system/yrc_proof.lean b/lib/system/yrc_proof.lean index 64a501ed03..81d84197b6 100644 --- a/lib/system/yrc_proof.lean +++ b/lib/system/yrc_proof.lean @@ -459,9 +459,18 @@ theorem cross_target_live (D : Obj → Prop) (claimedB : Obj → Prop) A concurrent capture holds raw `(slot, value)` snapshots (TraceEntry); the value pointer is dereferenced later (header read in claimCell). A capture that overlapped our validation may have snapshotted a slot - that USED to point into our dead set. commitDead therefore waits, for - every other slot that is in capture phase (gSlotPhase == 1), until - that capture ends — captures never wait on anyone, so this is bounded. + that USED to point into our dead set. The dead batch must therefore + outlive every other slot that was in capture phase (gSlotPhase == 1) + at commit time — captures never wait on anyone, so this is bounded. + + commitDead no longer BLOCKS on that: it parks the batch + (`gPendingCells`) with a watch list of those captures and + `releasePending` frees it at the start of this thread's next + collection, off the commit path and outside the GC fence. The parking + collection's tag stays in `gActiveTags` so a foreign capture cannot + claim a parked cell. See yrc_opt_proof.lean §C for the model of the + deferral; the theorems below are the invariant it preserves, with the + free time merely moved later. Two obligations: (a) captures that started BEFORE our commit are waited out — temporal @@ -498,9 +507,10 @@ structure CaptureWindow where /-- **Grace safety**: no capture dereferences a dead cell at or after its free time. `commitT` is when the dead set validated; `freeT` is - when commitDead's free loop runs. The premises are exactly the - protocol: (grace) commitDead's spin means any capture that started - before commit has finished before we free; (miss) §6(b) above. -/ + when the free loop runs (in releasePending, one collection later). + The premises are exactly the protocol: (grace) the watch list means + any capture that started before commit has finished before we free; + (miss) §6(b) above. -/ theorem grace_no_use_after_free (C : CaptureWindow) (D : Obj → Prop) (commitT freeT : Nat) (h_deref : ∀ x t, C.derefs x t → C.start ≤ t ∧ t ≤ C.finish ∧ C.snap x) @@ -676,8 +686,8 @@ theorem no_deadlock_from_total_order {n : Nat} referenced across a partition boundary is never freed by its owner this round (soundness of claimCell's -1 + crossPend). §6 `post_commit_snap_misses_dead`, `grace_no_use_after_free` — with - commitDead's grace spin, no capture ever dereferences freed - memory. + the grace period (now enforced by the deferred batch's watch list, + yrc_opt_proof.lean §C), no capture ever dereferences freed memory. §7 `fence_mutual_exclusion` — the SEQ_CST Dekker pairing in seqs_v2.nim excludes seq structure mutation during collection. §8 `lockLevel_injective`, `mergeLock_level_min`, @@ -714,7 +724,12 @@ theorem no_deadlock_from_total_order {n : Nat} Commit re-stamps proven-live cells with (epochBase|epoch, survivalAge) in the claim word; a capture treats a current-epoch stamp of age ≥ YrcPromoteAge on a DESCENDANT as an opaque live external and does not - descend. Soundness needs no new lemmas: a pruned cell is simply an + descend. The age is the SCC's, not the cell's — every member is + stamped with the age of the SCC's YOUNGEST member, so promotion is + all-or-nothing and no INTERNAL edge is ever pruned; see + yrc_opt_proof.lean §A, which also shows the minimum can only delay a + promotion, so the float bound below is unaffected. Soundness needs no + new lemmas: a pruned cell is simply an uncaptured cell, so the captured set shrinks and every §3–§6 statement quantifies over a smaller S. Pruning can only ADD unexplained external refs to captured SCCs (a pruned predecessor's refs are never explained