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

YRC: optimizations (#26042)

Browse Source
This commit is contained in:
Andreas Rumpf
2026-07-30 14:54:12 +02:00
committed by GitHub
parent c2cef51b62
commit 3126a47590
5 changed files with 1115 additions and 156 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
compiler/liftdestructors.nim
View File

@@ -806,8 +806,22 @@ proc atomicRefOp(c: var TLiftCtx; t: PType; body, x, y: PNode) =
createTypeBoundOps(c.g, c.c, elemType, c.info, c.idgen)
# YRC uses dedicated runtime procs for the entire write barrier:
if c.g.config.selectedGC == gcYrc:
# YRC uses dedicated runtime procs for the entire write barrier -- but ONLY
# for refs that can actually form cycles. Routing an acyclic ref through
# `nimAsgnYrc` defeats the entire purpose of `.acyclic`: the barrier defers
# the dec into a stripe queue, `drainStripe` then hands the cell to
# `registerLocal`, and it enters the collector as a capture ROOT -- so a
# type annotated precisely to stay out of the cycle collector gets traced
# by it anyway. (The collector never reaches such a cell by TRAVERSAL: the
# attachedTrace hook below only emits `nimTraceRef` when `isCyclic`. The
# queued dec was the only way in.)
#
# Falling through instead gives acyclic refs the same prompt arc-style
# reclamation they get under --mm:arc/orc, which is also what lets a thread
# that avoids cycles at compile time avoid the collector entirely at run
# time. `canFormAcycle` is the same predicate ccgtypes.nim:1903 uses to set
# the descriptor's acyclic flag, so codegen and runtime cannot disagree.
if c.g.config.selectedGC == gcYrc and types.canFormAcycle(c.g, elemType):
let desc =
if isFinal(elemType):
let ti = genBuiltin(c, mGetTypeInfoV2, "getTypeInfoV2", newNodeIT(nkType, x.info, elemType))

10
lib/core/locks.nim
View File

@@ -25,7 +25,15 @@ type
## or not is unspecified!
Cond* = SysCond ## Nim condition variable
{.push stackTrace: off.}
# `enforceNoRaises`: these are thin wrappers over the OS primitives and
# cannot raise. Without the flag `canRaiseDisp` falls into its conservative
# branch (they are not in the system module), so the codegen emits an
# `if (*nimErr_) goto BeforeRet_` right after every `acquire` -- which sits
# BETWEEN the acquire and the `try` that `withLock` generates, so the
# `finally` cannot cover it. A caller entered with the error flag already
# set then acquires the lock and jumps straight past the `release`,
# leaking it. See lib/system/yrc.nim's drainStripe.
{.push stackTrace: off, enforceNoRaises.}
proc `$`*(lock: Lock): string =

542
lib/system/yrc.nim
View File

@@ -5,8 +5,10 @@
# See yrc_proof.lean for a machine-checked (Lean 4) proof of the core
# invariants — garbage stability, validation soundness, capture partition
# disjointness, grace periods, fence mutual exclusion, deadlock freedom —
# and yrc_tarjan_proof.lean for soundness AND completeness of the SCC
# deadness algorithm.
# yrc_tarjan_proof.lean for soundness AND completeness of the SCC
# deadness algorithm, and yrc_opt_proof.lean for the three optimizations
# that changed those invariants: SCC-uniform epoch ages, the demand-grown
# `gParSlots` pool, and deferred reclamation (gPendingCells).
#
# ## Synchronization at a Glance
#
@@ -25,7 +27,7 @@
# collection anywhere. A cell sits in at most one buffer, guarded by an
# atomic test-and-set of inRootsFlag; buffered cells are forced live.
#
# Up to MaxPar collections run CONCURRENTLY — with the mutators and with
# Up to one collection PER THREAD runs CONCURRENTLY — with the mutators and with
# each other — each capturing a disjoint partition of the heap by CAS-ing
# a claim tag into the rootIdx header word. gMergeLock covers only the
# tag-slot claim and orphan adoption. All waiting (for a free slot, for a
@@ -255,10 +257,6 @@ proc setLenZeroed[T](s: var RawSeq[T]; n: int) =
s.len = n
zeroMem(s.d, n *% sizeof(T))
proc setLenUninit[T](s: var RawSeq[T]; n: int) =
if s.cap < n: resize(s, n)
s.len = n
type
TraceEntry = object
## (slot, value) snapshot taken at trace time. The value is read exactly
@@ -270,6 +268,7 @@ type
TarjanFrame = object
u: int32 # dense index of the cell this frame belongs to
ebase: int32 # edges.len when this cell's frame was pushed
base: int # traceStack.len before this cell's trace ran
CaptureRec = object
@@ -281,7 +280,7 @@ type
desc: PNimTypeV2
rcWord: int # rc word as captured
lowlink: int32
sccOf: int32 # -1 while the cell is on the Tarjan stack
selfRefs: int32 # self edges, folded out of the edge array
SccRec = object
## per SCC of the condensation; the deadness pass reads all of these
@@ -293,7 +292,6 @@ type
deadIn: int # number of edges from dead SCCs
memStart: int32 # offset into sccMembers
crossOff: int32 # offset into crossTgt (cross edges by source)
crossCursor: int32
flags: uint8
CaptureBufs = object
@@ -301,9 +299,19 @@ type
## threadvar) and persistent across collections, so that frequent
## small collections don't pay per-collection allocations
recs: RawSeq[CaptureRec]
sccIdx: RawSeq[int32] # per captured cell: its SCC, -1 while the cell
# is on the Tarjan stack. Deliberately NOT a
# CaptureRec field: it is read once per captured
# EDGE, and a 4-byte stride keeps that array
# L1-resident where a 32-byte record stride would
# miss on almost every edge.
tstack: RawSeq[int32]
frames: RawSeq[TarjanFrame]
edges: RawSeq[int64] # (u shl 32) or v, dense indices
edges: RawSeq[int32] # PENDING out-edge targets (dense indices) of the
# SCCs still being built. An SCC's edges are
# classified and dropped the moment it is emitted
# (see `capture`), so this stays proportional to
# the DFS frontier, not to the captured graph.
sccs: RawSeq[SccRec]
sccMembers: RawSeq[int32]
crossTgt: RawSeq[int32]
@@ -336,10 +344,11 @@ proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} =
# The spare rootIdx header word (unused by YRC's root registration, which
# relies on inRootsFlag) doubles as the capture claim: it packs the owning
# collection's tag with the cell's dense discovery index. Up to MaxPar
# collections run CONCURRENTLY, each capturing a disjoint partition of the
# heap: the first collection to CAS its tag into a cell owns it; everyone
# else treats the cell as an opaque survivor. Stale tags (from retired
# collection's tag with the cell's dense discovery index. Collections run
# CONCURRENTLY — one slot per collecting thread, see gParSlots — each
# capturing a disjoint partition of the heap: the first collection to CAS
# its tag into a cell owns it; everyone else treats the cell as an opaque
# survivor. Stale tags (from retired
# collections) never need clearing, they are simply reclaimable.
#
# The word does double duty a second time: commit re-stamps proven-live
@@ -350,13 +359,29 @@ proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} =
# collection. Roots always bypass the stamp: every death has a dec-witness
# that gets registered, and registered cells are always scanned as roots.
const
MaxPar {.intdefine.} = 8 # max concurrent collections
MaxPar {.intdefine.} = 256
## CAPACITY of the slot table, not a tuning knob: a hard ceiling on
## concurrent collections, sized to stay out of the way (16 bytes of BSS
## per entry, and scans only ever run over `gParSlots`, below). Raise it
## only for programs with more than this many threads collecting AT ONCE.
ParSlots = MaxPar
var
gMergeLock: Lock # protects the tag slots + orphaned roots
gActiveTags: array[ParSlots, int64] # 0 = free slot
gSlotPhase: array[ParSlots, int] # 0 idle, 1 capturing, 2 committing
gParSlots: int = 1
## How many slots are IN PLAY. Every scan below runs over this prefix
## rather than over the whole table, and it is raised (under gMergeLock,
## never lowered) exactly when a thread wants to collect and every slot
## already in play is busy. It therefore converges on the number of
## threads that actually collect CONCURRENTLY — one slot each — and then
## stops: the parallelism is auto-tuned to the workload instead of being
## a compile-time guess. A fixed bound throttled hard whenever the thread
## count exceeded it, because the surplus threads did not just collect
## later, they PARKED in `parkUntil(anySlotFree())` waiting for a slot
## (32 threads against 8 slots: 6.3s vs 2.6s with a slot each).
## Starting at 1 also means single-threaded programs scan one entry.
gSoloCapture: int # a solo collection is in its capture phase
gTagCounter: int64
gMyTag {.threadvar.}: int64
@@ -399,9 +424,19 @@ const
epochBase = 0x40000000 # stamp namespace: tags stay below this
epochMask = 0x3FFFFFFF
# stamp layout: high word = epochBase|epoch, low word = survival age
# Every packed word in this file squeezes two 32-bit fields into one int64 as
# `(hi shl 32) or lo`. The claim word (a cell's `rootIdx`, see above) is either
# hi = owning collection's tag, lo = the cell's dense capture index
# hi = epochBase|epoch (a stamp), lo = the cell's survival age
# and a `gPendingWatch` entry is hi = slot, lo = tag. The high half is read
# with a plain `shr 32` — every value stored there is below 2^31, so the shift
# keeps it positive and needs no mask. The low half is the one that needs
# masking: `shl 32` left the high half sitting above it, and `and 0xFFFFFFFF`
# is what clears those bits back out.
template loWord(w: int64): int64 = w and 0xFFFFFFFF
template epochStamp(e: int): int64 = int64(epochBase or (e and epochMask)) shl 32
template stampAge(w: int64): int = int(w and 0xFFFFFFFF)
template stampAge(w: int64): int = int(loWord(w))
template isEpochStamp(w: int64): bool = (w shr 32) >= epochBase
template parkUntil(cond: untyped) =
@@ -426,9 +461,17 @@ proc collectorEvent() {.inline.} =
broadcast gWaitCond
release gWaitLock
proc slotsInPlay(): int {.inline.} =
## Must be loaded AFTER whatever claim word the caller is validating: a
## slot is put in play before the collection owning it can tag any cell,
## so a load ordered after reading a tagged word is guaranteed to cover
## the slot that wrote the tag. `gParSlots` only ever grows, so a scan
## over this prefix can never shrink under a reader.
atomicLoadN(addr gParSlots, ATOMIC_ACQUIRE)
proc anySlotFree(): bool {.inline.} =
result = false
for sl in 0 ..< ParSlots:
for sl in 0 ..< slotsInPlay():
if atomicLoadN(addr gActiveTags[sl], ATOMIC_ACQUIRE) == 0:
return true
@@ -438,12 +481,12 @@ template isStamped(c: Cell): bool =
# value routes into claimCell which re-validates with acquire + CAS.
(atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) shr 32) == gMyTag
template denseIdx(c: Cell): int32 =
int32(atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) and 0xFFFFFFFF)
int32(loWord(atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED)))
proc isActiveTag(t: int64): bool {.inline.} =
result = false
if t != 0:
for s in 0 ..< ParSlots:
for s in 0 ..< slotsInPlay():
if atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) == t:
return true
@@ -485,6 +528,25 @@ var
## draining this thread's stripe queue registers candidates here, and
## this thread's collections steal it as their slice — no lock, and
## collections keep the cache locality of thread-local data.
gPendingCells {.threadvar.}: CellSeq[Cell]
## Cells this thread committed dead — slots nil'ed, references already
## decremented — but has not handed back to the allocator yet, because a
## capture that was in flight at commit time may still hold a stale
## (slot, value) snapshot pointing at them. Released at the start of this
## thread's next collection; see `releasePending`.
gPendingWatch {.threadvar.}: RawSeq[int64]
## The captures that batch must outlive, packed as (slot shl 32) or tag.
gPendingSlot {.threadvar.}: int
gPendingActive {.threadvar.}: bool
gSpareRoots {.threadvar.}: CellSeq[Cell]
## The buffer a finished collection hands back, so that stealing
## `gLocalRoots` costs no allocation in steady state.
gTraceBuf {.threadvar.}: CellSeq[TraceEntry]
gFreeBuf {.threadvar.}: CellSeq[Cell]
## Storage for `GcEnv.traceStack` / `GcEnv.toFree`, kept across
## collections like the `gCap` arrays: both grow to the size of the
## captured graph, so re-allocating and re-growing them per collection
## was a memcpy of the whole trace frontier every time.
stripes: array[NumStripes, Stripe]
rootsThreshold: int = 128 # shared adaptive heuristic; races are benign
defaultThreshold = when defined(nimFixedOrc): 10_000 else: 128
@@ -677,6 +739,62 @@ template orcAssert(cond, msg) =
cfprintf(cstderr, "[Bug!] %s\n", msg)
rawQuit 1
proc graceSatisfied(): bool =
## Has every capture recorded in `gPendingWatch` finished? A capture that
## started later cannot hold a stale snapshot of the batch: it reads every
## slot fresh, and the batch's cells are unreachable by then.
result = true
for i in 0 ..< gPendingWatch.len:
let w = gPendingWatch.d[i]
let s = int(w shr 32)
let tg = loWord(w)
if atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) == tg and
atomicLoadN(addr gSlotPhase[s], ATOMIC_ACQUIRE) == 1:
return false
proc buildPendingWatch(): bool =
## Record the collections that are in their CAPTURE phase right now: they
## are the only ones that can hold a stale (slot, value) snapshot of the
## cells we are about to release. `false` (nothing capturing) is the common
## case below a handful of threads, and means the batch can be freed on the
## spot with no deferral and no destructor-timing change at all.
if gPendingWatch.d == nil: init gPendingWatch
gPendingWatch.len = 0
for s in 0 ..< slotsInPlay():
if s != gMySlot:
let tg = atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE)
if tg != 0 and atomicLoadN(addr gSlotPhase[s], ATOMIC_ACQUIRE) == 1:
gPendingWatch.add((int64(s) shl 32) or tg)
result = gPendingWatch.len > 0
proc releasePending() =
## Hand this thread's parked batch back to the allocator and give its slot
## up. Called at the start of every collection, so by the time it runs the
## watched captures have had a whole collection's worth of time to finish
## and the wait below is virtually always already satisfied — that is the
## whole point: the wait moved off the commit path, where it blocked BOTH
## the committing collector and (because commit runs inside the GC fence)
## every mutator doing a seq operation.
if not gPendingActive: return
parkUntil(graceSatisfied())
# Give the slot up FIRST: the batch is unreachable and no capture can hold
# a snapshot of it any more, so the tag has nothing left to protect.
gPendingActive = false
gPendingWatch.len = 0
atomicStoreN(addr gActiveTags[gPendingSlot], 0, ATOMIC_SEQ_CST)
collectorEvent()
# Destructors run here. `Collecting` is the existing re-entrancy guard: a
# destructor-driven dec that overflows a stripe must drain it, not start a
# nested collection that would write into the batch we are walking.
let prev = lockState
lockState = Collecting
for i in 0 ..< gPendingCells.len:
when orcLeakDetector:
writeCell("CYCLIC OBJECT FREED", gPendingCells.d[i][0], gPendingCells.d[i][1])
free(gPendingCells.d[i][0], gPendingCells.d[i][1])
gPendingCells.len = 0
lockState = prev
proc nimTraceRef(q: pointer; desc: PNimTypeV2; env: pointer) {.compilerRtl, inl.} =
let p = cast[ptr pointer](q)
# read the slot exactly once: mutators may exchange it concurrently.
@@ -698,6 +816,7 @@ proc nimTraceRefDyn(q: pointer; env: pointer) {.compilerRtl, inl.} =
proc prepareCapture() =
if gCap.recs.d == nil:
init gCap.recs
init gCap.sccIdx
init gCap.tstack
init gCap.frames
init gCap.edges
@@ -709,11 +828,13 @@ proc prepareCapture() =
init gCap.ages
else:
gCap.recs.len = 0
gCap.sccIdx.len = 0
gCap.tstack.len = 0
gCap.frames.len = 0
gCap.edges.len = 0
gCap.sccs.len = 0
gCap.sccMembers.len = 0
gCap.crossTgt.len = 0
gCap.crossPend.len = 0
gCap.prunedSrc.len = 0
gCap.ages.len = 0
@@ -722,18 +843,22 @@ proc prepareCapture() =
# inRootsFlag between capture and commit, which must not look like a
# mutation to the commit-time rc validation.
proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs;
pruneLive: bool): int32 =
pruneLive: bool; old0: int64): int32 =
## Dense index if this collection owns `c` (claiming and registering it
## if it was unclaimed), -1 if another ACTIVE collection owns it, or
## -2 if `pruneLive` and the cell was proven live in the current epoch
## (treat as an opaque live external, don't descend).
##
## `old0` is `c`'s claim word as the caller already read it (acquire): the
## DFS reads it to test ownership, and re-reading it here would be a second
## dependent load of the same cold header word on every traversed edge.
if gAmSolo:
# no other collection is (or can start) capturing: plain stores.
# This recovers the sequential capture speed of the single-collector
# design whenever collections do not actually overlap.
let old = c.rootIdx
let old = old0
if (old shr 32) == gMyTag:
return int32(old and 0xFFFFFFFF)
return int32(loWord(old))
if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and
stampAge(old) >= YrcPromoteAge:
return -2
@@ -744,18 +869,22 @@ proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs;
if old != 0: bumpStat gStatCapRepeat
cap.recs.add CaptureRec(cell: c, desc: desc,
rcWord: loadRc(c) and not rcMask,
lowlink: int32(idx), sccOf: -1'i32)
lowlink: int32(idx), selfRefs: 0'i32)
cap.sccIdx.add -1'i32
cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0)
cap.tstack.add int32(idx)
return int32(idx)
var old = old0
while true:
var old = atomicLoadN(addr c.rootIdx, ATOMIC_ACQUIRE)
if (old shr 32) == gMyTag:
return int32(old and 0xFFFFFFFF)
return int32(loWord(old))
if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and
stampAge(old) >= YrcPromoteAge:
return -2
if isActiveTag(old shr 32):
# an epoch stamp is never a tag (tags are allocated below `epochBase`),
# so the scan over the active-tag slots is skipped for the common
# "cell survived an earlier collection" word
if not isEpochStamp(old) and isActiveTag(old shr 32):
return -1
let idx = cap.recs.len
if atomicCompareExchangeN(addr c.rootIdx, addr old,
@@ -766,38 +895,69 @@ proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs;
if old != 0: bumpStat gStatCapRepeat
cap.recs.add CaptureRec(cell: c, desc: desc,
rcWord: loadRc(c) and not rcMask,
lowlink: int32(idx), sccOf: -1'i32)
lowlink: int32(idx), selfRefs: 0'i32)
cap.sccIdx.add -1'i32
cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0)
cap.tstack.add int32(idx)
return int32(idx)
# a failed CAS leaves the fresh claim word in `old`; loop with it
proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) =
## Iterative Tarjan SCC over everything reachable from `s`. A frame's
## pending out-edges are the traceStack entries above frame.base; a child
## pushes and drains its own segment above ours, so when the child's frame
## pops, the stack is back at our segment and we resume popping our edges.
if isStamped(s): return
##
## An SCC's out-edges are classified into internal/cross the moment the SCC
## is emitted, not in a later pass over a whole-graph edge list. That works
## because `cap.edges` is truncated back to a frame's `ebase` whenever that
## frame's cell turns out to be an SCC root: edges of already-emitted
## sub-SCCs are gone, so `edges[ebase(u) ..< len]` at u's emission holds
## exactly the out-edges of u's SCC. Every one of them targets either a
## member (u would not be an SCC root if a member pointed at a cell still
## on the stack below u) or an SCC emitted earlier, so `sccIdx` is final
## for all of them and the cross targets can be appended to `crossTgt`
## contiguously — which makes `crossOff` a prefix offset for free.
let rootWord = atomicLoadN(addr s.rootIdx, ATOMIC_ACQUIRE)
if (rootWord shr 32) == gMyTag: return
orcAssert(j.traceStack.len == 0, "capture: trace stack not empty")
# roots never prune: a dec-witnessed suspicion overrides any epoch stamp
let root = claimCell(s, desc, cap, pruneLive = false)
let root = claimCell(s, desc, cap, pruneLive = false, old0 = rootWord)
if root < 0:
return # another active collection owns this candidate; it handles it
trace(s, desc, j)
cap.frames.add TarjanFrame(u: root, base: 0)
while cap.frames.len > 0:
let u = cap.frames.d[cap.frames.len -% 1].u
let base = cap.frames.d[cap.frames.len -% 1].base
# The innermost frame is kept in `u`/`base` instead of being re-read from
# `cap.frames` on every iteration: the loop body runs once per captured
# EDGE, so reloading the frame there costs more than the frame stack itself.
# `cap.frames` therefore only holds the ANCESTORS of `u`.
var u = root
var base = 0
var ebase = 0'i32
while true:
if j.traceStack.len > base:
let (entry, tdesc) = j.traceStack.pop()
let t = head(entry.val)
if isStamped(t):
let v = denseIdx(t)
cap.edges.add (int64(u) shl 32) or int64(v)
if cap.recs.d[v].sccOf < 0 and v < cap.recs.d[u].lowlink:
cap.recs.d[u].lowlink = v
# inlined pop: the stamped path never needs the entry's descriptor
let last = j.traceStack.len -% 1
j.traceStack.len = last
let t = head(j.traceStack.d[last][0].val)
# one load of the target's claim word serves both the ownership test
# and the dense-index extraction
let cw = atomicLoadN(addr t.rootIdx, ATOMIC_ACQUIRE)
if (cw shr 32) == gMyTag:
let v = int32(loWord(cw))
if v == u:
# A self edge is internal by construction and its reference is
# already in `rcWord`, so it cancels out of `sumRefs - internal`
# exactly. Counting it here keeps it out of the edge array and out
# of the classification pass below.
inc cap.recs.d[u].selfRefs
else:
cap.edges.add v
if cap.sccIdx.d[v] < 0 and v < cap.recs.d[u].lowlink:
cap.recs.d[u].lowlink = v
else:
let tdesc = j.traceStack.d[last][1]
let childBase = j.traceStack.len
let v = claimCell(t, tdesc, cap, pruneLive = true)
let v = claimCell(t, tdesc, cap, pruneLive = true, old0 = cw)
if v == -1:
# cross-collection edge: the owner sees our reference in the rc
# word and classifies the target live; we re-register it as a
@@ -810,75 +970,72 @@ proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) =
when defined(nimOrcStats):
bumpStat gStatCapPruned
else:
cap.edges.add (int64(u) shl 32) or int64(v)
cap.edges.add v
trace(t, tdesc, j)
cap.frames.add TarjanFrame(u: v, base: childBase)
cap.frames.add TarjanFrame(u: u, ebase: ebase, base: base)
u = v
ebase = int32(cap.edges.len)
base = childBase
else:
cap.frames.len = cap.frames.len -% 1
if cap.frames.len > 0:
let pu = cap.frames.d[cap.frames.len -% 1].u
if cap.recs.d[u].lowlink < cap.recs.d[pu].lowlink:
cap.recs.d[pu].lowlink = cap.recs.d[u].lowlink
if cap.recs.d[u].lowlink == u:
let lowU = cap.recs.d[u].lowlink
if lowU == u:
# u is the root of an SCC: pop the members off the Tarjan stack
let sid = int32(j.nScc)
let memStart = int32(cap.sccMembers.len)
var sum = 0
while true:
let w = cap.tstack.pop()
cap.recs.d[w].sccOf = int32(j.nScc)
cap.sccMembers.add w
sum = sum +% (cap.recs.d[w].rcWord shr rcShift) +% 1
if w == u: break
cap.sccs.add SccRec(sumRefs: sum, memStart: memStart)
let m = cap.tstack.pop()
cap.sccIdx.d[m] = sid
cap.sccMembers.add m
# `- selfRefs`: a self edge counts in both `sumRefs` and `internal`
# and was folded out of the edge array in the loop above
sum = sum +% (cap.recs.d[m].rcWord shr rcShift) +% 1 -%
cap.recs.d[m].selfRefs
if m == u: break
# classify this SCC's out-edges now that every target's SCC is final
let crossOff = int32(cap.crossTgt.len)
var internal = 0
for i in ebase ..< int32(cap.edges.len):
let sv = cap.sccIdx.d[cap.edges.d[i]]
if sv == sid: inc internal
else: cap.crossTgt.add sv
cap.edges.len = ebase
cap.sccs.add SccRec(sumRefs: sum, internal: internal,
memStart: memStart, crossOff: crossOff)
inc j.nScc
if cap.frames.len == 0: break
let pi = cap.frames.len -% 1
cap.frames.len = pi
let pu = cap.frames.d[pi].u
if lowU < cap.recs.d[pu].lowlink:
cap.recs.d[pu].lowlink = lowU
u = pu
ebase = cap.frames.d[pi].ebase
base = cap.frames.d[pi].base
# ---------------- phase 2: deadness, side arrays only ----------------
proc computeDeadness(j: var GcEnv; cap: ptr CaptureBufs) =
let nScc = j.nScc
# append the sentinel record ([nScc]); capture left internal/deadIn/flags
# zero-initialized and memStart valid. crossOff is filled below as a prefix
# sum, so the sentinel closes the last SCC's member and cross-edge slices.
cap.sccs.add SccRec(memStart: int32(cap.sccMembers.len))
# classify captured edges: internal to an SCC vs condensation cross edges
var nCross = 0
for i in 0 ..< cap.edges.len:
let e = cap.edges.d[i]
let su = cap.recs.d[int32(e shr 32)].sccOf
let sv = cap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf
if su == sv:
inc cap.sccs.d[su].internal
else:
inc cap.sccs.d[su].crossOff
inc nCross
var total = 0'i32
for s in 0 ..< nScc:
let c = cap.sccs.d[s].crossOff
cap.sccs.d[s].crossOff = total
cap.sccs.d[s].crossCursor = total
total = total +% c
cap.sccs.d[nScc].crossOff = total
setLenUninit cap.crossTgt, nCross
for i in 0 ..< cap.edges.len:
let e = cap.edges.d[i]
let su = cap.recs.d[int32(e shr 32)].sccOf
let sv = cap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf
if su != sv:
cap.crossTgt.d[cap.sccs.d[su].crossCursor] = sv
inc cap.sccs.d[su].crossCursor
# append the sentinel record ([nScc]) that closes the last SCC's member and
# cross-edge slices; capture left deadIn/flags zero-initialized and filled
# sumRefs/internal/memStart/crossOff in already, so the condensation is
# complete the moment the DFS ends.
cap.sccs.add SccRec(memStart: int32(cap.sccMembers.len),
crossOff: int32(cap.crossTgt.len))
# pruned out-edges taint the source SCC: pruning cannot cause a false
# "dead" (an untraced target only ever ADDS unexplained external refs),
# but a "live" verdict may lean on a stamp that went stale within the
# epoch, so validate re-registers surviving pruned SCCs
for i in 0 ..< cap.prunedSrc.len:
let s = cap.recs.d[cap.prunedSrc.d[i]].sccOf
let s = cap.sccIdx.d[cap.prunedSrc.d[i]]
cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagPruned
# cells that stay registered as roots (partial collection) count as
# externally referenced: the roots buffer itself points at them
for mi in 0 ..< cap.sccMembers.len:
let m = cap.sccMembers.d[mi]
if (loadRc(cap.recs.d[m].cell) and inRootsFlag) != 0:
let s = cap.recs.d[m].sccOf
let s = cap.sccIdx.d[m]
cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagForcedLive
# deadness over the condensation. Tarjan emits sinks first, so higher SCC
# ids are sources and every cross edge goes from a higher id to a lower
@@ -910,7 +1067,7 @@ proc markDirtyFromQueues(j: var GcEnv; cap: ptr CaptureBufs) =
template taint(cp: Cell) =
let c = cp
if isStamped(c):
let s = cap.recs.d[denseIdx(c)].sccOf
let s = cap.sccIdx.d[denseIdx(c)]
cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagDirty
for i in 0..<NumStripes:
when useIncQueue:
@@ -1004,21 +1161,32 @@ proc commitDead(j: var GcEnv; cap: ptr CaptureBufs) =
# 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 (cap.sccs.d[cap.recs.d[denseIdx(t)].sccOf].flags 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.
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)
template deadCell(w: int64): bool =
## `w` is the target's claim word, read once by the caller
(w shr 32) == gMyTag and
(cap.sccs.d[cap.sccIdx.d[int32(loWord(w))]].flags and flagDead) != 0
# Grace period: a 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. This used to BLOCK here until
# every such capture ended, which serialized each committing collector
# against every capturing one — and did so while holding the GC fence, so
# mutators doing seq operations spun for the duration too. Instead the
# batch is parked (`gPendingCells`) together with the set of captures it
# must outlive, and `releasePending` frees it at the start of this
# thread's next collection. Our tag stays in `gActiveTags` until then, so
# a capture that reaches a parked cell through a stale snapshot still sees
# it as owned by an active collection and cannot claim — and free — it.
# The batch's destructors therefore run one collection later than they
# used to; nothing else observes the delay, since the cells are
# unreachable, their slots are nil and their references already dropped.
template parkBatch(): bool = (if cap.recs.len == 0: false else: buildPendingWatch())
template holdOrFree(c: Cell; d: PNimTypeV2; deferred: bool) =
if deferred:
gPendingCells.add(c, d)
else:
when orcLeakDetector:
writeCell("CYCLIC OBJECT FREED", c, d)
free(c, d)
# 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.
@@ -1033,8 +1201,9 @@ proc commitDead(j: var GcEnv; cap: ptr CaptureBufs) =
# 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()
# and a parked batch is not touched until its watch list is clear).
let deferred = parkBatch()
if deferred and gPendingCells.d == nil: init gPendingCells
for m in 0 ..< cap.recs.len:
let cell = cap.recs.d[m].cell
let desc = cap.recs.d[m].desc
@@ -1043,12 +1212,15 @@ proc commitDead(j: var GcEnv; cap: ptr CaptureBufs) =
while j.traceStack.len > 0:
let (entry, _) = j.traceStack.pop()
entry.slot[] = nil
when orcLeakDetector:
writeCell("CYCLIC OBJECT FREED", cell, desc)
free(cell, desc)
holdOrFree(cell, desc, deferred)
j.freed = cap.recs.len
if deferred:
gPendingSlot = gMySlot
gPendingActive = true
else:
init j.toFree
if gFreeBuf.d == nil: init gFreeBuf
gFreeBuf.len = 0
j.toFree = gFreeBuf
for s in 0 ..< j.nScc:
if (cap.sccs.d[s].flags and flagDead) != 0:
for mi in cap.sccs.d[s].memStart ..< cap.sccs.d[s+1].memStart:
@@ -1067,32 +1239,60 @@ proc commitDead(j: var GcEnv; cap: ptr CaptureBufs) =
let (entry, tdesc) = j.traceStack.pop()
let t = head(entry.val)
entry.slot[] = nil
if not deadCell(t):
let tw = atomicLoadN(addr t.rootIdx, ATOMIC_RELAXED)
if not deadCell(tw):
trialDec(t)
# a stamped target was not analyzed by THIS collection, so
# this dec may be the death blow: keep the cell examinable
if isEpochStamp(atomicLoadN(addr t.rootIdx, ATOMIC_RELAXED)):
if isEpochStamp(tw):
registerLocal(t, tdesc)
# epoch-stamp what this collection PROVED live, carrying the cell's
# survival age: only cells that keep surviving get promoted to ages
# where captures prune them, so die-young data is never deferred.
# Demoted (dirty) and pruned SCCs stay unproven — leave their stale
# tags claimable. Our tag is still active, so no foreign claim can
# race these stores.
# epoch-stamp what this collection PROVED live, carrying the survival
# age: only cells that keep surviving get promoted to ages where
# captures prune them, so die-young data is never deferred. Demoted
# (dirty) and pruned SCCs stay unproven — leave their stale tags
# claimable. Our tag is still active, so no foreign claim can race
# these stores.
#
# The age is the SCC's, not the cell's: the whole SCC gets the age of
# its YOUNGEST member, so promotion is all-or-nothing. A per-cell age
# lets one member of an SCC promote ahead of its own SCC-mates; the
# next capture then prunes that INTERNAL edge, which taints the SCC as
# flagPruned, which stops it from ever being stamped again — freezing
# every member's age at its current value and re-tracing the whole
# structure on every collection from then on. Members age at different
# rates whenever a structure is built incrementally (a list appended to
# across several collections), so this is the common case, not a corner
# one. Taking the minimum can only delay a promotion, never hasten one,
# so it cannot widen the floating-garbage bound.
for s in 0 ..< j.nScc:
if (cap.sccs.d[s].flags and (flagDead or flagDirty or flagPruned)) == 0:
for mi in cap.sccs.d[s].memStart ..< cap.sccs.d[s+1].memStart:
let m = cap.sccMembers.d[mi]
atomicStoreN(addr cap.recs.d[m].cell.rootIdx,
gMyEpochStamp or int64(cap.ages.d[m] +% 1),
ATOMIC_RELAXED)
graceWait()
for i in 0 ..< j.toFree.len:
when orcLeakDetector:
writeCell("CYCLIC OBJECT FREED", j.toFree.d[i][0], j.toFree.d[i][1])
free(j.toFree.d[i][0], j.toFree.d[i][1])
let memStart = cap.sccs.d[s].memStart
let memEnd = cap.sccs.d[s+1].memStart
var age = high(int32)
for mi in memStart ..< memEnd:
let a = cap.ages.d[cap.sccMembers.d[mi]]
if a < age: age = a
let stamp = gMyEpochStamp or int64(age +% 1)
for mi in memStart ..< memEnd:
atomicStoreN(addr cap.recs.d[cap.sccMembers.d[mi]].cell.rootIdx,
stamp, ATOMIC_RELAXED)
j.freed = j.toFree.len
deinit j.toFree
if j.toFree.len > 0 and buildPendingWatch():
# park the whole batch by swapping buffers: the collection keeps the
# (now empty) buffer the previous batch used, so neither side allocates
let spare = gPendingCells
gPendingCells = j.toFree
j.toFree = spare
j.toFree.len = 0
gPendingSlot = gMySlot
gPendingActive = true
else:
for i in 0 ..< j.toFree.len:
when orcLeakDetector:
writeCell("CYCLIC OBJECT FREED", j.toFree.d[i][0], j.toFree.d[i][1])
free(j.toFree.d[i][0], j.toFree.d[i][1])
j.toFree.len = 0
gFreeBuf = j.toFree
proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell];
wait: bool; drainAll = false): bool =
@@ -1100,11 +1300,12 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell];
## collect) and try to become a collector over THIS THREAD's candidates:
## claim a tag slot — the only step still under gMergeLock — and steal
## the thread-local buffer as this collection's slice, lock-free. When
## there is enough work but all ParSlots collections are running, `wait`
## decides between parking until a slot frees (backpressure for
## overflowing mutators) and giving up. Either way the drain happened,
## there is enough work but the slot table is full (more than MaxPar
## threads collecting at once), `wait` decides between parking until a
## slot frees and giving up. Either way the drain happened,
## so the caller's overflowing queue has room again.
result = false
releasePending() # last collection's batch: its watch list is long clear
if drainAll: drainAllStripes()
else: drainStripe(getStripeIdx())
adoptOrphans()
@@ -1112,15 +1313,23 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell];
mayRunCycleCollect():
acquire gMergeLock
var slot = -1
for sl in 0 ..< ParSlots:
let inPlay = gParSlots
for sl in 0 ..< inPlay:
if atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) == 0:
slot = sl
break
if slot < 0 and inPlay < ParSlots:
# Every slot in play is busy and the table has room: widen the pool
# instead of throttling this thread. Publishing the wider bound before
# the tag lands in the new slot is what makes `slotsInPlay` safe.
slot = inPlay
atomicStoreN(addr gParSlots, inPlay +% 1, ATOMIC_SEQ_CST)
if slot < 0:
release gMergeLock
if not wait: break
# backpressure: all ParSlots collections are running; park until one
# finishes (finishCollection broadcasts) instead of burning a core
# the table itself is full (more than MaxPar threads collecting at
# once): park until one finishes (finishCollection broadcasts)
# instead of burning a core
parkUntil(anySlotFree())
drainStripe(getStripeIdx()) # the world moved while we waited
adoptOrphans()
@@ -1131,7 +1340,7 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell];
gMySlot = slot
gMyEpochStamp = epochStamp(atomicLoadN(addr gEpoch, ATOMIC_RELAXED))
var othersActive = false
for sl in 0 ..< ParSlots:
for sl in 0 ..< gParSlots:
if sl != slot and atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) != 0:
othersActive = true
gAmSolo = not othersActive
@@ -1143,7 +1352,12 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell];
# our buffer, our slice: no lock needed
if keepBelow == 0:
slice = gLocalRoots # steal the whole buffer
init(gLocalRoots)
if gSpareRoots.d != nil:
gLocalRoots = gSpareRoots
gLocalRoots.len = 0
gSpareRoots = default(CellSeq[Cell])
else:
init(gLocalRoots)
else:
init(slice, max(gLocalRoots.len - keepBelow, 8))
for i in keepBelow ..< gLocalRoots.len:
@@ -1155,8 +1369,16 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell];
proc finishCollection() =
if atomicAddFetch(addr gCollectionCounter, 1, ATOMIC_RELAXED) mod YrcEpochLen == 0:
discard atomicAddFetch(addr gEpoch, 1, ATOMIC_RELAXED)
atomicStoreN(addr gActiveTags[gMySlot], 0, ATOMIC_SEQ_CST)
atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE)
if gPendingActive:
# A batch is parked under this collection's tag. Clear only the PHASE —
# so nobody's grace check waits on us — and leave the tag in
# `gActiveTags`: it is what stops a foreign capture from claiming, and
# then freeing, a cell that is sitting in the batch. `releasePending`
# gives the slot back.
atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE)
else:
atomicStoreN(addr gActiveTags[gMySlot], 0, ATOMIC_SEQ_CST)
atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE)
gMyTag = 0
gAmSolo = false
collectorEvent() # wake backpressure and grace waiters
@@ -1170,7 +1392,9 @@ proc collectCyclesImpl(j: var GcEnv; slice: var CellSeq[Cell]) =
for i in countdown(last, 0):
writeCell("root", slice.d[i][0], slice.d[i][1])
init j.traceStack
if gTraceBuf.d == nil: init gTraceBuf
gTraceBuf.len = 0
j.traceStack = gTraceBuf
prepareCapture()
let cap = addr gCap # hoist the TLS lookup out of the hot loops
j.nScc = 0
@@ -1194,11 +1418,11 @@ proc collectCyclesImpl(j: var GcEnv; slice: var CellSeq[Cell]) =
commitDead(j, cap)
j.keepThreshold = j.freed == j.touched and j.touched > 0
deinit j.traceStack
gTraceBuf = j.traceStack # hand the (possibly grown) buffer back
proc runCollection(j: var GcEnv; slice: var CellSeq[Cell]) =
## Runs one collection over the stolen slice, concurrently with mutators
## AND with up to ParSlots-1 other collections over disjoint partitions.
## AND with the other collecting threads over disjoint partitions.
yrcGcFenceEnter() # freeze seq structure mutations, not ref writes
if not gAmSolo:
# a solo collection claims with plain stores; nobody else may claim
@@ -1210,7 +1434,10 @@ proc runCollection(j: var GcEnv; slice: var CellSeq[Cell]) =
lockState = prev
yrcGcFenceExit()
finishCollection()
deinit slice
if gSpareRoots.d == nil and slice.d != nil:
gSpareRoots = slice # recycle it as the next steal's replacement
else:
deinit slice
when defined(nimOrcStats):
var freedCyclicObjects {.threadvar.}: int
@@ -1283,6 +1510,7 @@ proc GC_runOrc* =
if startCollection(1, 0, slice, wait = true, drainAll = true):
var j: GcEnv
runCollection(j, slice)
releasePending() # GC_fullCollect must not leave a batch parked
# note: aborted SCCs and cross-collection targets legitimately leave
# re-registered roots behind; other RUNNING threads' local candidates
# are theirs to collect (exiting threads spill to the orphan buffer)
@@ -1315,6 +1543,7 @@ proc nimYrcThreadTeardown() =
## of ours is stranded in a queue no other thread hashes to, then spill
## our candidate buffer to the global orphan buffer, where the next
## collection on any thread adopts it.
releasePending() # nobody else can release this thread's parked batch
drainStripe(getStripeIdx())
if gLocalRoots.len > 0:
acquire gMergeLock
@@ -1326,6 +1555,11 @@ proc nimYrcThreadTeardown() =
deinit(gLocalRoots)
gLocalRoots.d = nil
gLocalRoots.len = 0
deinit(gSpareRoots)
deinit(gTraceBuf)
deinit(gFreeBuf)
deinit(gPendingCells)
deinit(gPendingWatch)
proc GC_enableMarkAndSweep*() = GC_enableOrc()
proc GC_disableMarkAndSweep*() = GC_disableOrc()
@@ -1362,7 +1596,27 @@ proc nimDecRefIsLastCyclicDyn(p: pointer): bool {.compilerRtl, inl.} =
enqueueDec(head(p), cast[ptr PNimTypeV2](p)[])
proc nimDecRefIsLastDyn(p: pointer): bool {.compilerRtl, inl.} =
nimDecRefIsLastCyclicDyn(p)
## ACYCLIC ref: prompt reclamation, exactly as under --mm:arc. This used to
## forward to `nimDecRefIsLastCyclicDyn`, which enqueued the dec and so
## dragged every `.acyclic` type through capture/deadness/commit -- the
## precise opposite of what the annotation asks for.
##
## No grace period is needed here, and that is not an accident: the
## collector has no way to be holding this cell. It cannot reach it by
## traversal, because liftdestructors only emits `nimTraceRef` for fields
## whose type is cyclic; and it cannot hold it as a capture root, because
## roots come only from `registerLocal` on a drained dec, and an acyclic
## dec is never queued now that `nimAsgnYrc` is gated on `canFormAcycle`.
## Both halves must stay true together -- prompt reclamation here is only
## sound while nothing else puts an acyclic cell into the collector.
result = false
if p != nil:
when hasThreadSupport:
result = atomicDec(head(p).rc, rcIncrement) == -rcIncrement
else:
let cell = head(p)
if (cell.rc and not rcMask) == 0: result = true
else: cell.rc = cell.rc -% rcIncrement
proc nimDecRefIsLastCyclicStatic(p: pointer; desc: PNimTypeV2): bool {.compilerRtl, inl.} =
result = false

