From 08c31ad24792e6da7f5b62ba0091b0a6b95397b7 Mon Sep 17 00:00:00 2001 From: Araq Date: Sat, 21 Feb 2026 07:16:01 +0100 Subject: [PATCH] YRC improvements: wip --- lib/system.nim | 2 +- lib/system/rwlocks.nim | 121 ++++++++++++++++++ lib/system/seqs_v2.nim | 136 ++++++++++++++------ lib/system/seqs_v2_reimpl.nim | 9 +- lib/system/yrc.nim | 23 ++-- lib/system/yrc_proof.tla | 230 +++++++++++++++++++++++++++++++--- 6 files changed, 443 insertions(+), 78 deletions(-) create mode 100644 lib/system/rwlocks.nim diff --git a/lib/system.nim b/lib/system.nim index 6104c1b928..19f5b12804 100644 --- a/lib/system.nim +++ b/lib/system.nim @@ -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. diff --git a/lib/system/rwlocks.nim b/lib/system/rwlocks.nim new file mode 100644 index 0000000000..95142b402b --- /dev/null +++ b/lib/system/rwlocks.nim @@ -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: "", final, pure, byref.} = object + p: pointer + + proc initializeSRWLock(L: var RwLock) {.importc: "InitializeSRWLock", + header: "".} + proc acquireSRWLockShared(L: var RwLock) {.importc: "AcquireSRWLockShared", + header: "".} + proc releaseSRWLockShared(L: var RwLock) {.importc: "ReleaseSRWLockShared", + header: "".} + proc acquireSRWLockExclusive(L: var RwLock) {.importc: "AcquireSRWLockExclusive", + header: "".} + proc releaseSRWLockExclusive(L: var RwLock) {.importc: "ReleaseSRWLockExclusive", + header: "".} + + 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 + #include """, 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: "", noSideEffect.} + proc pthread_rwlock_destroy(rwlock: var SysRwLockObj): cint {. + importc: "pthread_rwlock_destroy", header: "", noSideEffect.} + proc pthread_rwlock_rdlock(rwlock: var SysRwLockObj): cint {. + importc: "pthread_rwlock_rdlock", header: "", noSideEffect.} + proc pthread_rwlock_wrlock(rwlock: var SysRwLockObj): cint {. + importc: "pthread_rwlock_wrlock", header: "", noSideEffect.} + proc pthread_rwlock_unlock(rwlock: var SysRwLockObj): cint {. + importc: "pthread_rwlock_unlock", header: "", 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: "".} + proc c_free(p: pointer) {.importc: "free", header: "".} + 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: "".} + 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.} diff --git a/lib/system/seqs_v2.nim b/lib/system/seqs_v2.nim index f0c880115c..9ac756aacf 100644 --- a/lib/system/seqs_v2.nim +++ b/lib/system/seqs_v2.nim @@ -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..= 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.. 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 == <> \* 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 <> + /\ UNCHANGED <> \* ============================================================================ \* 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 <> + /\ UNCHANGED <> \* ============================================================================ \* 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 <> + /\ UNCHANGED <> \* 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 <> + /\ UNCHANGED <> \* ============================================================================ \* 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 <> + /\ UNCHANGED <> \* ============================================================================ \* 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 <> + /\ UNCHANGED <> \* ============================================================================ \* Scan Phase @@ -422,7 +471,7 @@ Scan(obj, desc) == ELSE \* Mark white (part of closed cycle) /\ color' = [color EXCEPT ![obj] = colWhite] /\ UNCHANGED <> - /\ UNCHANGED <> + /\ UNCHANGED <> \* ============================================================================ \* 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 <> + /\ UNCHANGED <> \* ============================================================================ \* Collection Cycle: collectCyclesBacon @@ -454,7 +503,7 @@ StartCollection == /\ Len(mergedRoots) >= RootsThreshold /\ collecting' = TRUE /\ gcEnv' = [touched |-> 0, edges |-> 0, rcSum |-> 0, toFree |-> {}] - /\ UNCHANGED <> + /\ UNCHANGED <> 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 <> + /\ UNCHANGED <> \* ============================================================================ \* 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 <> + /\ UNCHANGED <> ELSE \* No overflow: buffer normally /\ WriteBarrier(thread, destObj, destField, oldVal, newVal, desc) /\ UNCHANGED <> @@ -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 <> + /\ UNCHANGED <> CollectorMerge == /\ globalLock # NULL @@ -571,7 +623,93 @@ CollectorEnd == CollectorReleaseLock(thread) == /\ globalLock = thread /\ globalLock' = NULL - /\ UNCHANGED <> + /\ UNCHANGED <> + +\* ============================================================================ +\* 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 <> + +\* Mutator releases read lock after seq mutation completes. +MutatorReleaseSeqLock(thread) == + /\ thread \in rwLockReaders + /\ rwLockReaders' = rwLockReaders \ {thread} + /\ UNCHANGED <> + +\* 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 <> + +\* 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 <> + +\* 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 <> \* ============================================================================ \* 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]_<> +Spec == Init /\ [][Next]_<> THEOREM Spec => []Safety THEOREM Spec => []RCInvariant THEOREM Spec => []CycleInvariant +THEOREM Spec => []SeqPayloadSafety +THEOREM Spec => []RWLockInvariant ====