mirror of
https://github.com/nim-lang/Nim.git
synced 2026-08-05 06:58:42 +00:00
Merge branch 'devel' into pr_quiry
This commit is contained in:
2
.github/workflows/stale.yml
vendored
2
.github/workflows/stale.yml
vendored
@@ -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
|
||||
|
||||
@@ -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..<b.len:
|
||||
let res = isPartOf(a, b[i][1])
|
||||
let res = isPartOf(a, b[i][1], flags)
|
||||
if res != arNo:
|
||||
result = res
|
||||
if res == arYes: break
|
||||
if pfBidirectional in flags:
|
||||
let res2 = isPartOf(b[i][1], a, {pfStructural})
|
||||
if res2 != arNo:
|
||||
result = res2
|
||||
if res2 == arYes: break
|
||||
of nkCallKinds:
|
||||
result = arNo
|
||||
for i in 1..<b.len:
|
||||
let res = isPartOf(a, b[i])
|
||||
let res = isPartOf(a, b[i], flags)
|
||||
if res != arNo:
|
||||
result = res
|
||||
if res == arYes: break
|
||||
of nkBracket:
|
||||
if b.len > 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..<b.safeLen:
|
||||
if isPartOf(a, b[i], flags) != arNo: return arMaybe
|
||||
result = arNo
|
||||
|
||||
@@ -51,7 +51,7 @@ proc preventNrvo(p: BProc; dest, le, ri: PNode): bool =
|
||||
if le != nil:
|
||||
for i in 1..<ri.len:
|
||||
let r = ri[i]
|
||||
if isPartOf(le, r) != arNo: return true
|
||||
if isPartOf(le, r, {pfStructural}) != arNo: return true
|
||||
# we use the weaker 'canRaise' here in order to prevent too many
|
||||
# annoying warnings, see #14514
|
||||
if canRaise(ri[0]) and
|
||||
@@ -61,7 +61,7 @@ proc preventNrvo(p: BProc; dest, le, ri: PNode): bool =
|
||||
if dest != nil and dest != le:
|
||||
for i in 1..<ri.len:
|
||||
let r = ri[i]
|
||||
if isPartOf(dest, r) != arNo: return true
|
||||
if isPartOf(dest, r, {pfStructural}) != arNo: return true
|
||||
|
||||
proc hasNoInit(call: PNode): bool {.inline.} =
|
||||
result = call[0].kind == nkSym and sfNoInit in call[0].sym.flags
|
||||
|
||||
@@ -1907,7 +1907,7 @@ proc genObjConstr(p: BProc, e: PNode, d: var TLoc) =
|
||||
isRef or
|
||||
d.k == locNone or
|
||||
(d.t != nil and not sameBackendType(t, d.t.skipTypes(abstractInstOwned))) or
|
||||
(isPartOf(d.lode, e) != arNo)
|
||||
(isPartOf(d.lode, e, {pfStructural, pfBidirectional}) != arNo)
|
||||
|
||||
var tmp: TLoc = default(TLoc)
|
||||
var r: Rope
|
||||
|
||||
@@ -336,9 +336,14 @@ proc collectExceptState(ctx: var Ctx, n: PNode): PNode {.inline.} =
|
||||
var cond: PNode = nil
|
||||
for i in 0..<c.len - 1:
|
||||
assert(c[i].kind == nkType)
|
||||
# Use the :curExc env field (set by the wrapper before entering the
|
||||
# except landing state) instead of calling getCurrentException():
|
||||
# injectdestructors does not process the args of this raw generic
|
||||
# `of` magic call, so an owning getCurrentException() temp would
|
||||
# never be destroyed and the caught exception would leak (#23615).
|
||||
let nextCond = newTreeIT(nkCall, c.info, ctx.g.getSysType(c.info, tyBool),
|
||||
newSymNode(g.getSysMagic(c.info, "of", mOf)),
|
||||
g.callCodegenProc("getCurrentException"),
|
||||
ctx.newCurExcAccess(),
|
||||
c[i])
|
||||
|
||||
cond = if cond.isNil: nextCond
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -451,7 +451,13 @@ proc emitTok*(em: var Emitter; L: Lexer; tok: Token) =
|
||||
elif tok.indent >= 0:
|
||||
var newlineKind = ltCrucialNewline
|
||||
if em.keepIndents > 0:
|
||||
em.indentLevel = tok.indent
|
||||
# Apply the requested --indent width to "don't touch" regions (if/block
|
||||
# expressions) too: keep the relative offset from the enclosing block
|
||||
# baseline, but rebase it onto indWidth. Otherwise a non-default
|
||||
# --indent would leave these lines at the original column and inject
|
||||
# invalid indentation (see #20078).
|
||||
em.indentLevel = em.indentStack.high * em.indWidth +
|
||||
(tok.indent - em.indentStack[^1])
|
||||
elif (em.lastTok in (splitters + oprSet) and
|
||||
tok.tokType notin (closedPars - {tkBracketDotRi})):
|
||||
if tok.tokType in openPars and tok.indent > em.indentStack[^1]:
|
||||
|
||||
@@ -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 =
|
||||
@@ -796,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))
|
||||
|
||||
@@ -606,10 +606,16 @@ proc setHookDisamb*(g: ModuleGraph; hook: PSym; opName: string; typ: PType) =
|
||||
break
|
||||
hook.disamb = h
|
||||
|
||||
proc hasDisabledAsgn*(g: ModuleGraph; t: PType): bool =
|
||||
let op = getAttachedOp(g, t, attachedAsgn)
|
||||
proc hasDisabledOp(g: ModuleGraph; t: PType; kind: TTypeAttachedOp): bool =
|
||||
let op = getAttachedOp(g, t, kind)
|
||||
result = op != nil and sfError in op.flags
|
||||
|
||||
proc hasDisabledAsgn*(g: ModuleGraph; t: PType): bool =
|
||||
result = hasDisabledOp(g, t, attachedAsgn)
|
||||
|
||||
proc hasDisabledDup*(g: ModuleGraph; t: PType): bool =
|
||||
result = hasDisabledOp(g, t, attachedDup)
|
||||
|
||||
proc copyTypeProps*(g: ModuleGraph; module: int; dest, src: PType) =
|
||||
for k in low(TTypeAttachedOp)..high(TTypeAttachedOp):
|
||||
let op = getAttachedOp(g, src, k)
|
||||
|
||||
@@ -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)
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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):
|
||||
|
||||
@@ -2087,7 +2087,18 @@ proc typeRel(c: var TCandidate, f, aOrig: PType,
|
||||
result = typeRel(c, f.base, a, flags)
|
||||
else:
|
||||
result = isGeneric
|
||||
if result != isNone: put(c, f, aOrig)
|
||||
if result != isNone:
|
||||
if f.base.kind notin {tyNone, tyGenericParam} and
|
||||
aOrig.kind == tyStatic and aOrig.n != nil and aOrig.n.typ != nil and
|
||||
aOrig.n.typ.isEmptyContainer:
|
||||
# we need to infer the inner type for empty containers
|
||||
let literal = aOrig.n.copyTree
|
||||
literal.typ = f.base
|
||||
let staticArg = newTypeS(tyStatic, c.c, f.base)
|
||||
staticArg.n = literal
|
||||
put(c, f, staticArg)
|
||||
else:
|
||||
put(c, f, aOrig)
|
||||
elif aOrig.n != nil and aOrig.n.typ != nil:
|
||||
result = if f.base.kind != tyNone:
|
||||
typeRel(c, f.last, aOrig.n.typ, flags)
|
||||
|
||||
@@ -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..<n.len-1:
|
||||
if n[i].kind notin {nkEmpty, nkCommentStmt}: return false
|
||||
|
||||
@@ -1024,8 +1024,8 @@ proc computeCursors*(s: PSym; n: PNode; g: ModuleGraph) =
|
||||
v.sym.flags * {sfThread, sfGlobal} == {} and
|
||||
(hasDestructor(v.sym.typ) or (jsCursors and jsDeepCopied(v.sym.typ))) and
|
||||
v.sym.typ.skipTypes({tyGenericInst, tyAlias}).kind != tyOwned and
|
||||
(getAttachedOp(g, v.sym.typ, attachedAsgn) == nil or
|
||||
sfError notin getAttachedOp(g, v.sym.typ, attachedAsgn).flags):
|
||||
not hasDisabledAsgn(g, v.sym.typ) and
|
||||
not hasDisabledDup(g, v.sym.typ):
|
||||
let rid = root(par, i)
|
||||
if par.s[rid].con.kind == isRootOf and dangerousMutation(par.graphs[par.s[rid].con.graphIndex], par.s[i]):
|
||||
discard "cannot cursor into a graph that is mutated"
|
||||
|
||||
@@ -134,11 +134,11 @@ nimblepath="$home/.nimble/pkgs/"
|
||||
# BSD got posix_spawn only recently, so we deactivate it for osproc:
|
||||
define:useFork
|
||||
@elif haiku:
|
||||
gcc.options.linker = "-Wl,--as-needed -lnetwork -lbsd"
|
||||
gcc.cpp.options.linker = "-Wl,--as-needed -lnetwork -lbsd"
|
||||
clang.options.linker = "-Wl,--as-needed -lnetwork -lbsd"
|
||||
clang.cpp.options.linker = "-Wl,--as-needed -lnetwork -lbsd"
|
||||
tcc.options.linker = "-Wl,--as-needed -lnetwork -lbsd"
|
||||
gcc.options.linker = "-Wl,--as-needed -lnetwork"
|
||||
gcc.cpp.options.linker = "-Wl,--as-needed -lnetwork"
|
||||
clang.options.linker = "-Wl,--as-needed -lnetwork"
|
||||
clang.cpp.options.linker = "-Wl,--as-needed -lnetwork"
|
||||
tcc.options.linker = "-Wl,--as-needed -lnetwork"
|
||||
@elif not genode:
|
||||
# -fopenmp
|
||||
gcc.options.linker = "-ldl"
|
||||
|
||||
19
doc/mm.md
19
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`
|
||||
|
||||
@@ -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 =
|
||||
|
||||
@@ -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..<count:
|
||||
@@ -1447,10 +1461,7 @@ else:
|
||||
if writeCbListCount > 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]) =
|
||||
|
||||
@@ -95,7 +95,7 @@ template withValue*[A, B](t: var SharedTable[A, B], key: A,
|
||||
release(t.lock)
|
||||
|
||||
template withValue*[A, B](t: var SharedTable[A, B], key: A,
|
||||
value, body1, body2: untyped) =
|
||||
value, body1, body2: untyped): untyped =
|
||||
## Retrieves the value at `t[key]`.
|
||||
## `value` can be modified in the scope of the `withValue` call.
|
||||
runnableExamples:
|
||||
|
||||
@@ -636,7 +636,7 @@ template withValue*[A, B](t: var Table[A, B], key: A, value, body: untyped) =
|
||||
body
|
||||
|
||||
template withValue*[A, B](t: var Table[A, B], key: A,
|
||||
value, body1, body2: untyped) =
|
||||
value, body1, body2: untyped): untyped =
|
||||
## Retrieves the value at `t[key]`.
|
||||
##
|
||||
## `value` can be modified in the scope of the `withValue` call.
|
||||
@@ -677,7 +677,7 @@ template withValue*[A, B](t: var Table[A, B], key: A,
|
||||
body2
|
||||
|
||||
template withValue*[A, B](t: Table[A, B], key: A,
|
||||
value, body1, body2: untyped) =
|
||||
value, body1, body2: untyped): untyped =
|
||||
## Retrieves the value at `t[key]` if it exists, assigns
|
||||
## it to the variable `value` and executes `body`
|
||||
runnableExamples:
|
||||
|
||||
@@ -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`.
|
||||
|
||||
@@ -103,7 +103,6 @@ when defined(windows):
|
||||
import std/os
|
||||
|
||||
const
|
||||
DUPLICATE_SAME_ACCESS = 2
|
||||
FOREGROUND_BLUE = 1
|
||||
FOREGROUND_GREEN = 2
|
||||
FOREGROUND_RED = 4
|
||||
@@ -115,14 +114,7 @@ when defined(windows):
|
||||
FOREGROUND_RGB = FOREGROUND_RED or FOREGROUND_GREEN or FOREGROUND_BLUE
|
||||
BACKGROUND_RGB = BACKGROUND_RED or BACKGROUND_GREEN or BACKGROUND_BLUE
|
||||
|
||||
ENABLE_VIRTUAL_TERMINAL_PROCESSING = 0x0004
|
||||
|
||||
type
|
||||
SHORT = int16
|
||||
COORD = object
|
||||
x: SHORT
|
||||
y: SHORT
|
||||
|
||||
SMALL_RECT = object
|
||||
left: SHORT
|
||||
top: SHORT
|
||||
@@ -140,13 +132,6 @@ when defined(windows):
|
||||
dwSize: DWORD
|
||||
bVisible: WINBOOL
|
||||
|
||||
proc duplicateHandle(hSourceProcessHandle: Handle, hSourceHandle: Handle,
|
||||
hTargetProcessHandle: Handle, lpTargetHandle: ptr Handle,
|
||||
dwDesiredAccess: DWORD, bInheritHandle: WINBOOL,
|
||||
dwOptions: DWORD): WINBOOL{.stdcall, dynlib: "kernel32",
|
||||
importc: "DuplicateHandle".}
|
||||
proc getCurrentProcess(): Handle{.stdcall, dynlib: "kernel32",
|
||||
importc: "GetCurrentProcess".}
|
||||
proc getConsoleScreenBufferInfo(hConsoleOutput: Handle,
|
||||
lpConsoleScreenBufferInfo: ptr CONSOLE_SCREEN_BUFFER_INFO): WINBOOL{.stdcall,
|
||||
dynlib: "kernel32", importc: "GetConsoleScreenBufferInfo".}
|
||||
@@ -191,30 +176,6 @@ when defined(windows):
|
||||
if h > 0: return h
|
||||
return 0
|
||||
|
||||
proc setConsoleCursorPosition(hConsoleOutput: Handle,
|
||||
dwCursorPosition: COORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "SetConsoleCursorPosition".}
|
||||
|
||||
proc fillConsoleOutputCharacter(hConsoleOutput: Handle, cCharacter: char,
|
||||
nLength: DWORD, dwWriteCoord: COORD,
|
||||
lpNumberOfCharsWritten: ptr DWORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "FillConsoleOutputCharacterA".}
|
||||
|
||||
proc fillConsoleOutputAttribute(hConsoleOutput: Handle, wAttribute: int16,
|
||||
nLength: DWORD, dwWriteCoord: COORD,
|
||||
lpNumberOfAttrsWritten: ptr DWORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "FillConsoleOutputAttribute".}
|
||||
|
||||
proc setConsoleTextAttribute(hConsoleOutput: Handle,
|
||||
wAttributes: int16): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "SetConsoleTextAttribute".}
|
||||
|
||||
proc getConsoleMode(hConsoleHandle: Handle, dwMode: ptr DWORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "GetConsoleMode".}
|
||||
|
||||
proc setConsoleMode(hConsoleHandle: Handle, dwMode: DWORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "SetConsoleMode".}
|
||||
|
||||
proc getCursorPos(h: Handle): tuple [x, y: int] =
|
||||
var c: CONSOLE_SCREEN_BUFFER_INFO
|
||||
if getConsoleScreenBufferInfo(h, addr(c)) == 0:
|
||||
@@ -915,9 +876,6 @@ when defined(windows):
|
||||
var mode = DWORD 0
|
||||
discard getConsoleMode(hi, addr mode)
|
||||
let origMode = mode
|
||||
const
|
||||
ENABLE_PROCESSED_INPUT = 1
|
||||
ENABLE_ECHO_INPUT = 4
|
||||
mode = (mode or ENABLE_PROCESSED_INPUT) and not ENABLE_ECHO_INPUT
|
||||
|
||||
discard setConsoleMode(hi, mode)
|
||||
|
||||
@@ -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:
|
||||
|
||||
@@ -17,19 +17,30 @@ when defined(nimPreviewSlimSystem):
|
||||
|
||||
const whitespaces = {' ', '\t', '\v', '\r', '\l', '\f'}
|
||||
|
||||
const notJSnotNims = not defined(js) and not defined(nimscript)
|
||||
template whenNotVmJsNims(normalBody, restrictedBody: untyped) =
|
||||
## hack, see: #12517 #12518; Edit together with identical in `system`
|
||||
when nimvm:
|
||||
restrictedBody
|
||||
else:
|
||||
when notJSnotNims:
|
||||
normalBody
|
||||
else:
|
||||
restrictedBody
|
||||
|
||||
proc add*(x: var string, y: openArray[char]) =
|
||||
## Concatenates `x` and `y` in place. `y` must not overlap with `x` to
|
||||
## allow future `memcpy` optimizations.
|
||||
## Concatenates `x` and `y` in place. `y` must not overlap with `x`
|
||||
# Use `{.noalias.}` ?
|
||||
let n = x.len
|
||||
x.setLen n + y.len
|
||||
# pending #19727
|
||||
# setLen unnecessarily zeros memory
|
||||
var i = 0
|
||||
while i < y.len:
|
||||
x[n + i] = y[i]
|
||||
i.inc
|
||||
# xxx use `nimCopyMem(x[n].addr, y[0].addr, y.len)` after some refactoring
|
||||
if y.len == 0: return
|
||||
let oldLen = x.len
|
||||
x.setLenUninit(oldLen + y.len)
|
||||
whenNotVmJsNims():
|
||||
{.cast(noSideEffect).}:
|
||||
copyMem(beginStore(x, oldLen + y.len, oldLen), addr(y[0]), y.len)
|
||||
endStore(x)
|
||||
do:
|
||||
for i, ch in y:
|
||||
x[oldLen + i] = ch
|
||||
|
||||
func stripSlice(s: openArray[char], leading = true, trailing = true, chars: set[char] = whitespaces): Slice[int] =
|
||||
## Returns the slice range of `s` which is stripped `chars`.
|
||||
@@ -74,19 +85,14 @@ func setSlice*(s: var string, slice: Slice[int]) =
|
||||
if first > last:
|
||||
s.setLen(0)
|
||||
return
|
||||
template impl =
|
||||
for index in first .. last:
|
||||
s[index - first] = s[index]
|
||||
if first > 0:
|
||||
when nimvm: impl()
|
||||
else:
|
||||
# not JS and not Nimscript
|
||||
when not declared(moveMem):
|
||||
impl()
|
||||
else:
|
||||
let p = beginStore(s, s.len)
|
||||
moveMem(p, addr p[first], last - first + 1)
|
||||
endStore(s)
|
||||
whenNotVmJsNims():
|
||||
let p = beginStore(s, s.len)
|
||||
moveMem(p, addr p[first], last - first + 1)
|
||||
endStore(s)
|
||||
do:
|
||||
for index in first .. last:
|
||||
s[index - first] = s[index]
|
||||
s.setLen(last - first + 1)
|
||||
|
||||
func strip*(a: var string, leading = true, trailing = true, chars: set[char] = whitespaces) {.inline.} =
|
||||
|
||||
@@ -252,7 +252,36 @@ proc nimDecRefIsLast(p: pointer): bool {.compilerRtl, inl.} =
|
||||
writeStackTrace()
|
||||
cfprintf(cstderr, "[DecRef] %p %ld\n", p, cell.count)
|
||||
|
||||
when (defined(gcAtomicArc) or defined(gcYrc)) and hasThreadSupport:
|
||||
when defined(gcAtomicArc) and hasThreadSupport and
|
||||
not defined(nimNoAtomicArcFastPath):
|
||||
# Uniquely-referenced fast path: skip the RMW entirely.
|
||||
#
|
||||
# A counted reference can only be derived from the location being
|
||||
# destroyed (which happens-before this destructor, or the program races
|
||||
# on that location) or from another counted reference (whose
|
||||
# contribution is already in `rc`, forcing the RMW below). So observing
|
||||
# a zero count proves no other thread holds a reference to this cell and
|
||||
# therefore none can be inside this destructor: there is nothing to
|
||||
# adjudicate and no RMW is needed. This is only sound because
|
||||
# `--mm:atomicArc` has no collector -- ORC/YRC mutate `rc` from a
|
||||
# participant that holds no counted reference at all.
|
||||
#
|
||||
# The load must be ACQUIRE: the count may have reached zero because
|
||||
# another thread's release-decrement got there first, and we have to see
|
||||
# its writes before destroying the object.
|
||||
#
|
||||
# The slow path stays self-testing (it frees on the value the RMW
|
||||
# returned, never on a separate load), which is what keeps this out of
|
||||
# the nim-lang/threading#45 bug class.
|
||||
if (atomicLoadN(addr cell.rc, ATOMIC_ACQUIRE) and not rcMask) == 0:
|
||||
result = true
|
||||
when traceCollector:
|
||||
cprintf("[ABOUT TO DESTROY] %p\n", cell)
|
||||
elif atomicDec(cell.rc, rcIncrement) == -rcIncrement:
|
||||
result = true
|
||||
when traceCollector:
|
||||
cprintf("[ABOUT TO DESTROY] %p\n", cell)
|
||||
elif (defined(gcAtomicArc) or defined(gcYrc)) and hasThreadSupport:
|
||||
# `atomicDec` returns the new value
|
||||
if atomicDec(cell.rc, rcIncrement) == -rcIncrement:
|
||||
result = true
|
||||
|
||||
File diff suppressed because it is too large
Load Diff
668
lib/system/yrc_opt_proof.lean
Normal file
668
lib/system/yrc_opt_proof.lean
Normal file
@@ -0,0 +1,668 @@
|
||||
/-
|
||||
YRC Optimization Proofs — SCC-uniform ages, demand-grown slots, deferred
|
||||
reclamation
|
||||
=======================================================================
|
||||
Self-contained, no Mathlib. Checked with Lean 4 (v4.32.0).
|
||||
|
||||
Companion to yrc_proof.lean (core safety: garbage stability, validation
|
||||
soundness, partitions, grace, fence, deadlock freedom) and to
|
||||
yrc_tarjan_proof.lean (soundness AND completeness of the SCC deadness
|
||||
scan). This file models the three changes of the "YRC: optimizations"
|
||||
round, each of which touches an invariant the other two files rely on:
|
||||
|
||||
§A SCC-UNIFORM EPOCH AGES (commitDead's re-stamp loop).
|
||||
Before: every proven-live cell was stamped with its OWN survival
|
||||
age + 1. One member of an SCC could then reach `YrcPromoteAge`
|
||||
ahead of its SCC-mates; the next capture pruned that INTERNAL edge,
|
||||
tainting the SCC `flagPruned`, which stops it from ever being
|
||||
re-stamped — freezing every member's age and re-tracing the whole
|
||||
structure on every collection from then on. Members age at
|
||||
different rates whenever a structure is built incrementally, so
|
||||
this was the common case.
|
||||
After: the whole SCC is stamped with the age of its YOUNGEST
|
||||
member + 1, so promotion is all-or-nothing.
|
||||
|
||||
§B DEMAND-GROWN COLLECTOR SLOTS (`gParSlots`, startCollection).
|
||||
Before: `MaxPar` was a fixed 8 and the 9th collecting thread PARKED
|
||||
in `parkUntil(anySlotFree())` instead of collecting. After:
|
||||
`gParSlots` counts the slots in play, starts at 1, and is raised
|
||||
under gMergeLock exactly when a thread wants to collect and every
|
||||
slot in play is busy; `MaxPar` (256) is only the table capacity.
|
||||
Every scan (`isActiveTag`, `anySlotFree`, `buildPendingWatch`) now
|
||||
runs over a prefix that GROWS under the reader, which is sound only
|
||||
because of the ordering rule at `slotsInPlay`.
|
||||
|
||||
§C DEFERRED RECLAMATION (`gPendingCells` / `releasePending`).
|
||||
Before: commitDead BLOCKED until every concurrent capture ended
|
||||
(the grace period), inside the GC fence — stalling both the
|
||||
committing collector and every mutator doing a seq operation.
|
||||
After: the dead batch is parked together with a watch list of the
|
||||
captures it must outlive, and released at the start of this
|
||||
thread's next collection. The parked collection's TAG STAYS in
|
||||
`gActiveTags` (only the phase is cleared): that is what stops a
|
||||
foreign capture from claiming — and then freeing — a parked cell.
|
||||
|
||||
Nothing here weakens yrc_proof.lean: §A only changes which cells a
|
||||
capture skips (pruning shrinks the captured set, the conservative
|
||||
direction), §B only changes how many slots a scan covers, and §C only
|
||||
moves the free of an already-validated, already-closed dead set later
|
||||
in time, where garbage stability (yrc_proof.lean §3) keeps it dead.
|
||||
-/
|
||||
|
||||
abbrev Obj := Nat
|
||||
abbrev Tag := Nat
|
||||
-- Slot indices and times are plain `Nat`: `omega` ignores atoms whose type
|
||||
-- is an abbreviation, and both appear in arithmetic below.
|
||||
|
||||
/-! ## §A SCC-uniform epoch ages
|
||||
|
||||
The spare header word (`rootIdx`) is a three-way namespace: 0 for a
|
||||
cell no collection ever touched, a claim tag while a collection owns
|
||||
the cell, or an epoch stamp (`epochBase | epoch` in the high word, the
|
||||
survival age in the low word). Tags are allocated strictly below
|
||||
`epochBase`, so a stamp is never mistaken for a tag — modelled here by
|
||||
keeping the three cases as separate constructors. -/
|
||||
|
||||
inductive Word where
|
||||
| fresh -- 0: never claimed, never stamped
|
||||
| tag (t : Tag) -- a collection's claim word
|
||||
| stamp (e : Nat) (age : Nat) -- an epoch stamp written by commitDead
|
||||
|
||||
/-- The age a capture reads out of a claim word (`cap.ages`): a stamp
|
||||
contributes its recorded age, anything else contributes 0. -/
|
||||
def ageOf : Word → Nat
|
||||
| .stamp _ a => a
|
||||
| _ => 0
|
||||
|
||||
def capturedAge (w : Obj → Word) (x : Obj) : Nat := ageOf (w x)
|
||||
|
||||
/-- `claimCell(pruneLive = true)` prunes at a target whose stamp is of the
|
||||
CURRENT epoch and whose age reached `YrcPromoteAge`: the target is
|
||||
treated as an opaque live external and is not descended into. Roots
|
||||
are always claimed with `pruneLive = false`, so this never applies to
|
||||
them. -/
|
||||
def prunable (curEpoch promoteAge : Nat) : Word → Prop
|
||||
| .stamp e a => e = curEpoch ∧ promoteAge ≤ a
|
||||
| _ => False
|
||||
|
||||
/-- `high(int32)`, the seed of commitDead's per-SCC minimum. -/
|
||||
def bigAge : Nat := 2147483647
|
||||
|
||||
/-- Minimum of a list with a default (the `var age = high(int32)` fold). -/
|
||||
def listMin : List Nat → Nat → Nat
|
||||
| [], d => d
|
||||
| a :: l, d => Nat.min a (listMin l d)
|
||||
|
||||
theorem listMin_le : ∀ (l : List Nat) (d a : Nat), a ∈ l → listMin l d ≤ a := by
|
||||
intro l
|
||||
induction l with
|
||||
| nil => intro d a ha; cases ha
|
||||
| cons b t ih =>
|
||||
intro d a ha
|
||||
cases List.mem_cons.mp ha with
|
||||
| inl h =>
|
||||
simp only [listMin, Nat.min_def]
|
||||
split <;> omega
|
||||
| inr h =>
|
||||
have := ih d a h
|
||||
simp only [listMin, Nat.min_def]
|
||||
split <;> omega
|
||||
|
||||
theorem listMin_ge : ∀ (l : List Nat) (d b : Nat), b ≤ d →
|
||||
(∀ x, x ∈ l → b ≤ x) → b ≤ listMin l d := by
|
||||
intro l
|
||||
induction l with
|
||||
| nil => intro d b hd _; simpa [listMin] using hd
|
||||
| cons a t ih =>
|
||||
intro d b hd hall
|
||||
have h1 : b ≤ a := hall a (by simp)
|
||||
have h2 := ih d b hd (fun x hx => hall x (List.mem_cons_of_mem a hx))
|
||||
simp only [listMin, Nat.min_def]
|
||||
split <;> omega
|
||||
|
||||
theorem listMin_const (l : List Nat) (d a : Nat) (hne : l ≠ [])
|
||||
(hall : ∀ x, x ∈ l → x = a) (had : a ≤ d) : listMin l d = a := by
|
||||
have hlo : a ≤ listMin l d :=
|
||||
listMin_ge l d a had (fun x hx => by have := hall x hx; omega)
|
||||
cases l with
|
||||
| nil => exact absurd rfl hne
|
||||
| cons b t =>
|
||||
have hb : b ∈ b :: t := by simp
|
||||
have hhi := listMin_le (b :: t) d b hb
|
||||
have := hall b hb
|
||||
omega
|
||||
|
||||
/-- **The change.** commitDead stamps a proven-live SCC with ONE word: the
|
||||
current epoch and 1 + the age of its YOUNGEST member. -/
|
||||
def sccAge (w : Obj → Word) (ms : List Obj) : Nat :=
|
||||
listMin (ms.map (fun m => capturedAge w m)) bigAge + 1
|
||||
|
||||
/-- The post-state of commitDead's re-stamp loop, as committed: every
|
||||
member of the SCC gets the same word, nothing else is touched. -/
|
||||
structure StampedUniform (w w' : Obj → Word) (e : Nat) (ms : List Obj) : Prop where
|
||||
members : ∀ m, m ∈ ms → w' m = .stamp e (sccAge w ms)
|
||||
others : ∀ x, x ∉ ms → w' x = w x
|
||||
|
||||
/-- The previous, per-cell scheme, for contrast. -/
|
||||
structure StampedPerCell (w w' : Obj → Word) (e : Nat) (ms : List Obj) : Prop where
|
||||
members : ∀ m, m ∈ ms → w' m = .stamp e (capturedAge w m + 1)
|
||||
others : ∀ x, x ∉ ms → w' x = w x
|
||||
|
||||
/-- **A1 Uniformity**: after commit, all members of a stamped SCC carry
|
||||
the identical claim word — same epoch AND same age. -/
|
||||
theorem stamped_uniform (w w' : Obj → Word) (e : Nat) (ms : List Obj)
|
||||
(h : StampedUniform w w' e ms) :
|
||||
∀ x y, x ∈ ms → y ∈ ms → w' x = w' y := by
|
||||
intro x y hx hy
|
||||
rw [h.members x hx, h.members y hy]
|
||||
|
||||
/-- **A2 No internal prune**: a capture descends into a member `u` of an
|
||||
SCC only through an edge that was NOT pruned (or because `u` is a
|
||||
root, which bypasses stamps entirely). With uniform words, every
|
||||
other member `v` is then unprunable too — so no INTERNAL edge of the
|
||||
SCC can be pruned, and the SCC is never tainted `flagPruned` by its
|
||||
own topology. This is precisely the failure the per-cell age caused. -/
|
||||
theorem uniform_no_internal_prune
|
||||
(w : Obj → Word) (curEpoch promoteAge : Nat) (ms : List Obj)
|
||||
(huni : ∀ x y, x ∈ ms → y ∈ ms → w x = w y)
|
||||
(u v : Obj) (hu : u ∈ ms) (hv : v ∈ ms)
|
||||
(hdescended : ¬ prunable curEpoch promoteAge (w u)) :
|
||||
¬ prunable curEpoch promoteAge (w v) := by
|
||||
rw [← huni u v hu hv]
|
||||
exact hdescended
|
||||
|
||||
/-- A2 applied to the state commitDead actually leaves behind. -/
|
||||
theorem committed_scc_no_internal_prune
|
||||
(w w' : Obj → Word) (e curEpoch promoteAge : Nat) (ms : List Obj)
|
||||
(hst : StampedUniform w w' e ms)
|
||||
(u v : Obj) (hu : u ∈ ms) (hv : v ∈ ms)
|
||||
(hdescended : ¬ prunable curEpoch promoteAge (w' u)) :
|
||||
¬ prunable curEpoch promoteAge (w' v) :=
|
||||
uniform_no_internal_prune w' curEpoch promoteAge ms
|
||||
(stamped_uniform w w' e ms hst) u v hu hv hdescended
|
||||
|
||||
/-- **A3 The per-cell scheme diverges**: two members of ONE SCC whose
|
||||
captured ages differ (the normal case for a structure built
|
||||
incrementally across collections) end up with different ages. -/
|
||||
theorem perCell_ages_diverge (w w'' : Obj → Word) (e : Nat) (ms : List Obj)
|
||||
(hp : StampedPerCell w w'' e ms) (u v : Obj) (hu : u ∈ ms) (hv : v ∈ ms)
|
||||
(hdiff : capturedAge w u ≠ capturedAge w v) :
|
||||
ageOf (w'' u) ≠ ageOf (w'' v) := by
|
||||
rw [hp.members u hu, hp.members v hv]
|
||||
simp only [ageOf]
|
||||
omega
|
||||
|
||||
/-- ...and diverged ages inside one SCC mean exactly one prunable end of
|
||||
an internal edge: the promoted member is pruned while its unpromoted
|
||||
SCC-mate is still being traced. -/
|
||||
theorem diverged_ages_prune_internally (curEpoch promoteAge au av : Nat)
|
||||
(hu : au < promoteAge) (hv : promoteAge ≤ av) :
|
||||
¬ prunable curEpoch promoteAge (.stamp curEpoch au) ∧
|
||||
prunable curEpoch promoteAge (.stamp curEpoch av) := by
|
||||
constructor
|
||||
· intro h
|
||||
obtain ⟨-, h2⟩ := h
|
||||
omega
|
||||
· exact ⟨rfl, hv⟩
|
||||
|
||||
/-- **A4 The minimum can only delay a promotion, never hasten one**, so
|
||||
taking it cannot widen the floating-garbage bound (~2 epochs). -/
|
||||
theorem uniform_age_le_perCell (w w' w'' : Obj → Word) (e : Nat) (ms : List Obj)
|
||||
(hu : StampedUniform w w' e ms) (hp : StampedPerCell w w'' e ms)
|
||||
(m : Obj) (hm : m ∈ ms) :
|
||||
ageOf (w' m) ≤ ageOf (w'' m) := by
|
||||
have hmem : capturedAge w m ∈ ms.map (fun x => capturedAge w x) :=
|
||||
List.mem_map_of_mem hm
|
||||
have hle := listMin_le (ms.map (fun x => capturedAge w x)) bigAge
|
||||
(capturedAge w m) hmem
|
||||
rw [hu.members m hm, hp.members m hm]
|
||||
simp only [ageOf, sccAge]
|
||||
omega
|
||||
|
||||
/-- Corollary: wherever the SCC-uniform stamp prunes, the per-cell stamp
|
||||
would have pruned too. Pruning is the only thing a stamp does, so the
|
||||
change cannot make any capture skip MORE than before. -/
|
||||
theorem uniform_never_hastens_promotion (w w' w'' : Obj → Word) (e : Nat)
|
||||
(ms : List Obj) (promoteAge : Nat)
|
||||
(hu : StampedUniform w w' e ms) (hp : StampedPerCell w w'' e ms)
|
||||
(m : Obj) (hm : m ∈ ms) (h : promoteAge ≤ ageOf (w' m)) :
|
||||
promoteAge ≤ ageOf (w'' m) := by
|
||||
have := uniform_age_le_perCell w w' w'' e ms hu hp m hm
|
||||
omega
|
||||
|
||||
/-- **A5 The uniform age is exactly the common age + 1**, so a surviving
|
||||
SCC's age advances by one per collection and stays uniform: the
|
||||
invariant of A1/A2 is inductive. -/
|
||||
theorem uniform_age_succ (w w' : Obj → Word) (e a : Nat) (ms : List Obj)
|
||||
(hne : ms ≠ []) (hcap : a ≤ bigAge)
|
||||
(hall : ∀ m, m ∈ ms → capturedAge w m = a)
|
||||
(h : StampedUniform w w' e ms) :
|
||||
∀ m, m ∈ ms → ageOf (w' m) = a + 1 := by
|
||||
intro m hm
|
||||
have hmin : listMin (ms.map (fun x => capturedAge w x)) bigAge = a := by
|
||||
apply listMin_const
|
||||
· cases ms with
|
||||
| nil => exact absurd rfl hne
|
||||
| cons b t => simp
|
||||
· intro x hx
|
||||
obtain ⟨y, hy, rfl⟩ := List.mem_map.mp hx
|
||||
exact hall y hy
|
||||
· exact hcap
|
||||
rw [h.members m hm]
|
||||
simp only [ageOf, sccAge, hmin]
|
||||
|
||||
/-- **A6 The freeze**: an SCC that is never re-stamped (the `flagPruned`
|
||||
taint excludes it from commitDead's stamp loop) keeps its age
|
||||
forever. Below `YrcPromoteAge` that means it is fully re-traced by
|
||||
every collection until the epoch turns — the regression A2 removes. -/
|
||||
theorem age_frozen_if_never_restamped (age : Nat → Nat) (a : Nat)
|
||||
(h0 : age 0 = a) (hfreeze : ∀ n, age (n + 1) = age n) :
|
||||
∀ n, age n = a := by
|
||||
intro n
|
||||
induction n with
|
||||
| zero => exact h0
|
||||
| succ n ih => rw [hfreeze n, ih]
|
||||
|
||||
/-- **A7 Progress**: an SCC that IS re-stamped every round promotes after
|
||||
`YrcPromoteAge` collections, and by A2 stays promoted uniformly — so
|
||||
a long-lived structure is traced once per epoch, not once per
|
||||
collection. -/
|
||||
theorem age_promotes_if_restamped (age : Nat → Nat) (a promoteAge : Nat)
|
||||
(h0 : age 0 = a) (hstep : ∀ n, age (n + 1) = age n + 1) :
|
||||
promoteAge ≤ age promoteAge := by
|
||||
have h : ∀ n, age n = a + n := by
|
||||
intro n
|
||||
induction n with
|
||||
| zero => simpa using h0
|
||||
| succ n ih => rw [hstep n, ih]; omega
|
||||
rw [h promoteAge]
|
||||
omega
|
||||
|
||||
/-! ## §B Demand-grown collector slots
|
||||
|
||||
`gParSlots` counts the slots IN PLAY. It starts at 1, is raised under
|
||||
gMergeLock when a thread wants to collect and every slot in play is
|
||||
busy, and is NEVER lowered. Two things must hold:
|
||||
|
||||
(i) a scan over the prefix `0 ..< slotsInPlay()` must never MISS an
|
||||
active tag — a missed tag would let a second collection claim a
|
||||
cell another collection already owns, breaking partition
|
||||
disjointness (yrc_proof.lean §5) and admitting a double free;
|
||||
(ii) a thread must not park while the table still has room — that was
|
||||
the throttle the fixed `MaxPar = 8` imposed.
|
||||
|
||||
(i) rests on the publication order in startCollection: the wider bound
|
||||
is stored BEFORE the tag lands in the new slot, and `gParSlots` only
|
||||
grows. So a load of `slotsInPlay()` ordered AFTER the read of a tagged
|
||||
claim word is guaranteed to cover the slot that wrote that tag. -/
|
||||
|
||||
/-- `gParSlots` never shrinks, so a prefix scan cannot shrink under a
|
||||
reader either. -/
|
||||
theorem in_play_persists (parSlots : Nat → Nat)
|
||||
(hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j)
|
||||
(k : Nat) (t t' : Nat) (h : t ≤ t') (hk : k < parSlots t) :
|
||||
k < parSlots t' := by
|
||||
have := hmono t t' h
|
||||
omega
|
||||
|
||||
/-- **B1 The scan covers the slot that wrote the tag.** `tGrow` is when
|
||||
the slot was put in play (under gMergeLock), `tTag` the tag store,
|
||||
`tRead` the reader's load of the claim word, `tScan` its subsequent
|
||||
load of `slotsInPlay()`. -/
|
||||
theorem scan_covers_tagged_slot (parSlots : Nat → Nat)
|
||||
(hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j)
|
||||
(k : Nat) (tGrow tTag tRead tScan : Nat)
|
||||
(hgrow : k < parSlots tGrow)
|
||||
(hpub : tGrow ≤ tTag) -- wider bound published before the tag store
|
||||
(hread : tTag ≤ tRead) -- the reader observed the tag
|
||||
(hafter : tRead ≤ tScan) :-- slotsInPlay() loaded AFTER the claim word
|
||||
k < parSlots tScan := by
|
||||
have := hmono tGrow tScan (by omega)
|
||||
omega
|
||||
|
||||
/-- **B2 `isActiveTag` is complete**: an active tag is always found by the
|
||||
prefix scan, so `claimCell` never claims a cell another collection
|
||||
owns. -/
|
||||
theorem active_tag_never_missed (parSlots : Nat → Nat)
|
||||
(tagAt : Nat → Nat → Tag)
|
||||
(hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j)
|
||||
(k : Nat) (t : Tag) (tGrow tTag tRead tScan : Nat)
|
||||
(hgrow : k < parSlots tGrow) (hpub : tGrow ≤ tTag)
|
||||
(hread : tTag ≤ tRead) (hafter : tRead ≤ tScan)
|
||||
(hheld : tagAt k tScan = t) :
|
||||
∃ j, j < parSlots tScan ∧ tagAt j tScan = t :=
|
||||
⟨k, scan_covers_tagged_slot parSlots hmono k tGrow tTag tRead tScan
|
||||
hgrow hpub hread hafter, hheld⟩
|
||||
|
||||
/-- **B3 The ordering rule is load-bearing**: a `slotsInPlay()` load
|
||||
ordered BEFORE the read of the claim word can legitimately miss the
|
||||
slot, because the pool may widen in between. -/
|
||||
theorem scan_before_read_may_miss :
|
||||
∃ (parSlots : Nat → Nat) (k : Nat) (tScan tGrow : Nat),
|
||||
(∀ i j, i ≤ j → parSlots i ≤ parSlots j) ∧ tScan < tGrow ∧
|
||||
k < parSlots tGrow ∧ ¬ (k < parSlots tScan) := by
|
||||
refine ⟨fun t => t + 1, 1, 0, 1, ?_, ?_, ?_, ?_⟩
|
||||
· intro i j h
|
||||
show i + 1 ≤ j + 1
|
||||
omega
|
||||
· decide
|
||||
· decide
|
||||
· decide
|
||||
|
||||
/-- startCollection's slot decision. -/
|
||||
inductive SlotOutcome where
|
||||
| reuse (k : Nat) -- a slot already in play was free
|
||||
| grow (k : Nat) -- pool widened; the new slot is `k = inPlay`
|
||||
| park -- table full: MaxPar collections already running
|
||||
|
||||
inductive SlotClaim (busy : Nat → Prop) (inPlay maxPar : Nat) : SlotOutcome → Prop where
|
||||
| reuse (k : Nat) (hk : k < inPlay) (hfree : ¬ busy k) :
|
||||
SlotClaim busy inPlay maxPar (.reuse k)
|
||||
| grow (hfull : ∀ k, k < inPlay → busy k) (hroom : inPlay < maxPar) :
|
||||
SlotClaim busy inPlay maxPar (.grow inPlay)
|
||||
| park (hfull : ∀ k, k < inPlay → busy k) (hno : maxPar ≤ inPlay) :
|
||||
SlotClaim busy inPlay maxPar .park
|
||||
|
||||
/-- **B4 Parking means saturation**, not throttling: a thread blocks in
|
||||
`parkUntil(anySlotFree())` only when `MaxPar` collections are running
|
||||
concurrently. Under the old fixed bound this triggered at the 9th
|
||||
collecting thread (32 threads vs 8 slots: 6.3s against 2.6s). -/
|
||||
theorem park_only_when_saturated (busy : Nat → Prop) (inPlay maxPar : Nat)
|
||||
(h : SlotClaim busy inPlay maxPar .park) :
|
||||
maxPar ≤ inPlay ∧ ∀ k, k < inPlay → busy k := by
|
||||
cases h with
|
||||
| park hfull hno => exact ⟨hno, hfull⟩
|
||||
|
||||
/-- **B5 No parking below capacity.** -/
|
||||
theorem no_park_below_capacity (busy : Nat → Prop) (inPlay maxPar : Nat)
|
||||
(hroom : inPlay < maxPar) : ¬ SlotClaim busy inPlay maxPar .park := by
|
||||
intro h
|
||||
cases h with
|
||||
| park hfull hno => omega
|
||||
|
||||
/-- **B6 A grown slot is fresh**: `k = inPlay` is distinct from every slot
|
||||
already in play, so the widening thread cannot collide with a
|
||||
collection that is already running. -/
|
||||
theorem grown_slot_not_in_play (inPlay k : Nat) (hk : k < inPlay) :
|
||||
inPlay ≠ k := by omega
|
||||
|
||||
/-! ## §C Deferred reclamation
|
||||
|
||||
commitDead used to spin until every concurrent capture had ended before
|
||||
freeing, INSIDE the GC fence. Now the batch is parked in
|
||||
`gPendingCells` with a watch list `gPendingWatch` of the (slot, tag)
|
||||
pairs that were in capture phase at commit time, and `releasePending`
|
||||
— the FIRST thing startCollection does, outside the fence and holding
|
||||
no lock — waits out that list and then frees.
|
||||
|
||||
Three obligations:
|
||||
(C1) the watch list is COMPLETE: every capture that could hold a stale
|
||||
`(slot, value)` snapshot of the batch is on it;
|
||||
(C2) the grace check is SOUND: `graceSatisfied` reports "finished" only
|
||||
when the watched capture really has finished;
|
||||
(C3) the batch is PROTECTED while parked: no foreign capture may claim
|
||||
(and hence free) one of its cells. This is why finishCollection
|
||||
clears only `gSlotPhase` and leaves the tag in `gActiveTags`. -/
|
||||
|
||||
/-- One slot's published state. -/
|
||||
structure SlotState where
|
||||
tag : Tag
|
||||
phase : Nat -- 0 idle, 1 capturing, 2 committing
|
||||
|
||||
/-- finishCollection with a batch parked: phase → 0, tag RETAINED. -/
|
||||
def finishParked (st : SlotState) : SlotState := { st with phase := 0 }
|
||||
|
||||
/-- releasePending, after the grace wait: the tag is given up first, then
|
||||
the destructors and `nimRawDispose` run. -/
|
||||
def releaseSlot (st : SlotState) : SlotState := { st with tag := 0 }
|
||||
|
||||
theorem finishParked_keeps_tag (st : SlotState) :
|
||||
(finishParked st).tag = st.tag := rfl
|
||||
|
||||
/-- A parked slot blocks nobody's grace period: its phase is 0, so every
|
||||
other collector's `graceSatisfied` passes over it. -/
|
||||
theorem parked_slot_blocks_nobody (st : SlotState) (tg : Tag) :
|
||||
¬ ((finishParked st).tag = tg ∧ (finishParked st).phase = 1) := by
|
||||
intro h
|
||||
simp [finishParked] at h
|
||||
|
||||
/-- ...yet the tag survives, which is what protects the parked cells. -/
|
||||
theorem parked_slot_still_tagged (st : SlotState) (t : Tag) (h : st.tag = t) :
|
||||
(finishParked st).tag = t := h
|
||||
|
||||
/-- `gPendingWatch`, as `(slot shl 32) or tag` pairs. -/
|
||||
abbrev WatchList := List (Nat × Tag)
|
||||
|
||||
/-- `graceSatisfied()` evaluated at time `t`. -/
|
||||
def graceSatisfied (tagAt : Nat → Nat → Tag) (phaseAt : Nat → Nat → Nat)
|
||||
(W : WatchList) (t : Nat) : Prop :=
|
||||
∀ p, p ∈ W → ¬ (tagAt p.1 t = p.2 ∧ phaseAt p.1 t = 1)
|
||||
|
||||
/-- **C1 The watch list is complete.** A capture that was in flight at
|
||||
commit time is running on a slot that was in play when its tag was
|
||||
stored; by B1 the `buildPendingWatch` scan — which loads
|
||||
`slotsInPlay()` after reading the claim state — covers that slot, and
|
||||
the capture's phase is 1, so it is recorded. -/
|
||||
theorem watch_covers_inflight_capture (parSlots : Nat → Nat)
|
||||
(tagAt : Nat → Nat → Tag) (phaseAt : Nat → Nat → Nat)
|
||||
(hmono : ∀ i j, i ≤ j → parSlots i ≤ parSlots j)
|
||||
(s : Nat) (tg : Tag) (tGrow tTag commitT : Nat)
|
||||
(hgrow : s < parSlots tGrow) (hpub : tGrow ≤ tTag) (hread : tTag ≤ commitT)
|
||||
(hcapturing : tagAt s commitT = tg ∧ phaseAt s commitT = 1) :
|
||||
s < parSlots commitT ∧ tagAt s commitT = tg ∧ phaseAt s commitT = 1 :=
|
||||
⟨scan_covers_tagged_slot parSlots hmono s tGrow tTag commitT commitT
|
||||
hgrow hpub hread (Nat.le_refl commitT), hcapturing.1, hcapturing.2⟩
|
||||
|
||||
/-- **C2 The grace check is sound**: if `graceSatisfied` holds at `t` and
|
||||
a watched capture was still running at `t`, we have a contradiction —
|
||||
so every watched capture finished strictly before `t`. There is no
|
||||
ABA on the (slot, tag) pair: tags come from a monotonic counter
|
||||
(yrc_proof.lean §5 `tags_distinct`), so a later collection on the
|
||||
same slot carries a different tag. -/
|
||||
theorem grace_check_sound (tagAt : Nat → Nat → Tag) (phaseAt : Nat → Nat → Nat)
|
||||
(W : WatchList) (s : Nat) (tg : Tag) (start finish t : Nat)
|
||||
(hw : (s, tg) ∈ W)
|
||||
(hcap : ∀ u, start ≤ u → u ≤ finish → tagAt s u = tg ∧ phaseAt s u = 1)
|
||||
(hstart : start ≤ t)
|
||||
(hsat : graceSatisfied tagAt phaseAt W t) :
|
||||
finish < t := by
|
||||
cases Nat.lt_or_ge finish t with
|
||||
| inl h => exact h
|
||||
| inr h => exact absurd (hcap t hstart h) (hsat (s, tg) hw)
|
||||
|
||||
/-- A capture's window and the values it ever snapshots (TraceEntry), as
|
||||
in yrc_proof.lean §6. -/
|
||||
structure CaptureWindow where
|
||||
start : Nat
|
||||
finish : Nat
|
||||
snap : Obj → Prop
|
||||
derefs : Obj → Nat → Prop
|
||||
|
||||
/-- **C3 Grace safety survives the deferral.** `commitT` is when the dead
|
||||
set validated, `releaseT` when releasePending's wait succeeded (C2),
|
||||
`freeT` when the batch is actually disposed. The only change from
|
||||
yrc_proof.lean's `grace_no_use_after_free` is that `freeT` moved
|
||||
LATER — the wait is unchanged in strength, it just happens off the
|
||||
commit path. -/
|
||||
theorem deferred_grace_no_use_after_free
|
||||
(C : CaptureWindow) (D : Obj → Prop) (commitT releaseT freeT : Nat)
|
||||
(h_deref : ∀ x t, C.derefs x t → C.start ≤ t ∧ t ≤ C.finish ∧ C.snap x)
|
||||
(h_watched : C.start < commitT → C.finish < releaseT)
|
||||
(h_release : releaseT ≤ freeT)
|
||||
(h_miss : commitT ≤ C.start → ∀ x, D x → ¬ C.snap x) :
|
||||
∀ x t, D x → C.derefs x t → t < freeT := by
|
||||
intro x t hD hd
|
||||
obtain ⟨h1, h2, h3⟩ := h_deref x t hd
|
||||
cases Nat.lt_or_ge C.start commitT with
|
||||
| inl h => have := h_watched h; omega
|
||||
| inr h => exact absurd h3 (h_miss h x hD)
|
||||
|
||||
/-- claimCell's decision on a cell, as a relation over its claim word. -/
|
||||
inductive ClaimResult where
|
||||
| mine -- our own tag: already captured this round
|
||||
| refuse -- owned by another ACTIVE collection (-1, crossPend)
|
||||
| prune -- proven live this epoch (-2, opaque live external)
|
||||
| claim -- CAS it into our partition
|
||||
|
||||
inductive ClaimDecision (myTag curEpoch promoteAge : Nat) (active : Tag → Prop) :
|
||||
Word → ClaimResult → Prop where
|
||||
| mine (t : Tag) (h : t = myTag) :
|
||||
ClaimDecision myTag curEpoch promoteAge active (.tag t) .mine
|
||||
| refuse (t : Tag) (hne : t ≠ myTag) (ha : active t) :
|
||||
ClaimDecision myTag curEpoch promoteAge active (.tag t) .refuse
|
||||
| claimTag (t : Tag) (hne : t ≠ myTag) (ha : ¬ active t) :
|
||||
ClaimDecision myTag curEpoch promoteAge active (.tag t) .claim
|
||||
| prune (e a : Nat) (hp : prunable curEpoch promoteAge (.stamp e a)) :
|
||||
ClaimDecision myTag curEpoch promoteAge active (.stamp e a) .prune
|
||||
| claimStamp (e a : Nat) (hp : ¬ prunable curEpoch promoteAge (.stamp e a)) :
|
||||
ClaimDecision myTag curEpoch promoteAge active (.stamp e a) .claim
|
||||
| claimFresh :
|
||||
ClaimDecision myTag curEpoch promoteAge active .fresh .claim
|
||||
|
||||
/-- **C4 A cell carrying an active foreign tag is always refused.** -/
|
||||
theorem tagged_cell_refused (myTag curEpoch promoteAge : Nat) (active : Tag → Prop)
|
||||
(ownerTag : Tag) (hne : ownerTag ≠ myTag) (ha : active ownerTag)
|
||||
(r : ClaimResult)
|
||||
(h : ClaimDecision myTag curEpoch promoteAge active (.tag ownerTag) r) :
|
||||
r = .refuse := by
|
||||
cases h with
|
||||
| mine t ht => exact absurd ht hne
|
||||
| refuse t hne' ha' => rfl
|
||||
| claimTag t hne' ha' => exact absurd ha ha'
|
||||
|
||||
/-- **C5 No double free while parked.** The parked cells still carry the
|
||||
parking collection's tag, and finishCollection left that tag in
|
||||
`gActiveTags` (only the phase was cleared, C-`finishParked`). So a
|
||||
foreign capture that reaches a parked cell through a stale snapshot
|
||||
refuses it: it can neither traverse it nor claim it, hence never
|
||||
classifies it dead and never frees it. Without the tag retention this
|
||||
is exactly a double free — the batch's owner will free it too. -/
|
||||
theorem no_foreign_claim_while_parked
|
||||
(activeAt : Nat → Tag → Prop) (ownerTag myTag : Tag)
|
||||
(curEpoch promoteAge : Nat) (commitT releaseT u : Nat)
|
||||
(hretain : ∀ v, commitT ≤ v → v ≤ releaseT → activeAt v ownerTag)
|
||||
(hne : ownerTag ≠ myTag) (h1 : commitT ≤ u) (h2 : u ≤ releaseT)
|
||||
(r : ClaimResult)
|
||||
(h : ClaimDecision myTag curEpoch promoteAge (activeAt u) (.tag ownerTag) r) :
|
||||
r = .refuse :=
|
||||
tagged_cell_refused myTag curEpoch promoteAge (activeAt u) ownerTag hne
|
||||
(hretain u h1 h2) r h
|
||||
|
||||
/-- **C6 Deferring the free is safe.** The batch was closed (unreachable)
|
||||
at commit time — that is what validation established (yrc_proof.lean
|
||||
§4 `validated_closed`) — and `hstable` is exactly
|
||||
yrc_proof.lean §3 `garbage_stability`: a closed set stays closed
|
||||
under every mutator step, allocation and foreign free. Freeing one
|
||||
collection later therefore satisfies the same §1 free condition as
|
||||
freeing immediately. -/
|
||||
theorem deferred_free_safe (unreachable : Nat → Obj → Prop) (D : Obj → Prop)
|
||||
(commitT freeT : Nat)
|
||||
(hcommit : ∀ x, D x → unreachable commitT x)
|
||||
(hstable : ∀ x t t', D x → t ≤ t' → unreachable t x → unreachable t' x)
|
||||
(hlater : commitT ≤ freeT) :
|
||||
∀ x, D x → unreachable freeT x :=
|
||||
fun x hx => hstable x commitT freeT hx hlater (hcommit x hx)
|
||||
|
||||
/-- **C7 The grace wait left the GC fence.** It now runs at the start of
|
||||
startCollection, before `yrcGcFenceEnter`, so no mutator seq
|
||||
operation can be stalled by it — the property the deferral was made
|
||||
for. -/
|
||||
theorem grace_wait_outside_fence (waitStart waitEnd fenceEnter fenceExit t : Nat)
|
||||
(horder : waitEnd < fenceEnter) (hw : waitStart ≤ t ∧ t ≤ waitEnd) :
|
||||
¬ (fenceEnter ≤ t ∧ t ≤ fenceExit) := by
|
||||
intro hf
|
||||
omega
|
||||
|
||||
/-- `waits a b`: thread `a` is blocked in releasePending on thread `b`'s
|
||||
capture. -/
|
||||
def waits (capturing releasing : Nat → Prop) (a b : Nat) : Prop :=
|
||||
releasing a ∧ capturing b
|
||||
|
||||
/-- **C8 The new wait cannot deadlock.** releasePending runs BEFORE this
|
||||
thread claims a slot, so a releasing thread is never itself
|
||||
capturing; the wait-for graph therefore has depth one and cannot
|
||||
contain a cycle of any length. (Captures never wait on anything:
|
||||
claimCell returns -1 immediately on contention.) -/
|
||||
theorem release_wait_depth_one (capturing releasing : Nat → Prop)
|
||||
(hexcl : ∀ t, releasing t → ¬ capturing t)
|
||||
(a b c : Nat) (h1 : waits capturing releasing a b) :
|
||||
¬ waits capturing releasing b c := by
|
||||
intro h2
|
||||
exact hexcl b h2.1 h1.2
|
||||
|
||||
/-- Corollary: no 2-cycle, hence no mutual wait between two parked
|
||||
collectors. -/
|
||||
theorem release_wait_acyclic (capturing releasing : Nat → Prop)
|
||||
(hexcl : ∀ t, releasing t → ¬ capturing t) (a b : Nat)
|
||||
(h1 : waits capturing releasing a b) :
|
||||
¬ waits capturing releasing b a :=
|
||||
release_wait_depth_one capturing releasing hexcl a b a h1
|
||||
|
||||
/-! ## Summary of verified properties (all QED, no sorry)
|
||||
|
||||
§A `stamped_uniform` — a committed SCC's members carry one identical
|
||||
claim word.
|
||||
`uniform_no_internal_prune`, `committed_scc_no_internal_prune` — a
|
||||
capture that descends into a member cannot prune an internal edge,
|
||||
so an SCC is never tainted `flagPruned` by its own topology.
|
||||
`perCell_ages_diverge` + `diverged_ages_prune_internally` — the
|
||||
pre-fix scheme admits exactly that taint.
|
||||
`uniform_age_le_perCell`, `uniform_never_hastens_promotion` — the
|
||||
minimum only delays promotions, so the float bound is unchanged.
|
||||
`uniform_age_succ` — uniformity is inductive: age advances by one
|
||||
and stays uniform.
|
||||
`age_frozen_if_never_restamped` / `age_promotes_if_restamped` — the
|
||||
frozen-age regression versus the intended once-per-epoch trace.
|
||||
|
||||
§B `in_play_persists`, `scan_covers_tagged_slot`,
|
||||
`active_tag_never_missed` — a growing `gParSlots` prefix scan never
|
||||
misses an active tag, PROVIDED `slotsInPlay()` is loaded after the
|
||||
claim word; `scan_before_read_may_miss` shows the order is
|
||||
load-bearing.
|
||||
`park_only_when_saturated`, `no_park_below_capacity`,
|
||||
`grown_slot_not_in_play` — a collector parks only when `MaxPar`
|
||||
collections run at once, and a widened slot collides with nobody.
|
||||
|
||||
§C `watch_covers_inflight_capture` — the watch list records every
|
||||
capture that could hold a stale snapshot of the batch (via §B).
|
||||
`grace_check_sound` — `graceSatisfied` reports "finished" only when
|
||||
the watched capture has finished.
|
||||
`deferred_grace_no_use_after_free` — no capture dereferences a
|
||||
parked cell at or after its free time.
|
||||
`tagged_cell_refused`, `no_foreign_claim_while_parked` — retaining
|
||||
the tag (finishCollection clears only the phase) is what prevents a
|
||||
foreign collection from claiming and freeing a parked cell.
|
||||
`parked_slot_blocks_nobody`, `parked_slot_still_tagged` — the two
|
||||
halves of that split: protection without blocking.
|
||||
`deferred_free_safe` — deferring the free preserves the §1 free
|
||||
condition, by garbage stability.
|
||||
`grace_wait_outside_fence` — the wait no longer overlaps the GC
|
||||
fence, so it cannot stall a mutator's seq operation.
|
||||
`release_wait_depth_one`, `release_wait_acyclic` — the new wait
|
||||
adds no cycle to the wait-for structure of yrc_proof.lean §8.
|
||||
|
||||
## What is NOT proved
|
||||
|
||||
• Slot-retention liveness. A parked batch holds its tag slot until the
|
||||
owning thread's NEXT collection (or GC_runOrc / nimYrcThreadTeardown,
|
||||
both of which call releasePending). A thread that parks a batch and
|
||||
then never collects again keeps a slot occupied; with enough such
|
||||
threads the table could saturate and other collectors would park
|
||||
(§B4). Bounded in practice by `MaxPar = 256` and by teardown, not
|
||||
formalized.
|
||||
• That `buildPendingWatch` returning false (nothing capturing) really
|
||||
is the common case — a performance claim, measured, not proved.
|
||||
• Destructor timing. Deferral runs a dead batch's destructors one
|
||||
collection later. Safety is C6; the observable-behaviour claim
|
||||
("nothing else observes the delay, the cells are unreachable and
|
||||
their references already dropped") is an argument about the Nim
|
||||
language semantics, not modelled here.
|
||||
• Conservatism of tag retention. While a batch is parked, the tag also
|
||||
protects SURVIVORS that kept a stale tag (dirty and pruned SCCs are
|
||||
deliberately not re-stamped), so a foreign capture refuses them for
|
||||
one extra collection. That delays their re-examination; it cannot
|
||||
lose them, because §A's E1–E4 hooks keep a dec-witness registered.
|
||||
• Everything already listed as unproved in yrc_proof.lean (rc-exactness
|
||||
mechanics, the C11 memory model, liveness/completeness of the retry
|
||||
loop, tag wrap-around).
|
||||
-/
|
||||
@@ -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
|
||||
|
||||
@@ -26,6 +26,7 @@ type WinChar* = Utf16Char
|
||||
# See https://docs.microsoft.com/en-us/windows/win32/winprog/windows-data-types
|
||||
type
|
||||
Handle* = int
|
||||
SHORT* = int16
|
||||
LONG* = int32
|
||||
ULONG* = int32
|
||||
PULONG* = ptr int
|
||||
@@ -1013,10 +1014,57 @@ type
|
||||
uChar*: int16
|
||||
dwControlKeyState*: DWORD
|
||||
|
||||
# https://learn.microsoft.com/en-us/windows/console/coord-str
|
||||
COORD* = object
|
||||
x*: SHORT
|
||||
y*: SHORT
|
||||
|
||||
const
|
||||
# used by std/terminal
|
||||
# https://learn.microsoft.com/en-us/windows/console/setconsolemode
|
||||
ENABLE_ECHO_INPUT* = 0x0004
|
||||
ENABLE_INSERT_MODE* = 0x0020
|
||||
ENABLE_LINE_INPUT* = 0x0002
|
||||
ENABLE_MOUSE_INPUT* = 0x0010
|
||||
ENABLE_PROCESSED_INPUT* = 0x0001
|
||||
ENABLE_QUICK_EDIT_MODE* = 0x0040
|
||||
ENABLE_WINDOW_INPUT* = 0x0008
|
||||
ENABLE_VIRTUAL_TERMINAL_INPUT* = 0x0200
|
||||
|
||||
ENABLE_PROCESSED_OUTPUT* = 0x0001
|
||||
ENABLE_WRAP_AT_EOL_OUTPUT* = 0x0002
|
||||
ENABLE_VIRTUAL_TERMINAL_PROCESSING* = 0x0004
|
||||
DISABLE_NEWLINE_AUTO_RETURN* = 0x0008
|
||||
ENABLE_LVB_GRID_WORLDWIDE* = 0x0010
|
||||
|
||||
proc readConsoleInput*(hConsoleInput: Handle, lpBuffer: pointer, nLength: cint,
|
||||
lpNumberOfEventsRead: ptr cint): cint
|
||||
{.stdcall, dynlib: "kernel32", importc: "ReadConsoleInputW".}
|
||||
|
||||
proc getConsoleMode*(hConsoleHandle: Handle, dwMode: ptr DWORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "GetConsoleMode".}
|
||||
|
||||
proc setConsoleMode*(hConsoleHandle: Handle, dwMode: DWORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "SetConsoleMode".}
|
||||
|
||||
proc setConsoleCursorPosition*(hConsoleOutput: Handle,
|
||||
dwCursorPosition: COORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "SetConsoleCursorPosition".}
|
||||
|
||||
proc fillConsoleOutputCharacter*(hConsoleOutput: Handle, cCharacter: char,
|
||||
nLength: DWORD, dwWriteCoord: COORD,
|
||||
lpNumberOfCharsWritten: ptr DWORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "FillConsoleOutputCharacterA".}
|
||||
|
||||
proc fillConsoleOutputAttribute*(hConsoleOutput: Handle, wAttribute: int16,
|
||||
nLength: DWORD, dwWriteCoord: COORD,
|
||||
lpNumberOfAttrsWritten: ptr DWORD): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "FillConsoleOutputAttribute".}
|
||||
|
||||
proc setConsoleTextAttribute*(hConsoleOutput: Handle,
|
||||
wAttributes: int16): WINBOOL{.
|
||||
stdcall, dynlib: "kernel32", importc: "SetConsoleTextAttribute".}
|
||||
|
||||
type
|
||||
LPFIBER_START_ROUTINE* = proc (param: pointer) {.stdcall.}
|
||||
|
||||
|
||||
@@ -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)
|
||||
|
||||
@@ -528,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
|
||||
|
||||
@@ -559,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)
|
||||
|
||||
23
tests/arc/t26010.nim
Normal file
23
tests/arc/t26010.nim
Normal file
@@ -0,0 +1,23 @@
|
||||
discard """
|
||||
action: reject
|
||||
matrix: "--mm:orc; --mm:refc"
|
||||
errormsg: "cannot move cursor 'a'; a cursor does not own its value"
|
||||
"""
|
||||
|
||||
# bug #26010: a cursor is a non-owning alias and cannot transfer ownership.
|
||||
|
||||
type Xxx = object
|
||||
|
||||
proc `=destroy`(v: var Xxx) =
|
||||
debugEcho "dest"
|
||||
|
||||
proc test(v: ref Xxx) =
|
||||
var a {.cursor.} = v
|
||||
var b = move(a)
|
||||
discard
|
||||
|
||||
proc main() =
|
||||
var x = new Xxx
|
||||
test(x)
|
||||
|
||||
main()
|
||||
71
tests/arc/tconcurrentdecref.nim
Normal file
71
tests/arc/tconcurrentdecref.nim
Normal file
@@ -0,0 +1,71 @@
|
||||
discard """
|
||||
matrix: "--mm:atomicArc --threads:on"
|
||||
output: "ok"
|
||||
"""
|
||||
|
||||
# Every thread here holds its OWN counted reference to the same cell and drops
|
||||
# it concurrently with the others. Exactly one free per object must happen: a
|
||||
# leak (nobody frees) and a double free (two threads free) are both caught.
|
||||
#
|
||||
# This is the shape that went wrong in nim-lang/threading#45, where the
|
||||
# destructor decided who frees from a separate load and discarded the result
|
||||
# of the read-modify-write, so the role could be dropped by every participant
|
||||
# at once. `nimDecRefIsLast` must always decide on the value its own RMW
|
||||
# returned. The uniquely-referenced fast path added on top of it may only
|
||||
# skip the RMW when the load proves no other thread holds a reference.
|
||||
|
||||
import std/atomics
|
||||
|
||||
type
|
||||
Payload = object
|
||||
id: int
|
||||
Obj = ref Payload
|
||||
|
||||
var freeCount: Atomic[int]
|
||||
|
||||
proc `=destroy`(p: Payload) =
|
||||
discard freeCount.fetchAdd(1, moRelease)
|
||||
|
||||
const
|
||||
NumObjects = 2000
|
||||
NumThreads = 6
|
||||
Rounds = 3
|
||||
|
||||
type
|
||||
Arg = object
|
||||
refs: seq[Obj]
|
||||
|
||||
var
|
||||
go: Atomic[bool]
|
||||
threads: array[NumThreads, Thread[ptr Arg]]
|
||||
args: array[NumThreads, Arg]
|
||||
|
||||
proc worker(a: ptr Arg) {.thread.} =
|
||||
while not go.load(moAcquire): cpuRelax()
|
||||
a.refs.setLen(0) # drop them all, as fast as possible
|
||||
|
||||
proc main =
|
||||
var expected = 0
|
||||
for round in 1..Rounds:
|
||||
var mine = newSeq[Obj](NumObjects)
|
||||
for i in 0 ..< NumObjects:
|
||||
mine[i] = Obj(id: i)
|
||||
for t in 0 ..< NumThreads:
|
||||
args[t].refs = newSeq[Obj](NumObjects)
|
||||
for i in 0 ..< NumObjects:
|
||||
args[t].refs[i] = mine[i] # counted copy
|
||||
go.store(false, moRelease)
|
||||
for t in 0 ..< NumThreads:
|
||||
createThread(threads[t], worker, addr args[t])
|
||||
go.store(true, moRelease) # everybody drops at once...
|
||||
mine.setLen(0) # ...including this thread
|
||||
joinThreads(threads)
|
||||
expected += NumObjects
|
||||
let got = freeCount.load(moAcquire)
|
||||
if got != expected:
|
||||
echo "round ", round, ": got ", got, " frees, expected ", expected,
|
||||
(if got < expected: " (leak)" else: " (double free)")
|
||||
quit 1
|
||||
echo "ok"
|
||||
|
||||
main()
|
||||
@@ -65,3 +65,17 @@ method handleConn*(myParam: PubSub,
|
||||
proto: string) {.base, async.} =
|
||||
myParam.peers.withValue(conn.peerInfo.peerId, peer):
|
||||
let peerB = peer[]
|
||||
|
||||
|
||||
|
||||
block:
|
||||
type M = object
|
||||
|
||||
proc `=dup`(_: M): M {.error.}
|
||||
proc take(_: sink M) = discard
|
||||
|
||||
proc test() =
|
||||
var value: M
|
||||
take(value)
|
||||
|
||||
test()
|
||||
|
||||
52
tests/async/t23615.nim
Normal file
52
tests/async/t23615.nim
Normal file
@@ -0,0 +1,52 @@
|
||||
discard """
|
||||
valgrind: true
|
||||
cmd: '''nim c --mm:orc -d:nimAllocStats -d:useMalloc $file'''
|
||||
output: '''ok'''
|
||||
"""
|
||||
|
||||
# bug #23615: exceptions caught by a typed except branch in a closure
|
||||
# iterator (and thus in any async proc) leaked under ARC/ORC.
|
||||
|
||||
import std/[asyncdispatch, importutils]
|
||||
|
||||
privateAccess(AllocStats)
|
||||
|
||||
block: # pure closure iterator, the minimal form of the bug
|
||||
proc runIter() =
|
||||
iterator it(): int {.closure.} =
|
||||
try:
|
||||
yield 1
|
||||
raise newException(ValueError, "x")
|
||||
except ValueError:
|
||||
discard
|
||||
yield 2
|
||||
var f = it
|
||||
doAssert f() == 1
|
||||
doAssert f() == 2
|
||||
let base = getAllocStats()
|
||||
runIter()
|
||||
GC_fullCollect()
|
||||
let after = getAllocStats()
|
||||
doAssert after.allocCount - after.deallocCount ==
|
||||
base.allocCount - base.deallocCount, $base & " " & $after
|
||||
|
||||
block: # the async incarnation from the issue
|
||||
proc err {.async.} =
|
||||
raise newException(ValueError, "err1")
|
||||
|
||||
proc amain {.async.} =
|
||||
await sleepAsync(1)
|
||||
for _ in 0..<50:
|
||||
try:
|
||||
await err()
|
||||
except ValueError:
|
||||
discard
|
||||
|
||||
waitFor amain()
|
||||
doAssert not hasPendingOperations()
|
||||
setGlobalDispatcher(nil)
|
||||
GC_fullCollect()
|
||||
|
||||
let stats = getAllocStats()
|
||||
doAssert stats.allocCount - stats.deallocCount < 10, $stats
|
||||
echo "ok"
|
||||
@@ -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
|
||||
|
||||
32
tests/async/tasyncdispatchordering.nim
Normal file
32
tests/async/tasyncdispatchordering.nim
Normal file
@@ -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
|
||||
113
tests/benchmarks/yrcbech.nim
Normal file
113
tests/benchmarks/yrcbech.nim
Normal file
@@ -0,0 +1,113 @@
|
||||
discard """
|
||||
output: '''true peak memory: true'''
|
||||
cmd: "nim c --mm:orc -d:release --threads:on $file"
|
||||
"""
|
||||
|
||||
## torcbench (tests/arc/torcbench.nim), threaded — plus the smallest changes
|
||||
## that let the generational scheme show up in the number.
|
||||
##
|
||||
## Each thread runs its own private copy of the torcbench workload: one long
|
||||
## doubly-linked list of strings, and a stream of short-lived cyclic trees
|
||||
## whose every node embeds a copy of the list header — that is a reference
|
||||
## into the list per tree node. Nothing is shared between threads, so the same
|
||||
## program is a fair measurement under --mm:orc and --mm:yrc.
|
||||
##
|
||||
## Two changes vs torcbench, each needed to make the young -> old pattern
|
||||
## measurable rather than incidental:
|
||||
##
|
||||
## 1. The list is built once per THREAD, not once per outer iteration, so it
|
||||
## survives long enough to be promoted. It is the old generation; the trees
|
||||
## are the young one.
|
||||
## 2. Collection runs at a fixed cadence (GC_partialCollect per outer
|
||||
## iteration) instead of being left to each collector's threshold
|
||||
## heuristic. Without this the benchmark measures how often each collector
|
||||
## decides to collect rather than what a collection over this heap costs —
|
||||
## and ORC's threshold scales with heap size, so a bigger list makes it
|
||||
## collect LESS and the re-trace it is supposed to be paying never appears.
|
||||
##
|
||||
## Nothing seeds the promotion: the tree stream itself is what ages the list,
|
||||
## which is why the workload can stay an ordinary one. `DoublyLinkedNode.prev`
|
||||
## and `DoublyLinkedList.tail` are `{.cursor.}`, so copying a `parent` header
|
||||
## incRefs `head` alone, and the list is a chain of one-node SCCs rather than
|
||||
## a single big one. Dirtiness is per-SCC, so the churn only ever dirties
|
||||
## `head`; every node behind it is traced clean by the collections the trees
|
||||
## trigger anyway and promotes after YrcPromoteAge of them. The capture then
|
||||
## prunes one edge in — at `head.next` — instead of walking 60000 nodes.
|
||||
##
|
||||
## --mm:orc every collection follows `parent` into the list and re-traces
|
||||
## all ListLen nodes of it.
|
||||
## --mm:yrc once the list is promoted, capture prunes at the epoch-stamp
|
||||
## boundary and walks only the young frontier.
|
||||
##
|
||||
## Sizing matters: the win is the ratio of old-generation size to young work
|
||||
## per collection, so ListLen is large and TreeIters small. Total young work
|
||||
## is about the same as torcbench's (200x51 trees vs 25x401). NumThreads=4 is
|
||||
## the default because 8 threads on a 4-performance-core machine dilutes the
|
||||
## result (1.15x vs 1.69x measured on an M1).
|
||||
##
|
||||
## nim c -r --mm:orc -d:release --threads:on yrcbech.nim
|
||||
## nim c -r --mm:yrc -d:release --threads:on yrcbech.nim
|
||||
##
|
||||
## Add -d:yrcBenchTime for a wall-clock line, -d:nimOrcStats for capture and
|
||||
## prune counts (YRC only).
|
||||
|
||||
import std/[lists, monotimes, times]
|
||||
|
||||
const
|
||||
NumThreads {.intdefine.} = 4
|
||||
OuterIters {.intdefine.} = 200 ## per thread; also the collection count
|
||||
ListLen {.intdefine.} = 60000 ## the old generation
|
||||
TreeIters {.intdefine.} = 50 ## young trees per collection
|
||||
TreeDepth {.intdefine.} = 8
|
||||
|
||||
type
|
||||
Node = ref object
|
||||
parent: DoublyLinkedList[string] ## copy of the header: a ref into the list
|
||||
le, ri: Node
|
||||
self: Node ## self-cycle, forces cycle detection
|
||||
|
||||
proc buildTree(parent: DoublyLinkedList[string]; depth: int): Node =
|
||||
if depth == 0:
|
||||
result = nil
|
||||
elif depth == 1:
|
||||
result = Node(parent: parent)
|
||||
result.self = result
|
||||
else:
|
||||
result = Node(parent: parent,
|
||||
le: buildTree(parent, depth - 1),
|
||||
ri: buildTree(parent, depth - 2))
|
||||
result.self = result
|
||||
|
||||
proc threadWork() {.thread.} =
|
||||
# (1) built once per thread: the old generation
|
||||
var leakList = initDoublyLinkedList[string]()
|
||||
for j in 1 .. ListLen:
|
||||
leakList.append(newString(200))
|
||||
|
||||
for i in 1 .. OuterIters:
|
||||
for k in 0 .. TreeIters:
|
||||
discard buildTree(leakList, TreeDepth) # young: dead the moment it returns
|
||||
GC_partialCollect(0) # (2) fixed cadence
|
||||
|
||||
var threads: array[NumThreads, Thread[void]]
|
||||
|
||||
let t0 = getMonoTime()
|
||||
for i in 0 ..< NumThreads:
|
||||
createThread(threads[i], threadWork)
|
||||
joinThreads(threads)
|
||||
GC_fullCollect()
|
||||
let dtMs = inMilliseconds(getMonoTime() - t0)
|
||||
|
||||
when defined(yrcBenchTime):
|
||||
echo "wall_ms ", dtMs
|
||||
|
||||
when not defined(useMalloc):
|
||||
echo getOccupiedMem() < 10 * 1024 * 1024, " peak memory: ",
|
||||
getMaxMem() < 256 * 1024 * 1024
|
||||
else:
|
||||
echo "true peak memory: true"
|
||||
|
||||
when defined(nimOrcStats) and defined(gcYrc):
|
||||
let s = GC_orcStats()
|
||||
echo "capTotal ", s.capTotal, " capPruned ", s.capPruned,
|
||||
" capRepeat ", s.capRepeat
|
||||
85
tests/ccgbugs/tobjconstr_self_alias.nim
Normal file
85
tests/ccgbugs/tobjconstr_self_alias.nim
Normal file
@@ -0,0 +1,85 @@
|
||||
discard """
|
||||
matrix: "--mm:refc; --mm:arc; --mm:orc"
|
||||
output: '''42
|
||||
55
|
||||
42
|
||||
42
|
||||
42
|
||||
42'''
|
||||
"""
|
||||
|
||||
# bug #25993 : an object constructor assigned to a location zeroed the
|
||||
# destination before evaluating a field value that reads from inside that same
|
||||
# destination, so `tp.h = H(a: tp.h.a)` produced `a == 0`.
|
||||
|
||||
type
|
||||
Inner = object
|
||||
a: int
|
||||
b: int
|
||||
Mid = object
|
||||
inner: Inner
|
||||
x: int
|
||||
RefT = ref object
|
||||
h: Inner
|
||||
other: Inner
|
||||
m: Mid
|
||||
|
||||
# --------------------------------------------------------------------------
|
||||
# bug demonstrations: each printed 0 before the fix
|
||||
# --------------------------------------------------------------------------
|
||||
|
||||
proc refDotField(v: int) =
|
||||
# dest `t.h` is a field of a ref; value reads `t.h.a` (nested in dest)
|
||||
let t = RefT()
|
||||
t.h.a = v
|
||||
t.h = Inner(a: t.h.a)
|
||||
echo t.h.a
|
||||
|
||||
proc nestedConstr(v: int) =
|
||||
# dest `t.m`; nested constructor value reads `t.m.inner.a` (nested in dest)
|
||||
let t = RefT()
|
||||
t.m.inner.a = v
|
||||
t.m = Mid(inner: Inner(a: t.m.inner.a), x: 0)
|
||||
echo t.m.inner.a
|
||||
|
||||
proc refDeepField(v: int) =
|
||||
# dest `t.m.inner`; value reads `t.m.inner.a` (nested in dest)
|
||||
let t = RefT()
|
||||
t.m.inner.a = v
|
||||
t.m.inner = Inner(a: t.m.inner.a)
|
||||
echo t.m.inner.a
|
||||
|
||||
var gT: RefT
|
||||
|
||||
proc readsField(t: RefT): int = t.h.a
|
||||
|
||||
proc viaCall(v: int) =
|
||||
# read of dest hidden behind a call whose argument is the root ref
|
||||
let t = RefT()
|
||||
t.h.a = v
|
||||
t.h = Inner(a: readsField(t))
|
||||
echo t.h.a
|
||||
|
||||
proc viaClosureGlobal(v: int) =
|
||||
# read of dest hidden behind a closure reaching it through a global
|
||||
let t = RefT()
|
||||
t.h.a = v
|
||||
gT = t
|
||||
let cl = proc(): int = gT.h.a
|
||||
t.h = Inner(a: cl())
|
||||
echo t.h.a
|
||||
|
||||
proc viaClosureCapture(v: int) =
|
||||
# read of dest hidden behind a closure that captures the root ref
|
||||
let t = RefT()
|
||||
t.h.a = v
|
||||
let cl = proc(): int = t.h.a
|
||||
t.h = Inner(a: cl())
|
||||
echo t.h.a
|
||||
|
||||
refDotField(42)
|
||||
nestedConstr(55)
|
||||
refDeepField(42)
|
||||
viaCall(42)
|
||||
viaClosureGlobal(42)
|
||||
viaClosureCapture(42)
|
||||
39
tests/set/tset_range_trait.nim
Normal file
39
tests/set/tset_range_trait.nim
Normal file
@@ -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])
|
||||
@@ -457,3 +457,20 @@ block: # bug #22600
|
||||
|
||||
var x: c[2]
|
||||
x.init()
|
||||
|
||||
block:
|
||||
# bug #25938
|
||||
|
||||
proc p(h: static set[bool] = {}) =
|
||||
discard false in h
|
||||
|
||||
p()
|
||||
p({})
|
||||
|
||||
block:
|
||||
# bug #25942
|
||||
|
||||
proc p(h: static set[bool]) = discard len(h)
|
||||
p({})
|
||||
|
||||
|
||||
|
||||
@@ -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)
|
||||
|
||||
|
||||
@@ -90,7 +90,8 @@ proc main() =
|
||||
var a0 = "hi"
|
||||
var b0 = "foobar"
|
||||
when nimvm:
|
||||
discard # pending bug #15952
|
||||
a0.add b0.toOpenArray(1,3)
|
||||
doAssert a0 == "hioob"
|
||||
else:
|
||||
a0.add b0.toOpenArray(1,3)
|
||||
doAssert a0 == "hioob"
|
||||
|
||||
@@ -33,6 +33,22 @@ s2[p2] = 45_000
|
||||
s3[p1] = 30_000
|
||||
s3[p2] = 45_000
|
||||
|
||||
block: # two-argument form of withValue forms expression
|
||||
block: # Present
|
||||
let sal = salaries.withValue(p1, sal):
|
||||
sal[]
|
||||
do:
|
||||
0
|
||||
doAssert sal == 30_000
|
||||
block: # Missing
|
||||
let sal = salaries.withValue(Person(), sal):
|
||||
sal[]
|
||||
do:
|
||||
0
|
||||
doAssert sal == 0
|
||||
block: # Short form
|
||||
doAssert salaries.withValue(p1, sal, sal[], 0) == 30_000
|
||||
|
||||
block: # Ordered table should preserve order after deletion
|
||||
var
|
||||
s4 = initOrderedTable[int, int]()
|
||||
|
||||
@@ -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 == """<rss xmlns:atom="http://www.w3.org/2005/Atom">
|
||||
<atom:link data-dummy="test" />
|
||||
</rss>"""
|
||||
|
||||
21
tests/whenstmt/twhen_nimvm_push.nim
Normal file
21
tests/whenstmt/twhen_nimvm_push.nim
Normal file
@@ -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"
|
||||
8
tests/whenstmt/twhen_nimvm_push_pop.nim
Normal file
8
tests/whenstmt/twhen_nimvm_push_pop.nim
Normal file
@@ -0,0 +1,8 @@
|
||||
discard """
|
||||
errormsg: "{.pop.} without a corresponding {.push.}"
|
||||
line: 8
|
||||
"""
|
||||
|
||||
when nimvm:
|
||||
{.push checks: off.}
|
||||
else: {.pop.}
|
||||
178
tests/yrc/tyrc_generational.nim
Normal file
178
tests/yrc/tyrc_generational.nim
Normal file
@@ -0,0 +1,178 @@
|
||||
discard """
|
||||
cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
|
||||
output: "ok"
|
||||
disabled: "windows"
|
||||
disabled: "freebsd"
|
||||
disabled: "openbsd"
|
||||
"""
|
||||
|
||||
# Generational epoch stamps, young -> old.
|
||||
#
|
||||
# Each thread keeps a long-lived cyclic web and promotes it past
|
||||
# YrcPromoteAge with a few seeded partial collects. After that, every
|
||||
# iteration allocates die-young cyclic rings that reference the web -- the
|
||||
# classic new-refers-to-old pattern. Capture then prunes at the stamp
|
||||
# boundary and commit `trialDec`s the young -> web edges WITHOUT re-rooting
|
||||
# the web, so from that point on the web's liveness no longer rests on being
|
||||
# traced: it rests on the deferred machinery (the per-thread suspect buffer
|
||||
# and the pruned-target list) keeping those cells examinable and alive until
|
||||
# the epoch advances.
|
||||
#
|
||||
# Two properties are asserted. The surviving web is walked in full at the
|
||||
# end, so a web that was collected or partially collected out from under the
|
||||
# deferred machinery shows up as a nil edge, a corrupted id or a short node
|
||||
# count. And after every web is dropped, a full collect must reclaim all of
|
||||
# it -- deferring reclamation to the epoch boundary must not turn into never
|
||||
# reclaiming.
|
||||
#
|
||||
# Sized so the shared epoch clock (YrcEpochLen collections) turns over
|
||||
# repeatedly mid-run: the steady-state suspect flush is on the path under
|
||||
# test, not just the one forced by the final GC_fullCollect. Measured on the
|
||||
# current collector this run remembers ~200 suspects across ~80 flushes.
|
||||
#
|
||||
# NOTE: this is a functional test of the generational path, not a regression
|
||||
# test for the dangling-suspect use-after-free that path once had. It was
|
||||
# tried in that role and does not reproduce it: the suspects it creates are
|
||||
# nearly always flushed before they die, so the bad ordering never comes up.
|
||||
# tests/async/tasyncawait.nim reproduces that one reliably.
|
||||
|
||||
const
|
||||
NumThreads = 4
|
||||
WebSize = 8_000 ## the web that survives to the integrity check
|
||||
DoomedSize = 800 ## promoted, given young -> old edges, then dropped
|
||||
WebDegree = 4
|
||||
SeedProbes = 6 ## must exceed YrcPromoteAge (3) to promote a web
|
||||
OuterIters = 40 ## with NumThreads, enough collections to cross epochs
|
||||
YoungBatches = 8
|
||||
YoungRing = 100
|
||||
|
||||
type
|
||||
WebNode = ref object
|
||||
id: int32
|
||||
seen: int32 ## walk marker, plain data: no GC interaction
|
||||
edges: array[WebDegree, WebNode]
|
||||
|
||||
Bridge = ref object
|
||||
toWeb: WebNode
|
||||
self: Bridge
|
||||
|
||||
YoungNode = ref object
|
||||
next: YoungNode
|
||||
hub: WebNode ## the young -> old edge under test
|
||||
self: YoungNode
|
||||
|
||||
var probeSlot {.threadvar.}: Bridge
|
||||
|
||||
proc buildWebNodes(n: int): seq[WebNode] =
|
||||
## Strongly connected mesh: one incoming edge pulls the whole web into any
|
||||
## collector that does not prune at the stamp boundary.
|
||||
result = newSeq[WebNode](n)
|
||||
for i in 0 ..< n:
|
||||
result[i] = WebNode(id: int32(i))
|
||||
for i in 0 ..< n:
|
||||
for d in 0 ..< WebDegree:
|
||||
result[i].edges[d] = result[(i + 1 + d * 97) mod n]
|
||||
|
||||
proc buildWeb(n: int): WebNode = buildWebNodes(n)[0]
|
||||
|
||||
proc checkWeb(root: WebNode; n: int) =
|
||||
## Every node reachable exactly once, every edge intact. A web that was
|
||||
## collected out from under us fails here instead of faulting later.
|
||||
var stack = @[root]
|
||||
root.seen = 1
|
||||
var count = 0
|
||||
while stack.len > 0:
|
||||
let x = stack.pop()
|
||||
inc count
|
||||
doAssert x.id >= 0'i32 and x.id < int32(n), "web node corrupted: id " & $x.id
|
||||
for d in 0 ..< WebDegree:
|
||||
let e = x.edges[d]
|
||||
doAssert e != nil, "web edge nil'ed at node " & $x.id
|
||||
if e.seen != 1:
|
||||
e.seen = 1
|
||||
stack.add e
|
||||
doAssert count == n, "web lost nodes: " & $count & " of " & $n
|
||||
|
||||
proc paintYoung(hub: WebNode; n: int) =
|
||||
## Ring of `n` self-referential nodes, each pointing at the web. When the
|
||||
## seq drops, the ring is garbage whose only external edges go into the
|
||||
## live (and by now stamp-pruned) web.
|
||||
var nodes = newSeq[YoungNode](n)
|
||||
for i in 0 ..< n:
|
||||
nodes[i] = YoungNode(hub: hub)
|
||||
for i in 0 ..< n:
|
||||
nodes[i].next = nodes[(i + 1) mod n]
|
||||
nodes[i].self = nodes[i]
|
||||
|
||||
proc paintYoungSpread(web: seq[WebNode]; n: int) =
|
||||
## Same, but every young node targets a DIFFERENT old cell, so the commit
|
||||
## deposits many distinct cells in the suspect buffer instead of just the
|
||||
## web root. Breadth here is what makes the "suspect dies before the epoch
|
||||
## flush" ordering likely rather than incidental.
|
||||
var nodes = newSeq[YoungNode](n)
|
||||
for i in 0 ..< n:
|
||||
nodes[i] = YoungNode(hub: web[(i * 7) mod web.len])
|
||||
for i in 0 ..< n:
|
||||
nodes[i].next = nodes[(i + 1) mod n]
|
||||
nodes[i].self = nodes[i]
|
||||
|
||||
proc probeBridge(b: Bridge) {.noinline.} =
|
||||
## Seeded false alarm so a partial collect traces -- and stamps -- the web.
|
||||
## The threadvar slot is deliberate: a stack temporary is not a reliable
|
||||
## way to get the bridge registered as a candidate root.
|
||||
probeSlot = b
|
||||
probeSlot = nil
|
||||
|
||||
proc promote(b: Bridge) =
|
||||
## Trace-and-stamp the bridge's web often enough that its cells pass
|
||||
## YrcPromoteAge and captures start pruning at them.
|
||||
for _ in 1 .. SeedProbes:
|
||||
probeBridge(b)
|
||||
# Deliberately not GC_fullCollect: that advances the epoch and wipes the
|
||||
# stamps this test needs.
|
||||
GC_partialCollect(0)
|
||||
|
||||
proc cycleDoomedWeb() =
|
||||
## Promote a web, hand it young -> old edges so its cells land in the
|
||||
## deferred suspect buffer, then drop it. Those cells are now garbage
|
||||
## while still listed, and an ordinary collection reclaims them well
|
||||
## before the epoch advance that flushes the buffer. THIS is the case a
|
||||
## live-forever web never produces: the list has to not be holding
|
||||
## pointers to cells anyone else was free to reclaim.
|
||||
let doomedNodes = buildWebNodes(DoomedSize)
|
||||
let b = Bridge(toWeb: doomedNodes[0])
|
||||
b.self = b
|
||||
promote(b)
|
||||
for _ in 1 .. YoungBatches:
|
||||
paintYoungSpread(doomedNodes, YoungRing)
|
||||
GC_partialCollect(0)
|
||||
# `doomedNodes` and `b` die with this scope: every cell that just landed
|
||||
# in the suspect buffer is now garbage while still listed there.
|
||||
|
||||
proc threadWork() {.thread.} =
|
||||
let web = buildWeb(WebSize)
|
||||
let bridge = Bridge(toWeb: web)
|
||||
bridge.self = bridge
|
||||
promote(bridge)
|
||||
|
||||
for i in 1 .. OuterIters:
|
||||
cycleDoomedWeb()
|
||||
for _ in 1 .. YoungBatches:
|
||||
paintYoung(web, YoungRing)
|
||||
GC_partialCollect(0)
|
||||
|
||||
checkWeb(web, WebSize)
|
||||
doAssert bridge.toWeb == web, "bridge lost its web"
|
||||
|
||||
var threads: array[NumThreads, Thread[void]]
|
||||
for i in 0 ..< NumThreads:
|
||||
createThread(threads[i], threadWork)
|
||||
joinThreads(threads)
|
||||
|
||||
# Every web is unreachable now. The full collect advances the epoch, which
|
||||
# flushes the suspect buffers into the root set -- the major-collection half
|
||||
# of the scheme -- so all of it must come back.
|
||||
GC_fullCollect()
|
||||
doAssert getOccupiedMem() < 8 * 1024 * 1024,
|
||||
"webs not reclaimed: " & $(getOccupiedMem() div 1024) & " KiB still occupied"
|
||||
echo "ok"
|
||||
Reference in New Issue
Block a user