mirrors/Nim
1
0
Fork 0
mirror of https://github.com/nim-lang/Nim.git synced 2026-08-24 15:41:43 +00:00
Code Issues Packages Projects Releases Wiki Activity

YRC improvements: wip

Browse Source
This commit is contained in:
Araq
2026-02-21 07:16:01 +01:00
parent 1e3caf457b
commit 08c31ad247
6 changed files with 443 additions and 78 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
lib/system.nim
View File

@@ -627,7 +627,7 @@ proc newSeq*[T](s: var seq[T], len: Natural) {.magic: "NewSeq", noSideEffect.}
## #inputStrings[3] = "out of bounds"
## ```
proc newSeq*[T](len = 0.Natural): seq[T] =
proc newSeq*[T](len = 0.Natural): seq[T] {.noSideEffect.} =
## Creates a new sequence of type `seq[T]` with length `len`.
##
## Note that the sequence will be filled with zeroed entries.

121
lib/system/rwlocks.nim Normal file
View File

@@ -0,0 +1,121 @@
#
#
# Nim's Runtime Library
# (c) Copyright 2026 Andreas Rumpf
#
# See the file "copying.txt", included in this
# distribution, for details about the copyright.
#
# Read-write lock (RwLock) for lib/system.
# Used by YRC and by traceable containers that perform topology-changing ops.
# POSIX: pthread_rwlock_* ; Windows: SRWLOCK (slim reader/writer).
{.push stackTrace: off.}
when defined(windows):
# SRWLOCK is pointer-sized; use single pointer for ABI compatibility
type
RwLock* {.importc: "SRWLOCK", header: "<synchapi.h>", final, pure, byref.} = object
p: pointer
proc initializeSRWLock(L: var RwLock) {.importc: "InitializeSRWLock",
header: "<synchapi.h>".}
proc acquireSRWLockShared(L: var RwLock) {.importc: "AcquireSRWLockShared",
header: "<synchapi.h>".}
proc releaseSRWLockShared(L: var RwLock) {.importc: "ReleaseSRWLockShared",
header: "<synchapi.h>".}
proc acquireSRWLockExclusive(L: var RwLock) {.importc: "AcquireSRWLockExclusive",
header: "<synchapi.h>".}
proc releaseSRWLockExclusive(L: var RwLock) {.importc: "ReleaseSRWLockExclusive",
header: "<synchapi.h>".}
proc initRwLock*(L: var RwLock) {.inline.} =
initializeSRWLock(L)
proc deinitRwLock*(L: var RwLock) {.inline.} =
discard
proc acquireRead*(L: var RwLock) {.inline.} =
acquireSRWLockShared(L)
proc releaseRead*(L: var RwLock) {.inline.} =
releaseSRWLockShared(L)
proc acquireWrite*(L: var RwLock) {.inline.} =
acquireSRWLockExclusive(L)
proc releaseWrite*(L: var RwLock) {.inline.} =
releaseSRWLockExclusive(L)
elif defined(genode):
{.error: "RwLock is not implemented for Genode".}
else:
# POSIX: pthread_rwlock_*
type
SysRwLockObj {.importc: "pthread_rwlock_t", pure, final,
header: """#include <sys/types.h>
#include <pthread.h>""", byref.} = object
when defined(linux) and defined(amd64):
abi: array[56 div sizeof(clong), clong]
proc pthread_rwlock_init(rwlock: var SysRwLockObj, attr: pointer): cint {.
importc: "pthread_rwlock_init", header: "<pthread.h>", noSideEffect.}
proc pthread_rwlock_destroy(rwlock: var SysRwLockObj): cint {.
importc: "pthread_rwlock_destroy", header: "<pthread.h>", noSideEffect.}
proc pthread_rwlock_rdlock(rwlock: var SysRwLockObj): cint {.
importc: "pthread_rwlock_rdlock", header: "<pthread.h>", noSideEffect.}
proc pthread_rwlock_wrlock(rwlock: var SysRwLockObj): cint {.
importc: "pthread_rwlock_wrlock", header: "<pthread.h>", noSideEffect.}
proc pthread_rwlock_unlock(rwlock: var SysRwLockObj): cint {.
importc: "pthread_rwlock_unlock", header: "<pthread.h>", noSideEffect.}
when defined(ios):
type RwLock* = ptr SysRwLockObj
proc initRwLock*(L: var RwLock) =
when not declared(c_malloc):
proc c_malloc(size: csize_t): pointer {.importc: "malloc", header: "<stdlib.h>".}
proc c_free(p: pointer) {.importc: "free", header: "<stdlib.h>".}
L = cast[RwLock](c_malloc(csize_t(sizeof(SysRwLockObj))))
discard pthread_rwlock_init(L[], nil)
proc deinitRwLock*(L: var RwLock) =
if L != nil:
discard pthread_rwlock_destroy(L[])
when not declared(c_free):
proc c_free(p: pointer) {.importc: "free", header: "<stdlib.h>".}
c_free(L)
L = nil
proc acquireRead*(L: var RwLock) =
discard pthread_rwlock_rdlock(L[])
proc releaseRead*(L: var RwLock) =
discard pthread_rwlock_unlock(L[])
proc acquireWrite*(L: var RwLock) =
discard pthread_rwlock_wrlock(L[])
proc releaseWrite*(L: var RwLock) =
discard pthread_rwlock_unlock(L[])
else:
type RwLock* = SysRwLockObj
proc initRwLock*(L: var RwLock) =
discard pthread_rwlock_init(L, nil)
proc deinitRwLock*(L: var RwLock) =
discard pthread_rwlock_destroy(L)
proc acquireRead*(L: var RwLock) =
discard pthread_rwlock_rdlock(L)
proc releaseRead*(L: var RwLock) =
discard pthread_rwlock_unlock(L)
proc acquireWrite*(L: var RwLock) =
discard pthread_rwlock_wrlock(L)
proc releaseWrite*(L: var RwLock) =
discard pthread_rwlock_unlock(L)
template withReadLock*(L: var RwLock, body: untyped) =
acquireRead(L)
try:
body
finally:
releaseRead(L)
template withWriteLock*(L: var RwLock, body: untyped) =
acquireWrite(L)
try:
body
finally:
releaseWrite(L)
{.pop.}

