mirrors/Nim
1
0
Fork 0
mirror of https://github.com/nim-lang/Nim.git synced 2026-08-02 05:29:01 +00:00
Code Issues Packages Projects Releases Wiki Activity

progress: much better algorithm

Browse Source
This commit is contained in:
Araq
2026-07-19 08:50:03 +02:00
parent 79469141a3
commit 0496b166a4
3 changed files with 1127 additions and 450 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
lib/system/threadimpl.nim
View File

@@ -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

765
lib/system/yrc.nim
View File

@@ -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..<NumStripes:
let len = atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQUIRE)
for j in 0..<min(len, QueueSize):
let x = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
x.rc = x.rc +% rcIncrement
trialInc(h)
for i in 0..<NumStripes:
let len = atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQUIRE)
for j in 0..<min(len, QueueSize):
let x = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
trialInc(x)
else:
let idx = getStripeIdx()
while true:
@@ -377,43 +454,67 @@ proc nimIncRefCyclic(p: pointer; cyclic: bool) {.compilerRtl, inl.} =
else:
overflow = true
if overflow:
yrcCollectorLock:
for i in 0..<NumStripes:
withLock stripes[i].lockInc:
for j in 0..<stripes[i].toIncLen:
let x = stripes[i].toInc[j]
x.rc = x.rc +% rcIncrement
stripes[i].toIncLen = 0
# flush the inc queues directly: incs are atomic, so this is safe
# concurrently with running collections (whose commit-time rc
# validation observes the change)
for i in 0..<NumStripes:
withLock stripes[i].lockInc:
for j in 0..<stripes[i].toIncLen:
trialInc(stripes[i].toInc[j])
stripes[i].toIncLen = 0
else:
break
proc mergePendingRoots() =
# Merge buffered RC operations. Note: Unlike truly concurrent collectors,
# we don't need any color handling on incRef because collection runs
# under the global lock, so no concurrent mutations happen during collection.
proc registerLocal(c: Cell; desc: PNimTypeV2) {.inline.} =
## Register a candidate in THIS thread's buffer. The atomic test-and-set
## keeps the invariant that a cell sits in at most one candidate buffer:
## whoever wins the flag owns the registration. Buffered cells are forced
## live by every collection (deadness checks the flag), so no buffer
## entry can ever dangle.
if rcTestSetFlag(c, inRootsFlag):
if gLocalRoots.d == nil: init(gLocalRoots)
add(gLocalRoots, c, desc)
proc drainStripe(i: int) =
## Apply the pending RC operations of one stripe queue; freshly
## dead-looking cells become THIS thread's candidates. rc mutations are
## atomic, so no global lock is needed: a running collection observes
## them through its commit-time validation (rc recheck / dirty peek).
when not defined(nimYrcAtomicIncs):
# Inc buffers only exist when increfs are buffered (not atomic)
when defined(yrcAtomics):
let incLen = atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQUIRE)
for j in 0..<min(incLen, QueueSize):
let x = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
trialInc(x)
else:
withLock stripes[i].lockInc:
for j in 0..<stripes[i].toIncLen:
trialInc(stripes[i].toInc[j])
stripes[i].toIncLen = 0
withLock stripes[i].lockDec:
for j in 0..<stripes[i].toDecLen:
let (c, desc) = stripes[i].toDec[j]
trialDec(c)
registerLocal(c, desc)
stripes[i].toDecLen = 0
proc drainAllStripes() =
## Full-collect path: apply every pending RC operation; every resulting
## candidate is adopted by the calling thread.
for i in 0..<NumStripes:
when not defined(nimYrcAtomicIncs):
# Inc buffers only exist when increfs are buffered (not atomic)
when defined(yrcAtomics):
let incLen = atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQUIRE)
for j in 0..<min(incLen, QueueSize):
let x = atomicLoadN(addr stripes[i].toInc[j], ATOMIC_ACQUIRE)
x.rc = x.rc +% rcIncrement
else:
withLock stripes[i].lockInc:
for j in 0..<stripes[i].toIncLen:
let x = stripes[i].toInc[j]
x.rc = x.rc +% rcIncrement
stripes[i].toIncLen = 0
withLock stripes[i].lockDec:
for j in 0..<stripes[i].toDecLen:
let (c, desc) = stripes[i].toDec[j]
trialDec(c)
if (loadRc(c) and inRootsFlag) == 0:
rcSetFlag(c, inRootsFlag)
if roots.d == nil: init(roots)
add(roots, c, desc)
stripes[i].toDecLen = 0
drainStripe(i)
proc adoptOrphans() =
## Adopt candidates spilled by exited threads. The cells stay flagged;
## they merely change buffers, so the one-buffer invariant holds.
if roots.len > 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..<NumStripes:
when not defined(nimYrcAtomicIncs):
when defined(yrcAtomics):
@@ -630,124 +779,261 @@ proc markDirtyFromQueues(j: var GcEnv) =
for k in 0..<stripes[i].toDecLen:
taint stripes[i].toDec[k][0]
proc validateDead(j: var GcEnv) =
proc validateDead(j: var GcEnv; cap: ptr CaptureBufs) =
## Demote every dead SCC that a mutator touched during capture: dirty via
## the queues, or a direct incRef visible as a changed rc word. Demoted
## SCCs become ordinary survivors (so committed neighbors decrement into
## them correctly) and one member is re-registered as a candidate root so
## the SCC is re-examined by the next collection.
markDirtyFromQueues(j)
for s in 0 ..< j.nScc:
if (gCap.sccFlags.d[s] and flagDead) != 0:
var ok = (gCap.sccFlags.d[s] and flagDirty) == 0
markDirtyFromQueues(j, cap)
# Descending ids = the deadness scan's order (sources before sinks):
# a demotion must propagate to the SCC's dead cross targets, whose
# deadIn had explained the edges away only under the assumption that
# this SCC dies with them. The demoted SCC survives with its slots
# intact, so any target left dead would be freed under a surviving
# reference. Targets have lower ids, so tainting them here demotes
# them (transitively) later in this very loop.
for s in countdown(j.nScc - 1, 0):
if (cap.sccFlags.d[s] and flagDead) != 0:
var ok = (cap.sccFlags.d[s] and flagDirty) == 0
if ok:
for mi in gCap.sccMemStart.d[s] ..< gCap.sccMemStart.d[s+1]:
let m = gCap.sccMembers.d[mi]
if (loadRc(gCap.recs.d[m].cell) and not rcMask) != gCap.recs.d[m].rcWord:
for mi in cap.sccMemStart.d[s] ..< cap.sccMemStart.d[s+1]:
let m = cap.sccMembers.d[mi]
if (loadRc(cap.recs.d[m].cell) and not rcMask) != cap.recs.d[m].rcWord:
ok = false
break
if not ok:
gCap.sccFlags.d[s] = gCap.sccFlags.d[s] and not flagDead
cap.sccFlags.d[s] = cap.sccFlags.d[s] and not flagDead
inc j.nAborted
let m = gCap.sccMembers.d[gCap.sccMemStart.d[s]]
let cell = gCap.recs.d[m].cell
if (loadRc(cell) and inRootsFlag) == 0:
rcSetFlag(cell, inRootsFlag)
if roots.d == nil: init(roots)
add(roots, cell, gCap.recs.d[m].desc)
for k in cap.crossOff.d[s] ..< cap.crossOff.d[s+1]:
let t = cap.crossTgt.d[k]
if (cap.sccFlags.d[t] and flagDead) != 0:
cap.sccFlags.d[t] = cap.sccFlags.d[t] or flagDirty
let m = cap.sccMembers.d[cap.sccMemStart.d[s]]
registerLocal(cap.recs.d[m].cell, cap.recs.d[m].desc)
proc commitDead(j: var GcEnv) =
init j.toFree
validateDead(j)
proc commitDead(j: var GcEnv; cap: ptr CaptureBufs) =
validateDead(j, cap)
# publish cross-collection edge targets as candidate roots BEFORE any of
# our commit decs could make them collectible: they are owner-live this
# round, and the registration keeps them examinable in a later round
for i in 0 ..< cap.crossPend.len:
registerLocal(cap.crossPend.d[i][0], cap.crossPend.d[i][1])
template deadCell(t: Cell): bool =
isStamped(t) and (gCap.sccFlags.d[gCap.recs.d[denseIdx(t)].sccOf] and flagDead) != 0
let allDead = j.nDeadScc == j.nScc and j.nAborted == 0
for s in 0 ..< j.nScc:
if (gCap.sccFlags.d[s] and flagDead) != 0:
for mi in gCap.sccMemStart.d[s] ..< gCap.sccMemStart.d[s+1]:
let m = gCap.sccMembers.d[mi]
let cell = gCap.recs.d[m].cell
let desc = gCap.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)
orcAssert(j.traceStack.len == 0, "commitDead: trace stack not empty")
trace(cell, desc, j)
if allDead:
# everything captured dies: no survivor can occur, just nil
while j.traceStack.len > 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..<NumLockStripes:
initRwLock(gYrcLocks[i].lock)
initLock(gMergeLock)
initLock(gWaitLock)
initCond(gWaitCond)
for i in 0..<NumStripes:
when not defined(yrcAtomics) and not defined(nimYrcAtomicIncs):
initLock(stripes[i].lockInc)

