---- MODULE yrc_proof ---- \* TLA+ specification of YRC (Thread-safe ORC cycle collector) \* Models the fine details of barriers, striped queues, and synchronization \* \* ## Key Barrier Semantics Modeled \* \* ### Write Barrier (nimAsgnYrc) \* 1. atomicStoreN(dest, src, ATOMIC_RELEASE) \* - Graph update is immediately visible to all threads (including collector) \* - ATOMIC_RELEASE ensures all prior writes are visible before this store \* - No lock required for graph updates (lock-free) \* \* 2. nimIncRefCyclic(src, true) \* - Acquires per-stripe lockInc[stripe] (fine-grained) \* - Buffers increment in toInc[stripe] queue \* - On overflow: acquires global lock, merges all stripes, applies increment \* \* 3. yrcDec(tmp, desc) \* - Acquires per-stripe lockDec[stripe] (fine-grained) \* - Buffers decrement in toDec[stripe] queue \* - On overflow: acquires global lock, merges all stripes, applies decrement, \* adds to roots array if not already present \* \* ### Merge Operation (mergePendingRoots) \* - Acquires global lock (exclusive access) \* - Sequentially acquires each stripe's lockInc and lockDec \* - Drains all buffers, applies RC adjustments \* - Adds decremented objects to roots array \* - After merge: mergedRC = logicalRC (current graph state) \* \* ### Collection Cycle (under global lock) \* 1. mergePendingRoots: reconcile buffered changes \* 2. markGray: trial deletion (subtract internal edges) \* 3. scan: rescue objects with RC >= 0 (scanBlack follows current graph) \* 4. collectColor: free white objects (closed cycles) \* \* ## Safety Argument \* \* The collector only frees closed cycles (zero external refs). Concurrent writes \* cannot cause "lost objects" because: \* - Graph updates are atomic and immediately visible \* - 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 CONSTANTS NumStripes, QueueSize, RootsThreshold, Objects, Threads, ObjTypes ASSUME NumStripes \in Nat /\ NumStripes > 0 ASSUME QueueSize \in Nat /\ QueueSize > 0 ASSUME RootsThreshold \in Nat 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 /\ NULL \notin SeqPayloads \* Helper functions \* Note: GetStripeIdx is not used, GetStripe is used instead \* Color constants colBlack == 0 colGray == 1 colWhite == 2 maybeCycle == 4 inRootsFlag == 8 colorMask == 3 \* State variables VARIABLES \* Physical heap graph (always up-to-date, atomic stores) edges, \* edges[obj1][obj2] = TRUE if obj1.field points to obj2 \* Stack roots per thread roots, \* roots[thread][obj] = TRUE if thread has local var pointing to obj \* Reference counts (stored in object header) rc, \* rc[obj] = reference count (logical, after merge) \* Color markers (stored in object header, bits 0-2) color, \* color[obj] \in {colBlack, colGray, colWhite} \* Root tracking flags inRoots, \* inRoots[obj] = TRUE if obj is in roots array \* Striped increment queues toIncLen, \* toIncLen[stripe] = current length of increment queue toInc, \* toInc[stripe][i] = object to increment \* Striped decrement queues toDecLen, \* toDecLen[stripe] = current length of decrement queue toDec, \* toDec[stripe][i] = (object, type) pair to decrement \* Per-stripe locks lockInc, \* lockInc[stripe] = thread holding increment lock (or NULL) lockDec, \* lockDec[stripe] = thread holding decrement 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 \* --- 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 == <> \* Type invariants TypeOK == /\ edges \in [Objects -> [Objects -> BOOLEAN]] /\ roots \in [Threads -> [Objects -> BOOLEAN]] /\ rc \in [Objects -> Int] /\ color \in [Objects -> {colBlack, colGray, colWhite}] /\ inRoots \in [Objects -> BOOLEAN] /\ toIncLen \in [0..(NumStripes-1) -> 0..QueueSize] /\ toInc \in [0..(NumStripes-1) -> Seq(Objects)] /\ toDecLen \in [0..(NumStripes-1) -> 0..QueueSize] /\ toDec \in [0..(NumStripes-1) -> Seq([obj: Objects, desc: ObjTypes])] /\ lockInc \in [0..(NumStripes-1) -> Threads \cup {NULL}] /\ lockDec \in [0..(NumStripes-1) -> Threads \cup {NULL}] /\ globalLock \in Threads \cup {NULL} /\ 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) == Cardinality({src \in Objects : edges[src][obj]}) \* Helper: external reference count (stack roots) ExternalRC(obj) == Cardinality({t \in Threads : roots[t][obj]}) \* Helper: logical reference count LogicalRC(obj) == InternalRC(obj) + ExternalRC(obj) \* Helper: get stripe index for thread \* Map threads to stripe indices deterministically \* Since threads are ModelValues, we use a simple deterministic mapping: \* Assign each thread to stripe 0 (for small models, this is fine) \* For larger models, TLC will handle the mapping deterministically GetStripe(thread) == 0 \* ============================================================================ \* Write Barrier: nimAsgnYrc \* ============================================================================ \* The write barrier does: \* 1. atomicStoreN(dest, src, ATOMIC_RELEASE) -- graph update is immediate \* 2. nimIncRefCyclic(src, true) -- buffer inc(src) \* 3. yrcDec(tmp, desc) -- buffer dec(old) \* \* Key barrier semantics: \* - ATOMIC_RELEASE on store ensures all prior writes are visible before the graph update \* - The graph update is immediately visible to all threads (including collector) \* - RC adjustments are buffered and only applied during merge \* ============================================================================ \* Phase 1: Atomic Store (Topology Update) \* ============================================================================ \* The atomic store always happens first, updating the graph topology. \* This is independent of RC operations and never blocks. MutatorWriteAtomicStore(thread, destObj, destField, oldVal, newVal, desc) == \* Atomic store with RELEASE barrier - updates graph topology immediately \* Clear ALL edges from destObj first (atomic store replaces old value completely), \* then set the new edge. This ensures destObj.field can only point to one object. /\ edges' = [edges EXCEPT ![destObj] = [x \in Objects |-> IF x = newVal /\ newVal # NULL THEN TRUE ELSE FALSE]] /\ UNCHANGED <> \* ============================================================================ \* Phase 2: RC Buffering (if space available) \* ============================================================================ \* Buffers increment/decrement if there's space. If overflow would happen, \* this action is disabled (blocked) until merge can happen. WriteBarrier(thread, destObj, destField, oldVal, newVal, desc) == LET stripe == GetStripe(thread) IN \* Determine if overflow happens for increment or decrement /\ LET incOverflow == (newVal # NULL) /\ (toIncLen[stripe] >= QueueSize) decOverflow == (oldVal # NULL) /\ (toDecLen[stripe] >= QueueSize) IN \* Buffering: only enabled if no overflow (otherwise blocked until merge can happen) /\ ~incOverflow \* Precondition: increment buffer has space (blocks if full) /\ ~decOverflow \* Precondition: decrement buffer has space (blocks if full) /\ toIncLen' = IF newVal # NULL /\ toIncLen[stripe] < QueueSize THEN [toIncLen EXCEPT ![stripe] = toIncLen[stripe] + 1] ELSE toIncLen /\ toInc' = IF newVal # NULL /\ toIncLen[stripe] < QueueSize THEN [toInc EXCEPT ![stripe] = Append(toInc[stripe], newVal)] ELSE toInc /\ toDecLen' = IF oldVal # NULL /\ toDecLen[stripe] < QueueSize THEN [toDecLen EXCEPT ![stripe] = toDecLen[stripe] + 1] ELSE toDecLen /\ toDec' = IF oldVal # NULL /\ toDecLen[stripe] < QueueSize THEN [toDec EXCEPT ![stripe] = Append(toDec[stripe], [obj |-> oldVal, desc |-> desc])] ELSE toDec /\ UNCHANGED <> \* ============================================================================ \* Phase 3: Overflow Handling (separate actions that can block) \* ============================================================================ \* Handle increment overflow: merge increment buffers when lock is available \* This merges ALL increment buffers (for all stripes), not just the one that overflowed MutatorWriteMergeInc(thread) == LET stripe == GetStripe(thread) IN /\ \E s \in 0..(NumStripes-1): toIncLen[s] >= QueueSize \* Some stripe has increment overflow /\ globalLock = NULL \* Lock must be available (blocks if held) /\ toIncLen' = [s \in 0..(NumStripes-1) |-> 0] /\ toInc' = [s \in 0..(NumStripes-1) |-> <<>>] /\ rc' = \* Compute RC from LogicalRC of current graph (increment buffers merged) \* The graph is already updated by atomic store, so we compute from current edges [x \in Objects |-> LET internalRC == Cardinality({src \in Objects : edges[src][x]}) externalRC == Cardinality({t \in Threads : roots[t][x]}) IN internalRC + externalRC] /\ globalLock' = NULL \* Release lock after merge /\ UNCHANGED <> \* Handle decrement overflow: merge ALL buffers when lock is available \* This calls collectCycles() which merges both increment and decrement buffers \* We inline MergePendingRoots here. The entire withLock block is atomic: \* lock is acquired, merge happens, lock is released. MutatorWriteMergeDec(thread) == LET stripe == GetStripe(thread) IN /\ \E s \in 0..(NumStripes-1): toDecLen[s] >= QueueSize \* Some stripe has decrement overflow /\ globalLock = NULL \* Lock must be available (blocks if held) /\ \* Merge all buffers (inlined MergePendingRoots logic) LET \* Compute new RC by merging all buffered increments and decrements \* For each object, count buffered increments and decrements bufferedInc == UNION {{toInc[s][i] : i \in 1..toIncLen[s]} : s \in 0..(NumStripes-1)} bufferedDec == UNION {{toDec[s][i].obj : i \in 1..toDecLen[s]} : s \in 0..(NumStripes-1)} \* Compute RC: current graph state (edges) + roots - buffered decrements + buffered increments \* Actually, we compute from LogicalRC of current graph (buffers are merged) newRC == [x \in Objects |-> LET internalRC == Cardinality({src \in Objects : edges[src][x]}) externalRC == Cardinality({t \in Threads : roots[t][x]}) IN internalRC + externalRC] \* Collect objects from decrement buffers for mergedRoots newRootsSet == UNION {{toDec[s][i].obj : i \in 1..toDecLen[s]} : s \in 0..(NumStripes-1)} newRootsSeq == IF newRootsSet = {} THEN <<>> ELSE LET ordered == CHOOSE f \in [1..Cardinality(newRootsSet) -> newRootsSet] : \A i, j \in DOMAIN f : i # j => f[i] # f[j] IN [i \in 1..Cardinality(newRootsSet) |-> ordered[i]] IN /\ rc' = newRC /\ mergedRoots' = mergedRoots \o newRootsSeq /\ inRoots' = [x \in Objects |-> IF newRootsSet = {} THEN inRoots[x] ELSE LET rootObjs == UNION {{mergedRoots'[i].obj : i \in DOMAIN mergedRoots'}} IN IF x \in rootObjs THEN TRUE ELSE inRoots[x]] /\ toIncLen' = [s \in 0..(NumStripes-1) |-> 0] /\ toInc' = [s \in 0..(NumStripes-1) |-> <<>>] /\ 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 <> \* ============================================================================ \* Merge Operation: mergePendingRoots \* ============================================================================ \* Drains all stripe buffers under global lock. \* Sequentially acquires each stripe's lockInc and lockDec to drain buffers. \* This reconciles buffered RC adjustments with the current graph state. \* \* Key invariant: After merge, mergedRC = logicalRC (current graph + buffered changes) MergePendingRoots == /\ globalLock # NULL /\ LET \* Count pending increments per object (across all stripes) pendingInc == [x \in Objects |-> Cardinality(UNION {{i \in DOMAIN toInc[s] : toInc[s][i] = x} : s \in 0..(NumStripes-1)})] \* Count pending decrements per object (across all stripes) pendingDec == [x \in Objects |-> Cardinality(UNION {{i \in DOMAIN toDec[s] : toDec[s][i].obj = x} : s \in 0..(NumStripes-1)})] \* After merge, RC should equal LogicalRC (current graph state) \* The buffered changes compensate for graph changes that already happened, \* so: mergedRC = currentRC + pendingInc - pendingDec = LogicalRC(current graph) \* But to ensure correctness, we compute directly from the current graph: newRC == [x \in Objects |-> LogicalRC(x)] \* RC after merge equals logical RC of current graph \* Add decremented objects to roots if not already there (check inRootsFlag) \* Collect all new roots as a set, then convert to sequence \* Build set by iterating over all (stripe, index) pairs \* Use UNION with explicit per-stripe sets (avoiding function enumeration issues) newRootsSet == UNION {UNION {IF inRoots[toDec[s][i].obj] = FALSE THEN {[obj |-> toDec[s][i].obj, desc |-> toDec[s][i].desc]} ELSE {} : i \in DOMAIN toDec[s]} : s \in 0..(NumStripes-1)} newRootsSeq == IF newRootsSet = {} THEN <<>> ELSE LET ordered == CHOOSE f \in [1..Cardinality(newRootsSet) -> newRootsSet] : \A i, j \in DOMAIN f : i # j => f[i] # f[j] IN [i \in 1..Cardinality(newRootsSet) |-> ordered[i]] IN /\ rc' = newRC /\ mergedRoots' = mergedRoots \o newRootsSeq \* Append new roots to sequence /\ \* Update inRoots: mark objects in mergedRoots' as being in roots \* Use explicit iteration to avoid enumeration issues inRoots' = [x \in Objects |-> IF mergedRoots' = <<>> THEN inRoots[x] ELSE LET rootObjs == UNION {{mergedRoots'[i].obj : i \in DOMAIN mergedRoots'}} IN IF x \in rootObjs THEN TRUE ELSE inRoots[x]] /\ toIncLen' = [s \in 0..(NumStripes-1) |-> 0] /\ toInc' = [s \in 0..(NumStripes-1) |-> <<>>] /\ toDecLen' = [s \in 0..(NumStripes-1) |-> 0] /\ toDec' = [s \in 0..(NumStripes-1) |-> <<>>] /\ UNCHANGED <> \* ============================================================================ \* Trial Deletion: markGray \* ============================================================================ \* Subtracts internal (heap-to-heap) edges from reference counts. \* This isolates external references (stack roots). \* \* Algorithm: \* 1. Mark obj gray \* 2. Trace obj's fields (via traceImpl) \* 3. For each child c: decrement c.rc (subtract internal edge) \* 4. Recursively markGray all children \* \* After markGray: trialRC(obj) = mergedRC(obj) - internalRefCount(obj) \* = externalRefCount(obj) (if merge was correct) MarkGray(obj, desc) == /\ globalLock # NULL /\ collecting = TRUE /\ color[obj] # colGray /\ \* Compute transitive closure of all objects reachable from obj \* This models the recursive traversal in the actual implementation LET children == {c \in Objects : edges[obj][c]} \* Compute all objects reachable from obj via heap edges \* This is the transitive closure starting from obj's direct children allReachable == {c \in Objects : \E path \in Seq(Objects): Len(path) > 0 /\ path[1] \in children /\ path[Len(path)] = c /\ \A i \in 1..(Len(path)-1): edges[path[i]][path[i+1]]} \* All objects to mark gray: obj itself + all reachable descendants objectsToMarkGray == {obj} \cup allReachable \* For each reachable object, count internal edges pointing to it \* from within the subgraph (obj + allReachable) \* This is the number of times its RC should be decremented subgraph == {obj} \cup allReachable internalEdgeCount == [x \in Objects |-> IF x \in allReachable THEN Cardinality({y \in subgraph : edges[y][x]}) ELSE 0] IN /\ \* Mark obj and all reachable objects gray color' = [x \in Objects |-> IF x \in objectsToMarkGray THEN colGray ELSE color[x]] /\ \* Subtract internal edges: for each reachable object, decrement its RC \* by the number of internal edges pointing to it from within the subgraph. \* This matches the Nim implementation which decrements once per edge traversed. \* Note: obj's RC is not decremented here (it has no parent in this subgraph). \* 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 <> \* ============================================================================ \* Scan Phase \* ============================================================================ \* Objects with RC >= 0 after trial deletion are rescued (scanBlack). \* Objects with RC < 0 remain white (part of closed cycle). \* \* Key insight: scanBlack follows the *current* physical edges (which may have \* changed since merge due to concurrent writes). This ensures objects written \* during collection are still rescued. \* \* Algorithm: \* IF rc[obj] >= 0: \* scanBlack(obj): mark black, restore RC, trace and rescue all children \* ELSE: \* mark white (closed cycle with zero external refs) Scan(obj, desc) == /\ globalLock # NULL /\ collecting = TRUE /\ color[obj] = colGray /\ IF rc[obj] >= 0 THEN \* scanBlack: rescue obj and all reachable objects \* This follows the current physical graph (atomic stores are visible) \* Restore RC for all reachable objects by incrementing by the number of \* internal edges pointing to each (matching what markGray subtracted) LET children == {c \in Objects : edges[obj][c]} allReachable == {c \in Objects : \E path \in Seq(Objects): Len(path) > 0 /\ path[1] \in children /\ path[Len(path)] = c /\ \A i \in 1..(Len(path)-1): edges[path[i]][path[i+1]]} objectsToMarkBlack == {obj} \cup allReachable \* For each reachable object, count internal edges pointing to it \* from within the subgraph (obj + allReachable) \* This is the number of times its RC should be incremented (restored) subgraph == {obj} \cup allReachable internalEdgeCount == [x \in Objects |-> IF x \in allReachable THEN Cardinality({y \in subgraph : edges[y][x]}) ELSE 0] IN /\ \* Restore RC: increment by the number of internal edges pointing to each \* reachable object. This restores what markGray subtracted. \* Note: obj's RC is not incremented here (it wasn't decremented in markGray). \* The root's RC already reflects external refs which survived trial deletion. rc' = [x \in Objects |-> IF x \in allReachable THEN rc[x] + internalEdgeCount[x] ELSE rc[x]] /\ \* Mark obj and all reachable objects black in one assignment color' = [x \in Objects |-> IF x \in objectsToMarkBlack THEN colBlack ELSE color[x]] ELSE \* Mark white (part of closed cycle) /\ color' = [color EXCEPT ![obj] = colWhite] /\ UNCHANGED <> /\ UNCHANGED <> \* ============================================================================ \* Collection Phase: collectColor \* ============================================================================ \* Frees objects of the target color that are not in roots. \* \* Safety: Only objects with color = targetColor AND ~inRoots[obj] are freed. \* These are closed cycles (zero external refs, not reachable from roots). CollectColor(obj, desc, targetColor) == /\ globalLock # NULL /\ collecting = TRUE /\ color[obj] = targetColor /\ ~inRoots[obj] /\ \* Free obj: nullify all its outgoing edges (prevents use-after-free) \* In the actual implementation, this happens during trace() when freeing 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 <> \* ============================================================================ \* Collection Cycle: collectCyclesBacon \* ============================================================================ StartCollection == /\ globalLock # NULL /\ ~collecting /\ Len(mergedRoots) >= RootsThreshold /\ collecting' = TRUE /\ gcEnv' = [touched |-> 0, edges |-> 0, rcSum |-> 0, toFree |-> {}] /\ UNCHANGED <> EndCollection == /\ globalLock # NULL /\ collecting = TRUE /\ \* Clear root flags inRoots' = [x \in Objects |-> IF x \in {r.obj : r \in mergedRoots} THEN FALSE ELSE inRoots[x]] /\ mergedRoots' = <<>> /\ collecting' = FALSE /\ UNCHANGED <> \* ============================================================================ \* Mutator Actions \* ============================================================================ \* Mutator can write at any time (graph updates are lock-free) \* The ATOMIC_RELEASE barrier ensures proper ordering \* ASSUMPTION: Users synchronize pointer assignments with locks, so oldVal always \* matches the current graph state (as read before the atomic store). \* This prevents races at the user level - the GC itself is lock-free. MutatorWrite(thread, destObj, destField, oldVal, newVal, desc) == \* ASSUMPTION: Users synchronize pointer assignments with locks, so oldVal always matches \* the value read before the atomic store. This prevents races at the user level. \* The precondition is enforced in the Next relation. \* Phase 1: Atomic store (topology update) - ALWAYS happens first /\ MutatorWriteAtomicStore(thread, destObj, destField, oldVal, newVal, desc) \* Phase 2: RC buffering - happens if no overflow, otherwise overflow is handled separately \* Note: In reality, if overflow happens, the thread blocks waiting for lock. \* We model this as: atomic store happens, buffering is deferred (handled by merge actions). /\ LET stripe == GetStripe(thread) incOverflow == (newVal # NULL) /\ (toIncLen[stripe] >= QueueSize) decOverflow == (oldVal # NULL) /\ (toDecLen[stripe] >= QueueSize) IN 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 <> ELSE \* No overflow: buffer normally /\ WriteBarrier(thread, destObj, destField, oldVal, newVal, desc) /\ UNCHANGED <> \* Stack root assignment: immediate RC increment (not buffered) \* When assigning val to a root variable named obj, we set roots[thread][val] = TRUE \* to indicate that thread has a stack reference to val \* Semantics: obj is root variable name, val is the object being assigned \* When val=NULL, obj was the old root value, so we decrement rc[obj] MutatorRootAssign(thread, obj, val) == /\ IF val # NULL THEN /\ roots' = [roots EXCEPT ![thread][val] = TRUE] /\ rc' = [rc EXCEPT ![val] = IF roots[thread][val] THEN @ ELSE @ + 1] \* Increment only if not already a root ELSE /\ roots' = [roots EXCEPT ![thread][obj] = FALSE] \* Clear root when assigning NULL /\ rc' = [rc EXCEPT ![obj] = IF roots[thread][obj] THEN @ - 1 ELSE @] \* Decrement old root value /\ edges' = edges /\ color' = color /\ inRoots' = inRoots /\ toIncLen' = toIncLen /\ toInc' = toInc /\ toDecLen' = toDecLen /\ toDec' = toDec /\ lockInc' = lockInc /\ lockDec' = lockDec /\ globalLock' = globalLock /\ mergedRoots' = mergedRoots /\ collecting' = collecting /\ gcEnv' = gcEnv /\ pendingWrites' = pendingWrites /\ UNCHANGED seqVars \* ============================================================================ \* Collector Actions \* ============================================================================ \* 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 <> CollectorMerge == /\ globalLock # NULL /\ MergePendingRoots CollectorStart == /\ globalLock # NULL /\ StartCollection \* Mark all roots gray (trial deletion phase) CollectorMarkGray == /\ globalLock # NULL /\ collecting = TRUE /\ \E rootIdx \in DOMAIN mergedRoots: LET root == mergedRoots[rootIdx] IN MarkGray(root.obj, root.desc) \* Scan all roots (rescue phase) CollectorScan == /\ globalLock # NULL /\ collecting = TRUE /\ \E rootIdx \in DOMAIN mergedRoots: LET root == mergedRoots[rootIdx] IN Scan(root.obj, root.desc) \* Collect white/gray objects (free phase) CollectorCollect == /\ globalLock # NULL /\ collecting = TRUE /\ \E rootIdx \in DOMAIN mergedRoots, targetColor \in {colGray, colWhite}: LET root == mergedRoots[rootIdx] IN CollectColor(root.obj, root.desc, targetColor) CollectorEnd == /\ globalLock # NULL /\ EndCollection CollectorReleaseLock(thread) == /\ globalLock = thread /\ globalLock' = NULL /\ 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 \* ============================================================================ Next == \/ \E thread \in Threads: \E destObj \in Objects, oldVal, newVal \in Objects \cup {NULL}, desc \in ObjTypes: \* Precondition: oldVal must match current graph state (user-level synchronization) \* ASSUMPTION: Users synchronize pointer assignments with locks, so oldVal always matches \* the value read before the atomic store. This prevents races at the user level. /\ LET oldValMatches == CASE oldVal = NULL -> TRUE [] oldVal \in Objects -> edges[destObj][oldVal] [] OTHER -> FALSE IN oldValMatches /\ MutatorWrite(thread, destObj, "field", oldVal, newVal, desc) \/ \E thread \in Threads: \* Handle increment overflow: merge increment buffers when lock becomes available MutatorWriteMergeInc(thread) \/ \E thread \in Threads: \* Handle decrement overflow: merge all buffers when lock becomes available MutatorWriteMergeDec(thread) \/ \E thread \in Threads: \E obj, val \in Objects \cup {NULL}: MutatorRootAssign(thread, obj, val) \/ \E thread \in Threads: CollectorAcquireLock(thread) \/ CollectorMerge \/ CollectorStart \/ CollectorMarkGray \/ CollectorScan \/ CollectorCollect \/ 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 \* ============================================================================ Init == /\ edges = [x \in Objects |-> [y \in Objects |-> IF x = y THEN FALSE ELSE FALSE]] \* Empty graph initially /\ roots = [t \in Threads |-> [x \in Objects |-> FALSE]] \* No stack roots initially /\ rc = [x \in Objects |-> 0] \* Zero reference counts /\ color = [x \in Objects |-> colBlack] \* All objects black initially /\ inRoots = [x \in Objects |-> FALSE] \* No objects in roots array /\ toIncLen = [s \in 0..(NumStripes-1) |-> 0] /\ toInc = [s \in 0..(NumStripes-1) |-> <<>>] /\ toDecLen = [s \in 0..(NumStripes-1) |-> 0] /\ toDec = [s \in 0..(NumStripes-1) |-> <<>>] /\ lockInc = [s \in 0..(NumStripes-1) |-> NULL] /\ lockDec = [s \in 0..(NumStripes-1) |-> NULL] /\ globalLock = NULL /\ mergedRoots = <<>> /\ 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 \* ============================================================================ \* Safety Properties \* ============================================================================ \* Safety: Objects are only freed if they are unreachable from any thread's stack \* \* An object is reachable if: \* - It is a direct stack root (roots[t][obj] = TRUE), OR \* - There exists a path from a stack root to obj via heap edges \* \* Safety guarantee: If an object is reachable, then: \* - It is not white (not marked for collection), OR \* - It is in roots array (protected from collection), OR \* - It is reachable from an object that will be rescued by scanBlack \* \* More precisely: Only closed cycles (zero external refs, unreachable) are freed. \* Helper: Compute next set of reachable objects (one step of transitive closure) ReachableStep(current) == current \cup UNION {{y \in Objects : edges[x][y]} : x \in current} \* Compute the set of all reachable objects using bounded iteration \* Since Objects is finite, we iterate at most Cardinality(Objects) times \* This computes the transitive closure of edges starting from stack roots \* We unroll the iteration explicitly to avoid recursion issues with TLC ReachableSet == LET StackRoots == {x \in Objects : \E t \in Threads : roots[t][x]} Step1 == ReachableStep(StackRoots) Step2 == ReachableStep(Step1) Step3 == ReachableStep(Step2) Step4 == ReachableStep(Step3) \* Add more steps if needed for larger object sets \* For small models (2 objects), 4 steps is sufficient IN Step4 \* Check if an object is reachable Reachable(obj) == obj \in ReachableSet \* Helper: Check if there's a path from 'from' to 'to' \* For small object sets, we check all possible paths by checking \* all combinations of intermediate objects \* Path of length 0: from = to \* Path of length 1: edges[from][to] \* Path of length 2: \E i1: edges[from][i1] /\ edges[i1][to] \* Path of length 3: \E i1, i2: edges[from][i1] /\ edges[i1][i2] /\ edges[i2][to] \* etc. up to Cardinality(Objects) HasPath(from, to) == \/ from = to \/ edges[from][to] \/ \E i1 \in Objects: edges[from][i1] /\ (edges[i1][to] \/ \E i2 \in Objects: edges[i1][i2] /\ (edges[i2][to] \/ \E i3 \in Objects: edges[i2][i3] /\ edges[i3][to])) \* Helper: Compute set of objects reachable from a given starting object \* Uses the same iterative approach as ReachableSet ReachableFrom(start) == LET Step1 == ReachableStep({start}) Step2 == ReachableStep(Step1) Step3 == ReachableStep(Step2) Step4 == ReachableStep(Step3) IN Step4 \* Safety: Reachable objects are never freed (remain white without being collected) \* A reachable object is safe if: \* - It's not white (not marked for collection), OR \* - It's in roots array (protected from collection), OR \* - There exists a black object in ReachableSet such that obj is reachable from it \* (the black object will be rescued by scanBlack, which rescues all white objects \* reachable from black objects) Safety == \A obj \in Objects: IF obj \in ReachableSet THEN \/ color[obj] # colWhite \* Not marked for collection \/ inRoots[obj] \* Protected in roots array \/ \E blackObj \in ReachableSet: /\ color[blackObj] = colBlack \* Black object will be rescued by scanBlack /\ obj \in ReachableFrom(blackObj) \* obj is reachable from blackObj ELSE TRUE \* Unreachable objects may be freed (this is safe) \* Invariant: Reference counts match logical counts after merge \* (This is maintained by MergePendingRoots) \* Note: Between merge and collection, RC = logicalRC. \* During collection (after markGray), RC may be modified by trial deletion. \* RC may be inconsistent when: \* - globalLock = NULL (buffered changes pending) \* - globalLock # NULL but merge hasn't happened yet (buffers still have pending changes) \* RC must equal LogicalRC when: \* - After merge (buffers are empty) and before collection starts RCInvariant == IF globalLock = NULL THEN TRUE \* Not in collection, RC may be inconsistent (buffered changes pending) ELSE IF collecting = FALSE /\ \A s \in 0..(NumStripes-1): toIncLen[s] = 0 /\ toDecLen[s] = 0 THEN \A obj \in Objects: rc[obj] = LogicalRC(obj) \* After merge, buffers empty, RC = logical RC ELSE TRUE \* During collection or before merge, RC may differ from logicalRC \* Invariant: Only closed cycles are collected \* (Objects with external refs are rescued by scanBlack) CycleInvariant == \A obj \in Objects: IF color[obj] = colWhite /\ ~inRoots[obj] 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]_<> THEOREM Spec => []Safety THEOREM Spec => []RCInvariant THEOREM Spec => []CycleInvariant THEOREM Spec => []SeqPayloadSafety THEOREM Spec => []RWLockInvariant ====