mirror of
https://github.com/nim-lang/Nim.git
synced 2026-07-31 20:49:06 +00:00
YRC: use a side-table for topology (#26022)
- Much better locking scheme - Run concurrently with the mutators - Thread local collections - Tarjan's algorithm for cycle collection
This commit is contained in:
Andreas Rumpf
@@ -25,31 +25,55 @@ when defined(gcYrc):
|
||||
HasCollectorLock
|
||||
Collecting
|
||||
|
||||
AlignedRwLock = object
|
||||
## One RwLock per cache line. {.align: 64.} causes the compiler to round
|
||||
## the struct size up to 64 bytes, so consecutive array elements never
|
||||
## share a cache line (sizeof(RwLock) = 56 on Linux x86_64 → 8 byte pad).
|
||||
lock {.align: 64.}: RwLock
|
||||
AlignedCounter = object
|
||||
## one counter per cache line to avoid false sharing between stripes
|
||||
c {.align: 64.}: int
|
||||
|
||||
# Asymmetric two-class exclusion: seq structure mutations and collections
|
||||
# exclude each other, but seq ops run concurrently with seq ops and
|
||||
# collections run concurrently with collections. This replaces the old
|
||||
# RwLock scheme (which allowed only ONE collector, serializing parallel
|
||||
# collection) and also sidesteps POSIX's requirement that a rwlock be
|
||||
# unlocked by its acquiring thread.
|
||||
var
|
||||
gYrcLocks: array[NumLockStripes, AlignedRwLock]
|
||||
gSeqActive: array[NumLockStripes, AlignedCounter] # in-flight seq ops
|
||||
gGcActive: int # active collections
|
||||
var
|
||||
lockState {.threadvar.}: YrcLockState
|
||||
|
||||
proc getYrcStripe(): int {.inline.} =
|
||||
## Map this thread to one of the NumLockStripes RwLock stripes.
|
||||
## Map this thread to one of the NumLockStripes counter stripes.
|
||||
## getThreadId() is already cached thread-locally in threadids.nim.
|
||||
getThreadId() and (NumLockStripes - 1)
|
||||
|
||||
proc acquireMutatorLock() {.compilerRtl, inl.} =
|
||||
if lockState == HasNoLock:
|
||||
acquireRead gYrcLocks[getYrcStripe()].lock
|
||||
let s = getYrcStripe()
|
||||
while true:
|
||||
# SEQ_CST inc-then-check pairs with the collector's SEQ_CST
|
||||
# inc-then-drain (Dekker-style store/load ordering)
|
||||
discard atomicFetchAdd(addr gSeqActive[s].c, 1, ATOMIC_SEQ_CST)
|
||||
if atomicLoadN(addr gGcActive, ATOMIC_SEQ_CST) == 0: break
|
||||
discard atomicFetchSub(addr gSeqActive[s].c, 1, ATOMIC_SEQ_CST)
|
||||
while atomicLoadN(addr gGcActive, ATOMIC_ACQUIRE) != 0:
|
||||
discard
|
||||
lockState = HasMutatorLock
|
||||
|
||||
proc releaseMutatorLock() {.compilerRtl, inl.} =
|
||||
if lockState == HasMutatorLock:
|
||||
lockState = HasNoLock
|
||||
releaseRead gYrcLocks[getYrcStripe()].lock
|
||||
discard atomicFetchSub(addr gSeqActive[getYrcStripe()].c, 1, ATOMIC_SEQ_CST)
|
||||
|
||||
proc yrcGcFenceEnter() =
|
||||
## A collection announces itself and waits for in-flight seq structure
|
||||
## mutations to drain. Multiple collections may hold the fence at once.
|
||||
discard atomicFetchAdd(addr gGcActive, 1, ATOMIC_SEQ_CST)
|
||||
for s in 0 ..< NumLockStripes:
|
||||
while atomicLoadN(addr gSeqActive[s].c, ATOMIC_SEQ_CST) > 0:
|
||||
discard
|
||||
|
||||
proc yrcGcFenceExit() =
|
||||
discard atomicFetchSub(addr gGcActive, 1, ATOMIC_SEQ_CST)
|
||||
|
||||
template yrcMutatorLock*(t: typedesc; body: untyped) =
|
||||
{.noSideEffect.}:
|
||||
@@ -71,23 +95,6 @@ when defined(gcYrc):
|
||||
{.noSideEffect.}:
|
||||
releaseMutatorLock()
|
||||
|
||||
template yrcCollectorLock(body: untyped) =
|
||||
if lockState == HasMutatorLock: releaseMutatorLock()
|
||||
let prevState = lockState
|
||||
let hadToAcquire = prevState < HasCollectorLock
|
||||
if hadToAcquire:
|
||||
# Acquire all stripes in ascending order — the only thread ever holding
|
||||
# multiple write locks is the collector, so there is no lock-order cycle.
|
||||
for yrcI in 0..<NumLockStripes:
|
||||
acquireWrite(gYrcLocks[yrcI].lock)
|
||||
lockState = HasCollectorLock
|
||||
try:
|
||||
body
|
||||
finally:
|
||||
if hadToAcquire:
|
||||
for yrcI in 0..<NumLockStripes:
|
||||
releaseWrite(gYrcLocks[yrcI].lock)
|
||||
lockState = prevState
|
||||
|
||||
else:
|
||||
template yrcMutatorLock*(t: typedesc; body: untyped) =
|
||||
|
||||
@@ -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
|
||||
|
||||
1472
lib/system/yrc.nim
1472
lib/system/yrc.nim
File diff suppressed because it is too large
Load Diff
@@ -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,597 @@ 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 queue producers went lock-free (reserve a slot by fetch-add, then
|
||||
publish it: incs with an RMW exchange — the validation peek must see
|
||||
every completed inc barrier — decs with a release store of the desc,
|
||||
self-protecting via the unexplained rc surplus). The validation peek
|
||||
is lock-free too. What remains:
|
||||
• gMergeLock (level 0: tag-slot claim + orphan roots)
|
||||
• stripes[i].consumerLock (level i + 1, i in 0..N-1: excludes
|
||||
DRAINS of the same stripe against each
|
||||
other — drains wait out the two-store
|
||||
publication window and close each batch
|
||||
with a CAS, so no producer coordination
|
||||
is needed)
|
||||
• 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 < consumerLock[0] < consumerLock[1] < ...
|
||||
|
||||
In fact the current paths never HOLD two of these at once — strictly
|
||||
stronger than the ascending-order requirement the theorem needs:
|
||||
|
||||
**nimIncRefCyclic / nimAsgnYrc / nimSinkYrc / enqueueDec /
|
||||
registerLocal / markDirtyFromQueues**: lock-free, no locks at all;
|
||||
enqueueDec's overflow calls collectCycles with nothing held. ✓
|
||||
**drainStripe**: consumerLock[i] alone; the processing inside
|
||||
(trialDec, registerLocal into the thread-local buffer) takes no
|
||||
lock. drainAllStripes: consumerLock[i] ascending, released between
|
||||
stripes. ✓
|
||||
**startCollection / nimYrcThreadTeardown**: drain first (consumerLock,
|
||||
released), THEN gMergeLock for the slot claim / orphan spill —
|
||||
sequential, never nested. adoptOrphans: gMergeLock alone. ✓
|
||||
**validateDead / commitDead**: no locks (candidate re-registration is
|
||||
the lock-free registerLocal). ✓
|
||||
|
||||
### 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
|
||||
| lockInc (i : Nat) (h : i < n) : LockId n
|
||||
| lockDec (i : Nat) (h : i < n) : LockId n
|
||||
| mergeLock : LockId n
|
||||
| consumerLock (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
|
||||
| .lockInc i _ => 2 * i + 1
|
||||
| .lockDec i _ => 2 * i + 2
|
||||
| .mergeLock => 0
|
||||
| .consumerLock i _ => i + 1
|
||||
|
||||
/-- 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
|
||||
| lockInc j hj => simp [lockLevel] at h
|
||||
| lockDec j hj => simp [lockLevel] at h
|
||||
| lockInc i hi =>
|
||||
| mergeLock => rfl
|
||||
| consumerLock j hj => simp [lockLevel] at h
|
||||
| consumerLock i hi =>
|
||||
cases b with
|
||||
| global => 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
|
||||
| lockInc j hj => simp [lockLevel] at h; omega
|
||||
| lockDec j hj =>
|
||||
have : i = j := by simp [lockLevel] at h; omega
|
||||
| mergeLock => simp [lockLevel] at h
|
||||
| consumerLock j hj =>
|
||||
have : i = j := by simp [lockLevel] at h; exact h
|
||||
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
|
||||
| lockInc i hi => simp [lockLevel]
|
||||
| lockDec i hi => simp [lockLevel]
|
||||
| mergeLock => exact absurd rfl h
|
||||
| consumerLock 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).
|
||||
• 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`).
|
||||
|
||||
4. `src_safe_in_window`: Even between the atomic store and
|
||||
the buffered inc, the collector cannot free src.
|
||||
## Epoch stamps (generational pruning)
|
||||
|
||||
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).
|
||||
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
|
||||
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
|
||||
by internal/deadIn), so it can force a false "live", never a false
|
||||
"dead" — the conservative direction. Completeness (bounded float,
|
||||
≤ ~2 epochs) rests on four hooks, each keeping a dec-witness
|
||||
registered:
|
||||
E1 roots never prune: a registered candidate is always fully
|
||||
root-scanned, stamps notwithstanding;
|
||||
E2 an SCC that pruned an out-edge and survives keeps one member
|
||||
registered (flagPruned) — its "live" verdict may lean on a stamp
|
||||
that went stale within the epoch;
|
||||
E3 a commit-time dec into a stamped cell re-registers the target —
|
||||
the dec may be the death blow to a cell no collection analyzed;
|
||||
E4 explicit full collects advance the epoch first, so all stamps
|
||||
are stale and nothing is pruned.
|
||||
Not formalized. Also noted: the epoch clock counts collections, and
|
||||
short epochs (≲ 4) resonate with the adaptive threshold — pruned
|
||||
collections are cheap, so collections and hence epoch turns speed up,
|
||||
re-tracing MORE than with no stamps; a work-based clock would fix it.
|
||||
|
||||
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.
|
||||
-/
|
||||
|
||||
594
lib/system/yrc_tarjan_proof.lean
Normal file
594
lib/system/yrc_tarjan_proof.lean
Normal file
@@ -0,0 +1,594 @@
|
||||
/-
|
||||
Tarjan-based deadness computation — correctness proof
|
||||
=====================================================
|
||||
Self-contained, no Mathlib. Checked with Lean 4 (v4.32.0).
|
||||
|
||||
Companion to yrc_proof.lean; models the NOVEL part of yrc.nim's
|
||||
collector: cycle detection via a single Tarjan SCC traversal plus one
|
||||
linear reverse scan over the condensation, replacing Bacon-style trial
|
||||
deletion (three traversals: markGray / scan / collectWhite).
|
||||
|
||||
## The algorithm (capture / computeDeadness in yrc.nim)
|
||||
|
||||
`capture` runs an iterative Tarjan DFS from the candidate roots. Each
|
||||
visited cell is claimed (dense index in the header), its rc word is
|
||||
snapshotted, and every traversed slot contributes one edge record.
|
||||
SCCs are numbered 0, 1, 2, … in POP (completion) order. Tarjan's
|
||||
invariant: when an SCC is completed, every SCC it points to was
|
||||
completed earlier — so every condensation cross edge goes from a
|
||||
HIGHER SCC id to a LOWER one ("sinks first").
|
||||
|
||||
`computeDeadness` then makes ONE pass s = nScc−1 … 0 (sources before
|
||||
sinks, since in-edges come from higher ids):
|
||||
|
||||
ext(s) = sumRefs(s) − internal(s) − deadIn(s)
|
||||
if not forcedLive(s) and ext(s) == 0:
|
||||
s is DEAD; for each cross edge s → t: deadIn(t) += 1
|
||||
else:
|
||||
s is LIVE; for each cross edge s → t: forcedLive(t) := true
|
||||
|
||||
where sumRefs(s) = Σ rc over members, internal(s) = # captured edges
|
||||
within s, and forcedLive is seeded from cells still registered in the
|
||||
roots buffer (inRootsFlag).
|
||||
|
||||
## What we prove
|
||||
|
||||
Fix the SPEC of liveness on the condensation: an SCC is live iff it
|
||||
has an external reference, a roots-buffer seed, or a captured cross
|
||||
edge from a live SCC (`LiveScc`, an inductive definition).
|
||||
|
||||
1. `scan_dead_iff_not_live` — any deadness assignment satisfying the
|
||||
scan's per-SCC equation (well-defined thanks to the sinks-first
|
||||
edge order) marks an SCC dead IFF it is not live. Soundness AND
|
||||
completeness in one theorem: the single reverse scan computes the
|
||||
garbage set EXACTLY on the captured snapshot.
|
||||
2. `impl_fixpoint_is_spec` — the implementation's ARITHMETIC form
|
||||
(ext = sumRefs − internal − deadIn with forcedLive propagation) is
|
||||
the same equation, given rc-exactness (sumRefs = external +
|
||||
internal + cross-in; established by merge + commit validation, see
|
||||
yrc_proof.lean §4).
|
||||
3. Cell-level bridge: `tarjan_sound` — cells of dead SCCs are
|
||||
unreachable in the snapshot; `tarjan_complete` — every captured
|
||||
garbage cell IS marked dead (this needs strong connectivity of the
|
||||
SCCs and exactness of the external counts; Bacon needs his second
|
||||
and third traversals for the same guarantee).
|
||||
4. `demotion_closure_sound` — validate-time demotion (an SCC dropped
|
||||
from the dead set because a mutator dirtied it) must PROPAGATE
|
||||
along captured cross edges: the freed set stays closed only if the
|
||||
demoted set is successor-closed within the dead set. A demoted SCC
|
||||
survives with its out-edges intact, so any still-dead target would
|
||||
be freed while a surviving cell points at it.
|
||||
|
||||
## What is assumed (and where it is discharged)
|
||||
|
||||
• The sinks-first edge order (`horder`) — Tarjan's classical
|
||||
invariant; the DFS itself is not modeled.
|
||||
• rc-exactness (`hcount`) — discharged operationally by yrc_proof §4
|
||||
(merge + dirty check + rc-word recheck).
|
||||
• That `capture` records exactly the heap edges among captured cells
|
||||
and that SCC members are mutually reachable (`h_edge_resp`,
|
||||
`h_conn`, `h_cross_real`) — properties of the traversal + Tarjan.
|
||||
-/
|
||||
|
||||
abbrev Obj := Nat
|
||||
|
||||
/-! ## §1 Descending induction
|
||||
|
||||
The scan processes higher SCC ids first; every recursive dependency
|
||||
of `dead s` is on some `u > s`. This induction principle is the
|
||||
well-definedness of the whole scheme. -/
|
||||
|
||||
theorem descending_induction {n : Nat} (P : Fin n → Prop)
|
||||
(step : ∀ s : Fin n, (∀ u : Fin n, s < u → P u) → P s) :
|
||||
∀ s, P s := by
|
||||
have key : ∀ k, ∀ s : Fin n, n - s.val ≤ k → P s := by
|
||||
intro k
|
||||
induction k with
|
||||
| zero =>
|
||||
intro s hs
|
||||
have := s.isLt
|
||||
omega
|
||||
| succ k ih =>
|
||||
intro s _
|
||||
apply step
|
||||
intro u hu
|
||||
apply ih
|
||||
have h1 := u.isLt
|
||||
have h2 : s.val < u.val := hu
|
||||
omega
|
||||
intro s
|
||||
exact key n s (by omega)
|
||||
|
||||
/-! ## §2 The condensation and the liveness spec
|
||||
|
||||
`edges` are the captured condensation cross edges (with multiplicity:
|
||||
one entry per traversed slot, exactly like cap.edges bucketed into
|
||||
crossTgt). `extRefs s` counts references into SCC `s` from OUTSIDE
|
||||
the capture: stack refs, uncaptured heap cells, other collections'
|
||||
partitions — everything in Σrc not explained by captured edges.
|
||||
`seed s` is the inRootsFlag forcedLive seeding. -/
|
||||
|
||||
section Condensation
|
||||
|
||||
variable {n : Nat}
|
||||
variable (edges : List (Fin n × Fin n))
|
||||
variable (extRefs : Fin n → Nat)
|
||||
variable (seed : Fin n → Bool)
|
||||
|
||||
/-- The SPEC: an SCC is live iff something external anchors it —
|
||||
directly or through a chain of captured cross edges. -/
|
||||
inductive LiveScc : Fin n → Prop where
|
||||
| ext (s : Fin n) : 0 < extRefs s → LiveScc s
|
||||
| root (s : Fin n) : seed s = true → LiveScc s
|
||||
| pred (u s : Fin n) : (u, s) ∈ edges → LiveScc u → LiveScc s
|
||||
|
||||
/-- The per-SCC equation the reverse scan establishes: dead iff no
|
||||
external refs, no seed, and ALL cross predecessors dead. (The
|
||||
sinks-first order makes this a valid definition: every predecessor
|
||||
has a higher id and is decided first — see `descending_induction`;
|
||||
without that order the "definition" would be circular.) -/
|
||||
def ScanEq (dead : Fin n → Bool) : Prop :=
|
||||
∀ s, dead s = true ↔
|
||||
(extRefs s = 0 ∧ seed s = false ∧
|
||||
∀ e ∈ edges, e.2 = s → dead e.1 = true)
|
||||
|
||||
/-- Live SCCs are never marked dead (soundness direction). -/
|
||||
theorem live_not_dead (dead : Fin n → Bool)
|
||||
(hfix : ScanEq edges extRefs seed dead) :
|
||||
∀ s, LiveScc edges extRefs seed s → dead s ≠ true := by
|
||||
intro s hl
|
||||
induction hl with
|
||||
| ext s h =>
|
||||
intro hd
|
||||
have := ((hfix s).mp hd).1
|
||||
omega
|
||||
| root s h =>
|
||||
intro hd
|
||||
have := ((hfix s).mp hd).2.1
|
||||
rw [h] at this
|
||||
cases this
|
||||
| pred u s hmem _ ih =>
|
||||
intro hd
|
||||
exact ih (((hfix s).mp hd).2.2 (u, s) hmem rfl)
|
||||
|
||||
/-- Non-live SCCs are always marked dead (completeness direction) —
|
||||
by descending induction along the scan order. -/
|
||||
theorem not_live_dead
|
||||
(horder : ∀ e ∈ edges, e.2 < e.1)
|
||||
(dead : Fin n → Bool)
|
||||
(hfix : ScanEq edges extRefs seed dead) :
|
||||
∀ s, ¬ LiveScc edges extRefs seed s → dead s = true := by
|
||||
refine descending_induction
|
||||
(fun s => ¬ LiveScc edges extRefs seed s → dead s = true) ?_
|
||||
intro s ihs hnl
|
||||
rw [hfix]
|
||||
refine ⟨?_, ?_, ?_⟩
|
||||
· cases Nat.eq_zero_or_pos (extRefs s) with
|
||||
| inl h => exact h
|
||||
| inr h => exact absurd (LiveScc.ext s h) hnl
|
||||
· cases hsd : seed s with
|
||||
| false => rfl
|
||||
| true => exact absurd (LiveScc.root s hsd) hnl
|
||||
· intro e he hes
|
||||
have hlt : s < e.1 := by
|
||||
have := horder e he
|
||||
rw [hes] at this
|
||||
exact this
|
||||
apply ihs e.1 hlt
|
||||
intro hlu
|
||||
have hmem : (e.1, s) ∈ edges := by
|
||||
rw [← hes]
|
||||
simpa using he
|
||||
exact hnl (LiveScc.pred e.1 s hmem hlu)
|
||||
|
||||
/-- **Main condensation theorem**: the single reverse scan computes
|
||||
EXACTLY the non-live SCCs. One Tarjan DFS + one linear scan replace
|
||||
Bacon's three graph traversals, with no loss of precision on the
|
||||
snapshot. -/
|
||||
theorem scan_dead_iff_not_live
|
||||
(horder : ∀ e ∈ edges, e.2 < e.1)
|
||||
(dead : Fin n → Bool)
|
||||
(hfix : ScanEq edges extRefs seed dead) :
|
||||
∀ s, dead s = true ↔ ¬ LiveScc edges extRefs seed s := by
|
||||
intro s
|
||||
constructor
|
||||
· intro hd hl
|
||||
exact live_not_dead edges extRefs seed dead hfix s hl hd
|
||||
· exact not_live_dead edges extRefs seed horder dead hfix s
|
||||
|
||||
/-! ## §3 The implementation's arithmetic form
|
||||
|
||||
computeDeadness does not test "all predecessors dead" directly; it
|
||||
maintains ext(s) = sumRefs(s) − internal(s) − deadIn(s) and a
|
||||
forcedLive flag pushed along cross edges of live SCCs. We show this
|
||||
is the same equation, given rc-exactness:
|
||||
|
||||
sumRefs s = extRefs s + internal s + (# cross edges into s).
|
||||
|
||||
ext(s) = 0 then says extRefs s = 0 AND every cross in-edge came from
|
||||
a dead predecessor; ¬forcedLive says no seed and no LIVE predecessor
|
||||
pushed the flag — together exactly `ScanEq`. -/
|
||||
|
||||
def inCount (s : Fin n) : Nat :=
|
||||
edges.countP (fun e => e.2 == s)
|
||||
|
||||
def deadInCount (dead : Fin n → Bool) (s : Fin n) : Nat :=
|
||||
edges.countP (fun e => e.2 == s && dead e.1)
|
||||
|
||||
/-- countP is monotone under pointwise implication. -/
|
||||
theorem countP_le_of_imp {α : Type} (l : List α) (p q : α → Bool)
|
||||
(himp : ∀ x ∈ l, p x = true → q x = true) :
|
||||
l.countP p ≤ l.countP q := by
|
||||
induction l with
|
||||
| nil => simp
|
||||
| cons a l ih =>
|
||||
have iht := ih (fun x hx => himp x (List.mem_cons_of_mem a hx))
|
||||
by_cases hpa : p a = true
|
||||
· have hqa := himp a (by simp) hpa
|
||||
simp [hpa, hqa]
|
||||
omega
|
||||
· simp only [List.countP_cons]
|
||||
have : p a = false := by
|
||||
cases h : p a
|
||||
· rfl
|
||||
· exact absurd h hpa
|
||||
simp [this]
|
||||
omega
|
||||
|
||||
/-- If a stronger predicate matches as often as a weaker one, they
|
||||
agree on every element. -/
|
||||
theorem countP_eq_forces_all {α : Type} (l : List α) (p q : α → Bool)
|
||||
(himp : ∀ x ∈ l, q x = true → p x = true)
|
||||
(heq : l.countP p = l.countP q) :
|
||||
∀ x ∈ l, p x = true → q x = true := by
|
||||
induction l with
|
||||
| nil => intro x hx; cases hx
|
||||
| cons a l ih =>
|
||||
have himpt : ∀ x ∈ l, q x = true → p x = true :=
|
||||
fun x hx => himp x (List.mem_cons_of_mem a hx)
|
||||
have hmono := countP_le_of_imp l q p himpt
|
||||
intro x hx hpx
|
||||
simp only [List.countP_cons] at heq
|
||||
cases List.mem_cons.mp hx with
|
||||
| inl hxa =>
|
||||
subst hxa
|
||||
cases hqx : q x with
|
||||
| true => rfl
|
||||
| false =>
|
||||
exfalso
|
||||
simp [hpx, hqx] at heq
|
||||
omega
|
||||
| inr hxl =>
|
||||
have hqa_pa : (if q a = true then 1 else 0) ≤ (if p a = true then 1 else 0) := by
|
||||
by_cases hq : q a = true
|
||||
· simp [hq, himp a (by simp) hq]
|
||||
· simp [hq]
|
||||
have heqt : l.countP p = l.countP q := by
|
||||
by_cases hq : q a = true
|
||||
· simp [hq, himp a (by simp) hq] at heq
|
||||
omega
|
||||
· have hqf : q a = false := by
|
||||
cases h : q a
|
||||
· rfl
|
||||
· exact absurd h hq
|
||||
by_cases hp : p a = true
|
||||
· simp [hp, hqf] at heq
|
||||
omega
|
||||
· have hpf : p a = false := by
|
||||
cases h : p a
|
||||
· rfl
|
||||
· exact absurd h hp
|
||||
simp [hpf, hqf] at heq
|
||||
omega
|
||||
exact ih himpt heqt x hxl hpx
|
||||
|
||||
/-- If all cross predecessors of `s` are dead, deadIn equals the full
|
||||
in-count (and vice versa). -/
|
||||
theorem deadIn_eq_inCount_iff (dead : Fin n → Bool) (s : Fin n) :
|
||||
deadInCount edges dead s = inCount edges s ↔
|
||||
(∀ e ∈ edges, e.2 = s → dead e.1 = true) := by
|
||||
constructor
|
||||
· intro heq e he hes
|
||||
have himp : ∀ x ∈ edges, (fun e => e.2 == s && dead e.1) x = true →
|
||||
(fun e => e.2 == s) x = true := by
|
||||
intro x _ hx
|
||||
simp only [Bool.and_eq_true] at hx
|
||||
exact hx.1
|
||||
have := countP_eq_forces_all edges
|
||||
(fun e => e.2 == s) (fun e => e.2 == s && dead e.1)
|
||||
himp heq.symm e he
|
||||
have hbeq : (e.2 == s) = true := by
|
||||
simp [hes]
|
||||
have := this hbeq
|
||||
simp only [Bool.and_eq_true] at this
|
||||
exact this.2
|
||||
· intro hall
|
||||
unfold deadInCount inCount
|
||||
apply List.countP_congr
|
||||
intro e he
|
||||
by_cases hes : e.2 = s
|
||||
· simp [hes, hall e he hes]
|
||||
· have : (e.2 == s) = false := by
|
||||
simp [hes]
|
||||
simp [this]
|
||||
|
||||
/-- The implementation's per-SCC decision, verbatim from
|
||||
computeDeadness: NOT forced (no seed, no live predecessor pushed
|
||||
the flag) and ext = sumRefs − internal − deadIn = 0 (stated
|
||||
subtraction-free). -/
|
||||
def ImplEq (sumRefs internal : Fin n → Nat) (dead : Fin n → Bool) : Prop :=
|
||||
∀ s, dead s = true ↔
|
||||
(¬ (seed s = true ∨ ∃ e ∈ edges, e.2 = s ∧ dead e.1 = false) ∧
|
||||
sumRefs s = internal s + deadInCount edges dead s)
|
||||
|
||||
/-- **The arithmetic is the spec**: under rc-exactness, the
|
||||
implementation's equation is `ScanEq`, so `scan_dead_iff_not_live`
|
||||
applies to computeDeadness as written. -/
|
||||
theorem impl_fixpoint_is_spec
|
||||
(sumRefs internal : Fin n → Nat) (dead : Fin n → Bool)
|
||||
(hcount : ∀ s, sumRefs s = extRefs s + internal s + inCount edges s)
|
||||
(himpl : ImplEq edges seed sumRefs internal dead) :
|
||||
ScanEq edges extRefs seed dead := by
|
||||
intro s
|
||||
rw [himpl s]
|
||||
constructor
|
||||
· rintro ⟨hnf, harith⟩
|
||||
have hor := hnf
|
||||
rw [not_or] at hor
|
||||
obtain ⟨hseed, hnopred⟩ := hor
|
||||
have hseedf : seed s = false := by
|
||||
cases h : seed s
|
||||
· rfl
|
||||
· exact absurd h hseed
|
||||
have hall : ∀ e ∈ edges, e.2 = s → dead e.1 = true := by
|
||||
intro e he hes
|
||||
cases h : dead e.1 with
|
||||
| true => rfl
|
||||
| false => exact absurd ⟨e, he, hes, h⟩ hnopred
|
||||
have hdc := (deadIn_eq_inCount_iff edges dead s).mpr hall
|
||||
have hc := hcount s
|
||||
refine ⟨by omega, hseedf, hall⟩
|
||||
· rintro ⟨hext, hseedf, hall⟩
|
||||
have hdc := (deadIn_eq_inCount_iff edges dead s).mpr hall
|
||||
refine ⟨?_, ?_⟩
|
||||
· rw [not_or]
|
||||
refine ⟨by simp [hseedf], ?_⟩
|
||||
rintro ⟨e, he, hes, hdf⟩
|
||||
rw [hall e he hes] at hdf
|
||||
cases hdf
|
||||
· have hc := hcount s
|
||||
omega
|
||||
|
||||
end Condensation
|
||||
|
||||
/-! ## §4 Cell-level correctness
|
||||
|
||||
Bridge from the condensation to the actual heap snapshot. `extRef`
|
||||
covers every reference source outside the capture: mutator stacks,
|
||||
the roots buffer, uncaptured heap cells' slots that the arithmetic
|
||||
cannot explain, and other collections' partitions (cross-collection
|
||||
edges — this is the SCC-side view of `cross_target_live` in
|
||||
yrc_proof.lean §5). -/
|
||||
|
||||
structure CellGraph where
|
||||
edge : Obj → Obj → Prop
|
||||
extRef : Obj → Prop
|
||||
|
||||
/-- A cell is live iff an external reference anchors it through heap
|
||||
edges (the cell-level ground truth; `anchored` of yrc_proof.lean). -/
|
||||
inductive CellLive (g : CellGraph) : Obj → Prop where
|
||||
| ext (x : Obj) : g.extRef x → CellLive g x
|
||||
| step (x y : Obj) : CellLive g x → g.edge x y → CellLive g y
|
||||
|
||||
/-- Paths through heap edges, used to move liveness around inside an
|
||||
SCC (Tarjan guarantees SCC members are mutually reachable). -/
|
||||
inductive EdgePath (g : CellGraph) : Obj → Obj → Prop where
|
||||
| refl (x : Obj) : EdgePath g x x
|
||||
| step (x y z : Obj) : EdgePath g x y → g.edge y z → EdgePath g x z
|
||||
|
||||
theorem cellLive_along_path (g : CellGraph) (u v : Obj)
|
||||
(hl : CellLive g u) (hp : EdgePath g u v) : CellLive g v := by
|
||||
induction hp with
|
||||
| refl => exact hl
|
||||
| step _ _ _ hedge ih => exact CellLive.step _ _ ih hedge
|
||||
|
||||
section CellBridge
|
||||
|
||||
variable {n : Nat}
|
||||
variable (g : CellGraph)
|
||||
variable (edges : List (Fin n × Fin n))
|
||||
variable (extRefs : Fin n → Nat)
|
||||
variable (seed : Fin n → Bool)
|
||||
variable (captured : Obj → Prop)
|
||||
variable (scc : Obj → Fin n)
|
||||
|
||||
/-- Any live captured cell sits in a live SCC.
|
||||
Premises are properties of `capture`:
|
||||
* `h_edge_resp` — every heap edge between captured cells was
|
||||
recorded (same SCC → internal; different → cross edge);
|
||||
* `h_closed` — an edge from an UNCAPTURED cell is unexplained by
|
||||
the captured arithmetic, so it lands in extRefs;
|
||||
* `h_ext` — direct external refs (stacks, roots buffer, foreign
|
||||
partitions) are counted in extRefs. -/
|
||||
theorem captured_live_scc
|
||||
(h_edge_resp : ∀ u v, captured u → captured v → g.edge u v →
|
||||
scc u = scc v ∨ (scc u, scc v) ∈ edges)
|
||||
(h_closed : ∀ u v, captured v → g.edge u v → ¬ captured u →
|
||||
0 < extRefs (scc v))
|
||||
(h_ext : ∀ v, captured v → g.extRef v → 0 < extRefs (scc v)) :
|
||||
∀ x, CellLive g x → captured x →
|
||||
LiveScc edges extRefs seed (scc x) := by
|
||||
intro x hl
|
||||
induction hl with
|
||||
| ext x h =>
|
||||
intro hc
|
||||
exact LiveScc.ext _ (h_ext x hc h)
|
||||
| step u v hu hedge ih =>
|
||||
intro hcv
|
||||
by_cases hcu : captured u
|
||||
· cases h_edge_resp u v hcu hcv hedge with
|
||||
| inl heq => rw [← heq]; exact ih hcu
|
||||
| inr hmem => exact LiveScc.pred _ _ hmem (ih hcu)
|
||||
· exact LiveScc.ext _ (h_closed u v hcv hedge hcu)
|
||||
|
||||
/-- **Soundness**: every cell of a dead SCC is unanchored in the
|
||||
snapshot — freeing it is justified by yrc_proof.lean §1
|
||||
(`yrc_safety`) + §3 (stability through the commit window). -/
|
||||
theorem tarjan_sound
|
||||
(dead : Fin n → Bool)
|
||||
(hfix : ScanEq edges extRefs seed dead)
|
||||
(h_edge_resp : ∀ u v, captured u → captured v → g.edge u v →
|
||||
scc u = scc v ∨ (scc u, scc v) ∈ edges)
|
||||
(h_closed : ∀ u v, captured v → g.edge u v → ¬ captured u →
|
||||
0 < extRefs (scc v))
|
||||
(h_ext : ∀ v, captured v → g.extRef v → 0 < extRefs (scc v)) :
|
||||
∀ x, captured x → dead (scc x) = true → ¬ CellLive g x := by
|
||||
intro x hc hd hl
|
||||
exact live_not_dead edges extRefs seed dead hfix (scc x)
|
||||
(captured_live_scc g edges extRefs seed captured scc
|
||||
h_edge_resp h_closed h_ext x hl hc) hd
|
||||
|
||||
/-- Every cell of a live SCC is genuinely live. Needs the converse
|
||||
premises: external counts are EXACT (no phantom refs — deferred
|
||||
decs inflate rc, so in the running system this holds only after
|
||||
the merge; overcounts delay collection by a round, they never
|
||||
cause a wrong free), cross edges are real edges, and SCC members
|
||||
are mutually reachable (Tarjan). -/
|
||||
theorem live_scc_cells_live
|
||||
(h_ext_exact : ∀ s : Fin n, 0 < extRefs s →
|
||||
∃ v, captured v ∧ scc v = s ∧ g.extRef v)
|
||||
(h_seed_exact : ∀ s : Fin n, seed s = true →
|
||||
∃ v, captured v ∧ scc v = s ∧ g.extRef v)
|
||||
(h_cross_real : ∀ (u s : Fin n), (u, s) ∈ edges →
|
||||
∃ cu cv, captured cu ∧ captured cv ∧ scc cu = u ∧ scc cv = s ∧
|
||||
g.edge cu cv)
|
||||
(h_conn : ∀ u v, captured u → captured v → scc u = scc v →
|
||||
EdgePath g u v) :
|
||||
∀ s, LiveScc edges extRefs seed s →
|
||||
∀ x, captured x → scc x = s → CellLive g x := by
|
||||
intro s hl
|
||||
induction hl with
|
||||
| ext s h =>
|
||||
intro x hc hs
|
||||
obtain ⟨v, hcv, hsv, hev⟩ := h_ext_exact s h
|
||||
exact cellLive_along_path g v x (CellLive.ext v hev)
|
||||
(h_conn v x hcv hc (by rw [hsv, hs]))
|
||||
| root s h =>
|
||||
intro x hc hs
|
||||
obtain ⟨v, hcv, hsv, hev⟩ := h_seed_exact s h
|
||||
exact cellLive_along_path g v x (CellLive.ext v hev)
|
||||
(h_conn v x hcv hc (by rw [hsv, hs]))
|
||||
| pred u s hmem _ ih =>
|
||||
intro x hc hs
|
||||
obtain ⟨cu, cv, hccu, hccv, hscu, hscv, he⟩ := h_cross_real u s hmem
|
||||
have hculive : CellLive g cu := ih cu hccu hscu
|
||||
exact cellLive_along_path g cv x (CellLive.step cu cv hculive he)
|
||||
(h_conn cv x hccv hc (by rw [hscv, hs]))
|
||||
|
||||
/-- **Completeness**: every captured garbage cell is marked dead — the
|
||||
scan collects ALL cycles reachable from the candidate set in one
|
||||
round (on the snapshot; concurrent inflation only defers). -/
|
||||
theorem tarjan_complete
|
||||
(horder : ∀ e ∈ edges, e.2 < e.1)
|
||||
(dead : Fin n → Bool)
|
||||
(hfix : ScanEq edges extRefs seed dead)
|
||||
(h_ext_exact : ∀ s : Fin n, 0 < extRefs s →
|
||||
∃ v, captured v ∧ scc v = s ∧ g.extRef v)
|
||||
(h_seed_exact : ∀ s : Fin n, seed s = true →
|
||||
∃ v, captured v ∧ scc v = s ∧ g.extRef v)
|
||||
(h_cross_real : ∀ (u s : Fin n), (u, s) ∈ edges →
|
||||
∃ cu cv, captured cu ∧ captured cv ∧ scc cu = u ∧ scc cv = s ∧
|
||||
g.edge cu cv)
|
||||
(h_conn : ∀ u v, captured u → captured v → scc u = scc v →
|
||||
EdgePath g u v) :
|
||||
∀ x, captured x → ¬ CellLive g x → dead (scc x) = true := by
|
||||
intro x hc hnl
|
||||
apply not_live_dead edges extRefs seed horder dead hfix
|
||||
intro hl
|
||||
exact hnl (live_scc_cells_live g edges extRefs seed captured scc
|
||||
h_ext_exact h_seed_exact h_cross_real h_conn (scc x) hl x hc rfl)
|
||||
|
||||
end CellBridge
|
||||
|
||||
/-! ## §5 Validate-time demotion must propagate
|
||||
|
||||
validateDead demotes a dead SCC when a mutator dirtied it (queue
|
||||
entry or changed rc word). A demoted SCC becomes a survivor: its
|
||||
slots are NOT nil'd at commit, so its captured out-edges remain in
|
||||
the heap. If a cross target of a demoted SCC stayed in the dead set,
|
||||
the commit would free a cell that a surviving cell still points to —
|
||||
deadIn had explained that edge away under the assumption that the
|
||||
predecessor dies too.
|
||||
|
||||
Minimal instance of the hazard: two SCCs, one edge 1 → 0, both
|
||||
computed dead (ext = 0 for both; SCC 0's only reference comes from
|
||||
SCC 1, subtracted as deadIn). Demote SCC 1 alone, and the freed set
|
||||
{0} has a live in-edge from the surviving SCC 1.
|
||||
|
||||
The theorem below states the repair: if the demoted set `K` is
|
||||
successor-closed within the dead set (demoting s also demotes every
|
||||
dead t with a captured edge s → t, transitively — one countdown pass
|
||||
suffices because edges go from higher to lower ids), then the freed
|
||||
set F = dead ∖ K is predecessor-closed: every captured edge into F
|
||||
comes from F. Combined with extRefs = 0 and no seed (ScanEq) this
|
||||
makes F closed in the sense of yrc_proof.lean §3, so freeing F is
|
||||
covered by `commit_free_safe` there. -/
|
||||
|
||||
theorem demotion_closure_sound {n : Nat}
|
||||
(edges : List (Fin n × Fin n))
|
||||
(extRefs : Fin n → Nat) (seed : Fin n → Bool)
|
||||
(dead : Fin n → Bool)
|
||||
(hfix : ScanEq edges extRefs seed dead)
|
||||
(K : Fin n → Prop) -- the demoted SCCs
|
||||
(hK_closed : ∀ e ∈ edges, K e.1 → dead e.2 = true → K e.2) :
|
||||
-- every captured edge into the freed set comes from the freed set
|
||||
∀ e ∈ edges, (dead e.2 = true ∧ ¬ K e.2) →
|
||||
(dead e.1 = true ∧ ¬ K e.1) := by
|
||||
intro e he ⟨hd2, hk2⟩
|
||||
have hd1 : dead e.1 = true :=
|
||||
((hfix e.2).mp hd2).2.2 e he rfl
|
||||
refine ⟨hd1, ?_⟩
|
||||
intro hk1
|
||||
exact hk2 (hK_closed e he hk1 hd2)
|
||||
|
||||
/-- Without successor-closure the guarantee genuinely fails: in the
|
||||
two-SCC instance above, demoting only SCC 1 leaves the freed set
|
||||
{0} with an in-edge from a survivor. (Concrete witness, checked by
|
||||
`decide`-style evaluation.) -/
|
||||
example :
|
||||
let edges : List (Fin 2 × Fin 2) := [(1, 0)]
|
||||
let dead : Fin 2 → Bool := fun _ => true
|
||||
let K : Fin 2 → Prop := fun s => s = 1 -- demote only SCC 1
|
||||
-- ScanEq holds for `dead` (both SCCs legitimately computed dead) …
|
||||
ScanEq edges (fun _ => 0) (fun _ => false) dead ∧
|
||||
-- … yet the freed set {0} has an in-edge from surviving SCC 1:
|
||||
((1, 0) ∈ edges ∧ dead 0 = true ∧ ¬ K 0 ∧ K 1) := by
|
||||
refine ⟨?_, ?_⟩
|
||||
· intro s
|
||||
simp
|
||||
· refine ⟨by simp, rfl, by simp, rfl⟩
|
||||
|
||||
/-! ## Summary (all QED, no sorry)
|
||||
|
||||
* `descending_induction` — the sinks-first SCC numbering makes the
|
||||
reverse scan a well-founded definition.
|
||||
* `scan_dead_iff_not_live` — the scan marks an SCC dead iff it is
|
||||
not externally anchored: exact garbage identification in ONE
|
||||
linear pass over the condensation.
|
||||
* `impl_fixpoint_is_spec` — the implementation's arithmetic
|
||||
(ext = sumRefs − internal − deadIn, forcedLive propagation) is
|
||||
that same equation under rc-exactness.
|
||||
* `tarjan_sound` / `tarjan_complete` — at the cell level: dead cells
|
||||
are unanchored (frees are safe) and unanchored captured cells are
|
||||
freed (nothing is missed on the snapshot).
|
||||
* `demotion_closure_sound` + counterexample — demotion is sound iff
|
||||
it propagates along captured cross edges to still-dead targets;
|
||||
a lone demotion can leave the freed set with a surviving
|
||||
predecessor.
|
||||
|
||||
Not modeled: the Tarjan DFS itself (its two classical invariants —
|
||||
SCC partition and sinks-first emission — enter as premises), the
|
||||
iterative traceStack encoding, crossPend (cross-collection edges are
|
||||
folded into `extRefs`, justified by yrc_proof.lean §5), and the
|
||||
temporal validity of rc-exactness (yrc_proof.lean §4).
|
||||
-/
|
||||
@@ -36,4 +36,4 @@ proc main() =
|
||||
main()
|
||||
GC_fullCollect()
|
||||
when not defined(useMalloc):
|
||||
echo getOccupiedMem() < 10 * 1024 * 1024, " peak memory: ", getMaxMem() < 10 * 1024 * 1024
|
||||
echo getOccupiedMem() < 10 * 1024 * 1024, " peak memory: ", getMaxMem() < 12 * 1024 * 1024
|
||||
|
||||
Reference in New Issue
Block a user