136
lib/system/seqs_v2.nim
View File

@@ -11,6 +11,55 @@
# import std/typetraits
# strs already imported allocateds for us.
when defined(gcYrc):
include rwlocks
type
YrcLockState = enum
HasNoLock
HasMutatorLock
HasCollectorLock
Collecting
var
gYrcGlobalLock: RWLock
var
lockState {.threadvar.}: YrcLockState
proc acquireMutatorLock() {.compilerRtl, inl.} =
acquireRead gYrcGlobalLock
lockState = HasMutatorLock
proc releaseMutatorLock() {.compilerRtl, inl.} =
if lockState == HasMutatorLock:
lockState = HasNoLock
releaseRead gYrcGlobalLock
template yrcMutatorLock*(body: untyped) =
{.noSideEffect.}:
acquireMutatorLock()
try:
body
finally:
{.noSideEffect.}:
releaseMutatorLock()
template yrcCollectorLock(body: untyped) =
if lockState == HasMutatorLock: releaseMutatorLock()
let hadToAcquire = lockState < HasCollectorLock
if hadToAcquire:
acquireWrite(gYrcGlobalLock)
lockState = HasCollectorLock
try:
body
finally:
if hadToAcquire:
releaseWrite(gYrcGlobalLock)
lockState = HasNoLock
else:
template yrcMutatorLock*(body: untyped) =
body
# Some optimizations here may be not to empty-seq-initialize some symbols, then StrictNotNil complains.
{.push warning[StrictNotNil]: off.} # See https://github.com/nim-lang/Nim/issues/21401
@@ -116,33 +165,35 @@ proc prepareSeqAddUninit(len: int; p: pointer; addlen, elemSize, elemAlign: int)
q.cap = newCap
result = q
proc shrink*[T](x: var seq[T]; newLen: Natural) {.tags: [], raises: [].} =
proc shrink*[T](x: var seq[T]; newLen: Natural) {.tags: [], raises: [], noSideEffect.} =
when nimvm:
{.cast(tags: []).}:
setLen(x, newLen)
else:
#sysAssert newLen <= x.len, "invalid newLen parameter for 'shrink'"
when not supportsCopyMem(T):
for i in countdown(x.len - 1, newLen):
reset x[i]
# XXX This is wrong for const seqs that were moved into 'x'!
{.noSideEffect.}:
cast[ptr NimSeqV2[T]](addr x).len = newLen
yrcMutatorLock:
when not supportsCopyMem(T):
for i in countdown(x.len - 1, newLen):
reset x[i]
# XXX This is wrong for const seqs that were moved into 'x'!
{.noSideEffect.}:
cast[ptr NimSeqV2[T]](addr x).len = newLen
proc grow*[T](x: var seq[T]; newLen: Natural; value: T) {.nodestroy.} =
let oldLen = x.len
#sysAssert newLen >= x.len, "invalid newLen parameter for 'grow'"
if newLen <= oldLen: return
var xu = cast[ptr NimSeqV2[T]](addr x)
if xu.p == nil or (xu.p.cap and not strlitFlag) < newLen:
xu.p = cast[typeof(xu.p)](prepareSeqAddUninit(oldLen, xu.p, newLen - oldLen, sizeof(T), alignof(T)))
xu.len = newLen
for i in oldLen .. newLen-1:
when (NimMajor, NimMinor, NimPatch) >= (2, 3, 1):
xu.p.data[i] = `=dup`(value)
else:
wasMoved(xu.p.data[i])
`=copy`(xu.p.data[i], value)
yrcMutatorLock:
var xu = cast[ptr NimSeqV2[T]](addr x)
if xu.p == nil or (xu.p.cap and not strlitFlag) < newLen:
xu.p = cast[typeof(xu.p)](prepareSeqAddUninit(oldLen, xu.p, newLen - oldLen, sizeof(T), alignof(T)))
xu.len = newLen
for i in oldLen .. newLen-1:
when (NimMajor, NimMinor, NimPatch) >= (2, 3, 1):
xu.p.data[i] = `=dup`(value)
else:
wasMoved(xu.p.data[i])
`=copy`(xu.p.data[i], value)
proc add*[T](x: var seq[T]; y: sink T) {.magic: "AppendSeqElem", noSideEffect, nodestroy.} =
## Generic proc for adding a data item `y` to a container `x`.
@@ -152,30 +203,32 @@ proc add*[T](x: var seq[T]; y: sink T) {.magic: "AppendSeqElem", noSideEffect, n
## Generic code becomes much easier to write if the Nim naming scheme is
## respected.
{.cast(noSideEffect).}:
let oldLen = x.len
var xu = cast[ptr NimSeqV2[T]](addr x)
if xu.p == nil or (xu.p.cap and not strlitFlag) < oldLen+1:
xu.p = cast[typeof(xu.p)](prepareSeqAddUninit(oldLen, xu.p, 1, sizeof(T), alignof(T)))
xu.len = oldLen+1
# .nodestroy means `xu.p.data[oldLen] = value` is compiled into a
# copyMem(). This is fine as know by construction that
# in `xu.p.data[oldLen]` there is nothing to destroy.
# We also save the `wasMoved + destroy` pair for the sink parameter.
xu.p.data[oldLen] = y
yrcMutatorLock:
let oldLen = x.len
var xu = cast[ptr NimSeqV2[T]](addr x)
if xu.p == nil or (xu.p.cap and not strlitFlag) < oldLen+1:
xu.p = cast[typeof(xu.p)](prepareSeqAddUninit(oldLen, xu.p, 1, sizeof(T), alignof(T)))
xu.len = oldLen+1
# .nodestroy means `xu.p.data[oldLen] = value` is compiled into a
# copyMem(). This is fine as know by construction that
# in `xu.p.data[oldLen]` there is nothing to destroy.
# We also save the `wasMoved + destroy` pair for the sink parameter.
xu.p.data[oldLen] = y
proc setLen[T](s: var seq[T], newlen: Natural) {.nodestroy.} =
{.noSideEffect.}:
if newlen < s.len:
shrink(s, newlen)
else:
let oldLen = s.len
if newlen <= oldLen: return
var xu = cast[ptr NimSeqV2[T]](addr s)
if xu.p == nil or (xu.p.cap and not strlitFlag) < newlen:
xu.p = cast[typeof(xu.p)](prepareSeqAddUninit(oldLen, xu.p, newlen - oldLen, sizeof(T), alignof(T)))
xu.len = newlen
for i in oldLen..<newlen:
xu.p.data[i] = default(T)
yrcMutatorLock:
let oldLen = s.len
if newlen <= oldLen: return
var xu = cast[ptr NimSeqV2[T]](addr s)
if xu.p == nil or (xu.p.cap and not strlitFlag) < newlen:
xu.p = cast[typeof(xu.p)](prepareSeqAddUninit(oldLen, xu.p, newlen - oldLen, sizeof(T), alignof(T)))
xu.len = newlen
for i in oldLen..<newlen:
xu.p.data[i] = default(T)
proc newSeq[T](s: var seq[T], len: Natural) =
shrink(s, 0)
@@ -214,11 +267,12 @@ func setLenUninit[T](s: var seq[T], newlen: Natural) {.nodestroy.} =
if newlen < s.len:
shrink(s, newlen)
else:
let oldLen = s.len
if newlen <= oldLen: return
var xu = cast[ptr NimSeqV2[T]](addr s)
if xu.p == nil or (xu.p.cap and not strlitFlag) < newlen:
xu.p = cast[typeof(xu.p)](prepareSeqAddUninit(oldLen, xu.p, newlen - oldLen, sizeof(T), alignof(T)))
xu.len = newlen
yrcMutatorLock:
let oldLen = s.len
if newlen <= oldLen: return
var xu = cast[ptr NimSeqV2[T]](addr s)
if xu.p == nil or (xu.p.cap and not strlitFlag) < newlen:
xu.p = cast[typeof(xu.p)](prepareSeqAddUninit(oldLen, xu.p, newlen - oldLen, sizeof(T), alignof(T)))
xu.len = newlen
{.pop.} # See https://github.com/nim-lang/Nim/issues/21401

9
lib/system/seqs_v2_reimpl.nim
View File

@@ -18,7 +18,8 @@ type
template frees(s: NimSeqV2Reimpl) =
if s.p != nil and (s.p.cap and strlitFlag) != strlitFlag:
when compileOption("threads"):
deallocShared(s.p)
else:
dealloc(s.p)
yrcMutatorLock:
when compileOption("threads"):
deallocShared(s.p)
else:
dealloc(s.p)

23
lib/system/yrc.nim
View File

@@ -137,7 +137,6 @@ type
## Invoked while holding the global lock; must not call back into YRC.
var
gYrcGlobalLock: Lock
roots: CellSeq[Cell] # merged roots, used under global lock
stripes: array[NumStripes, Stripe]
rootsThreshold: int = 128
@@ -188,7 +187,7 @@ proc nimIncRefCyclic(p: pointer; cyclic: bool) {.compilerRtl, inl.} =
if slot < QueueSize:
atomicStoreN(addr stripes[s].toInc[slot], h, ATOMIC_RELEASE)
else:
withLock gYrcGlobalLock:
yrcCollectorLock:
h.rc = h.rc +% rcIncrement
for i in 0..<NumStripes:
let len = atomicExchangeN(addr stripes[i].toIncLen, 0, ATOMIC_ACQUIRE)
@@ -206,7 +205,7 @@ proc nimIncRefCyclic(p: pointer; cyclic: bool) {.compilerRtl, inl.} =
else:
overflow = true
if overflow:
withLock gYrcGlobalLock:
yrcCollectorLock:
for i in 0..<NumStripes:
withLock stripes[i].lockInc:
for j in 0..<stripes[i].toIncLen:
@@ -351,6 +350,9 @@ proc collectColor(s: Cell; desc: PNimTypeV2; col: int; j: var GcEnv) =
proc collectCyclesBacon(j: var GcEnv; lowMark: int) =
# YRC defers all destruction to collection time - process ALL roots through Bacon's algorithm
# This is different from ORC which handles immediate garbage (rc == 0) directly
if lockState == Collecting:
return
lockState = Collecting
let last = roots.len -% 1
when logOrc:
for i in countdown(last, lowMark):
@@ -378,9 +380,6 @@ proc collectCyclesBacon(j: var GcEnv; lowMark: int) =
collectColor(s, roots.d[i][1], colToCollect, j)
# Clear roots before freeing to prevent nested collectCycles() from accessing freed cells
when not defined(nimStressOrc):
let oldThreshold = rootsThreshold
rootsThreshold = high(int)
roots.len = 0
# Free all collected objects
@@ -390,8 +389,6 @@ proc collectCyclesBacon(j: var GcEnv; lowMark: int) =
when orcLeakDetector:
writeCell("CYCLIC OBJECT FREED", s, j.toFree.d[i][1])
free(s, j.toFree.d[i][1])
when not defined(nimStressOrc):
rootsThreshold = oldThreshold
j.freed = j.freed +% j.toFree.len
deinit j.toFree
@@ -401,7 +398,7 @@ when defined(nimOrcStats):
proc collectCycles() =
when logOrc:
cfprintf(cstderr, "[collectCycles] begin\n")
withLock gYrcGlobalLock:
yrcCollectorLock:
mergePendingRoots()
if roots.len >= RootsThreshold and mayRunCycleCollect():
var j: GcEnv
@@ -436,7 +433,7 @@ when defined(nimOrcStats):
result = OrcStats(freedCyclicObjects: freedCyclicObjects)
proc GC_runOrc* =
withLock gYrcGlobalLock:
yrcCollectorLock:
mergePendingRoots()
if mayRunCycleCollect():
var j: GcEnv
@@ -455,12 +452,12 @@ proc GC_disableOrc*() =
rootsThreshold = high(int)
proc GC_prepareOrc*(): int {.inline.} =
withLock gYrcGlobalLock:
yrcCollectorLock:
mergePendingRoots()
result = roots.len
proc GC_partialCollect*(limit: int) =
withLock gYrcGlobalLock:
yrcCollectorLock:
mergePendingRoots()
if roots.len > limit and mayRunCycleCollect():
var j: GcEnv
@@ -560,7 +557,7 @@ proc nimMarkCyclic(p: pointer) {.compilerRtl, inl.} =
h.rc = h.rc or maybeCycle
# Initialize locks at module load
initLock(gYrcGlobalLock)
initRwLock(gYrcGlobalLock)
for i in 0..<NumStripes:
when not defined(yrcAtomics):
initLock(stripes[i].lockInc)

230
lib/system/yrc_proof.tla
View File

@@ -42,6 +42,32 @@
\* - Mutator must hold stack ref to modify object (external ref)
\* - scanBlack follows current physical edges (rescues newly written objects)
\* - Only objects unreachable from any stack root are freed
\*
\* ## Seq Payload Race and RWLock Fix
\*
\* Value types like seq[T] (where T can form cycles) have internal heap
\* allocations (data arrays / "payloads") that are freed by value-type
\* hooks (=sink, =destroy), NOT by the cycle collector. This creates a race:
\*
\* 1. Object O has a seq field with payload P containing refs
\* 2. Collector starts tracing O -- reads payload pointer P
\* 3. Mutator does O.seq = newSeq -- frees P (value-type destructor)
\* 4. Collector dereferences P -- use-after-free!
\*
\* Fix: Change the global YRC lock to a read-write lock (RWLock).
\* - Collector acquires the WRITE lock (exclusive access during tracing)
\* - Seq mutations (assign, setLen, add, etc.) acquire the READ lock
\* - Multiple seq mutations can proceed concurrently (read lock is shared)
\* - But seq mutations block while the collector traces (write lock is exclusive)
\*
\* This prevents the race: the mutator cannot free a payload while the
\* collector is tracing it, because acquiring the read lock requires
\* the write lock to be unheld.
\*
\* Deadlock avoidance: If a seq operation triggers collectCycles() via stripe
\* overflow while already holding the read lock, it must NOT attempt to
\* acquire the write lock. Instead, it should drain the overflow buffers
\* without running the full collection cycle.
EXTENDS Naturals, Integers, Sequences, FiniteSets, TLC
@@ -53,10 +79,14 @@ ASSUME IsFiniteSet(Objects)
ASSUME IsFiniteSet(Threads)
ASSUME IsFiniteSet(ObjTypes)
\* Seq payload identifiers (models heap-allocated data arrays of seq[T])
CONSTANTS SeqPayloads
ASSUME IsFiniteSet(SeqPayloads)
\* NULL constant (represents "no thread" for locks)
\* We use a sentinel value that's guaranteed not to be in Threads or Objects
NULL == "NULL" \* String literal that won't conflict with Threads/Objects
ASSUME NULL \notin Threads /\ NULL \notin Objects
ASSUME NULL \notin Threads /\ NULL \notin Objects /\ NULL \notin SeqPayloads
\* Helper functions
\* Note: GetStripeIdx is not used, GetStripe is used instead
@@ -90,15 +120,29 @@ VARIABLES
\* Per-stripe locks
lockInc, \* lockInc[stripe] = thread holding increment lock (or NULL)
lockDec, \* lockDec[stripe] = thread holding decrement lock (or NULL)
\* Global lock
globalLock, \* thread holding global lock (or NULL)
\* Global lock (now the WRITE side of the RWLock)
globalLock, \* thread holding write lock (or NULL)
\* Merged roots array (used during collection)
mergedRoots, \* sequence of (object, type) pairs
\* Collection state
collecting, \* TRUE if collection is in progress
gcEnv, \* GC environment: {touched, edges, rcSum, toFree, ...}
\* Pending operations (for modeling atomicity)
pendingWrites \* set of pending write barrier operations
pendingWrites, \* set of pending write barrier operations
\* --- Seq payload race modeling ---
\* Seq payloads: models the heap-allocated data arrays of seq[T] fields
seqData, \* [Objects -> SeqPayloads \cup {NULL}] -- current payload for obj's seq
payloadAlive, \* [SeqPayloads -> BOOLEAN] -- is this payload's memory valid?
\* RWLock read side: set of threads holding the read lock.
\* Seq mutations (assign, add, setLen, etc.) acquire the read lock.
\* The collector (write lock holder) gets exclusive access.
rwLockReaders, \* SUBSET Threads -- threads currently holding the read lock
\* Collector's in-progress seq trace: the payload pointer read during tracing.
\* Between reading the pointer and accessing the data, the payload could be freed.
collectorPayload \* SeqPayloads \cup {NULL} -- payload being traced by collector
\* Convenience tuple for seq-related variables (used in UNCHANGED clauses)
seqVars == <<seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* Type invariants
TypeOK ==
@@ -117,6 +161,11 @@ TypeOK ==
/\ mergedRoots \in Seq([obj: Objects, desc: ObjTypes])
/\ collecting \in BOOLEAN
/\ pendingWrites \in SUBSET ([thread: Threads, dest: Objects, old: Objects \cup {NULL}, src: Objects \cup {NULL}, phase: {"store", "inc", "dec"}])
\* Seq payload types
/\ seqData \in [Objects -> SeqPayloads \cup {NULL}]
/\ payloadAlive \in [SeqPayloads -> BOOLEAN]
/\ rwLockReaders \in SUBSET Threads
/\ collectorPayload \in SeqPayloads \cup {NULL}
\* Helper: internal reference count (heap-to-heap edges)
InternalRC(obj) ==
@@ -163,7 +212,7 @@ MutatorWriteAtomicStore(thread, destObj, destField, oldVal, newVal, desc) ==
IF x = newVal /\ newVal # NULL
THEN TRUE
ELSE FALSE]]
/\ UNCHANGED <<roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* ============================================================================
\* Phase 2: RC Buffering (if space available)
@@ -193,7 +242,7 @@ WriteBarrier(thread, destObj, destField, oldVal, newVal, desc) ==
/\ toDec' = IF oldVal # NULL /\ toDecLen[stripe] < QueueSize
THEN [toDec EXCEPT ![stripe] = Append(toDec[stripe], [obj |-> oldVal, desc |-> desc])]
ELSE toDec
/\ UNCHANGED <<edges, roots, rc, color, inRoots, mergedRoots, lockInc, lockDec, globalLock, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<edges, roots, rc, color, inRoots, mergedRoots, lockInc, lockDec, globalLock, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* ============================================================================
\* Phase 3: Overflow Handling (separate actions that can block)
@@ -215,7 +264,7 @@ MutatorWriteMergeInc(thread) ==
externalRC == Cardinality({t \in Threads : roots[t][x]})
IN internalRC + externalRC]
/\ globalLock' = NULL \* Release lock after merge
/\ UNCHANGED <<edges, roots, color, inRoots, toDecLen, toDec, lockInc, lockDec, mergedRoots, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<edges, roots, color, inRoots, toDecLen, toDec, lockInc, lockDec, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* Handle decrement overflow: merge ALL buffers when lock is available
\* This calls collectCycles() which merges both increment and decrement buffers
@@ -257,7 +306,7 @@ MutatorWriteMergeDec(thread) ==
/\ toDecLen' = [s \in 0..(NumStripes-1) |-> 0]
/\ toDec' = [s \in 0..(NumStripes-1) |-> <<>>]
/\ globalLock' = NULL \* Lock acquired, merge done, lock released (entire withLock block is atomic)
/\ UNCHANGED <<edges, roots, color, lockInc, lockDec, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<edges, roots, color, lockInc, lockDec, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* ============================================================================
\* Merge Operation: mergePendingRoots
@@ -311,7 +360,7 @@ MergePendingRoots ==
/\ toInc' = [s \in 0..(NumStripes-1) |-> <<>>]
/\ toDecLen' = [s \in 0..(NumStripes-1) |-> 0]
/\ toDec' = [s \in 0..(NumStripes-1) |-> <<>>]
/\ UNCHANGED <<edges, roots, color, lockInc, lockDec, globalLock, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<edges, roots, color, lockInc, lockDec, globalLock, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* ============================================================================
\* Trial Deletion: markGray
@@ -365,7 +414,7 @@ MarkGray(obj, desc) ==
\* For roots, the RC includes external refs which survive trial deletion.
rc' = [x \in Objects |->
IF x \in allReachable THEN rc[x] - internalEdgeCount[x] ELSE rc[x]]
/\ UNCHANGED <<edges, roots, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<edges, roots, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* ============================================================================
\* Scan Phase
@@ -422,7 +471,7 @@ Scan(obj, desc) ==
ELSE \* Mark white (part of closed cycle)
/\ color' = [color EXCEPT ![obj] = colWhite]
/\ UNCHANGED <<rc>>
/\ UNCHANGED <<edges, roots, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<edges, roots, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* ============================================================================
\* Collection Phase: collectColor
@@ -442,7 +491,7 @@ CollectColor(obj, desc, targetColor) ==
edges' = [edges EXCEPT ![obj] = [x \in Objects |->
IF x = obj THEN FALSE ELSE edges[obj][x]]]
/\ color' = [color EXCEPT ![obj] = colBlack] \* Mark as freed
/\ UNCHANGED <<roots, rc, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<roots, rc, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* ============================================================================
\* Collection Cycle: collectCyclesBacon
@@ -454,7 +503,7 @@ StartCollection ==
/\ Len(mergedRoots) >= RootsThreshold
/\ collecting' = TRUE
/\ gcEnv' = [touched |-> 0, edges |-> 0, rcSum |-> 0, toFree |-> {}]
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, pendingWrites>>
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
EndCollection ==
/\ globalLock # NULL
@@ -464,7 +513,7 @@ EndCollection ==
IF x \in {r.obj : r \in mergedRoots} THEN FALSE ELSE inRoots[x]]
/\ mergedRoots' = <<>>
/\ collecting' = FALSE
/\ UNCHANGED <<edges, roots, rc, color, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, gcEnv, pendingWrites>>
/\ UNCHANGED <<edges, roots, rc, color, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* ============================================================================
\* Mutator Actions
@@ -491,7 +540,7 @@ MutatorWrite(thread, destObj, destField, oldVal, newVal, desc) ==
IF incOverflow \/ decOverflow
THEN \* Overflow: atomic store happened, but buffering is deferred
\* Buffers stay full, merge will happen when lock is available (via MutatorWriteMergeInc/Dec)
/\ UNCHANGED <<roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
ELSE \* No overflow: buffer normally
/\ WriteBarrier(thread, destObj, destField, oldVal, newVal, desc)
/\ UNCHANGED <<roots, collecting, pendingWrites>>
@@ -521,16 +570,19 @@ MutatorRootAssign(thread, obj, val) ==
/\ collecting' = collecting
/\ gcEnv' = gcEnv
/\ pendingWrites' = pendingWrites
/\ UNCHANGED seqVars
\* ============================================================================
\* Collector Actions
\* ============================================================================
\* Collector acquires global lock for entire collection cycle
\* Collector acquires write lock (global lock) for entire collection cycle.
\* RWLock semantics: writer can only acquire when no readers hold the read lock.
CollectorAcquireLock(thread) ==
/\ globalLock = NULL
/\ rwLockReaders = {} \* RWLock: no readers allowed when acquiring write lock
/\ globalLock' = thread
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, mergedRoots, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
CollectorMerge ==
/\ globalLock # NULL
@@ -571,7 +623,93 @@ CollectorEnd ==
CollectorReleaseLock(thread) ==
/\ globalLock = thread
/\ globalLock' = NULL
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, mergedRoots, collecting, gcEnv, pendingWrites>>
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
\* ============================================================================
\* Seq Payload Actions (RWLock-protected)
\* ============================================================================
\* These actions model the race between the collector tracing seq payloads
\* and mutators replacing/freeing seq payloads.
\*
\* The collector traces seq payloads in two steps:
\* 1. CollectorStartTraceSeq: reads seqData[obj] (gets payload pointer)
\* 2. CollectorFinishTraceSeq: accesses the payload data
\* Between these steps, a mutator could free the payload (the race).
\*
\* The RWLock prevents this:
\* - Collector holds write lock (globalLock) during tracing
\* - MutatorSeqAssign requires read lock (rwLockReaders)
\* - Read lock requires globalLock = NULL
\* - Therefore MutatorSeqAssign is blocked during collection
\*
\* Note: This models the memory safety aspect of seq tracing.
\* The cycle collection algorithm (MarkGray, Scan, etc.) operates on the
\* logical edge graph. Seq payloads are a physical representation detail
\* that affects memory safety but not GC correctness (which is already
\* covered by the existing Safety property).
\* Mutator acquires read lock for seq mutation.
\* RWLock semantics: read lock can be acquired when no writer holds the write lock.
\* Multiple readers can hold the read lock simultaneously.
MutatorAcquireSeqLock(thread) ==
/\ globalLock = NULL \* RWLock: no writer allowed when acquiring read lock
/\ thread \notin rwLockReaders
/\ rwLockReaders' = rwLockReaders \cup {thread}
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, collectorPayload>>
\* Mutator releases read lock after seq mutation completes.
MutatorReleaseSeqLock(thread) ==
/\ thread \in rwLockReaders
/\ rwLockReaders' = rwLockReaders \ {thread}
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, collectorPayload>>
\* Mutator replaces a seq field's payload (e.g., r.list = newSeq).
\* This frees the old payload and installs a new one.
\* Requires the read lock (RWLock protection against concurrent collection).
\*
\* In the real implementation, this is a value-type assignment (=sink/=copy)
\* that frees the old data array and installs a new one. The old array is freed
\* immediately, NOT deferred to the cycle collector.
MutatorSeqAssign(thread, obj, newPayload) ==
/\ thread \in rwLockReaders \* Must hold read lock
/\ seqData[obj] # NULL \* Object has an existing seq payload
/\ newPayload \in SeqPayloads
/\ ~payloadAlive[newPayload] \* New payload is freshly allocated (not yet alive)
/\ LET oldPayload == seqData[obj]
IN
/\ seqData' = [seqData EXCEPT ![obj] = newPayload]
/\ payloadAlive' = [payloadAlive EXCEPT ![oldPayload] = FALSE,
![newPayload] = TRUE]
\* Note: In a complete model, this would also update edges[obj] to reflect
\* the new seq elements and buffer RC changes (inc new elements, dec old elements).
\* We omit this here to focus on the memory safety property (payload lifetime).
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, rwLockReaders, collectorPayload>>
\* Collector begins tracing an object's seq field.
\* Reads the seqData pointer and stores it in collectorPayload.
\* This is the first step of a two-step trace operation.
\* The collector must hold the write lock (globalLock).
CollectorStartTraceSeq(obj) ==
/\ globalLock # NULL \* Collector holds write lock
/\ collecting = TRUE \* In collection phase
/\ seqData[obj] # NULL \* Object has a seq field
/\ collectorPayload = NULL \* Not already mid-trace
/\ collectorPayload' = seqData[obj]
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders>>
\* Collector finishes tracing an object's seq field.
\* Accesses the payload data via collectorPayload.
\* The payload MUST still be alive (this is checked by SeqPayloadSafety).
\* After accessing the payload, clears collectorPayload.
CollectorFinishTraceSeq ==
/\ globalLock # NULL \* Collector holds write lock
/\ collecting = TRUE \* In collection phase
/\ collectorPayload # NULL \* Mid-trace on a payload
\* The actual work: read payloadEdges[collectorPayload] to discover children.
\* We don't model the trace results here; the safety property ensures
\* the read is valid (payload is alive).
/\ collectorPayload' = NULL
/\ UNCHANGED <<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders>>
\* ============================================================================
\* Next State Relation
@@ -607,6 +745,16 @@ Next ==
\/ CollectorEnd
\/ \E thread \in Threads:
CollectorReleaseLock(thread)
\* --- Seq payload actions ---
\/ \E thread \in Threads:
MutatorAcquireSeqLock(thread)
\/ \E thread \in Threads:
MutatorReleaseSeqLock(thread)
\/ \E thread \in Threads, obj \in Objects, p \in SeqPayloads:
MutatorSeqAssign(thread, obj, p)
\/ \E obj \in Objects:
CollectorStartTraceSeq(obj)
\/ CollectorFinishTraceSeq
\* ============================================================================
\* Initial State
@@ -642,6 +790,11 @@ Init ==
/\ collecting = FALSE
/\ gcEnv = [touched |-> 0, edges |-> 0, rcSum |-> 0, toFree |-> {}]
/\ pendingWrites = {}
\* Seq payload initial state
/\ seqData = [x \in Objects |-> NULL] \* No seq fields initially
/\ payloadAlive = [p \in SeqPayloads |-> FALSE] \* No payloads alive initially
/\ rwLockReaders = {} \* No threads hold read lock
/\ collectorPayload = NULL \* Collector not mid-trace
/\ TypeOK
\* ============================================================================
@@ -748,14 +901,53 @@ CycleInvariant ==
THEN ExternalRC(obj) = 0
ELSE TRUE
\* ============================================================================
\* Seq Payload Safety
\* ============================================================================
\* Memory safety: The collector never accesses a freed seq payload.
\*
\* collectorPayload holds the payload pointer the collector read during
\* CollectorStartTraceSeq. Between that action and CollectorFinishTraceSeq,
\* the collector will dereference this pointer to read the seq's elements.
\* If the payload has been freed in between, this is a use-after-free.
\*
\* The RWLock prevents this:
\* - collectorPayload is only set when globalLock # NULL (write lock held)
\* - MutatorSeqAssign (which frees payloads) requires rwLockReaders membership
\* - MutatorAcquireSeqLock requires globalLock = NULL (no writer)
\* - Therefore: while collectorPayload # NULL, no MutatorSeqAssign can execute
\* - Therefore: payloadAlive[collectorPayload] remains TRUE
\*
\* Without the RWLock (if MutatorSeqAssign didn't require the read lock),
\* the following interleaving would violate this property:
\* 1. Collector acquires write lock
\* 2. CollectorStartTraceSeq(obj) -- collectorPayload = P
\* 3. MutatorSeqAssign(thread, obj, Q) -- frees P, payloadAlive[P] = FALSE
\* 4. SeqPayloadSafety VIOLATED: collectorPayload = P but payloadAlive[P] = FALSE
SeqPayloadSafety ==
collectorPayload # NULL => payloadAlive[collectorPayload]
\* ============================================================================
\* RWLock Invariant
\* ============================================================================
\* The read-write lock ensures mutual exclusion between the collector (writer)
\* and seq mutations (readers). The writer and readers are never active at
\* the same time.
RWLockInvariant ==
globalLock # NULL => rwLockReaders = {}
\* ============================================================================
\* Specification
\* ============================================================================
Spec == Init /\ [][Next]_<<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites>>
Spec == Init /\ [][Next]_<<edges, roots, rc, color, inRoots, toIncLen, toInc, toDecLen, toDec, lockInc, lockDec, globalLock, mergedRoots, collecting, gcEnv, pendingWrites, seqData, payloadAlive, rwLockReaders, collectorPayload>>
THEOREM Spec => []Safety
THEOREM Spec => []RCInvariant
THEOREM Spec => []CycleInvariant
THEOREM Spec => []SeqPayloadSafety
THEOREM Spec => []RWLockInvariant
====