diff --git a/lib/system/threadimpl.nim b/lib/system/threadimpl.nim index dcd1b267a0..e35378db0e 100644 --- a/lib/system/threadimpl.nim +++ b/lib/system/threadimpl.nim @@ -27,6 +27,10 @@ else: template afterThreadRuns() = for i in countdown(nimThreadDestructionHandlers.len-1, 0): nimThreadDestructionHandlers[i]() + when declared(nimYrcThreadTeardown): + # YRC: spill this thread's candidate roots so its garbage remains + # collectible after the thread is gone + nimYrcThreadTeardown() proc onThreadDestruction*(handler: proc () {.closure, gcsafe, raises: [].}) = ## Registers a *thread local* handler that is called at the thread's diff --git a/lib/system/yrc.nim b/lib/system/yrc.nim index 56f196dc43..da4b073209 100644 --- a/lib/system/yrc.nim +++ b/lib/system/yrc.nim @@ -143,6 +143,19 @@ when useAtomicRc: 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 + ## cell sits in at most one candidate buffer. + block: + var expected = atomicLoadN(addr c.rc, ATOMIC_RELAXED) + var won = false + while (expected and flag) == 0: + if atomicCompareExchangeN(addr c.rc, addr expected, expected or flag, + true, ATOMIC_ACQ_REL, ATOMIC_RELAXED): + won = true + break + won else: template color(c): untyped = c.rc and colorMask template loadRc(c): int = c.rc @@ -150,6 +163,11 @@ else: 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 + if won: c.rc = c.rc or flag + won const optimizedOrc = false @@ -245,6 +263,7 @@ type crossOff: RawSeq[int32] # condensation cross edges, bucketed by source crossTgt: RawSeq[int32] crossCursor: RawSeq[int32] + crossPend: CellSeq[Cell] # edge targets owned by other active collections GcEnv = object traceStack: CellSeq[TraceEntry] @@ -255,7 +274,7 @@ type freed, touched: int keepThreshold: bool -var gCap: CaptureBufs +var gCap {.threadvar.}: CaptureBufs const flagDead = 1'u8 @@ -268,26 +287,78 @@ proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} = cast[TraceProc](desc.traceImpl)(p, addr(j)) # The spare rootIdx header word (unused by YRC's root registration, which -# relies on inRootsFlag) doubles as the capture stamp: it packs an epoch tag -# with the cell's dense discovery index, so node -> index lookup is one load -# and stale stamps from earlier collections never need clearing. -var gCaptureEpoch: int = 1 +# 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 +# collections) never need clearing, they are simply reclaimable. +const MaxPar {.intdefine.} = 4 # max concurrent collections when sizeof(int) == 8: - # 31-bit epoch, wraps after 2^31 collections (decades of uptime); on wrap - # a stale stamp collision is astronomically unlikely but not impossible. - template bumpEpoch() = - gCaptureEpoch = (gCaptureEpoch +% 1) and 0x7FFFFFFF - if gCaptureEpoch == 0: gCaptureEpoch = 1 - template isStamped(c: Cell): bool = (c.rootIdx shr 32) == gCaptureEpoch - template stamp(c: Cell; idx: int) = - c.rootIdx = gCaptureEpoch shl 32 or idx - template denseIdx(c: Cell): int32 = int32(c.rootIdx and 0xFFFFFFFF) + const ParSlots = MaxPar +else: + const ParSlots = 1 # no room to pack tags: single collector + +var + gMergeLock: Lock # protects the tag slots + orphaned roots + gActiveTags: array[ParSlots, int] # 0 = free slot + gSlotPhase: array[ParSlots, int] # 0 idle, 1 capturing, 2 committing + gSoloCapture: int # a solo collection is in its capture phase + gTagCounter: int + gMyTag {.threadvar.}: int + gMySlot {.threadvar.}: int + gAmSolo {.threadvar.}: bool + gWaitLock: Lock # pairs gWaitCond's wait/broadcast; leaf + gWaitCond: Cond # signaled on capture-end and collection-finish + +const SpinBeforePark = 4000 + +template parkUntil(cond: untyped) = + ## Bounded spin (collections transition in microseconds when the system is + ## healthy), then block on gWaitCond. `cond` must only read atomics, and + ## every write that can make it true is followed by collectorEvent(). + var spins {.inject.} = 0 + while not (cond): + inc spins + if spins >= SpinBeforePark: + acquire gWaitLock + while not (cond): + wait(gWaitCond, gWaitLock) + release gWaitLock + break + +proc collectorEvent() {.inline.} = + ## Wake every parked collector after a slot/phase/solo transition. The + ## broadcast happens under gWaitLock so that a waiter that saw the old + ## state is already inside wait() by the time we broadcast. + acquire gWaitLock + broadcast gWaitCond + release gWaitLock + +proc anySlotFree(): bool {.inline.} = + result = false + for sl in 0 ..< ParSlots: + if atomicLoadN(addr gActiveTags[sl], ATOMIC_ACQUIRE) == 0: + return true + +when sizeof(int) == 8: + template isStamped(c: Cell): bool = + # "stamped" means: claimed by THIS collection. A relaxed load suffices: + # only this thread ever stores gMyTag, and any stale read of a foreign + # 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) + + proc isActiveTag(t: int): bool {.inline.} = + result = false + if t != 0: + for s in 0 ..< ParSlots: + if atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) == t: + return true else: - # no room for an epoch: stamps are cleared at the end of each collection - template bumpEpoch() = discard template isStamped(c: Cell): bool = c.rootIdx != 0 - template stamp(c: Cell; idx: int) = c.rootIdx = idx +% 1 template denseIdx(c: Cell): int32 = int32(c.rootIdx -% 1) type @@ -307,9 +378,16 @@ type ## Invoked while holding the global lock; must not call back into YRC. var - roots: CellSeq[Cell] # merged roots, used under global lock + roots: CellSeq[Cell] # ORPHANED candidates only: spilled by exiting + # threads, adopted by the next collection on any + # thread. Guarded by gMergeLock. + gLocalRoots {.threadvar.}: CellSeq[Cell] + ## This thread's candidate roots. Only the owning thread touches it: + ## 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. stripes: array[NumStripes, Stripe] - rootsThreshold: int = 128 + rootsThreshold: int = 128 # shared adaptive heuristic; races are benign defaultThreshold = when defined(nimFixedOrc): 10_000 else: 128 gPreventThreadFromCollectProc: PreventThreadFromCollectProc = nil @@ -359,13 +437,12 @@ proc nimIncRefCyclic(p: pointer; cyclic: bool) {.compilerRtl, inl.} = if slot < QueueSize: atomicStoreN(addr stripes[s].toInc[slot], h, ATOMIC_RELEASE) else: - yrcCollectorLock: - h.rc = h.rc +% rcIncrement - for i in 0.. 0: # racy peek; exact under the lock + acquire gMergeLock + if gLocalRoots.d == nil: init(gLocalRoots) + for i in 0 ..< roots.len: + add(gLocalRoots, roots.d[i][0], roots.d[i][1]) + roots.len = 0 + release gMergeLock proc collectCycles() @@ -477,6 +578,7 @@ proc prepareCapture() = init gCap.crossOff init gCap.crossTgt init gCap.crossCursor + init gCap.crossPend else: gCap.recs.len = 0 gCap.tstack.len = 0 @@ -485,137 +587,184 @@ proc prepareCapture() = gCap.sccMemStart.len = 0 gCap.sccMembers.len = 0 gCap.sumRefs.len = 0 + gCap.crossPend.len = 0 -proc pushCell(c: Cell; desc: PNimTypeV2): int32 {.inline.} = - result = int32(gCap.recs.len) - stamp(c, gCap.recs.len) - # rc captured without the flag bits: the collector itself toggles - # inRootsFlag between capture and commit, which must not look like a - # mutation to the commit-time rc validation - gCap.recs.add CaptureRec(cell: c, desc: desc, rcWord: loadRc(c) and not rcMask, - lowlink: result, sccOf: -1'i32) - gCap.tstack.add result +# rc is captured without the flag bits: the collector itself toggles +# inRootsFlag between capture and commit, which must not look like a +# mutation to the commit-time rc validation. +when sizeof(int) == 8: + proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs): int32 = + ## Dense index if this collection owns `c` (claiming and registering it + ## if it was unclaimed), or -1 if another ACTIVE collection owns it. + 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 + if (old shr 32) == gMyTag: + return int32(old and 0xFFFFFFFF) + let idx = cap.recs.len + c.rootIdx = (gMyTag shl 32) or idx + cap.recs.add CaptureRec(cell: c, desc: desc, + rcWord: loadRc(c) and not rcMask, + lowlink: int32(idx), sccOf: -1'i32) + cap.tstack.add int32(idx) + return int32(idx) + while true: + var old = atomicLoadN(addr c.rootIdx, ATOMIC_ACQUIRE) + if (old shr 32) == gMyTag: + return int32(old and 0xFFFFFFFF) + if isActiveTag(old shr 32): + return -1 + let idx = cap.recs.len + if atomicCompareExchangeN(addr c.rootIdx, addr old, + (gMyTag shl 32) or idx, false, + ATOMIC_ACQ_REL, ATOMIC_RELAXED): + cap.recs.add CaptureRec(cell: c, desc: desc, + rcWord: loadRc(c) and not rcMask, + lowlink: int32(idx), sccOf: -1'i32) + cap.tstack.add int32(idx) + return int32(idx) +else: + proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs): int32 = + if c.rootIdx != 0: + result = int32(c.rootIdx -% 1) + else: + result = int32(cap.recs.len) + c.rootIdx = cap.recs.len +% 1 + cap.recs.add CaptureRec(cell: c, desc: desc, + rcWord: loadRc(c) and not rcMask, + lowlink: result, sccOf: -1'i32) + cap.tstack.add result -proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv) = +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 orcAssert(j.traceStack.len == 0, "capture: trace stack not empty") - let root = pushCell(s, desc) + let root = claimCell(s, desc, cap) + if root < 0: + return # another active collection owns this candidate; it handles it trace(s, desc, j) - gCap.frames.add TarjanFrame(u: root, base: 0) - while gCap.frames.len > 0: - let u = gCap.frames.d[gCap.frames.len -% 1].u - let base = gCap.frames.d[gCap.frames.len -% 1].base + 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 if j.traceStack.len > base: let (entry, tdesc) = j.traceStack.pop() let t = head(entry.val) if isStamped(t): let v = denseIdx(t) - gCap.edges.add (int64(u) shl 32) or int64(v) - if gCap.recs.d[v].sccOf < 0 and v < gCap.recs.d[u].lowlink: - gCap.recs.d[u].lowlink = v + 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 else: let childBase = j.traceStack.len - let v = pushCell(t, tdesc) - gCap.edges.add (int64(u) shl 32) or int64(v) - trace(t, tdesc, j) - gCap.frames.add TarjanFrame(u: v, base: childBase) + let v = claimCell(t, tdesc, cap) + if v < 0: + # cross-collection edge: the owner sees our reference in the rc + # word and classifies the target live; we re-register it as a + # candidate before our commit so it is re-examined later + cap.crossPend.add(t, tdesc) + else: + cap.edges.add (int64(u) shl 32) or int64(v) + trace(t, tdesc, j) + cap.frames.add TarjanFrame(u: v, base: childBase) else: - gCap.frames.len = gCap.frames.len -% 1 - if gCap.frames.len > 0: - let pu = gCap.frames.d[gCap.frames.len -% 1].u - if gCap.recs.d[u].lowlink < gCap.recs.d[pu].lowlink: - gCap.recs.d[pu].lowlink = gCap.recs.d[u].lowlink - if gCap.recs.d[u].lowlink == u: + 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: # u is the root of an SCC: pop the members off the Tarjan stack - gCap.sccMemStart.add int32(gCap.sccMembers.len) + cap.sccMemStart.add int32(cap.sccMembers.len) var sum = 0 while true: - let w = gCap.tstack.pop() - gCap.recs.d[w].sccOf = int32(j.nScc) - gCap.sccMembers.add w - sum = sum +% (gCap.recs.d[w].rcWord shr rcShift) +% 1 + 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 - gCap.sumRefs.add sum + cap.sumRefs.add sum inc j.nScc # ---------------- phase 2: deadness, side arrays only ---------------- -proc computeDeadness(j: var GcEnv) = +proc computeDeadness(j: var GcEnv; cap: ptr CaptureBufs) = let nScc = j.nScc - setLenZeroed gCap.internal, nScc - setLenZeroed gCap.deadIn, nScc - setLenZeroed gCap.sccFlags, nScc - setLenZeroed gCap.crossOff, nScc + 1 - setLenUninit gCap.crossCursor, nScc + setLenZeroed cap.internal, nScc + setLenZeroed cap.deadIn, nScc + setLenZeroed cap.sccFlags, nScc + setLenZeroed cap.crossOff, nScc + 1 + setLenUninit cap.crossCursor, nScc # classify captured edges: internal to an SCC vs condensation cross edges var nCross = 0 - for i in 0 ..< gCap.edges.len: - let e = gCap.edges.d[i] - let su = gCap.recs.d[int32(e shr 32)].sccOf - let sv = gCap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf + 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 gCap.internal.d[su] + inc cap.internal.d[su] else: - inc gCap.crossOff.d[su] + inc cap.crossOff.d[su] inc nCross var total = 0'i32 for s in 0 ..< nScc: - let c = gCap.crossOff.d[s] - gCap.crossOff.d[s] = total - gCap.crossCursor.d[s] = total + let c = cap.crossOff.d[s] + cap.crossOff.d[s] = total + cap.crossCursor.d[s] = total total = total +% c - gCap.crossOff.d[nScc] = total - setLenUninit gCap.crossTgt, nCross - for i in 0 ..< gCap.edges.len: - let e = gCap.edges.d[i] - let su = gCap.recs.d[int32(e shr 32)].sccOf - let sv = gCap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf + cap.crossOff.d[nScc] = 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: - gCap.crossTgt.d[gCap.crossCursor.d[su]] = sv - inc gCap.crossCursor.d[su] + cap.crossTgt.d[cap.crossCursor.d[su]] = sv + inc cap.crossCursor.d[su] # cells that stay registered as roots (partial collection) count as # externally referenced: the roots buffer itself points at them - for mi in 0 ..< gCap.sccMembers.len: - let m = gCap.sccMembers.d[mi] - if (loadRc(gCap.recs.d[m].cell) and inRootsFlag) != 0: - let s = gCap.recs.d[m].sccOf - gCap.sccFlags.d[s] = gCap.sccFlags.d[s] or flagForcedLive + 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 + cap.sccFlags.d[s] = cap.sccFlags.d[s] 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 # one: one reverse scan settles everything. for s in countdown(nScc - 1, 0): - let ext = gCap.sumRefs.d[s] -% gCap.internal.d[s] -% gCap.deadIn.d[s] + let ext = cap.sumRefs.d[s] -% cap.internal.d[s] -% cap.deadIn.d[s] when logOrc: cfprintf(cstderr, "[scc %ld] members %ld sumRefs %ld internal %ld deadIn %ld ext %ld forced %ld\n", - s, gCap.sccMemStart.d[s+1] - gCap.sccMemStart.d[s], gCap.sumRefs.d[s], - gCap.internal.d[s], gCap.deadIn.d[s], ext, int(gCap.sccFlags.d[s])) - if (gCap.sccFlags.d[s] and flagForcedLive) == 0 and ext == 0: - gCap.sccFlags.d[s] = gCap.sccFlags.d[s] or flagDead + s, cap.sccMemStart.d[s+1] - cap.sccMemStart.d[s], cap.sumRefs.d[s], + cap.internal.d[s], cap.deadIn.d[s], ext, int(cap.sccFlags.d[s])) + if (cap.sccFlags.d[s] and flagForcedLive) == 0 and ext == 0: + cap.sccFlags.d[s] = cap.sccFlags.d[s] or flagDead inc j.nDeadScc - for k in gCap.crossOff.d[s] ..< gCap.crossOff.d[s+1]: - inc gCap.deadIn.d[gCap.crossTgt.d[k]] + for k in cap.crossOff.d[s] ..< cap.crossOff.d[s+1]: + inc cap.deadIn.d[cap.crossTgt.d[k]] else: # a live SCC keeps everything it points to alive - for k in gCap.crossOff.d[s] ..< gCap.crossOff.d[s+1]: - let t = gCap.crossTgt.d[k] - gCap.sccFlags.d[t] = gCap.sccFlags.d[t] or flagForcedLive + for k in cap.crossOff.d[s] ..< cap.crossOff.d[s+1]: + let t = cap.crossTgt.d[k] + cap.sccFlags.d[t] = cap.sccFlags.d[t] or flagForcedLive # ---------------- phase 3: validate & commit ---------------- -proc markDirtyFromQueues(j: var GcEnv) = +proc markDirtyFromQueues(j: var GcEnv; cap: ptr CaptureBufs) = ## The SATB half of the design: any cell with an inc or dec enqueued since - ## mergePendingRoots had its reference set changed during capture. Peek + ## the last drain had its reference set changed during capture. Peek ## (don't drain!) the stripe queues and taint the affected SCCs; the ## entries stay queued and the next merge re-registers them as candidates. template taint(cp: Cell) = let c = cp if isStamped(c): - let s = gCap.recs.d[denseIdx(c)].sccOf - gCap.sccFlags.d[s] = gCap.sccFlags.d[s] or flagDirty + let s = cap.recs.d[denseIdx(c)].sccOf + cap.sccFlags.d[s] = cap.sccFlags.d[s] or flagDirty for i in 0.. 0: - let (entry, _) = j.traceStack.pop() - entry.slot[] = nil - else: + isStamped(t) and (cap.sccFlags.d[cap.recs.d[denseIdx(t)].sccOf] and flagDead) != 0 + template graceWait() = + # Grace period: another collection still in its CAPTURE phase may hold + # stale (slot, value) snapshots referencing our dead cells; disposing + # them now could hand reused memory to its traversal. Captures are + # bounded and never wait on us. New captures cannot reach our dead + # cells: they are unreachable, and our tag stays active until after + # the frees. + when sizeof(int) == 8: + for s in 0 ..< ParSlots: + if s != gMySlot: + let tg = atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) + if tg != 0: + parkUntil(atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) != tg or + atomicLoadN(addr gSlotPhase[s], ATOMIC_ACQUIRE) != 1) + # A dead cell's reference to another active collection's cell must still + # be decremented (the target survives this round), so the all-dead fast + # path additionally requires that no cross-collection edge was seen. + let allDead = j.nDeadScc == j.nScc and j.nAborted == 0 and cap.crossPend.len == 0 + if allDead: + # Everything captured dies and no slot can point outside the dead set: + # nil the slots and free in ONE pass over the cells — they went cold + # since capture, a second sweep would miss cache all over again. + # Freeing cell A before nil-ing a later cell B's slot that points at A + # is fine: nobody reads B's slots in between (mutators cannot reach the + # closed dead set, foreign captures never traverse our tagged cells, + # and the grace wait has retired stale snapshots before the first free). + graceWait() + for m in 0 ..< cap.recs.len: + let cell = cap.recs.d[m].cell + let desc = cap.recs.d[m].desc + orcAssert(j.traceStack.len == 0, "commitDead: trace stack not empty") + trace(cell, desc, j) + while j.traceStack.len > 0: + let (entry, _) = j.traceStack.pop() + entry.slot[] = nil + when sizeof(int) != 8: + cell.rootIdx = 0 # no epoch in the stamp: clear before the free + when orcLeakDetector: + writeCell("CYCLIC OBJECT FREED", cell, desc) + free(cell, desc) + j.freed = cap.recs.len + else: + init j.toFree + for s in 0 ..< j.nScc: + if (cap.sccFlags.d[s] and flagDead) != 0: + for mi in cap.sccMemStart.d[s] ..< cap.sccMemStart.d[s+1]: + let m = cap.sccMembers.d[mi] + let cell = cap.recs.d[m].cell + let desc = cap.recs.d[m].desc + j.toFree.add(cell, desc) + # nil every slot so the destructor cannot dec these edges again; + # references to survivors are decremented for real, references into + # the dead group die with the group (already accounted by deadIn). + # The dead cells must all outlive this pass: deadCell reads the + # TARGET's header, so no fusing with the free loop here. + orcAssert(j.traceStack.len == 0, "commitDead: trace stack not empty") + trace(cell, desc, j) while j.traceStack.len > 0: let (entry, _) = j.traceStack.pop() let t = head(entry.val) entry.slot[] = nil if not deadCell(t): trialDec(t) - when sizeof(int) != 8: - # no epoch in the stamp: clear them while all cells are still alive - for i in 0 ..< gCap.recs.len: - gCap.recs.d[i].cell.rootIdx = 0 - 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.freed = j.toFree.len - deinit j.toFree + when sizeof(int) != 8: + # no epoch in the stamp: clear them while all cells are still alive + for i in 0 ..< cap.recs.len: + cap.recs.d[i].cell.rootIdx = 0 + 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]) + j.freed = j.toFree.len + deinit j.toFree -proc collectCyclesImpl(j: var GcEnv; lowMark: int) = +proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; + wait: bool; drainAll = false): bool = + ## Drain pending RC operations (own stripe; all stripes for a full + ## 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, + ## so the caller's overflowing queue has room again. + result = false + if drainAll: drainAllStripes() + else: drainStripe(getStripeIdx()) + adoptOrphans() + while gLocalRoots.len >= minRoots and gLocalRoots.len > keepBelow and + mayRunCycleCollect(): + acquire gMergeLock + var slot = -1 + for sl in 0 ..< ParSlots: + if atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) == 0: + slot = sl + break + 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 + parkUntil(anySlotFree()) + drainStripe(getStripeIdx()) # the world moved while we waited + adoptOrphans() + else: + gTagCounter = (gTagCounter +% 1) and 0x7FFFFFFF + if gTagCounter == 0: gTagCounter = 1 + gMyTag = gTagCounter + gMySlot = slot + var othersActive = false + for sl in 0 ..< ParSlots: + if sl != slot and atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) != 0: + othersActive = true + gAmSolo = not othersActive + if gAmSolo: + atomicStoreN(addr gSoloCapture, 1, ATOMIC_RELEASE) + atomicStoreN(addr gSlotPhase[slot], 1, ATOMIC_RELEASE) + atomicStoreN(addr gActiveTags[slot], gMyTag, ATOMIC_SEQ_CST) + release gMergeLock + # our buffer, our slice: no lock needed + if keepBelow == 0: + slice = gLocalRoots # steal the whole buffer + init(gLocalRoots) + else: + init(slice, max(gLocalRoots.len - keepBelow, 8)) + for i in keepBelow ..< gLocalRoots.len: + slice.add(gLocalRoots.d[i][0], gLocalRoots.d[i][1]) + gLocalRoots.len = keepBelow + result = true + break + +proc finishCollection() = + 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 + +proc collectCyclesImpl(j: var GcEnv; slice: var CellSeq[Cell]) = # All destruction is deferred to collection time: plain rc==0 garbage in # the roots buffer forms singleton SCCs with external count 0 and is freed # by the same machinery as the cycles. - if lockState == Collecting: - return - lockState = Collecting - let last = roots.len -% 1 + let last = slice.len -% 1 when logOrc: - for i in countdown(last, lowMark): - writeCell("root", roots.d[i][0], roots.d[i][1]) + for i in countdown(last, 0): + writeCell("root", slice.d[i][0], slice.d[i][1]) - bumpEpoch() init j.traceStack prepareCapture() + let cap = addr gCap # hoist the TLS lookup out of the hot loops j.nScc = 0 - for i in countdown(last, lowMark): - capture(roots.d[i][0], roots.d[i][1], j) - gCap.sccMemStart.add int32(gCap.sccMembers.len) # sentinel - j.touched = gCap.recs.len + for i in countdown(last, 0): + capture(slice.d[i][0], slice.d[i][1], j, cap) + cap.sccMemStart.add int32(cap.sccMembers.len) # sentinel + j.touched = cap.recs.len + atomicStoreN(addr gSlotPhase[gMySlot], 2, ATOMIC_RELEASE) # capture done + if gAmSolo: + atomicStoreN(addr gSoloCapture, 0, ATOMIC_RELEASE) + collectorEvent() # wake solo-gate and grace waiters - # Unregister the processed roots before computing deadness: only cells that - # STAY registered (below lowMark, partial collection) count as externally - # referenced by the roots buffer. Doing this before freeing anything also - # ensures a nested collectCycles() (triggered from a destructor) cannot - # access freed cells. - for i in lowMark ..< roots.len: - rcClearFlag(roots.d[i][0], inRootsFlag) - roots.len = lowMark + # Unregister the processed candidates before computing deadness: only + # cells that STAY registered count as externally referenced by the roots + # buffer. Doing this before freeing anything also ensures a nested + # collectCycles() (triggered from a destructor) cannot access freed cells. + for i in 0 ..< slice.len: + rcClearFlag(slice.d[i][0], inRootsFlag) - computeDeadness(j) - commitDead(j) + computeDeadness(j, cap) + commitDead(j, cap) j.keepThreshold = j.freed == j.touched and j.touched > 0 deinit j.traceStack +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. + yrcGcFenceEnter() # freeze seq structure mutations, not ref writes + if not gAmSolo: + # a solo collection claims with plain stores; nobody else may claim + # cells until its capture phase is over + parkUntil(atomicLoadN(addr gSoloCapture, ATOMIC_ACQUIRE) == 0) + let prev = lockState + lockState = Collecting + collectCyclesImpl(j, slice) + lockState = prev + yrcGcFenceExit() + finishCollection() + deinit slice + when defined(nimOrcStats): var freedCyclicObjects {.threadvar.}: int proc collectCycles() = when logOrc: cfprintf(cstderr, "[collectCycles] begin\n") - yrcCollectorLock: - mergePendingRoots() - if roots.len >= rootsThreshold and mayRunCycleCollect(): - let nRoots = roots.len - var j: GcEnv - collectCyclesImpl(j, 0) - if roots.len == 0 and roots.d != nil: - deinit roots + if lockState == Collecting: return + if lockState == HasMutatorLock: + # We are inside a seq critical section (element destructors running + # under yrcMutatorLock, e.g. shrink or a seq's =destroy): becoming a + # collector here would fence-wait on our own gSeqActive counter — + # self-deadlock. Just make room in the overflowing queue; the next + # dec outside the critical section triggers the actual collection. + # (The pre-fence design instead released the mutator lock here.) + drainStripe(getStripeIdx()) + return + var slice: CellSeq[Cell] + if startCollection(rootsThreshold, 0, slice, wait = true): + let nRoots = slice.len + var j: GcEnv + runCollection(j, slice) + block: when not defined(nimStressOrc): if j.keepThreshold: discard @@ -777,12 +1063,14 @@ when defined(nimOrcStats): result = OrcStats(freedCyclicObjects: freedCyclicObjects) proc GC_runOrc* = - yrcCollectorLock: - mergePendingRoots() - if roots.len > 0 and mayRunCycleCollect(): - var j: GcEnv - collectCyclesImpl(j, 0) - # note: aborted SCCs legitimately leave re-registered roots behind + if lockState == Collecting: return + var slice: CellSeq[Cell] + if startCollection(1, 0, slice, wait = true, drainAll = true): + var j: GcEnv + runCollection(j, slice) + # 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) proc GC_enableOrc*() = when not defined(nimStressOrc): @@ -793,20 +1081,37 @@ proc GC_disableOrc*() = rootsThreshold = high(int) proc GC_prepareOrc*(): int {.inline.} = - yrcCollectorLock: - mergePendingRoots() - result = roots.len + drainAllStripes() + adoptOrphans() + result = gLocalRoots.len proc GC_partialCollect*(limit: int) = - yrcCollectorLock: - mergePendingRoots() - if roots.len > limit and mayRunCycleCollect(): - var j: GcEnv - collectCyclesImpl(j, limit) + if lockState == Collecting: return + var slice: CellSeq[Cell] + if startCollection(limit + 1, limit, slice, wait = true): + var j: GcEnv + runCollection(j, slice) proc GC_fullCollect* = GC_runOrc() +proc nimYrcThreadTeardown() = + ## Called when a thread exits (threadimpl): drain our stripe so nothing + ## 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. + drainStripe(getStripeIdx()) + if gLocalRoots.len > 0: + acquire gMergeLock + if roots.d == nil: init(roots) + for i in 0 ..< gLocalRoots.len: + add(roots, gLocalRoots.d[i][0], gLocalRoots.d[i][1]) + release gMergeLock + if gLocalRoots.d != nil: + deinit(gLocalRoots) + gLocalRoots.d = nil + gLocalRoots.len = 0 + proc GC_enableMarkAndSweep*() = GC_enableOrc() proc GC_disableMarkAndSweep*() = GC_disableOrc() @@ -899,9 +1204,9 @@ proc nimMarkCyclic(p: pointer) {.compilerRtl, inl.} = h.rc = h.rc or maybeCycle # Initialize locks at module load. -# RwLock stripes live in seqs_v2 (gYrcLocks); NumLockStripes is exported from there. -for i in 0.. exact hr | step _ _ _ hedge ih => exact Reachable.step _ _ ih hedge -/-! ### What the collector frees -/ - -/-- An object has an *external reference* if some thread's stack roots point to it. -/ +/-- An object has an *external reference* if some thread points to it. -/ def hasExternalRef (s : State) (x : Obj) : Prop := ∃ t, s.roots t x -/-- An object is *externally anchored* if it is heap-reachable from some - object that has an external reference. This is what scanBlack computes: - it starts from objects with trialRC ≥ 0 (= has external refs) and traces - the current physical graph. -/ +/-- Externally anchored: heap-reachable from an externally referenced + object. This is what deadness computation + survivor rescue computes. -/ def anchored (s : State) (x : Obj) : Prop := ∃ r, hasExternalRef s r ∧ HeapReachable s r x -/-- The collector frees `x` only if `x` is *not anchored*: - no external ref, and not reachable from any externally-referenced object. - This models: after trial deletion, x remained white, and scanBlack - didn't rescue it. -/ +/-- The collector frees `x` only if `x` is not anchored. -/ def collectorFrees (s : State) (x : Obj) : Prop := ¬ anchored s x -/-! ### Main safety theorem -/ - -/-- **Lemma**: Every reachable object is anchored. - If thread `t` reaches `x`, then there is a chain from a stack root - (which has an external ref) through heap edges to `x`. -/ +/-- Every reachable object is anchored. -/ theorem reachable_is_anchored (s : State) (x : Obj) (h : Reachable s x) : anchored s x := by induction h with | root t x hroot => exact ⟨x, ⟨t, hroot⟩, HeapReachable.refl x⟩ - | step a b h_reach_a h_edge ih => + | step a b _ h_edge ih => obtain ⟨r, h_ext_r, h_path_r_a⟩ := ih exact ⟨r, h_ext_r, HeapReachable.step r a b h_path_r_a h_edge⟩ -/-- **Main Safety Theorem**: If the collector frees `x`, then no thread - can reach `x`. Freed objects are unreachable. - - This is the contrapositive of `reachable_is_anchored`. -/ +/-- **Core Safety Theorem**: freed objects are unreachable. -/ theorem yrc_safety (s : State) (x : Obj) (h_freed : collectorFrees s x) : ¬ Reachable s x := by intro h_reach exact h_freed (reachable_is_anchored s x h_reach) -/-! ### The write barrier preserves reachability -/ +/-! ## §2 The write barrier -/-- Model of `nimAsgnYrc(dest_field_of_a, src)`: - Object `a` had a field pointing to `old`, now points to `src`. - Graph update is immediate. The new edge takes priority (handles src = old). -/ + `nimAsgnYrc` performs the atomic inc of `src` BEFORE the exchange, so + there is no instant at which the edge `a → src` exists without src's rc + accounting for it; and the exchange reads `old` atomically, so two + racing barriers on the same slot can never both dec the same old value. + The dec of `old` is deferred: until the next merge, old's rc is merely + inflated — always conservative. -/ + +/-- Model of `nimAsgnYrc(field a, src)`: `a`'s field pointed to `old`, + now points to `src`. The graph update is immediate (atomicExchange). -/ def writeBarrier (s : State) (a old src : Obj) : State := { s with edges := fun x y => if x = a ∧ y = src then True else if x = a ∧ y = old then False - else s.edges x y - pendingInc := fun x => if x = src then s.pendingInc x + 1 else s.pendingInc x - pendingDec := fun x => if x = old then s.pendingDec x + 1 else s.pendingDec x } + else s.edges x y } -/-- **No Lost Object Theorem**: If thread `t` holds a stack ref to `a` and - executes `a.field = b` (replacing old), then `b` is reachable afterward. +/-- Overwriting a slot with nil: only removes an edge. -/ +def storeNil (s : State) (a old : Obj) : State := + { s with + edges := fun x y => + if x = a ∧ y = old then False else s.edges x y } - This is why the "lost object" problem from concurrent GC literature - doesn't arise in YRC: the atomic store makes `a→b` visible immediately, - and `a` is anchored (thread `t` holds it), so scanBlack traces `a→b` - and rescues `b`. -/ +/-- **No Lost Object**: if thread `t` holds `a` and stores `a.f = b`, + then `b` is reachable afterwards — the exchange publishes the edge + atomically, so a concurrent collection's survivor rescue traces it. -/ theorem no_lost_object (s : State) (t : Thread) (a old b : Obj) (h_root_a : s.roots t a) : Reachable (writeBarrier s a old b) b := by @@ -129,225 +148,574 @@ theorem no_lost_object (s : State) (t : Thread) (a old b : Obj) · exact Reachable.root t a h_root_a · simp [writeBarrier] -/-! ### Non-atomic write barrier window safety +/-! ## §3 Mutator semantics and garbage stability - The write barrier does three steps non-atomically: - 1. atomicStore(dest, src) — graph update - 2. buffer inc(src) — deferred - 3. buffer dec(old) — deferred + The heart of optimistic capture/validate/commit is the *garbage + stability theorem*: a set with no external references cannot acquire + one later, because mutators can only copy references they can reach. + Hence a dead set that VALIDATES at commit time stays dead through the + grace window and until the actual `free` calls — no re-validation is + needed, and an aborted (dirty) capture merely wasted its own work. - If the collector runs between steps 1 and 2 (inc not yet buffered): - - src has a new incoming heap edge not yet reflected in RCs - - But src is reachable from the mutator's stack (mutator held a ref to store it) - - So src has an external ref → trialRC ≥ 1 → scanBlack rescues src ✓ + Every constructor's precondition encodes the fundamental capability + restriction: to use a reference you must hold it. `P` is the set of + cells protected from foreign frees (in yrc: cells stamped with an + active tag are never freed by another collection — §5). -/ - If the collector runs between steps 2 and 3 (dec not yet buffered): - - old's RC is inflated by 1 (the dec hasn't arrived) - - This is conservative: old appears to have more refs than it does - - Trial deletion won't spuriously free it ✓ --/ +def addRoot (s : State) (t : Thread) (x : Obj) : State := + { s with roots := fun t' y => (t' = t ∧ y = x) ∨ s.roots t' y } -/-- Model the state between steps 1-2: graph updated, inc not yet buffered. - `src` has new edge but RC doesn't reflect it yet. -/ -def stateAfterStore (s : State) (a old src : Obj) : State := +def delRoot (s : State) (t : Thread) (x : Obj) : State := + { s with roots := fun t' y => if t' = t ∧ y = x then False else s.roots t' y } + +def allocObj (s : State) (t : Thread) (x : Obj) : State := { s with - edges := fun x y => - if x = a ∧ y = src then True - else if x = a ∧ y = old then False - else s.edges x y } + roots := fun t' y => (t' = t ∧ y = x) ∨ s.roots t' y + allocated := fun y => y = x ∨ s.allocated y } -/-- Even in the window between atomic store and buffered inc, - src is still reachable (from the mutator's stack via a→src). -/ -theorem src_reachable_in_window (s : State) (t : Thread) (a old src : Obj) - (h_root_a : s.roots t a) : - Reachable (stateAfterStore s a old src) src := by - apply Reachable.step a src - · exact Reachable.root t a h_root_a - · simp [stateAfterStore] +def freeObj (s : State) (x : Obj) : State := + { s with + edges := fun u v => if u = x ∨ v = x then False else s.edges u v + allocated := fun y => if y = x then False else s.allocated y } -/-- Therefore src is anchored in the window → collector won't free it. -/ -theorem src_safe_in_window (s : State) (t : Thread) (a old src : Obj) - (h_root_a : s.roots t a) : - ¬ collectorFrees (stateAfterStore s a old src) src := by - intro h_freed - exact h_freed (reachable_is_anchored _ _ (src_reachable_in_window s t a old src h_root_a)) +/-- One step of the concurrent system, as seen by a fixed observer + protecting the cell set `P`. -/ +inductive MutStep (P : Obj → Prop) (s : State) : State → Prop where + /-- `a.f = src`: the mutator must hold refs to `a` and `src`. -/ + | write (a old src : Obj) + (ha : Reachable s a) (hsrc : Reachable s src) : + MutStep P s (writeBarrier s a old src) + /-- `a.f = nil`. -/ + | writeNil (a old : Obj) (ha : Reachable s a) : + MutStep P s (storeNil s a old) + /-- Copy a reachable ref into a local / the roots buffer. -/ + | rootCopy (t : Thread) (x : Obj) (hx : Reachable s x) : + MutStep P s (addRoot s t x) + /-- Drop a local ref (scope exit, roots-buffer unregistration). -/ + | rootDrop (t : Thread) (x : Obj) : + MutStep P s (delRoot s t x) + /-- Allocate: the allocator returns only unallocated addresses. -/ + | alloc (t : Thread) (x : Obj) (hfresh : ¬ s.allocated x) : + MutStep P s (allocObj s t x) + /-- A DIFFERENT collection frees one of its own dead cells: it is + unreachable (its own §1 safety) and not protected (§5 partition + disjointness: it carries the other collection's tag, not ours). -/ + | foreignFree (x : Obj) (hunreach : ¬ Reachable s x) (hprot : ¬ P x) : + MutStep P s (freeObj s x) -/-! ### Deadlock freedom +/-- Reflexive-transitive closure: an arbitrary interleaving of steps by + all mutators and all other collections. -/ +inductive MutSteps (P : Obj → Prop) (s : State) : State → Prop where + | refl : MutSteps P s s + | tail {s' s'' : State} : + MutSteps P s s' → MutStep P s' s'' → MutSteps P s s'' - YRC uses three classes of locks: - • gYrcGlobalLock (level 0) - • stripes[i].lockInc (level 2*i + 1, for i in 0..N-1) - • stripes[i].lockDec (level 2*i + 2, for i in 0..N-1) +/-- `S` is *closed*: no thread points into it and no heap edge enters it + from outside. This is exactly "validated dead set" (§4). -/ +def closed (s : State) (S : Obj → Prop) : Prop := + (∀ t x, S x → ¬ s.roots t x) ∧ + (∀ u v, S v → s.edges u v → S u) - Total order: global < lockInc[0] < lockDec[0] < lockInc[1] < lockDec[1] < ... +/-- Members of a closed set are unreachable. -/ +theorem closed_unreachable (s : State) (S : Obj → Prop) + (h : closed s S) : ∀ x, Reachable s x → ¬ S x := by + intro x hr + induction hr with + | root t x hroot => exact fun hS => h.1 t x hS hroot + | step a b _ hedge ih => exact fun hS => ih (h.2 a b hS hedge) - Every code path in yrc.nim acquires locks in strictly ascending level order: +/-- The invariant carried through the grace window: `S` closed and all + members still allocated (their memory has not been reused). -/ +def DeadInv (s : State) (S : Obj → Prop) : Prop := + closed s S ∧ ∀ x, S x → s.allocated x - **nimIncRefCyclic** (mutator fast path): - acquire lockInc[myStripe] → release → done. - Holds exactly one lock. ✓ +/-- **One-step stability**: no single action of any mutator, allocator or + other collection can break the invariant of a closed set. -/ +theorem step_preserves_deadInv (s s' : State) (S : Obj → Prop) + (hinv : DeadInv s S) (hstep : MutStep S s s') : DeadInv s' S := by + obtain ⟨hcl, halloc⟩ := hinv + cases hstep with + | write a old src ha hsrc => + refine ⟨⟨fun t x hS hroot => hcl.1 t x hS hroot, ?_⟩, fun x hS => halloc x hS⟩ + intro u v hSv hedge + simp only [writeBarrier] at hedge + by_cases h1 : u = a ∧ v = src + · exact absurd (h1.2 ▸ hSv) (closed_unreachable s S hcl src hsrc) + · by_cases h2 : u = a ∧ v = old + · -- corner case old = src: the "remove old" branch is overridden + -- by the "add src" branch, so the edge survives — but then + -- v = old = src is reachable, hence not in S + simp [h2] at hedge + have hSsrc : S src := by rw [← hedge, ← h2.2]; exact hSv + exact absurd hSsrc (closed_unreachable s S hcl src hsrc) + · simp [h1, h2] at hedge + exact hcl.2 u v hSv hedge + | writeNil a old ha => + refine ⟨⟨fun t x hS hroot => hcl.1 t x hS hroot, ?_⟩, fun x hS => halloc x hS⟩ + intro u v hSv hedge + simp only [storeNil] at hedge + by_cases h2 : u = a ∧ v = old + · simp [h2] at hedge + · simp [h2] at hedge + exact hcl.2 u v hSv hedge + | rootCopy t x hx => + refine ⟨⟨?_, fun u v hSv hedge => hcl.2 u v hSv hedge⟩, fun y hS => halloc y hS⟩ + intro t' y hSy hroot + simp only [addRoot] at hroot + cases hroot with + | inl h => exact absurd (h.2 ▸ hSy) (closed_unreachable s S hcl x hx) + | inr h => exact hcl.1 t' y hSy h + | rootDrop t x => + refine ⟨⟨?_, fun u v hSv hedge => hcl.2 u v hSv hedge⟩, fun y hS => halloc y hS⟩ + intro t' y hSy hroot + simp only [delRoot] at hroot + by_cases h : t' = t ∧ y = x + · simp [h] at hroot + · simp [h] at hroot + exact hcl.1 t' y hSy hroot + | alloc t x hfresh => + refine ⟨⟨?_, fun u v hSv hedge => hcl.2 u v hSv hedge⟩, ?_⟩ + · intro t' y hSy hroot + simp only [allocObj] at hroot + cases hroot with + | inl h => exact hfresh (h.2 ▸ halloc y hSy) + | inr h => exact hcl.1 t' y hSy h + · intro y hS + simp only [allocObj] + exact Or.inr (halloc y hS) + | foreignFree x hunreach hprot => + refine ⟨⟨fun t y hSy hroot => hcl.1 t y hSy hroot, ?_⟩, ?_⟩ + · intro u v hSv hedge + simp only [freeObj] at hedge + by_cases h : u = x ∨ v = x + · simp [h] at hedge + · simp [h] at hedge + exact hcl.2 u v hSv hedge + · intro y hSy + simp only [freeObj] + have hyx : ¬ y = x := fun he => hprot (he ▸ hSy) + simp [hyx] + exact halloc y hSy - **nimIncRefCyclic** (overflow path): - acquire gYrcGlobalLock (level 0), then for i=0..N-1: acquire lockInc[i] → release. - Ascending: 0 < 1 < 3 < 5 < ... ✓ +/-- **Garbage Stability Theorem**: once a set is closed, it stays closed + (and unreusable) under any interleaving of concurrent activity. -/ +theorem deadInv_stable (s s' : State) (S : Obj → Prop) + (hinv : DeadInv s S) (hsteps : MutSteps S s s') : DeadInv s' S := by + induction hsteps with + | refl => exact hinv + | tail _ hstep ih => exact step_preserves_deadInv _ _ S ih hstep - **nimDecRefIsLastCyclic{Dyn,Static}** (fast path): - acquire lockDec[myStripe] → release → done. - Holds exactly one lock. ✓ +/-- Snapshot garbage cannot be resurrected: members of a set that was + closed at commit time are unreachable at every later point. -/ +theorem garbage_stability (s s' : State) (S : Obj → Prop) + (hinv : DeadInv s S) (hsteps : MutSteps S s s') : + ∀ x, S x → ¬ Reachable s' x := by + intro x hS hr + exact closed_unreachable s' S (deadInv_stable s s' S hinv hsteps).1 x hr hS - **nimDecRefIsLastCyclic{Dyn,Static}** (overflow path): - calls collectCycles → acquire gYrcGlobalLock (level 0), - then mergePendingRoots which for i=0..N-1: - acquire lockInc[i] → release, acquire lockDec[i] → release. - Ascending: 0 < 1 < 2 < 3 < 4 < ... ✓ +/-- **Commit-then-free safety**: if the dead set validated (was closed) + at commit time, then freeing its members after ANY amount of further + concurrent activity (the grace window, other collections' frees, + destructor-driven mutations) satisfies the §1 free condition. -/ +theorem commit_free_safe (s s' : State) (S : Obj → Prop) + (hinv : DeadInv s S) (hsteps : MutSteps S s s') : + ∀ x, S x → collectorFrees s' x := by + intro x hS hanch + obtain ⟨r, ⟨t, hroot⟩, hpath⟩ := hanch + have hr : Reachable s' x := + heapReachable_of_reachable s' r x (Reachable.root t r hroot) hpath + exact closed_unreachable s' S (deadInv_stable s s' S hinv hsteps).1 x hr hS - **collectCycles / GC_runOrc** (collector): - acquire gYrcGlobalLock (level 0), - then mergePendingRoots (same ascending pattern as above). ✓ +/-! ## §4 Commit validation arithmetic - **nimAsgnYrc / nimSinkYrc** (write barrier): - Calls nimIncRefCyclic then nimDecRefIsLastCyclic*. - Each call acquires and releases its lock independently. - No nesting between the two calls. ✓ + `computeDeadness` marks an SCC dead when + ext(S) = sumRefs(S) − internal(S) − deadIn(S) = 0, + i.e. summed over the whole dead set D (union of dead SCCs): + Σ_{c∈D} rc(c) = #(edges within D). + `validateDead` then establishes that the captured rc words are the + COMMIT-TIME rc values (rc recheck) and that no unmerged queue entry + mentions a member (dirty check via markDirtyFromQueues — the deferred + dec queues double as the SATB log; direct incs are atomic rc mutations + caught by the recheck). Under yrc's invariant "rc counts every + reference: heap slots, stack refs, and the roots-buffer flag" (the + roots-buffer refs are excluded by clearing inRootsFlag on the slice + BEFORE computeDeadness — collectCyclesImpl), we get: every member's rc + splits into internal references (from D) and external ones, and the + totals matching forces every external count to zero. -/ - Since every path follows the total order, deadlock is impossible. --/ +theorem sum_map_split (l : List Obj) (f g h : Obj → Nat) + (hp : ∀ c, c ∈ l → f c = g c + h c) : + (l.map f).sum = (l.map g).sum + (l.map h).sum := by + induction l with + | nil => simp + | cons a l ih => + have ha : f a = g a + h a := hp a (by simp) + have ih' := ih (fun c hc => hp c (List.mem_cons_of_mem a hc)) + simp only [List.map_cons, List.sum_cons] + omega -/-- Lock levels in YRC. Each lock maps to a unique natural number. -/ +theorem sum_zero_all (l : List Nat) (h : l.sum = 0) : + ∀ x, x ∈ l → x = 0 := by + induction l with + | nil => intro x hx; cases hx + | cons a l ih => + simp only [List.sum_cons] at h + intro x hx + cases List.mem_cons.mp hx with + | inl he => subst he; omega + | inr hm => exact ih (by omega) x hm + +/-- **Validation soundness (arithmetic)**: if every member's commit-time + rc splits as internal + external, and the collector's check + Σ rc = Σ internal passed, then no member has any external ref. -/ +theorem validated_no_external + (members : List Obj) (rc inD extIn : Obj → Nat) + (h_exact : ∀ c, c ∈ members → rc c = inD c + extIn c) + (h_check : (members.map rc).sum = (members.map inD).sum) : + ∀ c, c ∈ members → extIn c = 0 := by + have hsplit := sum_map_split members rc inD extIn h_exact + have hzero : (members.map extIn).sum = 0 := by omega + intro c hc + exact sum_zero_all _ hzero (extIn c) (List.mem_map_of_mem hc) + +/-- **Validated implies closed**: bridging the counts to the graph. The + two counting premises say what `extIn` MEANS: any stack/root ref and + any heap edge from a non-member contributes at least one external + count (this is the rc-exactness established by merge + validate). -/ +theorem validated_closed (s : State) (D : Obj → Prop) + (members : List Obj) (extIn : Obj → Nat) + (hmem : ∀ x, D x → x ∈ members) + (h_roots_counted : ∀ t c, D c → s.roots t c → 1 ≤ extIn c) + (h_edges_counted : ∀ u c, D c → ¬ D u → s.edges u c → 1 ≤ extIn c) + (h_zero : ∀ c, c ∈ members → extIn c = 0) : + closed s D := by + constructor + · intro t x hD hroot + have h1 := h_roots_counted t x hD hroot + have h2 := h_zero x (hmem x hD) + omega + · intro u v hD hedge + by_cases hu : D u + · exact hu + · have h1 := h_edges_counted u v hD hu hedge + have h2 := h_zero v (hmem v hD) + omega + +/-! ## §5 Parallel collections: tags, partitions, cross-target liveness -/ + +/-- Tags are issued from a monotonic counter under gMergeLock + (startCollection). Distinct issue times give distinct tags, so a + stale stamp from a finished collection can never be mistaken for a + different active collection's tag. (The implementation wraps the + counter at 2³¹; the model assumes no wrap-around while a tag is + active — an ABA that would need 2³¹ collections to complete during + one collection's lifetime.) -/ +theorem tags_distinct (issue : Nat → Nat) + (hmono : ∀ i j, i < j → issue i < issue j) : + ∀ i j, issue i = issue j → i = j := by + intro i j heq + cases Nat.lt_trichotomy i j with + | inl h => have := hmono i j h; omega + | inr h => + cases h with + | inl h => exact h + | inr h => have := hmono j i h; omega + +/-- Each cell's header stores ONE stamp (claimCell CASes the whole + word), so two active collections with distinct tags claim disjoint + partitions. -/ +theorem partitions_disjoint (stamp : Obj → Nat) (tagA tagB : Nat) + (hne : tagA ≠ tagB) : + ∀ x, stamp x = tagA → stamp x = tagB → False := by + intro x hA hB + exact hne (hA ▸ hB) + +/-- **Cross-target liveness**: a cell claimed by collection B but + referenced from OUTSIDE B's partition is never in B's dead set. + B's internal count for the cell only includes edges from B's dead + members; the foreign edge contributes an external count, and + validation forces external counts to zero — so the cell's SCC fails + the deadness check (equivalently: it is demoted). This is why + claimCell may simply refuse foreign-claimed cells (return -1) and + crossPend defer them: their owner provably keeps them alive this + round, and re-registration makes them candidates for the next. -/ +theorem cross_target_live (D : Obj → Prop) (claimedB : Obj → Prop) + (members : List Obj) (extIn : Obj → Nat) + (s : State) + (hDsub : ∀ x, D x → claimedB x) + (hmem : ∀ x, D x → x ∈ members) + (h_edges_counted : ∀ u c, D c → ¬ D u → s.edges u c → 1 ≤ extIn c) + (h_zero : ∀ c, c ∈ members → extIn c = 0) + (u c : Obj) (hedge : s.edges u c) (hu : ¬ claimedB u) : + ¬ D c := by + intro hDc + have hDu : ¬ D u := fun h => hu (hDsub u h) + have h1 := h_edges_counted u c hDc hDu hedge + have h2 := h_zero c (hmem c hDc) + omega + +/-! ## §6 The grace period + + 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. + + Two obligations: + (a) captures that started BEFORE our commit are waited out — temporal + argument below (`grace_no_use_after_free`); + (b) captures that start AT/AFTER our commit never snapshot a dead + cell in the first place (`post_commit_snap_misses_dead`): they + only read slots of cells they claim; our dead cells carry our + still-active tag, so claimCell refuses them (never traversed), + and no slot OUTSIDE the dead set points into it (closedness, held + through the window by §3 stability). -/ + +/-- Any snapshot value read by a post-commit capture comes from a slot + of a cell that capture claimed; claimed cells are never dead cells + of another active collection (§5), and the dead set is closed. -/ +theorem post_commit_snap_misses_dead (s : State) + (D claimedC snap : Obj → Prop) + (hdisj : ∀ x, claimedC x → ¬ D x) + (hclosed : closed s D) + (hsnap : ∀ v, snap v → ∃ u, claimedC u ∧ s.edges u v) : + ∀ v, D v → ¬ snap v := by + intro v hD hs + obtain ⟨u, hu, he⟩ := hsnap v hs + exact hdisj u hu (hclosed.2 u v hD he) + +/-- One concurrent capture, with its interval in a global time order and + the set of values it ever snapshots. `derefs x t` = the capture + reads x's header at time t (always within its interval, always on a + snapshotted value). -/ +structure CaptureWindow where + start : Nat + finish : Nat + snap : Obj → Prop + derefs : Obj → Nat → Prop + +/-- **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. -/ +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) + (h_grace : C.start < commitT → C.finish < 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_grace h; omega + | inr h => exact absurd h3 (h_miss h x hD) + +/-! ## §7 The asymmetric seq/GC fence (seqs_v2.nim) + + Seq structure mutations (which may FREE the old buffer on realloc) + must not overlap a collection, but seq-vs-seq and collection-vs- + collection may run concurrently. The committed fence: + + mutator (acquireMutatorLock): collector (yrcGcFenceEnter): + 1. FetchAdd gSeqActive[s] SC 1. FetchAdd gGcActive SC + 2. Load gGcActive SC 2. Load gSeqActive[s] SC (each s) + proceed iff it read 0 proceed when all read 0 + (else back off: FetchSub, spin, retry) + + Under sequential consistency all four operations occupy positions in + one total order. Suppose both sides are in their critical sections + simultaneously (neither has executed its matching FetchSub). The + mutator read gGcActive = 0 AFTER its own inc: since the collector's + inc precedes its critical section and no dec intervened, the + collector's inc must be ordered after the mutator's read — and + symmetrically for the collector's read. That yields a cycle in the + total order: -/ + +theorem fence_mutual_exclusion + (mutInc mutChk gcInc gcChk : Nat) -- positions in the SC total order + (h_mut_po : mutInc < mutChk) -- program order, mutator + (h_gc_po : gcInc < gcChk) -- program order, collector + (h_mut_read0 : mutChk < gcInc) -- mutator read gGcActive = 0 + (h_gc_read0 : gcChk < mutInc) : -- collector read counter = 0 + False := by omega + +/-! ## §8 Deadlock freedom + + ### Locks + + The global collector lock is gone. What remains: + • gMergeLock (level 0) + • stripes[i].lockInc (level 2*i + 1, i in 0..N-1) + • stripes[i].lockDec (level 2*i + 2, i in 0..N-1) + • gWaitLock (leaf: pairs gWaitCond's wait/broadcast; + only ever held around a predicate check, + a wait(), or a broadcast() — never while + acquiring any other lock, and no other + lock is held when it is taken) + + Total order: gMergeLock < lockInc[0] < lockDec[0] < lockInc[1] < ... + + Every code path acquires in strictly ascending level order: + + **nimIncRefCyclic** fast path: lockInc[myStripe] alone. Overflow path: + lockInc[i] for i = 0..N-1, one at a time, no gMergeLock. ✓ + **nimDecRefIsLastCyclic*** fast path: lockDec[myStripe] alone; the + overflow calls collectCycles AFTER releasing it (overflow-flag + pattern). ✓ + **startCollection**: gMergeLock, then mergePendingRoots takes + lockInc[i], lockDec[i] ascending, releasing each. ✓ + **markDirtyFromQueues**: stripe locks only, ascending, and gMergeLock + is NOT held (commitDead's gMergeLock sections are disjoint from it). + **validateDead / commitDead / GC_prepareOrc root registration**: + gMergeLock alone, no stripe lock held or taken inside. ✓ + **nimAsgnYrc / nimSinkYrc**: lock-free (atomic inc + exchange); only + the deferred dec takes lockDec[myStripe] on its own. ✓ + + ### Blocking waits (parked on gWaitCond after a bounded spin) + + W1 backpressure (startCollection): waits for a free tag slot — + gMergeLock is RELEASED first; slots free when collections finish + (finishCollection broadcasts). + W2 solo gate (runCollection): a non-solo collection waits for + gSoloCapture = 0 — cleared when the solo collection's CAPTURE + ends (collectCyclesImpl broadcasts), before its commit. + W3 grace (commitDead): waits for other slots to leave capture phase + (broadcast at the phase 1→2 transition and at finish). + W4 fence (yrcGcFenceEnter): spins for in-flight seq ops — each is a + short critical section that never blocks (releaseMutatorLock is + a plain FetchSub). + + W1–W3 park on gWaitCond: the waiter re-checks its predicate under + gWaitLock before sleeping, and every state transition that can make a + predicate true (capture-end, collection-finish) broadcasts under the + same lock — so a transition either happens before the re-check (the + waiter never sleeps) or after it (the waiter is inside wait() and is + woken). No missed wakeups, and the wait-for structure is unchanged. + + No wait cycle exists: order the blocking conditions by what they wait + FOR. A capture phase terminates unconditionally (finite traversal, no + waits inside — claimCell returns -1 immediately on contention). W2 + waits only on a capture; W3 waits only on captures; a collection + executes W2 BEFORE its own capture and W3 AFTER it, so "X waits (W2) + on S's capture" and "S waits (W3) on X's capture" cannot hold + simultaneously: S clears gSoloCapture before entering commit, so by + the time S is in W3, X has passed W2. W1 waits on full collections, + which terminate because W2/W3/W4 do. Formally, the lock part is the + same ascending-order argument as before: -/ + +/-- Lock levels in YRC. -/ inductive LockId (n : Nat) where - | global : LockId n + | mergeLock : LockId n | lockInc (i : Nat) (h : i < n) : LockId n | lockDec (i : Nat) (h : i < n) : LockId n -/-- The level (priority) of each lock in the total order. -/ def lockLevel {n : Nat} : LockId n → Nat - | .global => 0 + | .mergeLock => 0 | .lockInc i _ => 2 * i + 1 | .lockDec i _ => 2 * i + 2 -/-- All lock levels are distinct (the level function is injective). -/ +/-- All lock levels are distinct (the order is total and well-defined). -/ theorem lockLevel_injective {n : Nat} (a b : LockId n) (h : lockLevel a = lockLevel b) : a = b := by cases a with - | global => + | mergeLock => cases b with - | global => rfl + | mergeLock => rfl | lockInc j hj => simp [lockLevel] at h | lockDec j hj => simp [lockLevel] at h | lockInc i hi => cases b with - | global => simp [lockLevel] at h + | mergeLock => simp [lockLevel] at h | lockInc j hj => have : i = j := by simp [lockLevel] at h; omega subst this; rfl | lockDec j hj => simp [lockLevel] at h; omega | lockDec i hi => cases b with - | global => simp [lockLevel] at h + | mergeLock => simp [lockLevel] at h | lockInc j hj => simp [lockLevel] at h; omega | lockDec j hj => have : i = j := by simp [lockLevel] at h; omega subst this; rfl -/-- Helper: stripe lock levels are strictly ascending across stripes. -/ -theorem stripe_levels_ascending (i : Nat) : - 2 * i + 1 < 2 * i + 2 ∧ 2 * i + 2 < 2 * (i + 1) + 1 := by - constructor <;> omega - -/-- lockInc levels are strictly ascending with index. -/ -theorem lockInc_level_strict_mono {n : Nat} (i j : Nat) (hi : i < n) (hj : j < n) - (hij : i < j) : lockLevel (.lockInc i hi : LockId n) < lockLevel (.lockInc j hj) := by - simp [lockLevel]; omega - -/-- lockDec levels are strictly ascending with index. -/ -theorem lockDec_level_strict_mono {n : Nat} (i j : Nat) (hi : i < n) (hj : j < n) - (hij : i < j) : lockLevel (.lockDec i hi : LockId n) < lockLevel (.lockDec j hj) := by - simp [lockLevel]; omega - -/-- Global lock has the lowest level (level 0). -/ -theorem global_level_min {n : Nat} (l : LockId n) (h : l ≠ .global) : - lockLevel (.global : LockId n) < lockLevel l := by +/-- gMergeLock has the lowest level. -/ +theorem mergeLock_level_min {n : Nat} (l : LockId n) (h : l ≠ .mergeLock) : + lockLevel (.mergeLock : LockId n) < lockLevel l := by cases l with - | global => exact absurd rfl h + | mergeLock => exact absurd rfl h | lockInc i hi => simp [lockLevel] | lockDec i hi => simp [lockLevel] -/-- **Deadlock Freedom**: Any sequence of lock acquisitions that follows the - "acquire in ascending level order" discipline cannot deadlock. - - This is a standard result: a total order on locks with the invariant that - every thread acquires locks in strictly ascending order prevents cycles - in the wait-for graph, which is necessary and sufficient for deadlock. - - We prove the 2-thread case (the general N-thread case follows by the - same transitivity argument on the wait-for cycle). -/ +/-- **Deadlock Freedom** (2-thread wait cycle; N-thread follows by the + same transitivity on the wait-for chain): impossible when every + thread acquires locks in strictly ascending level order. -/ theorem no_deadlock_from_total_order {n : Nat} - -- Two threads each hold a lock and wait for another (held₁ waited₁ held₂ waited₂ : LockId n) - -- Thread 1 holds held₁ and wants waited₁ (ascending order) (h1 : lockLevel held₁ < lockLevel waited₁) - -- Thread 2 holds held₂ and wants waited₂ (ascending order) (h2 : lockLevel held₂ < lockLevel waited₂) - -- Deadlock requires: thread 1 waits for what thread 2 holds, - -- and thread 2 waits for what thread 1 holds (h_wait1 : waited₁ = held₂) (h_wait2 : waited₂ = held₁) : False := by subst h_wait1; subst h_wait2 omega -/-! ### Summary of verified properties (all QED, no sorry) +/-! ## Summary of verified properties (all QED, no sorry) - 1. `reachable_is_anchored`: Every reachable object is anchored - (has a path from an externally-referenced object via heap edges). + §1 `yrc_safety` — the collector frees only unanchored objects, which + no thread can reach. No use-after-free at the graph level. + §2 `no_lost_object` — the atomically published edge is traced. + §3 `step_preserves_deadInv`, `deadInv_stable`, `garbage_stability` — + a closed set stays closed under every mutator write, root + copy/drop, allocation, and foreign free: snapshot garbage cannot + be resurrected. `commit_free_safe` — freeing a commit-validated + dead set after ANY further concurrent activity is safe. + §4 `validated_no_external`, `validated_closed` — the Σrc = Σinternal + check plus rc-exactness forces zero external references, i.e. the + dead set is closed at commit time (feeding §3). + §5 `tags_distinct`, `partitions_disjoint`, `cross_target_live` — + concurrent collections own disjoint partitions, and a cell + 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. + §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`, + `no_deadlock_from_total_order` — the remaining locks form a total + order acquired ascending; spin-waits form an acyclic wait-for + structure (prose above). - 2. `yrc_safety`: The collector only frees unanchored objects, - which are unreachable by all threads. **No use-after-free.** + ## What is NOT proved - 3. `no_lost_object`: After `a.field = b`, `b` is reachable - (atomic store makes the edge visible immediately). - - 4. `src_safe_in_window`: Even between the atomic store and - the buffered inc, the collector cannot free src. - - 5. `lockLevel_injective`: All lock levels are distinct (well-defined total order). - - 6. `global_level_min`: The global lock has the lowest level. - - 7. `lockInc_level_strict_mono`, `lockDec_level_strict_mono`: - Stripe locks are strictly ordered by index. - - 8. `no_deadlock_from_total_order`: A 2-thread deadlock cycle is impossible - when both threads acquire locks in ascending level order. - - Together these establish that YRC's write barrier protocol - (atomic store → buffer inc → buffer dec) is safe under concurrent - collection, and the locking discipline prevents deadlock. - - ## What is NOT proved: Completeness (liveness) - - This proof covers **safety** (no use-after-free) and **deadlock-freedom**, - but does NOT prove **completeness** — that all garbage cycles are eventually - collected. - - Completeness depends on the trial deletion algorithm (Bacon 2001) correctly - identifying closed cycles. Specifically it requires proving: - - 1. After `mergePendingRoots`, merged RCs equal logical RCs - (buffered inc/dec exactly compensate graph changes since last merge). - 2. `markGray` subtracts exactly the internal (heap→heap) edge count from - each node's merged RC, yielding `trialRC(x) = externalRefCount(x)`. - 3. `scan` correctly partitions: nodes with `trialRC ≥ 0` are rescued by - `scanBlack`; nodes with `trialRC < 0` remain white. - 4. White nodes form closed subgraphs with zero external refs → garbage. - - These properties follow from the well-known Bacon trial-deletion algorithm - and are assumed here rather than re-proved. The YRC-specific contribution - (buffered RCs, striped queues, concurrent mutators) is what our safety - proof covers — showing that concurrency does not break the preconditions - that trial deletion relies on (physical graph consistency, eventual RC - consistency after merge). + • Tarjan/SCC implementation correctness: that `capture` computes the + actual SCCs and that computeDeadness's per-SCC sums equal the model's + Σrc/Σinternal for the emitted dead set (condensation, sinks-first + order, deadIn accounting). §4 takes the counts as given. + • rc-exactness mechanics: that merge + the dirty check + the rc-word + recheck really imply "commit-time rc = internal + external" (§4's + h_exact). The argument: rc is only mutated by atomic direct incs + (caught by the recheck), merged queue entries (queues drained at + merge; later entries caught by the dirty peek), and the collector's + own inRootsFlag toggles (excluded from the compared word — see the + comment above claimCell). + • The C11 memory model: §7 assumes sequential consistency for the + SEQ_CST operations (sound: SEQ_CST ops do form a total order) and + the acquire/release reasoning elsewhere is informal. + • Liveness/completeness: every dead cycle is EVENTUALLY freed. + Aborted (dirty) SCCs and crossPend targets are re-registered as + candidates, so they are re-examined; termination of that loop under + adversarial mutators is not formalized. Also unproved: termination + bounds for the four spin-waits (prose in §8). + • Tag wrap-around: 2³¹ collections completing during one collection's + lifetime could forge a stale stamp (noted at `tags_distinct`). Reference: D.F. Bacon and V.T. Rajan, "Concurrent Cycle Collection in - Reference Counted Systems", ECOOP 2001. + Reference Counted Systems", ECOOP 2001 — the deadness arithmetic is + the condensation form of their trial deletion; the capture/validate/ + commit structure and the SATB use of the deferred-dec queues are + yrc-specific. -/