808
lib/system/yrc_proof.lean
View File

@@ -1,56 +1,83 @@
/-
YRC Safety Proof (self-contained, no Mathlib)
==============================================
Formal model of YRC's key invariant: the cycle collector never frees
an object that any mutator thread can reach.
YRC Safety Proof — lock-free SATB collector with parallel collections
=====================================================================
Self-contained, no Mathlib. Checked with Lean 4 (v4.32.0).
## Model overview
Formal model of the safety arguments behind lib/system/yrc.nim in its
current form: lock-free write barrier, optimistic capture / validate /
commit, and up to `MaxPar` concurrent collections over disjoint
CAS-claimed partitions.
We model the heap as a set of objects with directed edges (ref fields).
Each thread owns a set of *stack roots* — objects reachable from local variables.
The write barrier (nimAsgnYrc) does:
1. atomic store dest ← src (graph is immediately current)
2. buffer inc(src) (deferred)
3. buffer dec(old) (deferred)
## What the implementation does (the things we model)
The collector (under global lock) does:
1. Merge all buffered inc/dec into merged RCs
2. Trial deletion (markGray): subtract internal edges from merged RCs
3. scan: objects with RC ≥ 0 after trial deletion are rescued (scanBlack)
4. Free objects that remain white (closed cycles with zero external refs)
Write barrier `nimAsgnYrc(dest, src)`:
1. direct ATOMIC incRef of src (rc word mutation, visible to all)
2. atomicExchange dest ← src (graph is immediately current;
old value read atomically)
3. buffer dec(old) in a striped queue (deferred — this queue IS the
snapshot-at-the-beginning log)
A collection (any mutator thread can become a collector):
1. merge queues into rc words, steal candidate roots (under gMergeLock)
2. CAPTURE: Tarjan SCC traversal; each visited cell is claimed by
CAS-ing a collection tag into its spare header word (claimCell);
cells claimed by another ACTIVE collection are not traversed
(claimCell → -1, deferred via crossPend)
3. compute deadness per SCC: ext(S) = sumRefs − internal − deadIn
4. VALIDATE at commit: an SCC is freed only if no queue entry mentions
a member (dirty check) and every member's rc word is unchanged
since capture (recheck) — validateDead
5. COMMIT: nil all slots of dead cells, trialDec edges to survivors,
wait out concurrent captures (grace period), then free — commitDead
## Proof structure
§1 Heap model, reachability, the core safety theorem.
§2 Write barrier: no lost objects.
§3 Mutator operational semantics and GARBAGE STABILITY: a closed
(externally unreferenced) set stays closed under every mutator step,
allocation, and foreign frees. This is why optimistic
capture/validate/commit is sound and why aborts cost nothing.
§4 Commit validation arithmetic: validated ext(D) = 0 implies D is
closed; corollary CROSS-TARGET LIVENESS — a cell referenced from
outside a collection's partition is never freed by that collection.
§5 Tag uniqueness and partition disjointness for parallel collections.
§6 Grace period: no capture ever dereferences a freed cell.
§7 The asymmetric seq/GC fence (seqs_v2.nim): Dekker-style mutual
exclusion between seq structure mutations and collections.
§8 Deadlock freedom for the remaining locks (gMergeLock + stripes) and
the spin-wait ordering argument.
-/
-- Objects and threads are just natural numbers for simplicity.
abbrev Obj := Nat
abbrev Thread := Nat
/-! ### State -/
/-! ## §1 Heap model and reachability -/
/-- The state of the heap and collector at a point in time. -/
/-- The state of the heap at a point in time. -/
structure State where
/-- Physical heap edges: `edges x y` means object `x` has a ref field pointing to `y`.
Always up-to-date (atomic stores). -/
/-- Physical heap edges: `edges x y` means object `x` has a ref field
pointing to `y`. Always up-to-date (atomic stores/exchanges). -/
edges : Obj → Obj → Prop
/-- Stack roots per thread. `roots t x` means thread `t` has a local variable pointing to `x`. -/
/-- Stack roots per thread: local variables and the shared candidate
roots buffer (both are "external" to any captured subgraph). -/
roots : Thread → Obj → Prop
/-- Pending buffered increments (not yet merged). -/
pendingInc : Obj → Nat
/-- Pending buffered decrements (not yet merged). -/
pendingDec : Obj → Nat
/-- Live allocations. The allocator hands out only unallocated objects;
captured cells stay allocated until their collection frees them. -/
allocated : Obj → Prop
/-! ### Reachability -/
/-- An object is *reachable* if some thread can reach it via stack roots + heap edges. -/
/-- An object is *reachable* if some thread can reach it via stack roots
plus heap edges. -/
inductive Reachable (s : State) : Obj → Prop where
| root (t : Thread) (x : Obj) : s.roots t x → Reachable s x
| step (x y : Obj) : Reachable s x → s.edges x y → Reachable s y
/-- Directed reachability between heap objects (following physical edges only). -/
/-- Directed reachability following physical heap edges only. -/
inductive HeapReachable (s : State) : Obj → Obj → Prop where
| refl (x : Obj) : HeapReachable s x x
| step (x y z : Obj) : HeapReachable s x y → s.edges y z → HeapReachable s x z
/-- If a root reaches `r` and `r` heap-reaches `x`, then `x` is Reachable. -/
theorem heapReachable_of_reachable (s : State) (r x : Obj)
(hr : Reachable s r) (hp : HeapReachable s r x) :
Reachable s x := by
@@ -58,70 +85,62 @@ theorem heapReachable_of_reachable (s : State) (r x : Obj)
| refl => 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.
-/