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

YRC: bugfixes

Browse Source
This commit is contained in:
Araq
2026-07-27 12:04:28 +02:00
parent ecfca935c7
commit bd04876701
5 changed files with 718 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

14
compiler/liftdestructors.nim
View File

@@ -857,7 +857,19 @@ proc atomicRefOp(c: var TLiftCtx; t: PType; body, x, y: PNode) =
else:
cond = callCodegenProc(c.g, "nimDecRefIsLastCyclicDyn", c.info, tmp)
elif isInheritableAcyclicRef:
cond = callCodegenProc(c.g, "nimDecRefIsLastDyn", c.info, x)
if c.g.config.selectedGC == gcYrc and useStatic:
# YRC defers every dec, so the runtime must record a type descriptor
# at dec time instead of destroying immediately. The `Dyn` hook
# derives that descriptor from the object's m_type field -- which a
# FINAL object does not have, so it would read the first data field
# as a type pointer. Pass the static descriptor instead, the same
# convention the nimAsgnYrc/nimSinkYrc path above uses. (ORC is
# unaffected: its `Dyn` hook never looks at the descriptor.)
let typInfo = genBuiltin(c, mGetTypeInfoV2, "getTypeInfoV2", newNodeIT(nkType, x.info, elemType))
typInfo.typ = getSysType(c.g, c.info, tyPointer)
cond = callCodegenProc(c.g, "nimDecRefIsLastCyclicStatic", c.info, x, typInfo)
else:
cond = callCodegenProc(c.g, "nimDecRefIsLastDyn", c.info, x)
else:
cond = callCodegenProc(c.g, "nimDecRefIsLast", c.info, x)
cond.typ = getSysType(c.g, x.info, tyBool)

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 =

6
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
#

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