668
lib/system/yrc_opt_proof.lean Normal file
View File

@@ -0,0 +1,668 @@
/-
YRC Optimization Proofs — SCC-uniform ages, demand-grown slots, deferred
reclamation
=======================================================================
Self-contained, no Mathlib. Checked with Lean 4 (v4.32.0).
Companion to yrc_proof.lean (core safety: garbage stability, validation
soundness, partitions, grace, fence, deadlock freedom) and to
yrc_tarjan_proof.lean (soundness AND completeness of the SCC deadness
scan). This file models the three changes of the "YRC: optimizations"
round, each of which touches an invariant the other two files rely on:
§A SCC-UNIFORM EPOCH AGES (commitDead's re-stamp loop).
Before: every proven-live cell was stamped with its OWN survival
age + 1. One member of an SCC could then reach `YrcPromoteAge`
ahead of its SCC-mates; the next capture pruned that INTERNAL edge,
tainting the SCC `flagPruned`, which stops it from ever being
re-stamped — freezing every member's age and re-tracing the whole
structure on every collection from then on. Members age at
different rates whenever a structure is built incrementally, so
this was the common case.
After: the whole SCC is stamped with the age of its YOUNGEST
member + 1, so promotion is all-or-nothing.
§B DEMAND-GROWN COLLECTOR SLOTS (`gParSlots`, startCollection).
Before: `MaxPar` was a fixed 8 and the 9th collecting thread PARKED
in `parkUntil(anySlotFree())` instead of collecting. After:
`gParSlots` counts the slots in play, starts at 1, and is raised
under gMergeLock exactly when a thread wants to collect and every
slot in play is busy; `MaxPar` (256) is only the table capacity.
Every scan (`isActiveTag`, `anySlotFree`, `buildPendingWatch`) now
runs over a prefix that GROWS under the reader, which is sound only
because of the ordering rule at `slotsInPlay`.
§C DEFERRED RECLAMATION (`gPendingCells` / `releasePending`).
Before: commitDead BLOCKED until every concurrent capture ended
(the grace period), inside the GC fence — stalling both the
committing collector and every mutator doing a seq operation.
After: the dead batch is parked together with a watch list of the
captures it must outlive, and released at the start of this
thread's next collection. The parked collection's TAG STAYS in
`gActiveTags` (only the phase is cleared): that is what stops a
foreign capture from claiming — and then freeing — a parked cell.
Nothing here weakens yrc_proof.lean: §A only changes which cells a
capture skips (pruning shrinks the captured set, the conservative
direction), §B only changes how many slots a scan covers, and §C only
moves the free of an already-validated, already-closed dead set later
in time, where garbage stability (yrc_proof.lean §3) keeps it dead.
-/
abbrev Obj := Nat
abbrev Tag := Nat
-- Slot indices and times are plain `Nat`: `omega` ignores atoms whose type
-- is an abbreviation, and both appear in arithmetic below.
/-! ## §A SCC-uniform epoch ages
The spare header word (`rootIdx`) is a three-way namespace: 0 for a
cell no collection ever touched, a claim tag while a collection owns
the cell, or an epoch stamp (`epochBase | epoch` in the high word, the
survival age in the low word). Tags are allocated strictly below
`epochBase`, so a stamp is never mistaken for a tag — modelled here by
keeping the three cases as separate constructors. -/
inductive Word where
| fresh -- 0: never claimed, never stamped
| tag (t : Tag) -- a collection's claim word
| stamp (e : Nat) (age : Nat) -- an epoch stamp written by commitDead
/-- The age a capture reads out of a claim word (`cap.ages`): a stamp
contributes its recorded age, anything else contributes 0. -/
def ageOf : Word → Nat
| .stamp _ a => a
| _ => 0
def capturedAge (w : Obj → Word) (x : Obj) : Nat := ageOf (w x)
/-- `claimCell(pruneLive = true)` prunes at a target whose stamp is of the
CURRENT epoch and whose age reached `YrcPromoteAge`: the target is
treated as an opaque live external and is not descended into. Roots
are always claimed with `pruneLive = false`, so this never applies to
them. -/
def prunable (curEpoch promoteAge : Nat) : Word → Prop
| .stamp e a => e = curEpoch ∧ promoteAge ≤ a
| _ => False
/-- `high(int32)`, the seed of commitDead's per-SCC minimum. -/
def bigAge : Nat := 2147483647
/-- Minimum of a list with a default (the `var age = high(int32)` fold). -/
def listMin : List Nat → Nat → Nat
| [], d => d
| a :: l, d => Nat.min a (listMin l d)
theorem listMin_le : ∀ (l : List Nat) (d a : Nat), a ∈ l → listMin l d ≤ a := by
intro l
induction l with
| nil => intro d a ha; cases ha
| cons b t ih =>
intro d a ha
cases List.mem_cons.mp ha with
| inl h =>
simp only [listMin, Nat.min_def]
split <;> omega
| inr h =>
have := ih d a h
simp only [listMin, Nat.min_def]
split <;> omega
theorem listMin_ge : ∀ (l : List Nat) (d b : Nat), b ≤ d →
(∀ x, x ∈ l → b ≤ x) → b ≤ listMin l d := by
intro l
induction l with
| nil => intro d b hd _; simpa [listMin] using hd
| cons a t ih =>
intro d b hd hall
have h1 : b ≤ a := hall a (by simp)
have h2 := ih d b hd (fun x hx => hall x (List.mem_cons_of_mem a hx))
simp only [listMin, Nat.min_def]
split <;> omega
theorem listMin_const (l : List Nat) (d a : Nat) (hne : l ≠ [])
(hall : ∀ x, x ∈ l → x = a) (had : a ≤ d) : listMin l d = a := by
have hlo : a ≤ listMin l d :=
listMin_ge l d a had (fun x hx => by have := hall x hx; omega)
cases l with
| nil => exact absurd rfl hne
| cons b t =>
have hb : b ∈ b :: t := by simp
have hhi := listMin_le (b :: t) d b hb
have := hall b hb
omega
/-- **The change.** commitDead stamps a proven-live SCC with ONE word: the
current epoch and 1 + the age of its YOUNGEST member. -/
def sccAge (w : Obj → Word) (ms : List Obj) : Nat :=
listMin (ms.map (fun m => capturedAge w m)) bigAge + 1
/-- The post-state of commitDead's re-stamp loop, as committed: every
member of the SCC gets the same word, nothing else is touched. -/
structure StampedUniform (w w' : Obj → Word) (e : Nat) (ms : List Obj) : Prop where
members : ∀ m, m ∈ ms → w' m = .stamp e (sccAge w ms)
others : ∀ x, x ∉ ms → w' x = w x
/-- The previous, per-cell scheme, for contrast. -/
structure StampedPerCell (w w' : Obj → Word) (e : Nat) (ms : List Obj) : Prop where
members : ∀ m, m ∈ ms → w' m = .stamp e (capturedAge w m + 1)
others : ∀ x, x ∉ ms → w' x = w x
/-- **A1 Uniformity**: after commit, all members of a stamped SCC carry
the identical claim word — same epoch AND same age. -/
theorem stamped_uniform (w w' : Obj → Word) (e : Nat) (ms : List Obj)
(h : StampedUniform w w' e ms) :
∀ x y, x ∈ ms → y ∈ ms → w' x = w' y := by
intro x y hx hy
rw [h.members x hx, h.members y hy]
/-- **A2 No internal prune**: a capture descends into a member `u` of an
SCC only through an edge that was NOT pruned (or because `u` is a
root, which bypasses stamps entirely). With uniform words, every
other member `v` is then unprunable too — so no INTERNAL edge of the
SCC can be pruned, and the SCC is never tainted `flagPruned` by its
own topology. This is precisely the failure the per-cell age caused. -/
theorem uniform_no_internal_prune
(w : Obj → Word) (curEpoch promoteAge : Nat) (ms : List Obj)
(huni : ∀ x y, x ∈ ms → y ∈ ms → w x = w y)
(u v : Obj) (hu : u ∈ ms) (hv : v ∈ ms)
(hdescended : ¬ prunable curEpoch promoteAge (w u)) :
¬ prunable curEpoch promoteAge (w v) := by
rw [← huni u v hu hv]
exact hdescended
/-- A2 applied to the state commitDead actually leaves behind. -/
theorem committed_scc_no_internal_prune
(w w' : Obj → Word) (e curEpoch promoteAge : Nat) (ms : List Obj)
(hst : StampedUniform w w' e ms)
(u v : Obj) (hu : u ∈ ms) (hv : v ∈ ms)
(hdescended : ¬ prunable curEpoch promoteAge (w' u)) :
¬ prunable curEpoch promoteAge (w' v) :=
uniform_no_internal_prune w' curEpoch promoteAge ms
(stamped_uniform w w' e ms hst) u v hu hv hdescended
/-- **A3 The per-cell scheme diverges**: two members of ONE SCC whose
captured ages differ (the normal case for a structure built
incrementally across collections) end up with different ages. -/
theorem perCell_ages_diverge (w w'' : Obj → Word) (e : Nat) (ms : List Obj)
(hp : StampedPerCell w w'' e ms) (u v : Obj) (hu : u ∈ ms) (hv : v ∈ ms)
(hdiff : capturedAge w u ≠ capturedAge w v) :
ageOf (w'' u) ≠ ageOf (w'' v) := by
rw [hp.members u hu, hp.members v hv]
simp only [ageOf]
omega
/-- ...and diverged ages inside one SCC mean exactly one prunable end of
an internal edge: the promoted member is pruned while its unpromoted
SCC-mate is still being traced. -/
theorem diverged_ages_prune_internally (curEpoch promoteAge au av : Nat)
(hu : au < promoteAge) (hv : promoteAge ≤ av) :
¬ prunable curEpoch promoteAge (.stamp curEpoch au) ∧
prunable curEpoch promoteAge (.stamp curEpoch av) := by
constructor
· intro h
obtain ⟨-, h2⟩ := h
omega
· exact ⟨rfl, hv⟩
/-- **A4 The minimum can only delay a promotion, never hasten one**, so
taking it cannot widen the floating-garbage bound (~2 epochs). -/
theorem uniform_age_le_perCell (w w' w'' : Obj → Word) (e : Nat) (ms : List Obj)
(hu : StampedUniform w w' e ms) (hp : StampedPerCell w w'' e ms)
(m : Obj) (hm : m ∈ ms) :
ageOf (w' m) ≤ ageOf (w'' m) := by
have hmem : capturedAge w m ∈ ms.map (fun x => capturedAge w x) :=
List.mem_map_of_mem hm
have hle := listMin_le (ms.map (fun x => capturedAge w x)) bigAge
(capturedAge w m) hmem
rw [hu.members m hm, hp.members m hm]
simp only [ageOf, sccAge]
omega
/-- Corollary: wherever the SCC-uniform stamp prunes, the per-cell stamp
would have pruned too. Pruning is the only thing a stamp does, so the
change cannot make any capture skip MORE than before. -/
theorem uniform_never_hastens_promotion (w w' w'' : Obj → Word) (e : Nat)
(ms : List Obj) (promoteAge : Nat)
(hu : StampedUniform w w' e ms) (hp : StampedPerCell w w'' e ms)
(m : Obj) (hm : m ∈ ms) (h : promoteAge ≤ ageOf (w' m)) :
promoteAge ≤ ageOf (w'' m) := by
have := uniform_age_le_perCell w w' w'' e ms hu hp m hm
omega
/-- **A5 The uniform age is exactly the common age + 1**, so a surviving
SCC's age advances by one per collection and stays uniform: the
invariant of A1/A2 is inductive. -/
theorem uniform_age_succ (w w' : Obj → Word) (e a : Nat) (ms : List Obj)
(hne : ms ≠ []) (hcap : a ≤ bigAge)
(hall : ∀ m, m ∈ ms → capturedAge w m = a)
(h : StampedUniform w w' e ms) :
∀ m, m ∈ ms → ageOf (w' m) = a + 1 := by
intro m hm
have hmin : listMin (ms.map (fun x => capturedAge w x)) bigAge = a := by
apply listMin_const
· cases ms with
| nil => exact absurd rfl hne
| cons b t => simp
· intro x hx
obtain ⟨y, hy, rfl⟩ := List.mem_map.mp hx
exact hall y hy
· exact hcap
rw [h.members m hm]
simp only [ageOf, sccAge, hmin]
/-- **A6 The freeze**: an SCC that is never re-stamped (the `flagPruned`
taint excludes it from commitDead's stamp loop) keeps its age
forever. Below `YrcPromoteAge` that means it is fully re-traced by
every collection until the epoch turns — the regression A2 removes. -/
theorem age_frozen_if_never_restamped (age : Nat → Nat) (a : Nat)
(h0 : age 0 = a) (hfreeze : ∀ n, age (n + 1) = age n) :
∀ n, age n = a := by
intro n
induction n with
| zero => exact h0
| succ n ih => rw [hfreeze n, ih]
/-- **A7 Progress**: an SCC that IS re-stamped every round promotes after
`YrcPromoteAge` collections, and by A2 stays promoted uniformly — so
a long-lived structure is traced once per epoch, not once per
collection. -/
theorem age_promotes_if_restamped (age : Nat → Nat) (a promoteAge : Nat)
(h0 : age 0 = a) (hstep : ∀ n, age (n + 1) = age n + 1) :
promoteAge ≤ age promoteAge := by
have h : ∀ n, age n = a + n := by
intro n
induction n with
| zero => simpa using h0
| succ n ih => rw [hstep n, ih]; omega
rw [h promoteAge]
omega
/-! ## §B Demand-grown collector slots
`gParSlots` counts the slots IN PLAY. It starts at 1, is raised under
gMergeLock when a thread wants to collect and every slot in play is
busy, and is NEVER lowered. Two things must hold:
(i) a scan over the prefix `0 ..< slotsInPlay()` must never MISS an
active tag — a missed tag would let a second collection claim a
cell another collection already owns, breaking partition
disjointness (yrc_proof.lean §5) and admitting a double free;
(ii) a thread must not park while the table still has room — that was
the throttle the fixed `MaxPar = 8` imposed.
(i) rests on the publication order in startCollection: the wider bound
is stored BEFORE the tag lands in the new slot, and `gParSlots` only
grows. So a load of `slotsInPlay()` ordered AFTER the read of a tagged
claim word is guaranteed to cover the slot that wrote that tag. -/
/-- `gParSlots` never shrinks, so a prefix scan cannot shrink under a
reader either. -/
theorem in_play_persists (parSlots : Nat → Nat)
(hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j)
(k : Nat) (t t' : Nat) (h : t ≤ t') (hk : k < parSlots t) :
k < parSlots t' := by
have := hmono t t' h
omega
/-- **B1 The scan covers the slot that wrote the tag.** `tGrow` is when
the slot was put in play (under gMergeLock), `tTag` the tag store,
`tRead` the reader's load of the claim word, `tScan` its subsequent
load of `slotsInPlay()`. -/
theorem scan_covers_tagged_slot (parSlots : Nat → Nat)
(hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j)
(k : Nat) (tGrow tTag tRead tScan : Nat)
(hgrow : k < parSlots tGrow)
(hpub : tGrow ≤ tTag) -- wider bound published before the tag store
(hread : tTag ≤ tRead) -- the reader observed the tag
(hafter : tRead ≤ tScan) :-- slotsInPlay() loaded AFTER the claim word
k < parSlots tScan := by
have := hmono tGrow tScan (by omega)
omega
/-- **B2 `isActiveTag` is complete**: an active tag is always found by the
prefix scan, so `claimCell` never claims a cell another collection
owns. -/
theorem active_tag_never_missed (parSlots : Nat → Nat)
(tagAt : Nat → Nat → Tag)
(hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j)
(k : Nat) (t : Tag) (tGrow tTag tRead tScan : Nat)
(hgrow : k < parSlots tGrow) (hpub : tGrow ≤ tTag)
(hread : tTag ≤ tRead) (hafter : tRead ≤ tScan)
(hheld : tagAt k tScan = t) :
∃ j, j < parSlots tScan ∧ tagAt j tScan = t :=
⟨k, scan_covers_tagged_slot parSlots hmono k tGrow tTag tRead tScan
hgrow hpub hread hafter, hheld⟩
/-- **B3 The ordering rule is load-bearing**: a `slotsInPlay()` load
ordered BEFORE the read of the claim word can legitimately miss the
slot, because the pool may widen in between. -/
theorem scan_before_read_may_miss :
∃ (parSlots : Nat → Nat) (k : Nat) (tScan tGrow : Nat),
(∀ i j, i ≤ j → parSlots i ≤ parSlots j) ∧ tScan < tGrow ∧
k < parSlots tGrow ∧ ¬ (k < parSlots tScan) := by
refine ⟨fun t => t + 1, 1, 0, 1, ?_, ?_, ?_, ?_⟩
· intro i j h
show i + 1 ≤ j + 1
omega
· decide
· decide
· decide
/-- startCollection's slot decision. -/
inductive SlotOutcome where
| reuse (k : Nat) -- a slot already in play was free
| grow (k : Nat) -- pool widened; the new slot is `k = inPlay`
| park -- table full: MaxPar collections already running
inductive SlotClaim (busy : Nat → Prop) (inPlay maxPar : Nat) : SlotOutcome → Prop where
| reuse (k : Nat) (hk : k < inPlay) (hfree : ¬ busy k) :
SlotClaim busy inPlay maxPar (.reuse k)
| grow (hfull : ∀ k, k < inPlay → busy k) (hroom : inPlay < maxPar) :
SlotClaim busy inPlay maxPar (.grow inPlay)
| park (hfull : ∀ k, k < inPlay → busy k) (hno : maxPar ≤ inPlay) :
SlotClaim busy inPlay maxPar .park
/-- **B4 Parking means saturation**, not throttling: a thread blocks in
`parkUntil(anySlotFree())` only when `MaxPar` collections are running
concurrently. Under the old fixed bound this triggered at the 9th
collecting thread (32 threads vs 8 slots: 6.3s against 2.6s). -/
theorem park_only_when_saturated (busy : Nat → Prop) (inPlay maxPar : Nat)
(h : SlotClaim busy inPlay maxPar .park) :
maxPar ≤ inPlay ∧ ∀ k, k < inPlay → busy k := by
cases h with
| park hfull hno => exact ⟨hno, hfull⟩
/-- **B5 No parking below capacity.** -/
theorem no_park_below_capacity (busy : Nat → Prop) (inPlay maxPar : Nat)
(hroom : inPlay < maxPar) : ¬ SlotClaim busy inPlay maxPar .park := by
intro h
cases h with
| park hfull hno => omega
/-- **B6 A grown slot is fresh**: `k = inPlay` is distinct from every slot
already in play, so the widening thread cannot collide with a
collection that is already running. -/
theorem grown_slot_not_in_play (inPlay k : Nat) (hk : k < inPlay) :
inPlay ≠ k := by omega
/-! ## §C Deferred reclamation
commitDead used to spin until every concurrent capture had ended before
freeing, INSIDE the GC fence. Now the batch is parked in
`gPendingCells` with a watch list `gPendingWatch` of the (slot, tag)
pairs that were in capture phase at commit time, and `releasePending`
— the FIRST thing startCollection does, outside the fence and holding
no lock — waits out that list and then frees.
Three obligations:
(C1) the watch list is COMPLETE: every capture that could hold a stale
`(slot, value)` snapshot of the batch is on it;
(C2) the grace check is SOUND: `graceSatisfied` reports "finished" only
when the watched capture really has finished;
(C3) the batch is PROTECTED while parked: no foreign capture may claim
(and hence free) one of its cells. This is why finishCollection
clears only `gSlotPhase` and leaves the tag in `gActiveTags`. -/
/-- One slot's published state. -/
structure SlotState where
tag : Tag
phase : Nat -- 0 idle, 1 capturing, 2 committing
/-- finishCollection with a batch parked: phase → 0, tag RETAINED. -/
def finishParked (st : SlotState) : SlotState := { st with phase := 0 }
/-- releasePending, after the grace wait: the tag is given up first, then
the destructors and `nimRawDispose` run. -/
def releaseSlot (st : SlotState) : SlotState := { st with tag := 0 }
theorem finishParked_keeps_tag (st : SlotState) :
(finishParked st).tag = st.tag := rfl
/-- A parked slot blocks nobody's grace period: its phase is 0, so every
other collector's `graceSatisfied` passes over it. -/
theorem parked_slot_blocks_nobody (st : SlotState) (tg : Tag) :
¬ ((finishParked st).tag = tg ∧ (finishParked st).phase = 1) := by
intro h
simp [finishParked] at h
/-- ...yet the tag survives, which is what protects the parked cells. -/
theorem parked_slot_still_tagged (st : SlotState) (t : Tag) (h : st.tag = t) :
(finishParked st).tag = t := h
/-- `gPendingWatch`, as `(slot shl 32) or tag` pairs. -/
abbrev WatchList := List (Nat × Tag)
/-- `graceSatisfied()` evaluated at time `t`. -/
def graceSatisfied (tagAt : Nat → Nat → Tag) (phaseAt : Nat → Nat → Nat)
(W : WatchList) (t : Nat) : Prop :=
∀ p, p ∈ W → ¬ (tagAt p.1 t = p.2 ∧ phaseAt p.1 t = 1)
/-- **C1 The watch list is complete.** A capture that was in flight at
commit time is running on a slot that was in play when its tag was
stored; by B1 the `buildPendingWatch` scan — which loads
`slotsInPlay()` after reading the claim state — covers that slot, and
the capture's phase is 1, so it is recorded. -/
theorem watch_covers_inflight_capture (parSlots : Nat → Nat)
(tagAt : Nat → Nat → Tag) (phaseAt : Nat → Nat → Nat)
(hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j)
(s : Nat) (tg : Tag) (tGrow tTag commitT : Nat)
(hgrow : s < parSlots tGrow) (hpub : tGrow ≤ tTag) (hread : tTag ≤ commitT)
(hcapturing : tagAt s commitT = tg ∧ phaseAt s commitT = 1) :
s < parSlots commitT ∧ tagAt s commitT = tg ∧ phaseAt s commitT = 1 :=
⟨scan_covers_tagged_slot parSlots hmono s tGrow tTag commitT commitT
hgrow hpub hread (Nat.le_refl commitT), hcapturing.1, hcapturing.2⟩
/-- **C2 The grace check is sound**: if `graceSatisfied` holds at `t` and
a watched capture was still running at `t`, we have a contradiction —
so every watched capture finished strictly before `t`. There is no
ABA on the (slot, tag) pair: tags come from a monotonic counter
(yrc_proof.lean §5 `tags_distinct`), so a later collection on the
same slot carries a different tag. -/
theorem grace_check_sound (tagAt : Nat → Nat → Tag) (phaseAt : Nat → Nat → Nat)
(W : WatchList) (s : Nat) (tg : Tag) (start finish t : Nat)
(hw : (s, tg) ∈ W)
(hcap : ∀ u, start ≤ u → u ≤ finish → tagAt s u = tg ∧ phaseAt s u = 1)
(hstart : start ≤ t)
(hsat : graceSatisfied tagAt phaseAt W t) :
finish < t := by
cases Nat.lt_or_ge finish t with
| inl h => exact h
| inr h => exact absurd (hcap t hstart h) (hsat (s, tg) hw)
/-- A capture's window and the values it ever snapshots (TraceEntry), as
in yrc_proof.lean §6. -/
structure CaptureWindow where
start : Nat
finish : Nat
snap : Obj → Prop
derefs : Obj → Nat → Prop
/-- **C3 Grace safety survives the deferral.** `commitT` is when the dead
set validated, `releaseT` when releasePending's wait succeeded (C2),
`freeT` when the batch is actually disposed. The only change from
yrc_proof.lean's `grace_no_use_after_free` is that `freeT` moved
LATER — the wait is unchanged in strength, it just happens off the
commit path. -/
theorem deferred_grace_no_use_after_free
(C : CaptureWindow) (D : Obj → Prop) (commitT releaseT freeT : Nat)
(h_deref : ∀ x t, C.derefs x t → C.start ≤ t ∧ t ≤ C.finish ∧ C.snap x)
(h_watched : C.start < commitT → C.finish < releaseT)
(h_release : releaseT ≤ freeT)
(h_miss : commitT ≤ C.start → ∀ x, D x → ¬ C.snap x) :
∀ x t, D x → C.derefs x t → t < freeT := by
intro x t hD hd
obtain ⟨h1, h2, h3⟩ := h_deref x t hd
cases Nat.lt_or_ge C.start commitT with
| inl h => have := h_watched h; omega
| inr h => exact absurd h3 (h_miss h x hD)
/-- claimCell's decision on a cell, as a relation over its claim word. -/
inductive ClaimResult where
| mine -- our own tag: already captured this round
| refuse -- owned by another ACTIVE collection (-1, crossPend)
| prune -- proven live this epoch (-2, opaque live external)
| claim -- CAS it into our partition
inductive ClaimDecision (myTag curEpoch promoteAge : Nat) (active : Tag → Prop) :
Word → ClaimResult → Prop where
| mine (t : Tag) (h : t = myTag) :
ClaimDecision myTag curEpoch promoteAge active (.tag t) .mine
| refuse (t : Tag) (hne : t ≠ myTag) (ha : active t) :
ClaimDecision myTag curEpoch promoteAge active (.tag t) .refuse
| claimTag (t : Tag) (hne : t ≠ myTag) (ha : ¬ active t) :
ClaimDecision myTag curEpoch promoteAge active (.tag t) .claim
| prune (e a : Nat) (hp : prunable curEpoch promoteAge (.stamp e a)) :
ClaimDecision myTag curEpoch promoteAge active (.stamp e a) .prune
| claimStamp (e a : Nat) (hp : ¬ prunable curEpoch promoteAge (.stamp e a)) :
ClaimDecision myTag curEpoch promoteAge active (.stamp e a) .claim
| claimFresh :
ClaimDecision myTag curEpoch promoteAge active .fresh .claim
/-- **C4 A cell carrying an active foreign tag is always refused.** -/
theorem tagged_cell_refused (myTag curEpoch promoteAge : Nat) (active : Tag → Prop)
(ownerTag : Tag) (hne : ownerTag ≠ myTag) (ha : active ownerTag)
(r : ClaimResult)
(h : ClaimDecision myTag curEpoch promoteAge active (.tag ownerTag) r) :
r = .refuse := by
cases h with
| mine t ht => exact absurd ht hne
| refuse t hne' ha' => rfl
| claimTag t hne' ha' => exact absurd ha ha'
/-- **C5 No double free while parked.** The parked cells still carry the
parking collection's tag, and finishCollection left that tag in
`gActiveTags` (only the phase was cleared, C-`finishParked`). So a
foreign capture that reaches a parked cell through a stale snapshot
refuses it: it can neither traverse it nor claim it, hence never
classifies it dead and never frees it. Without the tag retention this
is exactly a double free — the batch's owner will free it too. -/
theorem no_foreign_claim_while_parked
(activeAt : Nat → Tag → Prop) (ownerTag myTag : Tag)
(curEpoch promoteAge : Nat) (commitT releaseT u : Nat)
(hretain : ∀ v, commitT ≤ v → v ≤ releaseT → activeAt v ownerTag)
(hne : ownerTag ≠ myTag) (h1 : commitT ≤ u) (h2 : u ≤ releaseT)
(r : ClaimResult)
(h : ClaimDecision myTag curEpoch promoteAge (activeAt u) (.tag ownerTag) r) :
r = .refuse :=
tagged_cell_refused myTag curEpoch promoteAge (activeAt u) ownerTag hne
(hretain u h1 h2) r h
/-- **C6 Deferring the free is safe.** The batch was closed (unreachable)
at commit time — that is what validation established (yrc_proof.lean
§4 `validated_closed`) — and `hstable` is exactly
yrc_proof.lean §3 `garbage_stability`: a closed set stays closed
under every mutator step, allocation and foreign free. Freeing one
collection later therefore satisfies the same §1 free condition as
freeing immediately. -/
theorem deferred_free_safe (unreachable : Nat → Obj → Prop) (D : Obj → Prop)
(commitT freeT : Nat)
(hcommit : ∀ x, D x → unreachable commitT x)
(hstable : ∀ x t t', D x → t ≤ t' → unreachable t x → unreachable t' x)
(hlater : commitT ≤ freeT) :
∀ x, D x → unreachable freeT x :=
fun x hx => hstable x commitT freeT hx hlater (hcommit x hx)
/-- **C7 The grace wait left the GC fence.** It now runs at the start of
startCollection, before `yrcGcFenceEnter`, so no mutator seq
operation can be stalled by it — the property the deferral was made
for. -/
theorem grace_wait_outside_fence (waitStart waitEnd fenceEnter fenceExit t : Nat)
(horder : waitEnd < fenceEnter) (hw : waitStart ≤ t ∧ t ≤ waitEnd) :
¬ (fenceEnter ≤ t ∧ t ≤ fenceExit) := by
intro hf
omega
/-- `waits a b`: thread `a` is blocked in releasePending on thread `b`'s
capture. -/
def waits (capturing releasing : Nat → Prop) (a b : Nat) : Prop :=
releasing a ∧ capturing b
/-- **C8 The new wait cannot deadlock.** releasePending runs BEFORE this
thread claims a slot, so a releasing thread is never itself
capturing; the wait-for graph therefore has depth one and cannot
contain a cycle of any length. (Captures never wait on anything:
claimCell returns -1 immediately on contention.) -/
theorem release_wait_depth_one (capturing releasing : Nat → Prop)
(hexcl : ∀ t, releasing t → ¬ capturing t)
(a b c : Nat) (h1 : waits capturing releasing a b) :
¬ waits capturing releasing b c := by
intro h2
exact hexcl b h2.1 h1.2
/-- Corollary: no 2-cycle, hence no mutual wait between two parked
collectors. -/
theorem release_wait_acyclic (capturing releasing : Nat → Prop)
(hexcl : ∀ t, releasing t → ¬ capturing t) (a b : Nat)
(h1 : waits capturing releasing a b) :
¬ waits capturing releasing b a :=
release_wait_depth_one capturing releasing hexcl a b a h1
/-! ## Summary of verified properties (all QED, no sorry)
§A `stamped_uniform` — a committed SCC's members carry one identical
claim word.
`uniform_no_internal_prune`, `committed_scc_no_internal_prune` — a
capture that descends into a member cannot prune an internal edge,
so an SCC is never tainted `flagPruned` by its own topology.
`perCell_ages_diverge` + `diverged_ages_prune_internally` — the
pre-fix scheme admits exactly that taint.
`uniform_age_le_perCell`, `uniform_never_hastens_promotion` — the
minimum only delays promotions, so the float bound is unchanged.
`uniform_age_succ` — uniformity is inductive: age advances by one
and stays uniform.
`age_frozen_if_never_restamped` / `age_promotes_if_restamped` — the
frozen-age regression versus the intended once-per-epoch trace.
§B `in_play_persists`, `scan_covers_tagged_slot`,
`active_tag_never_missed` — a growing `gParSlots` prefix scan never
misses an active tag, PROVIDED `slotsInPlay()` is loaded after the
claim word; `scan_before_read_may_miss` shows the order is
load-bearing.
`park_only_when_saturated`, `no_park_below_capacity`,
`grown_slot_not_in_play` — a collector parks only when `MaxPar`
collections run at once, and a widened slot collides with nobody.
§C `watch_covers_inflight_capture` — the watch list records every
capture that could hold a stale snapshot of the batch (via §B).
`grace_check_sound` — `graceSatisfied` reports "finished" only when
the watched capture has finished.
`deferred_grace_no_use_after_free` — no capture dereferences a
parked cell at or after its free time.
`tagged_cell_refused`, `no_foreign_claim_while_parked` — retaining
the tag (finishCollection clears only the phase) is what prevents a
foreign collection from claiming and freeing a parked cell.
`parked_slot_blocks_nobody`, `parked_slot_still_tagged` — the two
halves of that split: protection without blocking.
`deferred_free_safe` — deferring the free preserves the §1 free
condition, by garbage stability.
`grace_wait_outside_fence` — the wait no longer overlaps the GC
fence, so it cannot stall a mutator's seq operation.
`release_wait_depth_one`, `release_wait_acyclic` — the new wait
adds no cycle to the wait-for structure of yrc_proof.lean §8.
## What is NOT proved
• Slot-retention liveness. A parked batch holds its tag slot until the
owning thread's NEXT collection (or GC_runOrc / nimYrcThreadTeardown,
both of which call releasePending). A thread that parks a batch and
then never collects again keeps a slot occupied; with enough such
threads the table could saturate and other collectors would park
(§B4). Bounded in practice by `MaxPar = 256` and by teardown, not
formalized.
• That `buildPendingWatch` returning false (nothing capturing) really
is the common case — a performance claim, measured, not proved.
• Destructor timing. Deferral runs a dead batch's destructors one
collection later. Safety is C6; the observable-behaviour claim
("nothing else observes the delay, the cells are unreachable and
their references already dropped") is an argument about the Nim
language semantics, not modelled here.
• Conservatism of tag retention. While a batch is parked, the tag also
protects SURVIVORS that kept a stale tag (dirty and pruned SCCs are
deliberately not re-stamped), so a foreign capture refuses them for
one extra collection. That delays their re-examination; it cannot
lose them, because §A's E1–E4 hooks keep a dec-witness registered.
• Everything already listed as unproved in yrc_proof.lean (rc-exactness
mechanics, the C11 memory model, liveness/completeness of the retry
loop, tag wrap-around).
-/

33
lib/system/yrc_proof.lean
View File

@@ -459,9 +459,18 @@ theorem cross_target_live (D : Obj → Prop) (claimedB : Obj → Prop)
A concurrent capture holds raw `(slot, value)` snapshots (TraceEntry);
the value pointer is dereferenced later (header read in claimCell). A
capture that overlapped our validation may have snapshotted a slot
that USED to point into our dead set. commitDead therefore waits, for
every other slot that is in capture phase (gSlotPhase == 1), until
that capture ends — captures never wait on anyone, so this is bounded.
that USED to point into our dead set. The dead batch must therefore
outlive every other slot that was in capture phase (gSlotPhase == 1)
at commit time — captures never wait on anyone, so this is bounded.
commitDead no longer BLOCKS on that: it parks the batch
(`gPendingCells`) with a watch list of those captures and
`releasePending` frees it at the start of this thread's next
collection, off the commit path and outside the GC fence. The parking
collection's tag stays in `gActiveTags` so a foreign capture cannot
claim a parked cell. See yrc_opt_proof.lean §C for the model of the
deferral; the theorems below are the invariant it preserves, with the
free time merely moved later.
Two obligations:
(a) captures that started BEFORE our commit are waited out — temporal
@@ -498,9 +507,10 @@ structure CaptureWindow where
/-- **Grace safety**: no capture dereferences a dead cell at or after
its free time. `commitT` is when the dead set validated; `freeT` is
when commitDead's free loop runs. The premises are exactly the
protocol: (grace) commitDead's spin means any capture that started
before commit has finished before we free; (miss) §6(b) above. -/
when the free loop runs (in releasePending, one collection later).
The premises are exactly the protocol: (grace) the watch list means
any capture that started before commit has finished before we free;
(miss) §6(b) above. -/
theorem grace_no_use_after_free
(C : CaptureWindow) (D : Obj → Prop) (commitT freeT : Nat)
(h_deref : ∀ x t, C.derefs x t → C.start ≤ t ∧ t ≤ C.finish ∧ C.snap x)
@@ -676,8 +686,8 @@ theorem no_deadlock_from_total_order {n : Nat}
referenced across a partition boundary is never freed by its
owner this round (soundness of claimCell's -1 + crossPend).
§6 `post_commit_snap_misses_dead`, `grace_no_use_after_free` — with
commitDead's grace spin, no capture ever dereferences freed
memory.
the grace period (now enforced by the deferred batch's watch list,
yrc_opt_proof.lean §C), no capture ever dereferences freed memory.
§7 `fence_mutual_exclusion` — the SEQ_CST Dekker pairing in
seqs_v2.nim excludes seq structure mutation during collection.
§8 `lockLevel_injective`, `mergeLock_level_min`,
@@ -714,7 +724,12 @@ theorem no_deadlock_from_total_order {n : Nat}
Commit re-stamps proven-live cells with (epochBase|epoch, survivalAge)
in the claim word; a capture treats a current-epoch stamp of age ≥
YrcPromoteAge on a DESCENDANT as an opaque live external and does not
descend. Soundness needs no new lemmas: a pruned cell is simply an
descend. The age is the SCC's, not the cell's — every member is
stamped with the age of the SCC's YOUNGEST member, so promotion is
all-or-nothing and no INTERNAL edge is ever pruned; see
yrc_opt_proof.lean §A, which also shows the minimum can only delay a
promotion, so the float bound below is unaffected. Soundness needs no
new lemmas: a pruned cell is simply an
uncaptured cell, so the captured set shrinks and every §3–§6 statement
quantifies over a smaller S. Pruning can only ADD unexplained external
refs to captured SCCs (a pruned predecessor's refs are never explained