From cd3e9a46b24f80019c192cb27b05217df0385942 Mon Sep 17 00:00:00 2001 From: Andreas Rumpf Date: Fri, 24 Jul 2026 14:04:45 +0200 Subject: [PATCH 01/22] run async tests under --mm:yrc (#26033) --- compiler/liftdestructors.nim | 14 ++++++++++++-- doc/mm.md | 19 +++++++++++++++++-- testament/categories.nim | 4 +++- 3 files changed, 32 insertions(+), 5 deletions(-) diff --git a/compiler/liftdestructors.nim b/compiler/liftdestructors.nim index 0529812c3a..aa8a20bc2a 100644 --- a/compiler/liftdestructors.nim +++ b/compiler/liftdestructors.nim @@ -94,11 +94,21 @@ proc defaultOp(c: var TLiftCtx; t: PType; body, x, y: PNode) = body.add genBuiltin(c, mWasMoved, "wasMoved", x) proc genAddr(c: var TLiftCtx; x: PNode): PNode = - if x.kind == nkHiddenDeref: + # These synthesized addresses are always passed to codegen procs that expect a + # genuine pointer (nimAsgnYrc, nimSinkYrc, destructors, ...). `addr(deref x)` + # collapses to `x` only when `x` is a real pointer; on the C++ backend a `var` + # parameter is a C++ reference, so we must keep the `nkHiddenAddr` to actually + # take its address (`&dest`) instead of passing the reference's value. Likewise + # `tfVarIsPtr` keeps the C++ backend from lowering the synthesized address back + # to a reference and dropping the `&` (e.g. a closure's `tyPointer` env). See + # #26026 CI (yrc + cpp). + if x.kind == nkHiddenDeref and c.g.config.backend != backendCpp: checkSonsLen(x, 1, c.g.config) result = x[0] else: - result = newNodeIT(nkHiddenAddr, x.info, makeVarType(x.typ.owner, x.typ, c.idgen)) + let addrTyp = makeVarType(x.typ.owner, x.typ, c.idgen) + addrTyp.incl tfVarIsPtr + result = newNodeIT(nkHiddenAddr, x.info, addrTyp) result.add x proc genWhileLoop(c: var TLiftCtx; i, dest: PNode): PNode = diff --git a/doc/mm.md b/doc/mm.md index 5e0d2f3b94..df3b5b17f0 100644 --- a/doc/mm.md +++ b/doc/mm.md @@ -50,9 +50,23 @@ cycle collector's overhead but `--mm:orc` also produces more machine code than `--mm:arc`, so if you're on a target where code size matters and you know that your code does not produce cycles, you can use `--mm:arc`. Notice that the default `async`:idx: implementation produces cycles -and leaks memory with `--mm:arc`, in other words, for `async` you need to use `--mm:orc`. +and leaks memory with `--mm:arc`, in other words, for `async` you need to use `--mm:orc` +or `--mm:yrc`. +Atomic ARC/YRC +-------------- + +ARC/ORC are not threadsafe if `ref` or other automatically managed types are +accessed across thread boundaries. +Moving isolated subgraphs between threads is supported for ARC/ORC and the language has support +for that in the form of `isolate`. The modes `mm:atomicArc` and `mm:yrc` do offer this thread safety -- at the cost of atomic instructions. Whether that cost is acceptable depends on your program, it hard to give general guidelines. On a modern CPU the potential speedups in the form of increased multi-threading capabilities should outweigh the costs of atomic instructions by far. On an embedded device the atomics would probably only hurt though. + +`mm:atomicArc` is a threadsafe variant of ARC: All the optimizations in the form of move semantics etc are still applied. `mm:yrc` is the threadsafe variant of ORC. + +YRC is a novel concurrent cycle collection algorithm -- these are beasts to verify +and to get correct so there are dragons lurking here, use at your own risk. + Other MM modes -------------- @@ -66,7 +80,7 @@ Other MM modes Heaps are thread-local. --mm:boehm Boehm based garbage collector, it offers a shared heap. --mm:go Go's garbage collector, useful for interoperability with Go. - Offers a shared heap. + Offers a shared heap. Note that `mm:go` has seen little real world use. Use at your own risk. --mm:none No memory management strategy nor a garbage collector. Allocated memory is simply never freed. You should use `--mm:arc` instead. @@ -76,6 +90,7 @@ Here is a comparison of the different memory management modes: ================== ======== ================= ============== ====== =================== =================== Memory Management Heap Reference Cycles Stop-The-World Atomic Valgrind compatible Command line switch ================== ======== ================= ============== ====== =================== =================== +YRC Shared Cycle Collector No Yes Yes `--mm:yrc` ORC Shared Cycle Collector No No Yes `--mm:orc` ARC Shared Leak No No Yes `--mm:arc` Atomic ARC Shared Leak No Yes Yes `--mm:atomicArc` diff --git a/testament/categories.nim b/testament/categories.nim index 17e9a48a86..0d88943cd7 100644 --- a/testament/categories.nim +++ b/testament/categories.nim @@ -190,8 +190,10 @@ proc ioTests(r: var TResults, cat: Category, options: string) = # ------------------------- async tests --------------------------------------- proc asyncTests(r: var TResults, cat: Category, options: string) = + # Run async with yrc instead of the default orc; the CI already runs long + # enough that we cannot afford to test both. template test(filename: untyped) = - testSpec r, makeTest(filename, options, cat) + testSpec r, makeTest(filename, options & " --mm:yrc", cat) for t in os.walkFiles("tests/async/t*.nim"): test(t) From 8e8f8de1abb237db91df996943fbd9e65472abee Mon Sep 17 00:00:00 2001 From: cryo2010 Date: Fri, 24 Jul 2026 05:06:27 -0700 Subject: [PATCH 02/22] fix: exception leak in closure iterator typed except branches (#23615) (#26034) Fixes #23615 ## Root cause The leak does not require async at all -- this minimal closure iterator leaks the exception and its stacktrace seq under ARC/ORC: ```nim iterator it(): int {.closure.} = try: yield 1 # try spanning a yield => closureiters transform raise newException(ValueError, "x") except ValueError: # typed except => generated `of` check discard yield 2 ``` A bare `except:` does not leak; a *typed* `except` does: 1. `collectExceptState` in `compiler/closureiters.nim` generates the except-branch type check as `of(getCurrentException(), T)`, using the raw generic magic sym from `getSysMagic("of", mOf)`. 2. `injectdestructors` skips call arguments whose *formal* parameter type is `isCompileTimeOnly`, and the raw generic `of` sym's formal params are `tyGenericParam` so both arguments of the generated `of` call are never processed. 3. `getCurrentException()` increfs `currException` via `=copy` into its result. Since the arc pass never wraps that owned temp in a destroy (`--expandArc` shows the condition left untouched, while a user-written `if f() of ValueError` in the same iterator gets a `:tmpD` + `=destroy`), the caught exception's refcount stays +1 forever. Every `try: await x() except SomeError` in async code has this shape, so each caught async exception leaked once. ## Fix The state-machine wrapper already stores the active exception in the `:curExc` env field before jumping to the except landing state, and `currException == :curExc` on every path into that state. The generated condition now references the env field via `ctx.newCurExcAccess()` instead of calling `getCurrentException()` again -- no ownership transfer, no temp to destroy, one fewer runtime call. Note: the underlying `injectdestructors` behavior (skipping args of calls whose formal params are raw `tyGenericParam`, e.g. from `getSysMagic`) is a separate latent gap that could affect other compiler-generated code; it is intentionally left untouched here. ## Valgrind, before and after Exact code and command from the issue, on Linux (Valgrind 3.19): ``` nim c -d:danger --mm:orc --debugger:native --threads:off -d:useMalloc bug.nim valgrind --leak-check=full --show-leak-kinds=all ./bug ``` Before (devel): ``` ==14663== HEAP SUMMARY: ==14663== in use at exit: 136 bytes in 2 blocks ==14663== total heap usage: 22 allocs, 20 frees, 116,466 bytes allocated ==14663== ==14663== 56 bytes in 1 blocks are indirectly lost in loss record 1 of 2 ==14663== at 0x488A1C4: realloc (vg_replace_malloc.c:1437) ==14663== by 0x10C663: prepareSeqAddUninit (seqs_v2.nim:212) ==14663== by 0x10CF6F: raiseExceptionEx (excpt.nim:538) ==14663== by 0x11661F: amain::amainX20X28AsyncX29_(Future) (bug.nim:10) ==14663== ... ==14663== ==14663== 136 (80 direct, 56 indirect) bytes in 1 blocks are definitely lost in loss record 2 of 2 ==14663== at 0x48850C8: malloc (vg_replace_malloc.c:381) ==14663== by 0x10C8E3: nimNewObj (arc.nim:122) ==14663== by 0x115403: err::errX20X28AsyncX29_(Future) (asyncmacro.nim:274) ==14663== by 0x116027: err::errNimAsyncContinue(Future, ClosureIt) (asyncmacro.nim:44) ==14663== by 0x1163D3: bug::err (bug.nim:3) ==14663== ... ==14663== ==14663== LEAK SUMMARY: ==14663== definitely lost: 80 bytes in 1 blocks ==14663== indirectly lost: 56 bytes in 1 blocks ==14663== possibly lost: 0 bytes in 0 blocks ==14663== still reachable: 0 bytes in 0 blocks ==14663== ERROR SUMMARY: 1 errors from 1 contexts (suppressed: 0 from 0) ``` After (this PR): ``` ==14675== HEAP SUMMARY: ==14675== in use at exit: 0 bytes in 0 blocks ==14675== total heap usage: 22 allocs, 22 frees, 116,466 bytes allocated ==14675== ==14675== All heap blocks were freed -- no leaks are possible ==14675== ==14675== ERROR SUMMARY: 0 errors from 0 contexts (suppressed: 0 from 0) ``` ## Testing - New `tests/async/t23615.nim` (modeled on `t23212.nim`: `valgrind: true` + alloc-stats assertion) covers both the pure closure-iterator form and the async form from the issue, with the caught exception looped 50x so the leak blows well past the slack threshold. It passes with this PR and fails against devel. - Testament categories `async`, `arc`, `iter`, `exception` all pass with the patched compiler (323 tests). - Behavior is unchanged on a sanity program covering multi-branch dispatch, `as e` binding, nested try, and re-raise across yields: output is byte-identical to devel; the patched build just frees 2 more blocks per caught exception. --- compiler/closureiters.nim | 7 +++++- tests/async/t23615.nim | 52 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+), 1 deletion(-) create mode 100644 tests/async/t23615.nim diff --git a/compiler/closureiters.nim b/compiler/closureiters.nim index e85ad4975d..d71b62d555 100644 --- a/compiler/closureiters.nim +++ b/compiler/closureiters.nim @@ -336,9 +336,14 @@ proc collectExceptState(ctx: var Ctx, n: PNode): PNode {.inline.} = var cond: PNode = nil for i in 0.. Date: Fri, 24 Jul 2026 20:07:15 +0800 Subject: [PATCH 03/22] fixes #26010; Double destroy with {.cursor.} (#26031) fixes #26010 Cursors do not own their values and therefore cannot transfer ownership through move. Reject move(cursor) during semantic analysis and share the cursor-location check between semantic analysis and destructor injection. --- compiler/injectdestructors.nim | 13 +------------ compiler/semmagic.nim | 5 +++++ compiler/trees.nim | 11 +++++++++++ tests/arc/t26010.nim | 23 +++++++++++++++++++++++ 4 files changed, 40 insertions(+), 12 deletions(-) create mode 100644 tests/arc/t26010.nim diff --git a/compiler/injectdestructors.nim b/compiler/injectdestructors.nim index a145458a90..37969dfd31 100644 --- a/compiler/injectdestructors.nim +++ b/compiler/injectdestructors.nim @@ -24,7 +24,7 @@ import std/[strtabs, tables, strutils, intsets] when defined(nimPreviewSlimSystem): import std/assertions -from trees import exprStructuralEquivalent, getRoot, whichPragma, getPotentialWrites +from trees import exprStructuralEquivalent, getRoot, isCursor, whichPragma, getPotentialWrites type Con = object @@ -180,17 +180,6 @@ proc isFirstWrite(n: PNode; c: var Con): bool = let m = skipConvDfa(n) result = nfFirstWrite in m.flags -proc isCursor(n: PNode): bool = - case n.kind - of nkSym: - sfCursor in n.sym.flags - of nkDotExpr: - isCursor(n[1]) - of nkCheckedFieldExpr: - isCursor(n[0]) - else: - false - template isFullyUnpackedTuple(n: PNode): bool = ## we move out all elements of unpacked tuples, ## hence unpacked tuples themselves don't need to be destroyed diff --git a/compiler/semmagic.nim b/compiler/semmagic.nim index f5bf97c580..0e1eab91ea 100644 --- a/compiler/semmagic.nim +++ b/compiler/semmagic.nim @@ -693,5 +693,10 @@ proc magicsAfterOverloadResolution(c: PContext, n: PNode, if n[1].kind in {nkStmtListExpr, nkBlockExpr, nkIfExpr, nkCaseStmt, nkTryStmt}: localError(c.config, n.info, "Nested expressions cannot be moved: '" & $n[1] & "'") + of mMove: + result = n + if isCursor(n[1]): + localError(c.config, n.info, errFailedMove, + "cannot move cursor '" & $n[1] & "'; a cursor does not own its value") else: result = n diff --git a/compiler/trees.nim b/compiler/trees.nim index a42b616d97..24226e79d5 100644 --- a/compiler/trees.nim +++ b/compiler/trees.nim @@ -225,6 +225,17 @@ proc getRoot*(n: PNode): PSym = else: result = nil else: result = nil +proc isCursor*(n: PNode): bool = + case n.kind + of nkSym: + sfCursor in n.sym.flags + of nkDotExpr: + isCursor(n[1]) + of nkCheckedFieldExpr: + isCursor(n[0]) + else: + false + proc stupidStmtListExpr*(n: PNode): bool = for i in 0.. Date: Sat, 25 Jul 2026 05:32:23 +0900 Subject: [PATCH 04/22] makes `testament.nim` compiles with `--experimental:strictDefs` (#26037) --- testament/categories.nim | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/testament/categories.nim b/testament/categories.nim index 0d88943cd7..7ed98b8aa9 100644 --- a/testament/categories.nim +++ b/testament/categories.nim @@ -530,6 +530,7 @@ proc mmRaise(kind: TResultEnum, expected, given: string) = raise e proc isMetamorphicIcTest(content: string): bool = + result = false for line in content.splitLines: if line.strip == "#? metamorphic": return true @@ -561,7 +562,7 @@ proc stableBinary(path: string): string = ## so two builds seconds apart differ there even with identical codegen. Skipping ## a generous fixed window keeps the clean-vs-incremental check about codegen. const headerSkip = 4096 - var f: File + var f: File = nil if not open(f, path, fmRead): raise newException(IOError, "cannot open: " & path) defer: close(f) From f17755782ad11aa880e4e0325aae3ecc45e94b38 Mon Sep 17 00:00:00 2001 From: SirOlaf <34164198+SirOlaf@users.noreply.github.com> Date: Fri, 24 Jul 2026 22:33:56 +0200 Subject: [PATCH 05/22] Asyncdispatch: Process callbacks before timers (CI issue) (#26032) Should fix https://github.com/nim-lang/Nim/blob/devel/tests/async/tasyncclosestall.nim (the flaky one) in CI. Previously CI was somehow slow enough to race on completion through multiple callback layers. Also increased the message size to hopefully fill the socket's buffer quicker --- lib/pure/asyncdispatch.nim | 31 +++++++++++++++++-------- tests/async/tasyncclosestall.nim | 10 +++++--- tests/async/tasyncdispatchordering.nim | 32 ++++++++++++++++++++++++++ 3 files changed, 60 insertions(+), 13 deletions(-) create mode 100644 tests/async/tasyncdispatchordering.nim diff --git a/lib/pure/asyncdispatch.nim b/lib/pure/asyncdispatch.nim index 70d94b023e..3c0a2257b0 100644 --- a/lib/pure/asyncdispatch.nim +++ b/lib/pure/asyncdispatch.nim @@ -269,6 +269,23 @@ proc processPendingCallbacks(p: PDispatcherBase; didSomeWork: var bool) = cb() didSomeWork = true +proc processTimersBeforePoll( + p: PDispatcherBase, didSomeWork: var bool +): Option[int] {.inline.} = + # Do not let an expired timeout overtake completion callbacks which are + # already pending. `adjustTimeout` makes the I/O poll non-blocking when the + # callback queue is non-empty. + if p.callbacks.len == 0: + result = processTimers(p, didSomeWork) + +proc processCallbacksAndTimers(p: PDispatcherBase; didSomeWork: var bool) = + # A completed operation can take multiple queued callbacks to propagate + # through its public future. Process the whole chain before expired timers. + processPendingCallbacks(p, didSomeWork) + discard processTimers(p, didSomeWork) + # Timer futures must still propagate within this dispatcher iteration. + processPendingCallbacks(p, didSomeWork) + proc adjustTimeout( p: PDispatcherBase, pollTimeout: int, nextTimer: Option[int] ): int {.inline.} = @@ -399,7 +416,7 @@ when defined(windows) or defined(nimdoc): "No handles or timers registered in dispatcher.") result = false - let nextTimer = processTimers(p, result) + let nextTimer = processTimersBeforePoll(p, result) let at = adjustTimeout(p, timeout, nextTimer) var llTimeout = if at == -1: winlean.INFINITE @@ -450,10 +467,7 @@ when defined(windows) or defined(nimdoc): result = false else: raiseOSError(errCode) - # Timer processing. - discard processTimers(p, result) - # Callback queue processing - processPendingCallbacks(p, result) + processCallbacksAndTimers(p, result) var acceptEx: WSAPROC_ACCEPTEX @@ -1404,7 +1418,7 @@ else: result = false var keys: array[64, ReadyKey] - let nextTimer = processTimers(p, result) + let nextTimer = processTimersBeforePoll(p, result) var count = p.selector.selectInto(adjustTimeout(p, timeout, nextTimer), keys) for i in 0.. 0: incl(newEvents, Event.Write) p.selector.updateHandle(SocketHandle(fd), newEvents) - # Timer processing. - discard processTimers(p, result) - # Callback queue processing - processPendingCallbacks(p, result) + processCallbacksAndTimers(p, result) proc recv*(socket: AsyncFD, size: int, flags = {SocketFlag.SafeDisconn}): owned(Future[string]) = diff --git a/tests/async/tasyncclosestall.nim b/tests/async/tasyncclosestall.nim index 05348587c1..ea4865fc79 100644 --- a/tests/async/tasyncclosestall.nim +++ b/tests/async/tasyncclosestall.nim @@ -4,6 +4,7 @@ discard """ exitcode: 0 """ import asyncdispatch, asyncnet +import std/strutils when defined(windows): from winlean import ERROR_NETNAME_DELETED @@ -14,6 +15,7 @@ else: # even when the socket is closed. const timeout = 2000 + messagePaddingSize = 64 * 1024 var port = Port(0) var sent = 0 @@ -31,10 +33,12 @@ proc isExpectedDisconnectionError(errCode: int32): bool = errCode == EBADF or errCode == ECONNRESET or errCode == EPIPE proc keepSendingTo(c: AsyncSocket) {.async.} = + let messagePadding = repeat('x', messagePaddingSize) while true: - # This write will eventually get stuck because the client is not reading - # its messages. - let sendFut = c.send("Foobar" & $sent & "\n", flags = {}) + # Larger writes reach socket backpressure quickly even on slow CI machines. + # This write will eventually get stuck because the client is not reading. + # Keep the padding after the newline so recvLine does not drain it. + let sendFut = c.send("Foobar" & $sent & "\n" & messagePadding, flags = {}) var sendTimedOut = false try: # On some platforms (notably macOS ARM64), the kernel may return diff --git a/tests/async/tasyncdispatchordering.nim b/tests/async/tasyncdispatchordering.nim new file mode 100644 index 0000000000..5b226bad8a --- /dev/null +++ b/tests/async/tasyncdispatchordering.nim @@ -0,0 +1,32 @@ +discard """ + action: run +""" + +import asyncdispatch, os + +proc wrap(fut: Future[void]): Future[void] = + result = newFuture[void]("wrap") + let retFuture = result + fut.addCallback proc () = + if fut.failed: + retFuture.fail(fut.error) + else: + retFuture.complete() + +block: + let root = newFuture[void]("root") + let wrapped = wrap(wrap(wrap(root))) + let completedBeforeDeadline = withTimeout(wrapped, 20) + + # Completion has happened at the bottom of the future chain, but its + # callbacks cannot propagate until control reaches the dispatcher. + root.complete() + sleep(40) + + doAssert waitFor(completedBeforeDeadline) + +block: + var callbackRan = false + sleepAsync(0).addCallback proc () = callbackRan = true + poll(0) + doAssert callbackRan From 0021205854a703cb00121435df95a560a4abbf88 Mon Sep 17 00:00:00 2001 From: pacien Date: Sat, 25 Jul 2026 17:08:45 +0200 Subject: [PATCH 06/22] std/xmltree/constructor macro: fix quoting in output (#26039) (#26040) `toStrLit()` uses `repr()` internally, which forwards quotes and messes with dashes in the output. Let's use `newStrLitNode()` directly instead. GitHub: fixes https://github.com/nim-lang/Nim/issues/26039 --- lib/pure/xmltree.nim | 7 ++----- tests/stdlib/txmltree.nim | 11 +++++++++++ 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/lib/pure/xmltree.nim b/lib/pure/xmltree.nim index bbb03ad447..f7deb9879f 100644 --- a/lib/pure/xmltree.nim +++ b/lib/pure/xmltree.nim @@ -913,17 +913,14 @@ proc findAll*(n: XmlNode, tag: string, caseInsensitive = false): seq[XmlNode] = proc xmlConstructor(a: NimNode): NimNode = if a.kind == nnkCall: - result = newCall("newXmlTree", toStrLit(a[0])) + result = newCall("newXmlTree", newStrLitNode($a[0])) var attrs = newNimNode(nnkBracket, a) var newStringTabCall = newCall(bindSym"newStringTable", attrs, bindSym"modeCaseSensitive") var elements = newNimNode(nnkBracket, a) for i in 1..a.len-1: if a[i].kind == nnkExprEqExpr: - # In order to support attributes like `data-lang` we have to - # replace whitespace because `toStrLit` gives `data - lang`. - let attrName = toStrLit(a[i][0]).strVal.replace(" ", "") - attrs.add(newStrLitNode(attrName)) + attrs.add(newStrLitNode($a[i][0])) attrs.add(a[i][1]) #echo repr(attrs) else: diff --git a/tests/stdlib/txmltree.nim b/tests/stdlib/txmltree.nim index add12a3fc0..138cfe3166 100644 --- a/tests/stdlib/txmltree.nim +++ b/tests/stdlib/txmltree.nim @@ -118,3 +118,14 @@ block: #21541 doAssert temp.text == "Hello!" temp.text = "Hola!" doAssert temp.text == "Hola!" + +block: #26039 + let tree = <>rss( + "xmlns:atom" = "http://www.w3.org/2005/Atom", + <>"atom:link"( + `data-dummy` = "test", + ), + ) + doAssert $tree == """ + +""" From 2d8114929450ad621a2ef0108bbf1267c45145fc Mon Sep 17 00:00:00 2001 From: Ryan McConnell Date: Sun, 26 Jul 2026 12:08:44 -0400 Subject: [PATCH 07/22] unwrap typedesc in semSet to enable stuff like `set[T.distinctBase]` (#25924) `distinctBase` results in typedesc, so `set[T.distinctBase]` received `typedesc[range[...]]` as its element type, which `isOrdinalType` rejects. Strip the wrapper in `semSet` before storing the element type and checking ordinality. Also add `tyFromExpr` to the deferred-check set so the error doesn't fire prematurely inside generic bodies - same pattern already used by `semArray`. --- compiler/semtypes.nim | 3 ++- tests/set/tset_range_trait.nim | 39 ++++++++++++++++++++++++++++++++++ 2 files changed, 41 insertions(+), 1 deletion(-) create mode 100644 tests/set/tset_range_trait.nim diff --git a/compiler/semtypes.nim b/compiler/semtypes.nim index a026fc994a..1c4c81c64c 100644 --- a/compiler/semtypes.nim +++ b/compiler/semtypes.nim @@ -219,9 +219,10 @@ proc semSet(c: PContext, n: PNode, prev: PType): PType = result = newOrPrevType(tySet, prev, c) if n.len == 2 and n[1].kind != nkEmpty: var base = semTypeNode(c, n[1], nil) + if base.kind == tyTypeDesc: base = base.base # unwrap from type traits like distinctBase addSonSkipIntLit(result, base, c.idgen) if base.kind in {tyGenericInst, tyAlias, tySink}: base = skipModifier(base) - if base.kind notin {tyGenericParam, tyGenericInvocation}: + if base.kind notin {tyGenericParam, tyGenericInvocation, tyFromExpr}: if base.kind == tyForward: c.forwardTypeUpdates.add (getCurrOwner(c), result, n) elif not isOrdinalType(base, allowEnumWithHoles = true): diff --git a/tests/set/tset_range_trait.nim b/tests/set/tset_range_trait.nim new file mode 100644 index 0000000000..0eafdca1f8 --- /dev/null +++ b/tests/set/tset_range_trait.nim @@ -0,0 +1,39 @@ +# Test that set[] accepts range types via typedesc[R], and set[typedesc[R]] +# must unwrap the typedesc wrapper before checking ordinality. + +import std/typetraits + +type + TestDistinctRange = distinct range[0 .. 63] + +block: # explicit range type as set base + type S = set[range[0 .. 63]] + var s: S = {0, 1} + doAssert 0 in s + +block: # distinctBase result as set base (non-generic) + type S = set[TestDistinctRange.distinctBase] + var s: S = {0, 1} + doAssert 0 in s + +block: # range alias as set base + type RangeAlias = range[0 .. 63] + type S = set[RangeAlias] + var s: S = {0, 1} + doAssert 0 in s + +block: # set[T.distinctBase] in generic body type position + proc test[T: TestDistinctRange]() = + var s: set[T.distinctBase] + s = {0, 1} + doAssert 0 in s + + test[TestDistinctRange]() + +block: # passing set[T.distinctBase] to a proc expecting set[0..63] + proc accept(x: typedesc[set[0 .. 63]]) = discard + + proc pass[T: TestDistinctRange](p: typedesc[set[T]]) = + accept(set[T.distinctBase]) + + pass(set[TestDistinctRange]) From c2cef51b629dbade114ae4e74c30d123329a179c Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Thu, 30 Jul 2026 15:08:43 +0800 Subject: [PATCH 08/22] Bump actions/stale from 10 to 11 (#26055) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Bumps [actions/stale](https://github.com/actions/stale) from 10 to 11.
Release notes

Sourced from actions/stale's releases.

v11.0.0

What's Changed

Enhancement

Dependency Update

Full Changelog: https://github.com/actions/stale/compare/v10...v11.0.0

v10.4.0

What's Changed

Bug Fix

Dependency Updates

New Contributors

Full Changelog: https://github.com/actions/stale/compare/v10.3.0...v10.4.0

v10.3.0

What's Changed

Bug Fix

Dependency Updates

New Contributors

Full Changelog: https://github.com/actions/stale/compare/v10...v10.3.0

v10.2.0

What's Changed

Bug Fix

Dependency Updates

New Contributors

Full Changelog: https://github.com/actions/stale/compare/v10...v10.2.0

... (truncated)

Changelog

Sourced from actions/stale's changelog.

Changelog

[10.1.0]

What's Changed

[10.0.0]

What's Changed

Breaking Changes

Enhancement

Dependency Upgrades

Documentation changes

[9.1.0]

What's Changed

[9.0.0]

Breaking Changes

  1. Action is now stateful: If the action ends because of operations-per-run then the next run will start from the first unprocessed issue skipping the issues processed during the previous run(s). The state is reset when all the issues are processed. This should be considered for scheduling workflow runs.
  2. Version 9 of this action updated the runtime to Node.js 20. All scripts are now run with Node.js 20 instead of Node.js 16 and are affected by any breaking changes between Node.js 16 and 20.

... (truncated)

Commits
  • 4391f3d Fix 24 high severity vulnerabilities by overriding brace-expansion to 5.0.8 (...
  • eaf9131 refactor: update imports to use ES module syntax and improve test structure (...
  • See full diff in compare view

[![Dependabot compatibility score](https://dependabot-badges.githubapp.com/badges/compatibility_score?dependency-name=actions/stale&package-manager=github_actions&previous-version=10&new-version=11)](https://docs.github.com/en/github/managing-security-vulnerabilities/about-dependabot-security-updates#about-compatibility-scores) Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) ---
Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- .github/workflows/stale.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/stale.yml b/.github/workflows/stale.yml index b918b21050..a59bb5f91f 100644 --- a/.github/workflows/stale.yml +++ b/.github/workflows/stale.yml @@ -9,7 +9,7 @@ jobs: stale: runs-on: ubuntu-latest steps: - - uses: actions/stale@v10 + - uses: actions/stale@v11 with: days-before-pr-stale: 365 days-before-pr-close: 30 From 3126a47590bb2cf00834a6960691fd6530de45c7 Mon Sep 17 00:00:00 2001 From: Andreas Rumpf Date: Thu, 30 Jul 2026 14:54:12 +0200 Subject: [PATCH 09/22] YRC: optimizations (#26042) --- compiler/liftdestructors.nim | 18 +- lib/core/locks.nim | 10 +- lib/system/yrc.nim | 542 +++++++++++++++++++-------- lib/system/yrc_opt_proof.lean | 668 ++++++++++++++++++++++++++++++++++ lib/system/yrc_proof.lean | 33 +- 5 files changed, 1115 insertions(+), 156 deletions(-) create mode 100644 lib/system/yrc_opt_proof.lean diff --git a/compiler/liftdestructors.nim b/compiler/liftdestructors.nim index aa8a20bc2a..032a4623f2 100644 --- a/compiler/liftdestructors.nim +++ b/compiler/liftdestructors.nim @@ -806,8 +806,22 @@ proc atomicRefOp(c: var TLiftCtx; t: PType; body, x, y: PNode) = createTypeBoundOps(c.g, c.c, elemType, c.info, c.idgen) - # YRC uses dedicated runtime procs for the entire write barrier: - if c.g.config.selectedGC == gcYrc: + # YRC uses dedicated runtime procs for the entire write barrier -- but ONLY + # for refs that can actually form cycles. Routing an acyclic ref through + # `nimAsgnYrc` defeats the entire purpose of `.acyclic`: the barrier defers + # the dec into a stripe queue, `drainStripe` then hands the cell to + # `registerLocal`, and it enters the collector as a capture ROOT -- so a + # type annotated precisely to stay out of the cycle collector gets traced + # by it anyway. (The collector never reaches such a cell by TRAVERSAL: the + # attachedTrace hook below only emits `nimTraceRef` when `isCyclic`. The + # queued dec was the only way in.) + # + # Falling through instead gives acyclic refs the same prompt arc-style + # reclamation they get under --mm:arc/orc, which is also what lets a thread + # that avoids cycles at compile time avoid the collector entirely at run + # time. `canFormAcycle` is the same predicate ccgtypes.nim:1903 uses to set + # the descriptor's acyclic flag, so codegen and runtime cannot disagree. + if c.g.config.selectedGC == gcYrc and types.canFormAcycle(c.g, elemType): let desc = if isFinal(elemType): let ti = genBuiltin(c, mGetTypeInfoV2, "getTypeInfoV2", newNodeIT(nkType, x.info, elemType)) diff --git a/lib/core/locks.nim b/lib/core/locks.nim index 5237274792..d219771b76 100644 --- a/lib/core/locks.nim +++ b/lib/core/locks.nim @@ -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 = diff --git a/lib/system/yrc.nim b/lib/system/yrc.nim index 681fb1db94..0a73fd72ea 100644 --- a/lib/system/yrc.nim +++ b/lib/system/yrc.nim @@ -5,8 +5,10 @@ # See yrc_proof.lean for a machine-checked (Lean 4) proof of the core # invariants — garbage stability, validation soundness, capture partition # disjointness, grace periods, fence mutual exclusion, deadlock freedom — -# and yrc_tarjan_proof.lean for soundness AND completeness of the SCC -# deadness algorithm. +# yrc_tarjan_proof.lean for soundness AND completeness of the SCC +# deadness algorithm, and yrc_opt_proof.lean for the three optimizations +# that changed those invariants: SCC-uniform epoch ages, the demand-grown +# `gParSlots` pool, and deferred reclamation (gPendingCells). # # ## Synchronization at a Glance # @@ -25,7 +27,7 @@ # collection anywhere. A cell sits in at most one buffer, guarded by an # atomic test-and-set of inRootsFlag; buffered cells are forced live. # -# Up to MaxPar collections run CONCURRENTLY — with the mutators and with +# Up to one collection PER THREAD runs CONCURRENTLY — with the mutators and with # each other — each capturing a disjoint partition of the heap by CAS-ing # a claim tag into the rootIdx header word. gMergeLock covers only the # tag-slot claim and orphan adoption. All waiting (for a free slot, for a @@ -255,10 +257,6 @@ proc setLenZeroed[T](s: var RawSeq[T]; n: int) = s.len = n zeroMem(s.d, n *% sizeof(T)) -proc setLenUninit[T](s: var RawSeq[T]; n: int) = - if s.cap < n: resize(s, n) - s.len = n - type TraceEntry = object ## (slot, value) snapshot taken at trace time. The value is read exactly @@ -270,6 +268,7 @@ type TarjanFrame = object u: int32 # dense index of the cell this frame belongs to + ebase: int32 # edges.len when this cell's frame was pushed base: int # traceStack.len before this cell's trace ran CaptureRec = object @@ -281,7 +280,7 @@ type desc: PNimTypeV2 rcWord: int # rc word as captured lowlink: int32 - sccOf: int32 # -1 while the cell is on the Tarjan stack + selfRefs: int32 # self edges, folded out of the edge array SccRec = object ## per SCC of the condensation; the deadness pass reads all of these @@ -293,7 +292,6 @@ type deadIn: int # number of edges from dead SCCs memStart: int32 # offset into sccMembers crossOff: int32 # offset into crossTgt (cross edges by source) - crossCursor: int32 flags: uint8 CaptureBufs = object @@ -301,9 +299,19 @@ type ## threadvar) and persistent across collections, so that frequent ## small collections don't pay per-collection allocations recs: RawSeq[CaptureRec] + sccIdx: RawSeq[int32] # per captured cell: its SCC, -1 while the cell + # is on the Tarjan stack. Deliberately NOT a + # CaptureRec field: it is read once per captured + # EDGE, and a 4-byte stride keeps that array + # L1-resident where a 32-byte record stride would + # miss on almost every edge. tstack: RawSeq[int32] frames: RawSeq[TarjanFrame] - edges: RawSeq[int64] # (u shl 32) or v, dense indices + edges: RawSeq[int32] # PENDING out-edge targets (dense indices) of the + # SCCs still being built. An SCC's edges are + # classified and dropped the moment it is emitted + # (see `capture`), so this stays proportional to + # the DFS frontier, not to the captured graph. sccs: RawSeq[SccRec] sccMembers: RawSeq[int32] crossTgt: RawSeq[int32] @@ -336,10 +344,11 @@ proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} = # The spare rootIdx header word (unused by YRC's root registration, which # relies on inRootsFlag) doubles as the capture claim: it packs the owning -# collection's tag with the cell's dense discovery index. Up to MaxPar -# collections run CONCURRENTLY, each capturing a disjoint partition of the -# heap: the first collection to CAS its tag into a cell owns it; everyone -# else treats the cell as an opaque survivor. Stale tags (from retired +# collection's tag with the cell's dense discovery index. Collections run +# CONCURRENTLY — one slot per collecting thread, see gParSlots — each +# capturing a disjoint partition of the heap: the first collection to CAS +# its tag into a cell owns it; everyone else treats the cell as an opaque +# survivor. Stale tags (from retired # collections) never need clearing, they are simply reclaimable. # # The word does double duty a second time: commit re-stamps proven-live @@ -350,13 +359,29 @@ proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} = # collection. Roots always bypass the stamp: every death has a dec-witness # that gets registered, and registered cells are always scanned as roots. const - MaxPar {.intdefine.} = 8 # max concurrent collections + MaxPar {.intdefine.} = 256 + ## CAPACITY of the slot table, not a tuning knob: a hard ceiling on + ## concurrent collections, sized to stay out of the way (16 bytes of BSS + ## per entry, and scans only ever run over `gParSlots`, below). Raise it + ## only for programs with more than this many threads collecting AT ONCE. ParSlots = MaxPar var gMergeLock: Lock # protects the tag slots + orphaned roots gActiveTags: array[ParSlots, int64] # 0 = free slot gSlotPhase: array[ParSlots, int] # 0 idle, 1 capturing, 2 committing + gParSlots: int = 1 + ## How many slots are IN PLAY. Every scan below runs over this prefix + ## rather than over the whole table, and it is raised (under gMergeLock, + ## never lowered) exactly when a thread wants to collect and every slot + ## already in play is busy. It therefore converges on the number of + ## threads that actually collect CONCURRENTLY — one slot each — and then + ## stops: the parallelism is auto-tuned to the workload instead of being + ## a compile-time guess. A fixed bound throttled hard whenever the thread + ## count exceeded it, because the surplus threads did not just collect + ## later, they PARKED in `parkUntil(anySlotFree())` waiting for a slot + ## (32 threads against 8 slots: 6.3s vs 2.6s with a slot each). + ## Starting at 1 also means single-threaded programs scan one entry. gSoloCapture: int # a solo collection is in its capture phase gTagCounter: int64 gMyTag {.threadvar.}: int64 @@ -399,9 +424,19 @@ const epochBase = 0x40000000 # stamp namespace: tags stay below this epochMask = 0x3FFFFFFF -# stamp layout: high word = epochBase|epoch, low word = survival age +# Every packed word in this file squeezes two 32-bit fields into one int64 as +# `(hi shl 32) or lo`. The claim word (a cell's `rootIdx`, see above) is either +# hi = owning collection's tag, lo = the cell's dense capture index +# hi = epochBase|epoch (a stamp), lo = the cell's survival age +# and a `gPendingWatch` entry is hi = slot, lo = tag. The high half is read +# with a plain `shr 32` — every value stored there is below 2^31, so the shift +# keeps it positive and needs no mask. The low half is the one that needs +# masking: `shl 32` left the high half sitting above it, and `and 0xFFFFFFFF` +# is what clears those bits back out. +template loWord(w: int64): int64 = w and 0xFFFFFFFF + template epochStamp(e: int): int64 = int64(epochBase or (e and epochMask)) shl 32 -template stampAge(w: int64): int = int(w and 0xFFFFFFFF) +template stampAge(w: int64): int = int(loWord(w)) template isEpochStamp(w: int64): bool = (w shr 32) >= epochBase template parkUntil(cond: untyped) = @@ -426,9 +461,17 @@ proc collectorEvent() {.inline.} = broadcast gWaitCond release gWaitLock +proc slotsInPlay(): int {.inline.} = + ## Must be loaded AFTER whatever claim word the caller is validating: a + ## slot is put in play before the collection owning it can tag any cell, + ## so a load ordered after reading a tagged word is guaranteed to cover + ## the slot that wrote the tag. `gParSlots` only ever grows, so a scan + ## over this prefix can never shrink under a reader. + atomicLoadN(addr gParSlots, ATOMIC_ACQUIRE) + proc anySlotFree(): bool {.inline.} = result = false - for sl in 0 ..< ParSlots: + for sl in 0 ..< slotsInPlay(): if atomicLoadN(addr gActiveTags[sl], ATOMIC_ACQUIRE) == 0: return true @@ -438,12 +481,12 @@ template isStamped(c: Cell): bool = # value routes into claimCell which re-validates with acquire + CAS. (atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) shr 32) == gMyTag template denseIdx(c: Cell): int32 = - int32(atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) and 0xFFFFFFFF) + int32(loWord(atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED))) proc isActiveTag(t: int64): bool {.inline.} = result = false if t != 0: - for s in 0 ..< ParSlots: + for s in 0 ..< slotsInPlay(): if atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) == t: return true @@ -485,6 +528,25 @@ var ## draining this thread's stripe queue registers candidates here, and ## this thread's collections steal it as their slice — no lock, and ## collections keep the cache locality of thread-local data. + gPendingCells {.threadvar.}: CellSeq[Cell] + ## Cells this thread committed dead — slots nil'ed, references already + ## decremented — but has not handed back to the allocator yet, because a + ## capture that was in flight at commit time may still hold a stale + ## (slot, value) snapshot pointing at them. Released at the start of this + ## thread's next collection; see `releasePending`. + gPendingWatch {.threadvar.}: RawSeq[int64] + ## The captures that batch must outlive, packed as (slot shl 32) or tag. + gPendingSlot {.threadvar.}: int + gPendingActive {.threadvar.}: bool + gSpareRoots {.threadvar.}: CellSeq[Cell] + ## The buffer a finished collection hands back, so that stealing + ## `gLocalRoots` costs no allocation in steady state. + gTraceBuf {.threadvar.}: CellSeq[TraceEntry] + gFreeBuf {.threadvar.}: CellSeq[Cell] + ## Storage for `GcEnv.traceStack` / `GcEnv.toFree`, kept across + ## collections like the `gCap` arrays: both grow to the size of the + ## captured graph, so re-allocating and re-growing them per collection + ## was a memcpy of the whole trace frontier every time. stripes: array[NumStripes, Stripe] rootsThreshold: int = 128 # shared adaptive heuristic; races are benign defaultThreshold = when defined(nimFixedOrc): 10_000 else: 128 @@ -677,6 +739,62 @@ template orcAssert(cond, msg) = cfprintf(cstderr, "[Bug!] %s\n", msg) rawQuit 1 +proc graceSatisfied(): bool = + ## Has every capture recorded in `gPendingWatch` finished? A capture that + ## started later cannot hold a stale snapshot of the batch: it reads every + ## slot fresh, and the batch's cells are unreachable by then. + result = true + for i in 0 ..< gPendingWatch.len: + let w = gPendingWatch.d[i] + let s = int(w shr 32) + let tg = loWord(w) + if atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) == tg and + atomicLoadN(addr gSlotPhase[s], ATOMIC_ACQUIRE) == 1: + return false + +proc buildPendingWatch(): bool = + ## Record the collections that are in their CAPTURE phase right now: they + ## are the only ones that can hold a stale (slot, value) snapshot of the + ## cells we are about to release. `false` (nothing capturing) is the common + ## case below a handful of threads, and means the batch can be freed on the + ## spot with no deferral and no destructor-timing change at all. + if gPendingWatch.d == nil: init gPendingWatch + gPendingWatch.len = 0 + for s in 0 ..< slotsInPlay(): + if s != gMySlot: + let tg = atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) + if tg != 0 and atomicLoadN(addr gSlotPhase[s], ATOMIC_ACQUIRE) == 1: + gPendingWatch.add((int64(s) shl 32) or tg) + result = gPendingWatch.len > 0 + +proc releasePending() = + ## Hand this thread's parked batch back to the allocator and give its slot + ## up. Called at the start of every collection, so by the time it runs the + ## watched captures have had a whole collection's worth of time to finish + ## and the wait below is virtually always already satisfied — that is the + ## whole point: the wait moved off the commit path, where it blocked BOTH + ## the committing collector and (because commit runs inside the GC fence) + ## every mutator doing a seq operation. + if not gPendingActive: return + parkUntil(graceSatisfied()) + # Give the slot up FIRST: the batch is unreachable and no capture can hold + # a snapshot of it any more, so the tag has nothing left to protect. + gPendingActive = false + gPendingWatch.len = 0 + atomicStoreN(addr gActiveTags[gPendingSlot], 0, ATOMIC_SEQ_CST) + collectorEvent() + # Destructors run here. `Collecting` is the existing re-entrancy guard: a + # destructor-driven dec that overflows a stripe must drain it, not start a + # nested collection that would write into the batch we are walking. + let prev = lockState + lockState = Collecting + for i in 0 ..< gPendingCells.len: + when orcLeakDetector: + writeCell("CYCLIC OBJECT FREED", gPendingCells.d[i][0], gPendingCells.d[i][1]) + free(gPendingCells.d[i][0], gPendingCells.d[i][1]) + gPendingCells.len = 0 + lockState = prev + proc nimTraceRef(q: pointer; desc: PNimTypeV2; env: pointer) {.compilerRtl, inl.} = let p = cast[ptr pointer](q) # read the slot exactly once: mutators may exchange it concurrently. @@ -698,6 +816,7 @@ proc nimTraceRefDyn(q: pointer; env: pointer) {.compilerRtl, inl.} = proc prepareCapture() = if gCap.recs.d == nil: init gCap.recs + init gCap.sccIdx init gCap.tstack init gCap.frames init gCap.edges @@ -709,11 +828,13 @@ proc prepareCapture() = init gCap.ages else: gCap.recs.len = 0 + gCap.sccIdx.len = 0 gCap.tstack.len = 0 gCap.frames.len = 0 gCap.edges.len = 0 gCap.sccs.len = 0 gCap.sccMembers.len = 0 + gCap.crossTgt.len = 0 gCap.crossPend.len = 0 gCap.prunedSrc.len = 0 gCap.ages.len = 0 @@ -722,18 +843,22 @@ proc prepareCapture() = # inRootsFlag between capture and commit, which must not look like a # mutation to the commit-time rc validation. proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs; - pruneLive: bool): int32 = + pruneLive: bool; old0: int64): int32 = ## Dense index if this collection owns `c` (claiming and registering it ## if it was unclaimed), -1 if another ACTIVE collection owns it, or ## -2 if `pruneLive` and the cell was proven live in the current epoch ## (treat as an opaque live external, don't descend). + ## + ## `old0` is `c`'s claim word as the caller already read it (acquire): the + ## DFS reads it to test ownership, and re-reading it here would be a second + ## dependent load of the same cold header word on every traversed edge. if gAmSolo: # no other collection is (or can start) capturing: plain stores. # This recovers the sequential capture speed of the single-collector # design whenever collections do not actually overlap. - let old = c.rootIdx + let old = old0 if (old shr 32) == gMyTag: - return int32(old and 0xFFFFFFFF) + return int32(loWord(old)) if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and stampAge(old) >= YrcPromoteAge: return -2 @@ -744,18 +869,22 @@ proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs; if old != 0: bumpStat gStatCapRepeat cap.recs.add CaptureRec(cell: c, desc: desc, rcWord: loadRc(c) and not rcMask, - lowlink: int32(idx), sccOf: -1'i32) + lowlink: int32(idx), selfRefs: 0'i32) + cap.sccIdx.add -1'i32 cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0) cap.tstack.add int32(idx) return int32(idx) + var old = old0 while true: - var old = atomicLoadN(addr c.rootIdx, ATOMIC_ACQUIRE) if (old shr 32) == gMyTag: - return int32(old and 0xFFFFFFFF) + return int32(loWord(old)) if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and stampAge(old) >= YrcPromoteAge: return -2 - if isActiveTag(old shr 32): + # an epoch stamp is never a tag (tags are allocated below `epochBase`), + # so the scan over the active-tag slots is skipped for the common + # "cell survived an earlier collection" word + if not isEpochStamp(old) and isActiveTag(old shr 32): return -1 let idx = cap.recs.len if atomicCompareExchangeN(addr c.rootIdx, addr old, @@ -766,38 +895,69 @@ proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs; if old != 0: bumpStat gStatCapRepeat cap.recs.add CaptureRec(cell: c, desc: desc, rcWord: loadRc(c) and not rcMask, - lowlink: int32(idx), sccOf: -1'i32) + lowlink: int32(idx), selfRefs: 0'i32) + cap.sccIdx.add -1'i32 cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0) cap.tstack.add int32(idx) return int32(idx) + # a failed CAS leaves the fresh claim word in `old`; loop with it proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) = ## Iterative Tarjan SCC over everything reachable from `s`. A frame's ## pending out-edges are the traceStack entries above frame.base; a child ## pushes and drains its own segment above ours, so when the child's frame ## pops, the stack is back at our segment and we resume popping our edges. - if isStamped(s): return + ## + ## An SCC's out-edges are classified into internal/cross the moment the SCC + ## is emitted, not in a later pass over a whole-graph edge list. That works + ## because `cap.edges` is truncated back to a frame's `ebase` whenever that + ## frame's cell turns out to be an SCC root: edges of already-emitted + ## sub-SCCs are gone, so `edges[ebase(u) ..< len]` at u's emission holds + ## exactly the out-edges of u's SCC. Every one of them targets either a + ## member (u would not be an SCC root if a member pointed at a cell still + ## on the stack below u) or an SCC emitted earlier, so `sccIdx` is final + ## for all of them and the cross targets can be appended to `crossTgt` + ## contiguously — which makes `crossOff` a prefix offset for free. + let rootWord = atomicLoadN(addr s.rootIdx, ATOMIC_ACQUIRE) + if (rootWord shr 32) == gMyTag: return orcAssert(j.traceStack.len == 0, "capture: trace stack not empty") # roots never prune: a dec-witnessed suspicion overrides any epoch stamp - let root = claimCell(s, desc, cap, pruneLive = false) + let root = claimCell(s, desc, cap, pruneLive = false, old0 = rootWord) if root < 0: return # another active collection owns this candidate; it handles it trace(s, desc, j) - cap.frames.add TarjanFrame(u: root, base: 0) - while cap.frames.len > 0: - let u = cap.frames.d[cap.frames.len -% 1].u - let base = cap.frames.d[cap.frames.len -% 1].base + # The innermost frame is kept in `u`/`base` instead of being re-read from + # `cap.frames` on every iteration: the loop body runs once per captured + # EDGE, so reloading the frame there costs more than the frame stack itself. + # `cap.frames` therefore only holds the ANCESTORS of `u`. + var u = root + var base = 0 + var ebase = 0'i32 + while true: if j.traceStack.len > base: - let (entry, tdesc) = j.traceStack.pop() - let t = head(entry.val) - if isStamped(t): - let v = denseIdx(t) - cap.edges.add (int64(u) shl 32) or int64(v) - if cap.recs.d[v].sccOf < 0 and v < cap.recs.d[u].lowlink: - cap.recs.d[u].lowlink = v + # inlined pop: the stamped path never needs the entry's descriptor + let last = j.traceStack.len -% 1 + j.traceStack.len = last + let t = head(j.traceStack.d[last][0].val) + # one load of the target's claim word serves both the ownership test + # and the dense-index extraction + let cw = atomicLoadN(addr t.rootIdx, ATOMIC_ACQUIRE) + if (cw shr 32) == gMyTag: + let v = int32(loWord(cw)) + if v == u: + # A self edge is internal by construction and its reference is + # already in `rcWord`, so it cancels out of `sumRefs - internal` + # exactly. Counting it here keeps it out of the edge array and out + # of the classification pass below. + inc cap.recs.d[u].selfRefs + else: + cap.edges.add v + if cap.sccIdx.d[v] < 0 and v < cap.recs.d[u].lowlink: + cap.recs.d[u].lowlink = v else: + let tdesc = j.traceStack.d[last][1] let childBase = j.traceStack.len - let v = claimCell(t, tdesc, cap, pruneLive = true) + let v = claimCell(t, tdesc, cap, pruneLive = true, old0 = cw) if v == -1: # cross-collection edge: the owner sees our reference in the rc # word and classifies the target live; we re-register it as a @@ -810,75 +970,72 @@ proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) = when defined(nimOrcStats): bumpStat gStatCapPruned else: - cap.edges.add (int64(u) shl 32) or int64(v) + cap.edges.add v trace(t, tdesc, j) - cap.frames.add TarjanFrame(u: v, base: childBase) + cap.frames.add TarjanFrame(u: u, ebase: ebase, base: base) + u = v + ebase = int32(cap.edges.len) + base = childBase else: - cap.frames.len = cap.frames.len -% 1 - if cap.frames.len > 0: - let pu = cap.frames.d[cap.frames.len -% 1].u - if cap.recs.d[u].lowlink < cap.recs.d[pu].lowlink: - cap.recs.d[pu].lowlink = cap.recs.d[u].lowlink - if cap.recs.d[u].lowlink == u: + let lowU = cap.recs.d[u].lowlink + if lowU == u: # u is the root of an SCC: pop the members off the Tarjan stack + let sid = int32(j.nScc) let memStart = int32(cap.sccMembers.len) var sum = 0 while true: - let w = cap.tstack.pop() - cap.recs.d[w].sccOf = int32(j.nScc) - cap.sccMembers.add w - sum = sum +% (cap.recs.d[w].rcWord shr rcShift) +% 1 - if w == u: break - cap.sccs.add SccRec(sumRefs: sum, memStart: memStart) + let m = cap.tstack.pop() + cap.sccIdx.d[m] = sid + cap.sccMembers.add m + # `- selfRefs`: a self edge counts in both `sumRefs` and `internal` + # and was folded out of the edge array in the loop above + sum = sum +% (cap.recs.d[m].rcWord shr rcShift) +% 1 -% + cap.recs.d[m].selfRefs + if m == u: break + # classify this SCC's out-edges now that every target's SCC is final + let crossOff = int32(cap.crossTgt.len) + var internal = 0 + for i in ebase ..< int32(cap.edges.len): + let sv = cap.sccIdx.d[cap.edges.d[i]] + if sv == sid: inc internal + else: cap.crossTgt.add sv + cap.edges.len = ebase + cap.sccs.add SccRec(sumRefs: sum, internal: internal, + memStart: memStart, crossOff: crossOff) inc j.nScc + if cap.frames.len == 0: break + let pi = cap.frames.len -% 1 + cap.frames.len = pi + let pu = cap.frames.d[pi].u + if lowU < cap.recs.d[pu].lowlink: + cap.recs.d[pu].lowlink = lowU + u = pu + ebase = cap.frames.d[pi].ebase + base = cap.frames.d[pi].base # ---------------- phase 2: deadness, side arrays only ---------------- proc computeDeadness(j: var GcEnv; cap: ptr CaptureBufs) = let nScc = j.nScc - # append the sentinel record ([nScc]); capture left internal/deadIn/flags - # zero-initialized and memStart valid. crossOff is filled below as a prefix - # sum, so the sentinel closes the last SCC's member and cross-edge slices. - cap.sccs.add SccRec(memStart: int32(cap.sccMembers.len)) - # classify captured edges: internal to an SCC vs condensation cross edges - var nCross = 0 - for i in 0 ..< cap.edges.len: - let e = cap.edges.d[i] - let su = cap.recs.d[int32(e shr 32)].sccOf - let sv = cap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf - if su == sv: - inc cap.sccs.d[su].internal - else: - inc cap.sccs.d[su].crossOff - inc nCross - var total = 0'i32 - for s in 0 ..< nScc: - let c = cap.sccs.d[s].crossOff - cap.sccs.d[s].crossOff = total - cap.sccs.d[s].crossCursor = total - total = total +% c - cap.sccs.d[nScc].crossOff = total - setLenUninit cap.crossTgt, nCross - for i in 0 ..< cap.edges.len: - let e = cap.edges.d[i] - let su = cap.recs.d[int32(e shr 32)].sccOf - let sv = cap.recs.d[int32(e and 0xFFFFFFFF'i64)].sccOf - if su != sv: - cap.crossTgt.d[cap.sccs.d[su].crossCursor] = sv - inc cap.sccs.d[su].crossCursor + # append the sentinel record ([nScc]) that closes the last SCC's member and + # cross-edge slices; capture left deadIn/flags zero-initialized and filled + # sumRefs/internal/memStart/crossOff in already, so the condensation is + # complete the moment the DFS ends. + cap.sccs.add SccRec(memStart: int32(cap.sccMembers.len), + crossOff: int32(cap.crossTgt.len)) # pruned out-edges taint the source SCC: pruning cannot cause a false # "dead" (an untraced target only ever ADDS unexplained external refs), # but a "live" verdict may lean on a stamp that went stale within the # epoch, so validate re-registers surviving pruned SCCs for i in 0 ..< cap.prunedSrc.len: - let s = cap.recs.d[cap.prunedSrc.d[i]].sccOf + let s = cap.sccIdx.d[cap.prunedSrc.d[i]] cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagPruned # cells that stay registered as roots (partial collection) count as # externally referenced: the roots buffer itself points at them for mi in 0 ..< cap.sccMembers.len: let m = cap.sccMembers.d[mi] if (loadRc(cap.recs.d[m].cell) and inRootsFlag) != 0: - let s = cap.recs.d[m].sccOf + let s = cap.sccIdx.d[m] cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagForcedLive # deadness over the condensation. Tarjan emits sinks first, so higher SCC # ids are sources and every cross edge goes from a higher id to a lower @@ -910,7 +1067,7 @@ proc markDirtyFromQueues(j: var GcEnv; cap: ptr CaptureBufs) = template taint(cp: Cell) = let c = cp if isStamped(c): - let s = cap.recs.d[denseIdx(c)].sccOf + let s = cap.sccIdx.d[denseIdx(c)] cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagDirty for i in 0.. 0: let (entry, _) = j.traceStack.pop() entry.slot[] = nil - when orcLeakDetector: - writeCell("CYCLIC OBJECT FREED", cell, desc) - free(cell, desc) + holdOrFree(cell, desc, deferred) j.freed = cap.recs.len + if deferred: + gPendingSlot = gMySlot + gPendingActive = true else: - init j.toFree + if gFreeBuf.d == nil: init gFreeBuf + gFreeBuf.len = 0 + j.toFree = gFreeBuf for s in 0 ..< j.nScc: if (cap.sccs.d[s].flags and flagDead) != 0: for mi in cap.sccs.d[s].memStart ..< cap.sccs.d[s+1].memStart: @@ -1067,32 +1239,60 @@ proc commitDead(j: var GcEnv; cap: ptr CaptureBufs) = let (entry, tdesc) = j.traceStack.pop() let t = head(entry.val) entry.slot[] = nil - if not deadCell(t): + let tw = atomicLoadN(addr t.rootIdx, ATOMIC_RELAXED) + if not deadCell(tw): trialDec(t) # a stamped target was not analyzed by THIS collection, so # this dec may be the death blow: keep the cell examinable - if isEpochStamp(atomicLoadN(addr t.rootIdx, ATOMIC_RELAXED)): + if isEpochStamp(tw): registerLocal(t, tdesc) - # epoch-stamp what this collection PROVED live, carrying the cell's - # survival age: only cells that keep surviving get promoted to ages - # where captures prune them, so die-young data is never deferred. - # Demoted (dirty) and pruned SCCs stay unproven — leave their stale - # tags claimable. Our tag is still active, so no foreign claim can - # race these stores. + # epoch-stamp what this collection PROVED live, carrying the survival + # age: only cells that keep surviving get promoted to ages where + # captures prune them, so die-young data is never deferred. Demoted + # (dirty) and pruned SCCs stay unproven — leave their stale tags + # claimable. Our tag is still active, so no foreign claim can race + # these stores. + # + # The age is the SCC's, not the cell's: the whole SCC gets the age of + # its YOUNGEST member, so promotion is all-or-nothing. A per-cell age + # lets one member of an SCC promote ahead of its own SCC-mates; the + # next capture then prunes that INTERNAL edge, which taints the SCC as + # flagPruned, which stops it from ever being stamped again — freezing + # every member's age at its current value and re-tracing the whole + # structure on every collection from then on. Members age at different + # rates whenever a structure is built incrementally (a list appended to + # across several collections), so this is the common case, not a corner + # one. Taking the minimum can only delay a promotion, never hasten one, + # so it cannot widen the floating-garbage bound. for s in 0 ..< j.nScc: if (cap.sccs.d[s].flags and (flagDead or flagDirty or flagPruned)) == 0: - for mi in cap.sccs.d[s].memStart ..< cap.sccs.d[s+1].memStart: - let m = cap.sccMembers.d[mi] - atomicStoreN(addr cap.recs.d[m].cell.rootIdx, - gMyEpochStamp or int64(cap.ages.d[m] +% 1), - ATOMIC_RELAXED) - graceWait() - for i in 0 ..< j.toFree.len: - when orcLeakDetector: - writeCell("CYCLIC OBJECT FREED", j.toFree.d[i][0], j.toFree.d[i][1]) - free(j.toFree.d[i][0], j.toFree.d[i][1]) + let memStart = cap.sccs.d[s].memStart + let memEnd = cap.sccs.d[s+1].memStart + var age = high(int32) + for mi in memStart ..< memEnd: + let a = cap.ages.d[cap.sccMembers.d[mi]] + if a < age: age = a + let stamp = gMyEpochStamp or int64(age +% 1) + for mi in memStart ..< memEnd: + atomicStoreN(addr cap.recs.d[cap.sccMembers.d[mi]].cell.rootIdx, + stamp, ATOMIC_RELAXED) j.freed = j.toFree.len - deinit j.toFree + if j.toFree.len > 0 and buildPendingWatch(): + # park the whole batch by swapping buffers: the collection keeps the + # (now empty) buffer the previous batch used, so neither side allocates + let spare = gPendingCells + gPendingCells = j.toFree + j.toFree = spare + j.toFree.len = 0 + gPendingSlot = gMySlot + gPendingActive = true + else: + for i in 0 ..< j.toFree.len: + when orcLeakDetector: + writeCell("CYCLIC OBJECT FREED", j.toFree.d[i][0], j.toFree.d[i][1]) + free(j.toFree.d[i][0], j.toFree.d[i][1]) + j.toFree.len = 0 + gFreeBuf = j.toFree proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; wait: bool; drainAll = false): bool = @@ -1100,11 +1300,12 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; ## collect) and try to become a collector over THIS THREAD's candidates: ## claim a tag slot — the only step still under gMergeLock — and steal ## the thread-local buffer as this collection's slice, lock-free. When - ## there is enough work but all ParSlots collections are running, `wait` - ## decides between parking until a slot frees (backpressure for - ## overflowing mutators) and giving up. Either way the drain happened, + ## there is enough work but the slot table is full (more than MaxPar + ## threads collecting at once), `wait` decides between parking until a + ## slot frees and giving up. Either way the drain happened, ## so the caller's overflowing queue has room again. result = false + releasePending() # last collection's batch: its watch list is long clear if drainAll: drainAllStripes() else: drainStripe(getStripeIdx()) adoptOrphans() @@ -1112,15 +1313,23 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; mayRunCycleCollect(): acquire gMergeLock var slot = -1 - for sl in 0 ..< ParSlots: + let inPlay = gParSlots + for sl in 0 ..< inPlay: if atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) == 0: slot = sl break + if slot < 0 and inPlay < ParSlots: + # Every slot in play is busy and the table has room: widen the pool + # instead of throttling this thread. Publishing the wider bound before + # the tag lands in the new slot is what makes `slotsInPlay` safe. + slot = inPlay + atomicStoreN(addr gParSlots, inPlay +% 1, ATOMIC_SEQ_CST) if slot < 0: release gMergeLock if not wait: break - # backpressure: all ParSlots collections are running; park until one - # finishes (finishCollection broadcasts) instead of burning a core + # the table itself is full (more than MaxPar threads collecting at + # once): park until one finishes (finishCollection broadcasts) + # instead of burning a core parkUntil(anySlotFree()) drainStripe(getStripeIdx()) # the world moved while we waited adoptOrphans() @@ -1131,7 +1340,7 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; gMySlot = slot gMyEpochStamp = epochStamp(atomicLoadN(addr gEpoch, ATOMIC_RELAXED)) var othersActive = false - for sl in 0 ..< ParSlots: + for sl in 0 ..< gParSlots: if sl != slot and atomicLoadN(addr gActiveTags[sl], ATOMIC_RELAXED) != 0: othersActive = true gAmSolo = not othersActive @@ -1143,7 +1352,12 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; # our buffer, our slice: no lock needed if keepBelow == 0: slice = gLocalRoots # steal the whole buffer - init(gLocalRoots) + if gSpareRoots.d != nil: + gLocalRoots = gSpareRoots + gLocalRoots.len = 0 + gSpareRoots = default(CellSeq[Cell]) + else: + init(gLocalRoots) else: init(slice, max(gLocalRoots.len - keepBelow, 8)) for i in keepBelow ..< gLocalRoots.len: @@ -1155,8 +1369,16 @@ proc startCollection(minRoots, keepBelow: int; slice: var CellSeq[Cell]; proc finishCollection() = if atomicAddFetch(addr gCollectionCounter, 1, ATOMIC_RELAXED) mod YrcEpochLen == 0: discard atomicAddFetch(addr gEpoch, 1, ATOMIC_RELAXED) - atomicStoreN(addr gActiveTags[gMySlot], 0, ATOMIC_SEQ_CST) - atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE) + if gPendingActive: + # A batch is parked under this collection's tag. Clear only the PHASE — + # so nobody's grace check waits on us — and leave the tag in + # `gActiveTags`: it is what stops a foreign capture from claiming, and + # then freeing, a cell that is sitting in the batch. `releasePending` + # gives the slot back. + atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE) + else: + atomicStoreN(addr gActiveTags[gMySlot], 0, ATOMIC_SEQ_CST) + atomicStoreN(addr gSlotPhase[gMySlot], 0, ATOMIC_RELEASE) gMyTag = 0 gAmSolo = false collectorEvent() # wake backpressure and grace waiters @@ -1170,7 +1392,9 @@ proc collectCyclesImpl(j: var GcEnv; slice: var CellSeq[Cell]) = for i in countdown(last, 0): writeCell("root", slice.d[i][0], slice.d[i][1]) - init j.traceStack + if gTraceBuf.d == nil: init gTraceBuf + gTraceBuf.len = 0 + j.traceStack = gTraceBuf prepareCapture() let cap = addr gCap # hoist the TLS lookup out of the hot loops j.nScc = 0 @@ -1194,11 +1418,11 @@ proc collectCyclesImpl(j: var GcEnv; slice: var CellSeq[Cell]) = commitDead(j, cap) j.keepThreshold = j.freed == j.touched and j.touched > 0 - deinit j.traceStack + gTraceBuf = j.traceStack # hand the (possibly grown) buffer back proc runCollection(j: var GcEnv; slice: var CellSeq[Cell]) = ## Runs one collection over the stolen slice, concurrently with mutators - ## AND with up to ParSlots-1 other collections over disjoint partitions. + ## AND with the other collecting threads over disjoint partitions. yrcGcFenceEnter() # freeze seq structure mutations, not ref writes if not gAmSolo: # a solo collection claims with plain stores; nobody else may claim @@ -1210,7 +1434,10 @@ proc runCollection(j: var GcEnv; slice: var CellSeq[Cell]) = lockState = prev yrcGcFenceExit() finishCollection() - deinit slice + if gSpareRoots.d == nil and slice.d != nil: + gSpareRoots = slice # recycle it as the next steal's replacement + else: + deinit slice when defined(nimOrcStats): var freedCyclicObjects {.threadvar.}: int @@ -1283,6 +1510,7 @@ proc GC_runOrc* = if startCollection(1, 0, slice, wait = true, drainAll = true): var j: GcEnv runCollection(j, slice) + releasePending() # GC_fullCollect must not leave a batch parked # note: aborted SCCs and cross-collection targets legitimately leave # re-registered roots behind; other RUNNING threads' local candidates # are theirs to collect (exiting threads spill to the orphan buffer) @@ -1315,6 +1543,7 @@ proc nimYrcThreadTeardown() = ## of ours is stranded in a queue no other thread hashes to, then spill ## our candidate buffer to the global orphan buffer, where the next ## collection on any thread adopts it. + releasePending() # nobody else can release this thread's parked batch drainStripe(getStripeIdx()) if gLocalRoots.len > 0: acquire gMergeLock @@ -1326,6 +1555,11 @@ proc nimYrcThreadTeardown() = deinit(gLocalRoots) gLocalRoots.d = nil gLocalRoots.len = 0 + deinit(gSpareRoots) + deinit(gTraceBuf) + deinit(gFreeBuf) + deinit(gPendingCells) + deinit(gPendingWatch) proc GC_enableMarkAndSweep*() = GC_enableOrc() proc GC_disableMarkAndSweep*() = GC_disableOrc() @@ -1362,7 +1596,27 @@ proc nimDecRefIsLastCyclicDyn(p: pointer): bool {.compilerRtl, inl.} = enqueueDec(head(p), cast[ptr PNimTypeV2](p)[]) proc nimDecRefIsLastDyn(p: pointer): bool {.compilerRtl, inl.} = - nimDecRefIsLastCyclicDyn(p) + ## ACYCLIC ref: prompt reclamation, exactly as under --mm:arc. This used to + ## forward to `nimDecRefIsLastCyclicDyn`, which enqueued the dec and so + ## dragged every `.acyclic` type through capture/deadness/commit -- the + ## precise opposite of what the annotation asks for. + ## + ## No grace period is needed here, and that is not an accident: the + ## collector has no way to be holding this cell. It cannot reach it by + ## traversal, because liftdestructors only emits `nimTraceRef` for fields + ## whose type is cyclic; and it cannot hold it as a capture root, because + ## roots come only from `registerLocal` on a drained dec, and an acyclic + ## dec is never queued now that `nimAsgnYrc` is gated on `canFormAcycle`. + ## Both halves must stay true together -- prompt reclamation here is only + ## sound while nothing else puts an acyclic cell into the collector. + result = false + if p != nil: + when hasThreadSupport: + result = atomicDec(head(p).rc, rcIncrement) == -rcIncrement + else: + let cell = head(p) + if (cell.rc and not rcMask) == 0: result = true + else: cell.rc = cell.rc -% rcIncrement proc nimDecRefIsLastCyclicStatic(p: pointer; desc: PNimTypeV2): bool {.compilerRtl, inl.} = result = false diff --git a/lib/system/yrc_opt_proof.lean b/lib/system/yrc_opt_proof.lean new file mode 100644 index 0000000000..79bec0d009 --- /dev/null +++ b/lib/system/yrc_opt_proof.lean @@ -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). +-/ diff --git a/lib/system/yrc_proof.lean b/lib/system/yrc_proof.lean index 64a501ed03..81d84197b6 100644 --- a/lib/system/yrc_proof.lean +++ b/lib/system/yrc_proof.lean @@ -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 From 3d0bac8e5b21b8e0372f083bb4d4c5763cd14edd Mon Sep 17 00:00:00 2001 From: Andreas Rumpf Date: Fri, 31 Jul 2026 05:34:47 +0200 Subject: [PATCH 10/22] YRC: micro optimizations (#26056) --- lib/system/yrc.nim | 163 ++++++++++++++++++++++++++++++--------------- 1 file changed, 111 insertions(+), 52 deletions(-) diff --git a/lib/system/yrc.nim b/lib/system/yrc.nim index 0a73fd72ea..deb4550443 100644 --- a/lib/system/yrc.nim +++ b/lib/system/yrc.nim @@ -230,6 +230,12 @@ proc add[T](s: var RawSeq[T]; v: T) {.inline.} = s.d[s.len] = v s.len = s.len +% 1 +proc addUnchecked[T](s: var RawSeq[T]; v: T) {.inline.} = + ## `add` without the capacity branch; the caller guarantees the room. + ## Used by `claimCell`, which reserves for all four of its arrays at once. + s.d[s.len] = v + s.len = s.len +% 1 + proc pop[T](s: var RawSeq[T]): T {.inline.} = s.len = s.len -% 1 result = s.d[s.len] @@ -358,6 +364,13 @@ proc trace(s: Cell; desc: PNimTypeV2; j: var GcEnv) {.inline.} = # long-lived live structures are traced once per epoch instead of once per # collection. Roots always bypass the stamp: every death has a dec-witness # that gets registered, and registered cells are always scanned as roots. +type + CollCtx = object + tag: int64 + slot: int + epochStamp: int64 ## this collection's epoch, as a stamp word + amSolo: bool + const MaxPar {.intdefine.} = 256 ## CAPACITY of the slot table, not a tuning knob: a hard ceiling on @@ -384,12 +397,9 @@ var ## Starting at 1 also means single-threaded programs scan one entry. gSoloCapture: int # a solo collection is in its capture phase gTagCounter: int64 - gMyTag {.threadvar.}: int64 - gMySlot {.threadvar.}: int - gAmSolo {.threadvar.}: bool + gCtx {.threadvar.}: CollCtx gEpoch: int # advanced every YrcEpochLen collections gCollectionCounter: int - gMyEpochStamp {.threadvar.}: int64 # this collection's epoch, as a stamp word gWaitLock: Lock # pairs gWaitCond's wait/broadcast; leaf gWaitCond: Cond # signaled on capture-end and collection-finish @@ -475,11 +485,11 @@ proc anySlotFree(): bool {.inline.} = if atomicLoadN(addr gActiveTags[sl], ATOMIC_ACQUIRE) == 0: return true -template isStamped(c: Cell): bool = +template isStamped(c: Cell; ctx: ptr CollCtx): bool = # "stamped" means: claimed by THIS collection. A relaxed load suffices: - # only this thread ever stores gMyTag, and any stale read of a foreign + # only this thread ever stores ctx.tag, and any stale read of a foreign # value routes into claimCell which re-validates with acquire + CAS. - (atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) shr 32) == gMyTag + (atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) shr 32) == ctx.tag template denseIdx(c: Cell): int32 = int32(loWord(atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED))) @@ -628,7 +638,7 @@ proc registerLocal(c: Cell; desc: PNimTypeV2) {.inline.} = when defined(nimOrcStats): let st = atomicLoadN(addr c.rootIdx, ATOMIC_RELAXED) if st == 0: bumpStat gStatRegFresh - elif gMyTag != 0 and (st shr 32) == gMyTag: bumpStat gStatRegSelf + elif gCtx.tag != 0 and (st shr 32) == gCtx.tag: bumpStat gStatRegSelf elif isActiveTag(st shr 32): bumpStat gStatRegCross else: bumpStat gStatRegRepeat if gLocalRoots.d == nil: init(gLocalRoots) @@ -761,7 +771,7 @@ proc buildPendingWatch(): bool = if gPendingWatch.d == nil: init gPendingWatch gPendingWatch.len = 0 for s in 0 ..< slotsInPlay(): - if s != gMySlot: + if s != gCtx.slot: let tg = atomicLoadN(addr gActiveTags[s], ATOMIC_ACQUIRE) if tg != 0 and atomicLoadN(addr gSlotPhase[s], ATOMIC_ACQUIRE) == 1: gPendingWatch.add((int64(s) shl 32) or tg) @@ -839,11 +849,25 @@ proc prepareCapture() = gCap.prunedSrc.len = 0 gCap.ages.len = 0 +proc growCaptureArrays(cap: ptr CaptureBufs) {.noinline.} = + ## `recs`, `sccIdx`, `ages` and `tstack` are appended to together, and only + ## by `claimCell` — one entry each per claimed cell. So they are grown + ## together and ONE capacity check on `recs` covers all four: `recs` drives + ## the growth, the other three are topped up to at least its capacity. + ## `tstack` is popped as SCCs are emitted, so its length only ever trails + ## `recs.len`; matching capacities keeps its appends unchecked too. + ## Marked `noinline` to keep the cold resize path out of `claimCell`. + resize(cap.recs, cap.recs.len +% 1) + let n = cap.recs.cap + if cap.sccIdx.cap < n: resize(cap.sccIdx, n) + if cap.ages.cap < n: resize(cap.ages, n) + if cap.tstack.cap < n: resize(cap.tstack, n) + # rc is captured without the flag bits: the collector itself toggles # inRootsFlag between capture and commit, which must not look like a # mutation to the commit-time rc validation. proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs; - pruneLive: bool; old0: int64): int32 = + ctx: ptr CollCtx; pruneLive: bool; old0: int64): int32 = ## Dense index if this collection owns `c` (claiming and registering it ## if it was unclaimed), -1 if another ACTIVE collection owns it, or ## -2 if `pruneLive` and the cell was proven live in the current epoch @@ -852,33 +876,34 @@ proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs; ## `old0` is `c`'s claim word as the caller already read it (acquire): the ## DFS reads it to test ownership, and re-reading it here would be a second ## dependent load of the same cold header word on every traversed edge. - if gAmSolo: + if ctx.amSolo: # no other collection is (or can start) capturing: plain stores. # This recovers the sequential capture speed of the single-collector # design whenever collections do not actually overlap. let old = old0 - if (old shr 32) == gMyTag: + if (old shr 32) == ctx.tag: return int32(loWord(old)) - if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and + if pruneLive and (old shr 32) == (ctx.epochStamp shr 32) and stampAge(old) >= YrcPromoteAge: return -2 let idx = cap.recs.len - c.rootIdx = (gMyTag shl 32) or int64(idx) + c.rootIdx = (ctx.tag shl 32) or int64(idx) when defined(nimOrcStats): bumpStat gStatCapTotal if old != 0: bumpStat gStatCapRepeat - cap.recs.add CaptureRec(cell: c, desc: desc, + if idx >= cap.recs.cap: growCaptureArrays(cap) + cap.recs.addUnchecked CaptureRec(cell: c, desc: desc, rcWord: loadRc(c) and not rcMask, lowlink: int32(idx), selfRefs: 0'i32) - cap.sccIdx.add -1'i32 - cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0) - cap.tstack.add int32(idx) + cap.sccIdx.addUnchecked -1'i32 + cap.ages.addUnchecked int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0) + cap.tstack.addUnchecked int32(idx) return int32(idx) var old = old0 while true: - if (old shr 32) == gMyTag: + if (old shr 32) == ctx.tag: return int32(loWord(old)) - if pruneLive and (old shr 32) == (gMyEpochStamp shr 32) and + if pruneLive and (old shr 32) == (ctx.epochStamp shr 32) and stampAge(old) >= YrcPromoteAge: return -2 # an epoch stamp is never a tag (tags are allocated below `epochBase`), @@ -888,17 +913,18 @@ proc claimCell(c: Cell; desc: PNimTypeV2; cap: ptr CaptureBufs; return -1 let idx = cap.recs.len if atomicCompareExchangeN(addr c.rootIdx, addr old, - (gMyTag shl 32) or int64(idx), false, + (ctx.tag shl 32) or int64(idx), false, ATOMIC_ACQ_REL, ATOMIC_RELAXED): when defined(nimOrcStats): bumpStat gStatCapTotal if old != 0: bumpStat gStatCapRepeat - cap.recs.add CaptureRec(cell: c, desc: desc, + if idx >= cap.recs.cap: growCaptureArrays(cap) + cap.recs.addUnchecked CaptureRec(cell: c, desc: desc, rcWord: loadRc(c) and not rcMask, lowlink: int32(idx), selfRefs: 0'i32) - cap.sccIdx.add -1'i32 - cap.ages.add int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0) - cap.tstack.add int32(idx) + cap.sccIdx.addUnchecked -1'i32 + cap.ages.addUnchecked int32(if isEpochStamp(old): min(stampAge(old), 1000) else: 0) + cap.tstack.addUnchecked int32(idx) return int32(idx) # a failed CAS leaves the fresh claim word in `old`; loop with it @@ -918,11 +944,14 @@ proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) = ## on the stack below u) or an SCC emitted earlier, so `sccIdx` is final ## for all of them and the cross targets can be appended to `crossTgt` ## contiguously — which makes `crossOff` a prefix offset for free. + # one TLS resolution for the whole traversal; `claimCell` and the per-edge + # ownership tests below read the context through this pointer + let ctx = addr gCtx let rootWord = atomicLoadN(addr s.rootIdx, ATOMIC_ACQUIRE) - if (rootWord shr 32) == gMyTag: return + if (rootWord shr 32) == ctx.tag: return orcAssert(j.traceStack.len == 0, "capture: trace stack not empty") # roots never prune: a dec-witnessed suspicion overrides any epoch stamp - let root = claimCell(s, desc, cap, pruneLive = false, old0 = rootWord) + let root = claimCell(s, desc, cap, ctx, pruneLive = false, old0 = rootWord) if root < 0: return # another active collection owns this candidate; it handles it trace(s, desc, j) @@ -942,7 +971,7 @@ proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) = # one load of the target's claim word serves both the ownership test # and the dense-index extraction let cw = atomicLoadN(addr t.rootIdx, ATOMIC_ACQUIRE) - if (cw shr 32) == gMyTag: + if (cw shr 32) == ctx.tag: let v = int32(loWord(cw)) if v == u: # A self edge is internal by construction and its reference is @@ -957,7 +986,7 @@ proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) = else: let tdesc = j.traceStack.d[last][1] let childBase = j.traceStack.len - let v = claimCell(t, tdesc, cap, pruneLive = true, old0 = cw) + let v = claimCell(t, tdesc, cap, ctx, pruneLive = true, old0 = cw) if v == -1: # cross-collection edge: the owner sees our reference in the rc # word and classifies the target live; we re-register it as a @@ -966,7 +995,13 @@ proc capture(s: Cell; desc: PNimTypeV2; j: var GcEnv; cap: ptr CaptureBufs) = elif v == -2: # target proven live this epoch: opaque live external, no descent. # Taint u's SCC — its own "live" verdict may lean on the stamp. - cap.prunedSrc.add u + # The list is only ever read as a set (and for its emptiness), and + # one cell's out-edges are consumed consecutively, so suppressing a + # repeat of the previous entry removes nearly every duplicate a + # multi-pruned cell would otherwise contribute. + if cap.prunedSrc.len == 0 or + cap.prunedSrc.d[cap.prunedSrc.len -% 1] != u: + cap.prunedSrc.add u when defined(nimOrcStats): bumpStat gStatCapPruned else: @@ -1031,9 +1066,13 @@ proc computeDeadness(j: var GcEnv; cap: ptr CaptureBufs) = let s = cap.sccIdx.d[cap.prunedSrc.d[i]] cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagPruned # cells that stay registered as roots (partial collection) count as - # externally referenced: the roots buffer itself points at them - for mi in 0 ..< cap.sccMembers.len: - let m = cap.sccMembers.d[mi] + # externally referenced: the roots buffer itself points at them. + # Scanned over `recs` rather than over `sccMembers`: every claimed cell is + # pushed to the Tarjan stack once and popped into `sccMembers` once, so the + # two cover exactly the same set, and the SCC comes from `sccIdx` either + # way. Going through `sccMembers` would only add a random 32-byte-stride + # gather in front of a load that already misses on the cell header. + for m in 0 ..< cap.recs.len: if (loadRc(cap.recs.d[m].cell) and inRootsFlag) != 0: let s = cap.sccIdx.d[m] cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagForcedLive @@ -1064,9 +1103,10 @@ proc markDirtyFromQueues(j: var GcEnv; cap: ptr CaptureBufs) = ## the last drain had its reference set changed during capture. Peek ## (don't drain!) the stripe queues and taint the affected SCCs; the ## entries stay queued and the next merge re-registers them as candidates. + let ctx = addr gCtx template taint(cp: Cell) = let c = cp - if isStamped(c): + if isStamped(c, ctx): let s = cap.sccIdx.d[denseIdx(c)] cap.sccs.d[s].flags = cap.sccs.d[s].flags or flagDirty for i in 0.. Date: Mon, 3 Aug 2026 12:27:58 +0300 Subject: [PATCH 11/22] fixes #26027; use valid compare-exchange failure orders (#26066) Fixes #26027. Map the single-order compare-exchange failure ordering from `release` to `relaxed` and from `acquire-release` to `acquire`. Apply the mapping to the trivial and non-trivial strong and weak overloads, and correct the explicit-order test cases. Tested `tests/stdlib/concurrency/tatomics.nim` across C/C++, refc/orc, and native/C++ atomics (8 combinations). Also verified the original GCC 16.1 assertion reproducer. --- lib/pure/concurrency/atomics.nim | 27 +++++++++++++-------- tests/stdlib/concurrency/tatomics.nim | 34 +++++++++++++-------------- 2 files changed, 34 insertions(+), 27 deletions(-) diff --git a/lib/pure/concurrency/atomics.nim b/lib/pure/concurrency/atomics.nim index 818f1b37ac..9c652afdc1 100644 --- a/lib/pure/concurrency/atomics.nim +++ b/lib/pure/concurrency/atomics.nim @@ -256,12 +256,8 @@ else: cast[T](interlockedExchange(addr(location.value), cast[int64](desired))) proc compareExchange*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; success, failure: MemoryOrder): bool {.inline.} = cast[T](interlockedCompareExchange(addr(location.value), cast[nonAtomicType(T)](desired), cast[nonAtomicType(T)](expected))) == expected - proc compareExchange*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; order: MemoryOrder = moSequentiallyConsistent): bool {.inline.} = - compareExchange(location, expected, desired, order, order) proc compareExchangeWeak*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; success, failure: MemoryOrder): bool {.inline.} = compareExchange(location, expected, desired, success, failure) - proc compareExchangeWeak*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; order: MemoryOrder = moSequentiallyConsistent): bool {.inline.} = - compareExchangeWeak(location, expected, desired, order, order) proc fetchAdd*[T: SomeInteger](location: var Atomic[T]; value: T; order: MemoryOrder = moSequentiallyConsistent): T {.inline.} = var currentValue = location.load() @@ -358,13 +354,9 @@ else: cast[T](atomic_exchange_explicit(addr(location.value), cast[nonAtomicType(T)](desired), order)) proc compareExchange*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; success, failure: MemoryOrder): bool {.inline.} = atomic_compare_exchange_strong_explicit(addr(location.value), cast[ptr nonAtomicType(T)](addr(expected)), cast[nonAtomicType(T)](desired), success, failure) - proc compareExchange*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; order: MemoryOrder = moSequentiallyConsistent): bool {.inline.} = - compareExchange(location, expected, desired, order, order) proc compareExchangeWeak*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; success, failure: MemoryOrder): bool {.inline.} = atomic_compare_exchange_weak_explicit(addr(location.value), cast[ptr nonAtomicType(T)](addr(expected)), cast[nonAtomicType(T)](desired), success, failure) - proc compareExchangeWeak*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; order: MemoryOrder = moSequentiallyConsistent): bool {.inline.} = - compareExchangeWeak(location, expected, desired, order, order) # Numerical operations proc fetchAdd*[T: SomeInteger](location: var Atomic[T]; value: T; order: MemoryOrder = moSequentiallyConsistent): T {.inline.} = @@ -378,6 +370,21 @@ else: proc fetchXor*[T: SomeInteger](location: var Atomic[T]; value: T; order: MemoryOrder = moSequentiallyConsistent): T {.inline.} = cast[T](atomic_fetch_xor_explicit(addr(location.value), cast[nonAtomicType(T)](value), order)) + func compareExchangeFailureOrder(order: MemoryOrder): MemoryOrder {.inline.} = + case order + of moRelease: + moRelaxed + of moAcquireRelease: + moAcquire + else: + order + + proc compareExchange*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; order: MemoryOrder = moSequentiallyConsistent): bool {.inline.} = + compareExchange(location, expected, desired, order, compareExchangeFailureOrder(order)) + + proc compareExchangeWeak*[T: Trivial](location: var Atomic[T]; expected: var T; desired: T; order: MemoryOrder = moSequentiallyConsistent): bool {.inline.} = + compareExchangeWeak(location, expected, desired, order, compareExchangeFailureOrder(order)) + template withLock[T: not Trivial](location: var Atomic[T]; order: MemoryOrder; body: untyped): untyped = while testAndSet(location.guard, moAcquire): discard try: @@ -411,10 +418,10 @@ else: compareExchange(location, expected, desired, success, failure) proc compareExchange*[T: not Trivial](location: var Atomic[T]; expected: var T; desired: T; order: MemoryOrder = moSequentiallyConsistent): bool {.inline.} = - compareExchange(location, expected, desired, order, order) + compareExchange(location, expected, desired, order, compareExchangeFailureOrder(order)) proc compareExchangeWeak*[T: not Trivial](location: var Atomic[T]; expected: var T; desired: T; order: MemoryOrder = moSequentiallyConsistent): bool {.inline.} = - compareExchangeWeak(location, expected, desired, order, order) + compareExchangeWeak(location, expected, desired, order, compareExchangeFailureOrder(order)) proc atomicInc*[T: SomeInteger](location: var Atomic[T]; value: T = 1) {.inline.} = ## Atomically increments the atomic integer by some `value`. diff --git a/tests/stdlib/concurrency/tatomics.nim b/tests/stdlib/concurrency/tatomics.nim index 08f2e7d3ee..44760395eb 100644 --- a/tests/stdlib/concurrency/tatomics.nim +++ b/tests/stdlib/concurrency/tatomics.nim @@ -49,7 +49,7 @@ block trivialExchange: doAssert location.load == 6 -block trivialCompareExchangeDoesExchange: +block trivialCompareExchangeDoesExchange: # bug #26027 var location: Atomic[int] var expected = 1 location.store(1) @@ -115,11 +115,11 @@ block trivialCompareExchangeSuccessFailureDoesExchange: doAssert expected == 3 doAssert location.load == 4 expected = 4 - doAssert location.compareExchange(expected, 5, moRelease, moRelease) + doAssert location.compareExchange(expected, 5, moRelease, moRelaxed) doAssert expected == 4 doAssert location.load == 5 expected = 5 - doAssert location.compareExchange(expected, 6, moAcquireRelease, moAcquireRelease) + doAssert location.compareExchange(expected, 6, moAcquireRelease, moAcquire) doAssert expected == 5 doAssert location.load == 6 @@ -140,11 +140,11 @@ block trivialCompareExchangeSuccessFailureDoesNotExchange: doAssert expected == 1 doAssert location.load == 1 expected = 10 - doAssert not location.compareExchange(expected, 5, moRelease, moRelease) + doAssert not location.compareExchange(expected, 5, moRelease, moRelaxed) doAssert expected == 1 doAssert location.load == 1 expected = 10 - doAssert not location.compareExchange(expected, 6, moAcquireRelease, moAcquireRelease) + doAssert not location.compareExchange(expected, 6, moAcquireRelease, moAcquire) doAssert expected == 1 doAssert location.load == 1 @@ -215,11 +215,11 @@ block trivialCompareExchangeWeakSuccessFailureDoesExchange: doAssert expected == 3 doAssert location.load == 4 expected = 4 - doAssert location.compareExchangeWeak(expected, 5, moRelease, moRelease) + doAssert location.compareExchangeWeak(expected, 5, moRelease, moRelaxed) doAssert expected == 4 doAssert location.load == 5 expected = 5 - doAssert location.compareExchangeWeak(expected, 6, moAcquireRelease, moAcquireRelease) + doAssert location.compareExchangeWeak(expected, 6, moAcquireRelease, moAcquire) doAssert expected == 5 doAssert location.load == 6 @@ -240,11 +240,11 @@ block trivialCompareExchangeWeakSuccessFailureDoesNotExchange: doAssert expected == 1 doAssert location.load == 1 expected = 10 - doAssert not location.compareExchangeWeak(expected, 5, moRelease, moRelease) + doAssert not location.compareExchangeWeak(expected, 5, moRelease, moRelaxed) doAssert expected == 1 doAssert location.load == 1 expected = 10 - doAssert not location.compareExchangeWeak(expected, 6, moAcquireRelease, moAcquireRelease) + doAssert not location.compareExchangeWeak(expected, 6, moAcquireRelease, moAcquire) doAssert expected == 1 doAssert location.load == 1 @@ -349,11 +349,11 @@ block objectCompareExchangeSuccessFailureDoesExchange: doAssert expected == Object(val: 3) doAssert location.load == Object(val: 4) expected = Object(val: 4) - doAssert location.compareExchange(expected, Object(val: 5), moRelease, moRelease) + doAssert location.compareExchange(expected, Object(val: 5), moRelease, moRelaxed) doAssert expected == Object(val: 4) doAssert location.load == Object(val: 5) expected = Object(val: 5) - doAssert location.compareExchange(expected, Object(val: 6), moAcquireRelease, moAcquireRelease) + doAssert location.compareExchange(expected, Object(val: 6), moAcquireRelease, moAcquire) doAssert expected == Object(val: 5) doAssert location.load == Object(val: 6) @@ -374,11 +374,11 @@ block objectCompareExchangeSuccessFailureDoesNotExchange: doAssert expected == Object(val: 1) doAssert location.load == Object(val: 1) expected = Object(val: 10) - doAssert not location.compareExchange(expected, Object(val: 5), moRelease, moRelease) + doAssert not location.compareExchange(expected, Object(val: 5), moRelease, moRelaxed) doAssert expected == Object(val: 1) doAssert location.load == Object(val: 1) expected = Object(val: 10) - doAssert not location.compareExchange(expected, Object(val: 6), moAcquireRelease, moAcquireRelease) + doAssert not location.compareExchange(expected, Object(val: 6), moAcquireRelease, moAcquire) doAssert expected == Object(val: 1) doAssert location.load == Object(val: 1) @@ -449,11 +449,11 @@ block objectCompareExchangeWeakSuccessFailureDoesExchange: doAssert expected == Object(val: 3) doAssert location.load == Object(val: 4) expected = Object(val: 4) - doAssert location.compareExchangeWeak(expected, Object(val: 5), moRelease, moRelease) + doAssert location.compareExchangeWeak(expected, Object(val: 5), moRelease, moRelaxed) doAssert expected == Object(val: 4) doAssert location.load == Object(val: 5) expected = Object(val: 5) - doAssert location.compareExchangeWeak(expected, Object(val: 6), moAcquireRelease, moAcquireRelease) + doAssert location.compareExchangeWeak(expected, Object(val: 6), moAcquireRelease, moAcquire) doAssert expected == Object(val: 5) doAssert location.load == Object(val: 6) @@ -474,11 +474,11 @@ block objectCompareExchangeWeakSuccessFailureDoesNotExchange: doAssert expected == Object(val: 1) doAssert location.load == Object(val: 1) expected = Object(val: 10) - doAssert not location.compareExchangeWeak(expected, Object(val: 5), moRelease, moRelease) + doAssert not location.compareExchangeWeak(expected, Object(val: 5), moRelease, moRelaxed) doAssert expected == Object(val: 1) doAssert location.load == Object(val: 1) expected = Object(val: 10) - doAssert not location.compareExchangeWeak(expected, Object(val: 6), moAcquireRelease, moAcquireRelease) + doAssert not location.compareExchangeWeak(expected, Object(val: 6), moAcquireRelease, moAcquire) doAssert expected == Object(val: 1) doAssert location.load == Object(val: 1) From f6651e6c705300c48f7b846e998a7a02623d151f Mon Sep 17 00:00:00 2001 From: ringabout <43030857+ringabout@users.noreply.github.com> Date: Mon, 3 Aug 2026 17:49:48 +0800 Subject: [PATCH 12/22] fixes #26045; #26046; `when nimvm` leak push options (#26047) fixes #26045; fixes #26046 The fix isolates compiler option state while semantically checking each when nimvm branch. compiler/semexprs.nim:2745 snapshots the option stack, compiler options, diagnostics settings, and enabled features. It analyzes one branch and restores that state in finally. Both the nimvm and else branches use this function. This prevents: ```nim when nimvm: {.push overflowChecks: off.} ``` from disabling overflow checks in following runtime code. It also means a {.pop.} in the opposite branch correctly reports that it has no corresponding {.push.}. --- compiler/semexprs.nim | 21 +++++++++++++++++++-- tests/whenstmt/twhen_nimvm_push.nim | 21 +++++++++++++++++++++ tests/whenstmt/twhen_nimvm_push_pop.nim | 8 ++++++++ 3 files changed, 48 insertions(+), 2 deletions(-) create mode 100644 tests/whenstmt/twhen_nimvm_push.nim create mode 100644 tests/whenstmt/twhen_nimvm_push_pop.nim diff --git a/compiler/semexprs.nim b/compiler/semexprs.nim index 07564aa171..fe424ffdcb 100644 --- a/compiler/semexprs.nim +++ b/compiler/semexprs.nim @@ -2742,6 +2742,22 @@ proc semMagic(c: PContext, n: PNode, s: PSym, flags: TExprFlags; expectedType: P else: result = semDirectOp(c, n, flags, expectedType) +proc semNimvmBranch(c: PContext, n: PNode, flags: TExprFlags): PNode = + let + oldOptionStack = c.optionStack[0..^1] + oldOptions = c.config.options + oldNotes = c.config.notes + oldWarningAsErrors = c.config.warningAsErrors + oldFeatures = c.features + try: + result = semExpr(c, n, flags) + finally: + c.optionStack = oldOptionStack + c.config.options = oldOptions + c.config.notes = oldNotes + c.config.warningAsErrors = oldWarningAsErrors + c.features = oldFeatures + proc semWhen(c: PContext, n: PNode, semCheck = true): PNode = # If semCheck is set to false, ``when`` will return the verbatim AST of # the correct branch. Otherwise the AST will be passed through semStmt. @@ -2778,7 +2794,7 @@ proc semWhen(c: PContext, n: PNode, semCheck = true): PNode = checkSonsLen(it, 2, c.config) if whenNimvm: if semCheck: - it[1] = semExpr(c, it[1], flags) + it[1] = semNimvmBranch(c, it[1], flags) typ = commonType(c, typ, it[1].typ) result = n # when nimvm is not elimited until codegen elif c.inGenericContext > 0: @@ -2809,7 +2825,8 @@ proc semWhen(c: PContext, n: PNode, semCheck = true): PNode = discard elif result == nil or whenNimvm: if semCheck: - it[0] = semExpr(c, it[0], flags) + it[0] = if whenNimvm: semNimvmBranch(c, it[0], flags) + else: semExpr(c, it[0], flags) typ = commonType(c, typ, it[0].typ) if typ != nil and typ.kind != tyUntyped: it[0] = fitNode(c, typ, it[0], it[0].info) diff --git a/tests/whenstmt/twhen_nimvm_push.nim b/tests/whenstmt/twhen_nimvm_push.nim new file mode 100644 index 0000000000..7991239fcc --- /dev/null +++ b/tests/whenstmt/twhen_nimvm_push.nim @@ -0,0 +1,21 @@ +discard """ + output: "ok" +""" + +var overflowDetected = false +when nimvm: + {.push overflowChecks: off.} +else: + var branchX = high(int) + try: + inc branchX + except OverflowDefect: + overflowDetected = true + +doAssert overflowDetected + +var x = high(int) +try: + inc x +except OverflowDefect: + echo "ok" diff --git a/tests/whenstmt/twhen_nimvm_push_pop.nim b/tests/whenstmt/twhen_nimvm_push_pop.nim new file mode 100644 index 0000000000..31f44c4058 --- /dev/null +++ b/tests/whenstmt/twhen_nimvm_push_pop.nim @@ -0,0 +1,8 @@ +discard """ + errormsg: "{.pop.} without a corresponding {.push.}" + line: 8 +""" + +when nimvm: + {.push checks: off.} +else: {.pop.} From 5137d273e5356e4377247d79740b8736f1fcfece Mon Sep 17 00:00:00 2001 From: Ryan McConnell Date: Mon, 3 Aug 2026 05:51:16 -0400 Subject: [PATCH 13/22] fix #25993; In-place object construction zeroes destination before evaluating self-referencing field values (#25994) --- compiler/aliases.nim | 109 +++++++++++++++++++----- compiler/ccgcalls.nim | 4 +- compiler/ccgexprs.nim | 2 +- tests/ccgbugs/tobjconstr_self_alias.nim | 85 ++++++++++++++++++ 4 files changed, 177 insertions(+), 23 deletions(-) create mode 100644 tests/ccgbugs/tobjconstr_self_alias.nim diff --git a/compiler/aliases.nim b/compiler/aliases.nim index fa1167753f..6877028c3a 100644 --- a/compiler/aliases.nim +++ b/compiler/aliases.nim @@ -21,6 +21,44 @@ type TAnalysisResult* = enum arNo, arMaybe, arYes + PartFlag* = enum + pfStructural ## use structural prefix-chain detection and tree-walk + pfBidirectional ## also check reverse direction per field in nkObjConstr + +func sameLocation(a, b: PNode): bool = + template sameConstIndex(a, b: PNode): bool = + a.kind in nkLiterals and b.kind in nkLiterals and a.intVal == b.intVal + var a = a + var b = b + while a.kind in {nkHiddenStdConv, nkHiddenSubConv, nkConv}: a = a[1] + while b.kind in {nkHiddenStdConv, nkHiddenSubConv, nkConv}: b = b[1] + if a.kind != b.kind: return false + case a.kind + of nkSym: result = a.sym.id == b.sym.id + of nkDotExpr, nkCheckedFieldExpr: + result = a[1].kind == nkSym and b[1].kind == nkSym and + sameLocation(a[0], b[0]) and a[1].sym.id == b[1].sym.id + of nkBracketExpr: + result = sameLocation(a[0], b[0]) and sameConstIndex(a[1], b[1]) + of nkObjUpConv, nkObjDownConv, nkDerefExpr, nkHiddenDeref: + result = sameLocation(a[0], b[0]) + else: result = false + +proc isAccessorPrefixOf(a, b: PNode): bool = + var cur = b + while cur.kind in {nkDotExpr, nkBracketExpr, nkCheckedFieldExpr, nkObjUpConv, + nkObjDownConv, nkHiddenDeref, nkDerefExpr, + nkHiddenStdConv, nkHiddenSubConv, nkConv}: + if sameLocation(cur, a): return true + case cur.kind + of nkDotExpr, nkBracketExpr, nkCheckedFieldExpr, nkObjUpConv, nkObjDownConv, + nkHiddenDeref, nkDerefExpr: + cur = cur[0] + of nkHiddenStdConv, nkHiddenSubConv, nkConv: + cur = cur[1] + else: discard + result = sameLocation(cur, a) + proc isPartOfAux(a, b: PType, marker: var IntSet): TAnalysisResult proc isPartOfAux(n: PNode, b: PType, marker: var IntSet): TAnalysisResult = @@ -70,14 +108,28 @@ proc isPartOf(a, b: PType): TAnalysisResult = # watch out: parameters reversed because I'm too lazy to change the code... result = isPartOfAux(b, a, marker) -proc isPartOf*(a, b: PNode): TAnalysisResult = - ## checks if location `a` can be part of location `b`. We treat seqs and - ## strings as pointers because the code gen often just passes them as such. +proc isPartOf*(a, b: PNode; flags: set[PartFlag] = {}): TAnalysisResult = + ## Checks if location `a` can be part of location `b`: i.e. whether writing to + ## `b` could affect what `a` reads. We treat seqs and strings as pointers + ## because the code gen often just passes them as such. ## ## Note: `a` can only be part of `b`, if `a`'s type can be part of `b`'s ## type. Since however type analysis is more expensive, we perform it only ## if necessary. ## + ## When `pfStructural` is set additional aliasing is detected: + ## * a structural prefix of an accessor chain is considered part of it + ## (e.g. `x.f <| x.f.g`). Normally `x.f !<| x.f.g` because the + ## same-kind `nkDotExpr` comparison treats the differing field names as + ## siblings, but `pfStructural` walks the chain to recognise the + ## relationship. + ## * Unrecognised node kinds are traversed recursively. + ## + ## When `pfBidirectional` is set: + ## * In `nkObjConstr` the reverse direction `isPartOf(value, a)` is also + ## checked per field value so that reads hidden behind calls/closures + ## are detected. + ## ## cases: ## ## YES-cases: @@ -86,13 +138,14 @@ proc isPartOf*(a, b: PNode): TAnalysisResult = ## x[] <| x ## x[i] <| x ## x.f <| x + ## x.f <| x.f.g # when pfStructural (prefix chain) ## ``` ## ## NO-cases: ## ``` ## x !<| y # depending on type and symbol kind ## x[constA] !<| x[constB] - ## x.f !<| x.g + ## x.f !<| x.g # sibling fields at same level ## x.f !<| y.f iff x !<= y ## ``` ## @@ -121,7 +174,7 @@ proc isPartOf*(a, b: PNode): TAnalysisResult = else: result = arNo of nkBracketExpr: - result = isPartOf(a[0], b[0]) + result = isPartOf(a[0], b[0], flags) if a.len >= 2 and b.len >= 2: # array accesses: if result == arYes and isDeepConstExpr(a[1]) and isDeepConstExpr(b[1]): @@ -131,7 +184,11 @@ proc isPartOf*(a, b: PNode): TAnalysisResult = var y = if b[1].kind == nkHiddenStdConv: b[1][1] else: b[1] if sameValue(x, y): result = arYes + elif pfStructural in flags and isAccessorPrefixOf(a, b): + result = arYes else: result = arNo + elif pfStructural in flags and isAccessorPrefixOf(a, b): + result = arYes # else: maybe and no are accurate else: # pointer derefs: @@ -139,22 +196,25 @@ proc isPartOf*(a, b: PNode): TAnalysisResult = if isPartOf(a.typ, b.typ) != arNo: result = arMaybe of nkDotExpr: - result = isPartOf(a[0], b[0]) + result = isPartOf(a[0], b[0], flags) if result != arNo: # if the fields are different, it's not the same location if a[1].sym.id != b[1].sym.id: - result = arNo + if pfStructural in flags and isAccessorPrefixOf(a, b): + result = arYes + else: + result = arNo of nkHiddenDeref, nkDerefExpr: - result = isPartOf(a[0], b[0]) + result = isPartOf(a[0], b[0], flags) # weaken because of indirection: if result != arYes: if isPartOf(a.typ, b.typ) != arNo: result = arMaybe of nkHiddenStdConv, nkHiddenSubConv, nkConv: - result = isPartOf(a[1], b[1]) + result = isPartOf(a[1], b[1], flags) of nkObjUpConv, nkObjDownConv, nkCheckedFieldExpr: - result = isPartOf(a[0], b[0]) + result = isPartOf(a[0], b[0], flags) else: result = arNo # Calls return a new location, so a default of ``arNo`` is fine. else: @@ -167,31 +227,31 @@ proc isPartOf*(a, b: PNode): TAnalysisResult = case b.kind of Ix0Kinds: # a* !<| b.f iff a* !<| b - result = isPartOf(a, b[0]) + result = isPartOf(a, b[0], flags) of DerefKinds: # a* !<| b[] iff result = arNo if isPartOf(a.typ, b.typ) != arNo: - result = isPartOf(a, b[0]) + result = isPartOf(a, b[0], flags) if result == arNo: result = arMaybe of Ix1Kinds: # a* !<| T(b) iff a* !<| b - result = isPartOf(a, b[1]) + result = isPartOf(a, b[1], flags) of nkSym: # b is an atom, so we have to check a: case a.kind of Ix0Kinds: # a.f !<| b* iff a.f !<| b* - result = isPartOf(a[0], b) + result = isPartOf(a[0], b, flags) of Ix1Kinds: - result = isPartOf(a[1], b) + result = isPartOf(a[1], b, flags) of DerefKinds: if isPartOf(a.typ, b.typ) != arNo: - result = isPartOf(a[0], b) + result = isPartOf(a[0], b, flags) if result == arNo: result = arMaybe else: result = arNo @@ -199,20 +259,29 @@ proc isPartOf*(a, b: PNode): TAnalysisResult = of nkObjConstr: result = arNo for i in 1.. 0: - result = isPartOf(a, b[0]) + result = isPartOf(a, b[0], flags) else: result = arNo - else: result = arNo + else: + if pfStructural in flags: + for i in 0..