mirror of
https://github.com/nim-lang/Nim.git
synced 2026-08-20 22:00:57 +00:00
YRC: tests and correctness proof
This commit is contained in:
araq
@@ -2,6 +2,7 @@
|
||||
# YRC: Thread-safe ORC (concurrent cycle collector).
|
||||
# Same API as orc.nim but with striped queues and global lock for merge/collect.
|
||||
# Destructors for refs run at collection time, not immediately on last decRef.
|
||||
# See yrc_proof.lean for a Lean 4 proof of safety and deadlock freedom.
|
||||
#
|
||||
# ## Key Invariant: Topology vs. Reference Counts
|
||||
#
|
||||
|
||||
353
lib/system/yrc_proof.lean
Normal file
353
lib/system/yrc_proof.lean
Normal file
@@ -0,0 +1,353 @@
|
||||
/-
|
||||
YRC Safety Proof (self-contained, no Mathlib)
|
||||
==============================================
|
||||
Formal model of YRC's key invariant: the cycle collector never frees
|
||||
an object that any mutator thread can reach.
|
||||
|
||||
## Model overview
|
||||
|
||||
We model the heap as a set of objects with directed edges (ref fields).
|
||||
Each thread owns a set of *stack roots* — objects reachable from local variables.
|
||||
The write barrier (nimAsgnYrc) does:
|
||||
1. atomic store dest ← src (graph is immediately current)
|
||||
2. buffer inc(src) (deferred)
|
||||
3. buffer dec(old) (deferred)
|
||||
|
||||
The collector (under global lock) does:
|
||||
1. Merge all buffered inc/dec into merged RCs
|
||||
2. Trial deletion (markGray): subtract internal edges from merged RCs
|
||||
3. scan: objects with RC ≥ 0 after trial deletion are rescued (scanBlack)
|
||||
4. Free objects that remain white (closed cycles with zero external refs)
|
||||
-/
|
||||
|
||||
-- Objects and threads are just natural numbers for simplicity.
|
||||
abbrev Obj := Nat
|
||||
abbrev Thread := Nat
|
||||
|
||||
/-! ### State -/
|
||||
|
||||
/-- The state of the heap and collector at a point in time. -/
|
||||
structure State where
|
||||
/-- Physical heap edges: `edges x y` means object `x` has a ref field pointing to `y`.
|
||||
Always up-to-date (atomic stores). -/
|
||||
edges : Obj → Obj → Prop
|
||||
/-- Stack roots per thread. `roots t x` means thread `t` has a local variable pointing to `x`. -/
|
||||
roots : Thread → Obj → Prop
|
||||
/-- Pending buffered increments (not yet merged). -/
|
||||
pendingInc : Obj → Nat
|
||||
/-- Pending buffered decrements (not yet merged). -/
|
||||
pendingDec : Obj → Nat
|
||||
|
||||
/-! ### Reachability -/
|
||||
|
||||
/-- An object is *reachable* if some thread can reach it via stack roots + heap edges. -/
|
||||
inductive Reachable (s : State) : Obj → Prop where
|
||||
| root (t : Thread) (x : Obj) : s.roots t x → Reachable s x
|
||||
| step (x y : Obj) : Reachable s x → s.edges x y → Reachable s y
|
||||
|
||||
/-- Directed reachability between heap objects (following physical edges only). -/
|
||||
inductive HeapReachable (s : State) : Obj → Obj → Prop where
|
||||
| refl (x : Obj) : HeapReachable s x x
|
||||
| step (x y z : Obj) : HeapReachable s x y → s.edges y z → HeapReachable s x z
|
||||
|
||||
/-- If a root reaches `r` and `r` heap-reaches `x`, then `x` is Reachable. -/
|
||||
theorem heapReachable_of_reachable (s : State) (r x : Obj)
|
||||
(hr : Reachable s r) (hp : HeapReachable s r x) :
|
||||
Reachable s x := by
|
||||
induction hp with
|
||||
| refl => exact hr
|
||||
| step _ _ _ hedge ih => exact Reachable.step _ _ ih hedge
|
||||
|
||||
/-! ### What the collector frees -/
|
||||
|
||||
/-- An object has an *external reference* if some thread's stack roots point to it. -/
|
||||
def hasExternalRef (s : State) (x : Obj) : Prop :=
|
||||
∃ t, s.roots t x
|
||||
|
||||
/-- An object is *externally anchored* if it is heap-reachable from some
|
||||
object that has an external reference. This is what scanBlack computes:
|
||||
it starts from objects with trialRC ≥ 0 (= has external refs) and traces
|
||||
the current physical graph. -/
|
||||
def anchored (s : State) (x : Obj) : Prop :=
|
||||
∃ r, hasExternalRef s r ∧ HeapReachable s r x
|
||||
|
||||
/-- The collector frees `x` only if `x` is *not anchored*:
|
||||
no external ref, and not reachable from any externally-referenced object.
|
||||
This models: after trial deletion, x remained white, and scanBlack
|
||||
didn't rescue it. -/
|
||||
def collectorFrees (s : State) (x : Obj) : Prop :=
|
||||
¬ anchored s x
|
||||
|
||||
/-! ### Main safety theorem -/
|
||||
|
||||
/-- **Lemma**: Every reachable object is anchored.
|
||||
If thread `t` reaches `x`, then there is a chain from a stack root
|
||||
(which has an external ref) through heap edges to `x`. -/
|
||||
theorem reachable_is_anchored (s : State) (x : Obj)
|
||||
(h : Reachable s x) : anchored s x := by
|
||||
induction h with
|
||||
| root t x hroot =>
|
||||
exact ⟨x, ⟨t, hroot⟩, HeapReachable.refl x⟩
|
||||
| step a b h_reach_a h_edge ih =>
|
||||
obtain ⟨r, h_ext_r, h_path_r_a⟩ := ih
|
||||
exact ⟨r, h_ext_r, HeapReachable.step r a b h_path_r_a h_edge⟩
|
||||
|
||||
/-- **Main Safety Theorem**: If the collector frees `x`, then no thread
|
||||
can reach `x`. Freed objects are unreachable.
|
||||
|
||||
This is the contrapositive of `reachable_is_anchored`. -/
|
||||
theorem yrc_safety (s : State) (x : Obj)
|
||||
(h_freed : collectorFrees s x) : ¬ Reachable s x := by
|
||||
intro h_reach
|
||||
exact h_freed (reachable_is_anchored s x h_reach)
|
||||
|
||||
/-! ### The write barrier preserves reachability -/
|
||||
|
||||
/-- Model of `nimAsgnYrc(dest_field_of_a, src)`:
|
||||
Object `a` had a field pointing to `old`, now points to `src`.
|
||||
Graph update is immediate. The new edge takes priority (handles src = old). -/
|
||||
def writeBarrier (s : State) (a old src : Obj) : State :=
|
||||
{ s with
|
||||
edges := fun x y =>
|
||||
if x = a ∧ y = src then True
|
||||
else if x = a ∧ y = old then False
|
||||
else s.edges x y
|
||||
pendingInc := fun x => if x = src then s.pendingInc x + 1 else s.pendingInc x
|
||||
pendingDec := fun x => if x = old then s.pendingDec x + 1 else s.pendingDec x }
|
||||
|
||||
/-- **No Lost Object Theorem**: If thread `t` holds a stack ref to `a` and
|
||||
executes `a.field = b` (replacing old), then `b` is reachable afterward.
|
||||
|
||||
This is why the "lost object" problem from concurrent GC literature
|
||||
doesn't arise in YRC: the atomic store makes `a→b` visible immediately,
|
||||
and `a` is anchored (thread `t` holds it), so scanBlack traces `a→b`
|
||||
and rescues `b`. -/
|
||||
theorem no_lost_object (s : State) (t : Thread) (a old b : Obj)
|
||||
(h_root_a : s.roots t a) :
|
||||
Reachable (writeBarrier s a old b) b := by
|
||||
apply Reachable.step a b
|
||||
· exact Reachable.root t a h_root_a
|
||||
· simp [writeBarrier]
|
||||
|
||||
/-! ### Non-atomic write barrier window safety
|
||||
|
||||
The write barrier does three steps non-atomically:
|
||||
1. atomicStore(dest, src) — graph update
|
||||
2. buffer inc(src) — deferred
|
||||
3. buffer dec(old) — deferred
|
||||
|
||||
If the collector runs between steps 1 and 2 (inc not yet buffered):
|
||||
- src has a new incoming heap edge not yet reflected in RCs
|
||||
- But src is reachable from the mutator's stack (mutator held a ref to store it)
|
||||
- So src has an external ref → trialRC ≥ 1 → scanBlack rescues src ✓
|
||||
|
||||
If the collector runs between steps 2 and 3 (dec not yet buffered):
|
||||
- old's RC is inflated by 1 (the dec hasn't arrived)
|
||||
- This is conservative: old appears to have more refs than it does
|
||||
- Trial deletion won't spuriously free it ✓
|
||||
-/
|
||||
|
||||
/-- Model the state between steps 1-2: graph updated, inc not yet buffered.
|
||||
`src` has new edge but RC doesn't reflect it yet. -/
|
||||
def stateAfterStore (s : State) (a old src : Obj) : State :=
|
||||
{ s with
|
||||
edges := fun x y =>
|
||||
if x = a ∧ y = src then True
|
||||
else if x = a ∧ y = old then False
|
||||
else s.edges x y }
|
||||
|
||||
/-- Even in the window between atomic store and buffered inc,
|
||||
src is still reachable (from the mutator's stack via a→src). -/
|
||||
theorem src_reachable_in_window (s : State) (t : Thread) (a old src : Obj)
|
||||
(h_root_a : s.roots t a) :
|
||||
Reachable (stateAfterStore s a old src) src := by
|
||||
apply Reachable.step a src
|
||||
· exact Reachable.root t a h_root_a
|
||||
· simp [stateAfterStore]
|
||||
|
||||
/-- Therefore src is anchored in the window → collector won't free it. -/
|
||||
theorem src_safe_in_window (s : State) (t : Thread) (a old src : Obj)
|
||||
(h_root_a : s.roots t a) :
|
||||
¬ collectorFrees (stateAfterStore s a old src) src := by
|
||||
intro h_freed
|
||||
exact h_freed (reachable_is_anchored _ _ (src_reachable_in_window s t a old src h_root_a))
|
||||
|
||||
/-! ### Deadlock freedom
|
||||
|
||||
YRC uses three classes of locks:
|
||||
• gYrcGlobalLock (level 0)
|
||||
• stripes[i].lockInc (level 2*i + 1, for i in 0..N-1)
|
||||
• stripes[i].lockDec (level 2*i + 2, for i in 0..N-1)
|
||||
|
||||
Total order: global < lockInc[0] < lockDec[0] < lockInc[1] < lockDec[1] < ...
|
||||
|
||||
Every code path in yrc.nim acquires locks in strictly ascending level order:
|
||||
|
||||
**nimIncRefCyclic** (mutator fast path):
|
||||
acquire lockInc[myStripe] → release → done.
|
||||
Holds exactly one lock. ✓
|
||||
|
||||
**nimIncRefCyclic** (overflow path):
|
||||
acquire gYrcGlobalLock (level 0), then for i=0..N-1: acquire lockInc[i] → release.
|
||||
Ascending: 0 < 1 < 3 < 5 < ... ✓
|
||||
|
||||
**nimDecRefIsLastCyclic{Dyn,Static}** (fast path):
|
||||
acquire lockDec[myStripe] → release → done.
|
||||
Holds exactly one lock. ✓
|
||||
|
||||
**nimDecRefIsLastCyclic{Dyn,Static}** (overflow path):
|
||||
calls collectCycles → acquire gYrcGlobalLock (level 0),
|
||||
then mergePendingRoots which for i=0..N-1:
|
||||
acquire lockInc[i] → release, acquire lockDec[i] → release.
|
||||
Ascending: 0 < 1 < 2 < 3 < 4 < ... ✓
|
||||
|
||||
**collectCycles / GC_runOrc** (collector):
|
||||
acquire gYrcGlobalLock (level 0),
|
||||
then mergePendingRoots (same ascending pattern as above). ✓
|
||||
|
||||
**nimAsgnYrc / nimSinkYrc** (write barrier):
|
||||
Calls nimIncRefCyclic then nimDecRefIsLastCyclic*.
|
||||
Each call acquires and releases its lock independently.
|
||||
No nesting between the two calls. ✓
|
||||
|
||||
Since every path follows the total order, deadlock is impossible.
|
||||
-/
|
||||
|
||||
/-- Lock levels in YRC. Each lock maps to a unique natural number. -/
|
||||
inductive LockId (n : Nat) where
|
||||
| global : LockId n
|
||||
| lockInc (i : Nat) (h : i < n) : LockId n
|
||||
| lockDec (i : Nat) (h : i < n) : LockId n
|
||||
|
||||
/-- The level (priority) of each lock in the total order. -/
|
||||
def lockLevel {n : Nat} : LockId n → Nat
|
||||
| .global => 0
|
||||
| .lockInc i _ => 2 * i + 1
|
||||
| .lockDec i _ => 2 * i + 2
|
||||
|
||||
/-- All lock levels are distinct (the level function is injective). -/
|
||||
theorem lockLevel_injective {n : Nat} (a b : LockId n)
|
||||
(h : lockLevel a = lockLevel b) : a = b := by
|
||||
cases a with
|
||||
| global =>
|
||||
cases b with
|
||||
| global => rfl
|
||||
| lockInc j hj => simp [lockLevel] at h
|
||||
| lockDec j hj => simp [lockLevel] at h
|
||||
| lockInc i hi =>
|
||||
cases b with
|
||||
| global => simp [lockLevel] at h
|
||||
| lockInc j hj =>
|
||||
have : i = j := by simp [lockLevel] at h; omega
|
||||
subst this; rfl
|
||||
| lockDec j hj => simp [lockLevel] at h; omega
|
||||
| lockDec i hi =>
|
||||
cases b with
|
||||
| global => simp [lockLevel] at h
|
||||
| lockInc j hj => simp [lockLevel] at h; omega
|
||||
| lockDec j hj =>
|
||||
have : i = j := by simp [lockLevel] at h; omega
|
||||
subst this; rfl
|
||||
|
||||
/-- Helper: stripe lock levels are strictly ascending across stripes. -/
|
||||
theorem stripe_levels_ascending (i : Nat) :
|
||||
2 * i + 1 < 2 * i + 2 ∧ 2 * i + 2 < 2 * (i + 1) + 1 := by
|
||||
constructor <;> omega
|
||||
|
||||
/-- lockInc levels are strictly ascending with index. -/
|
||||
theorem lockInc_level_strict_mono {n : Nat} (i j : Nat) (hi : i < n) (hj : j < n)
|
||||
(hij : i < j) : lockLevel (.lockInc i hi : LockId n) < lockLevel (.lockInc j hj) := by
|
||||
simp [lockLevel]; omega
|
||||
|
||||
/-- lockDec levels are strictly ascending with index. -/
|
||||
theorem lockDec_level_strict_mono {n : Nat} (i j : Nat) (hi : i < n) (hj : j < n)
|
||||
(hij : i < j) : lockLevel (.lockDec i hi : LockId n) < lockLevel (.lockDec j hj) := by
|
||||
simp [lockLevel]; omega
|
||||
|
||||
/-- Global lock has the lowest level (level 0). -/
|
||||
theorem global_level_min {n : Nat} (l : LockId n) (h : l ≠ .global) :
|
||||
lockLevel (.global : LockId n) < lockLevel l := by
|
||||
cases l with
|
||||
| global => exact absurd rfl h
|
||||
| lockInc i hi => simp [lockLevel]
|
||||
| lockDec i hi => simp [lockLevel]
|
||||
|
||||
/-- **Deadlock Freedom**: Any sequence of lock acquisitions that follows the
|
||||
"acquire in ascending level order" discipline cannot deadlock.
|
||||
|
||||
This is a standard result: a total order on locks with the invariant that
|
||||
every thread acquires locks in strictly ascending order prevents cycles
|
||||
in the wait-for graph, which is necessary and sufficient for deadlock.
|
||||
|
||||
We prove the 2-thread case (the general N-thread case follows by the
|
||||
same transitivity argument on the wait-for cycle). -/
|
||||
theorem no_deadlock_from_total_order {n : Nat}
|
||||
-- Two threads each hold a lock and wait for another
|
||||
(held₁ waited₁ held₂ waited₂ : LockId n)
|
||||
-- Thread 1 holds held₁ and wants waited₁ (ascending order)
|
||||
(h1 : lockLevel held₁ < lockLevel waited₁)
|
||||
-- Thread 2 holds held₂ and wants waited₂ (ascending order)
|
||||
(h2 : lockLevel held₂ < lockLevel waited₂)
|
||||
-- Deadlock requires: thread 1 waits for what thread 2 holds,
|
||||
-- and thread 2 waits for what thread 1 holds
|
||||
(h_wait1 : waited₁ = held₂)
|
||||
(h_wait2 : waited₂ = held₁) :
|
||||
False := by
|
||||
subst h_wait1; subst h_wait2
|
||||
omega
|
||||
|
||||
/-! ### Summary of verified properties (all QED, no sorry)
|
||||
|
||||
1. `reachable_is_anchored`: Every reachable object is anchored
|
||||
(has a path from an externally-referenced object via heap edges).
|
||||
|
||||
2. `yrc_safety`: The collector only frees unanchored objects,
|
||||
which are unreachable by all threads. **No use-after-free.**
|
||||
|
||||
3. `no_lost_object`: After `a.field = b`, `b` is reachable
|
||||
(atomic store makes the edge visible immediately).
|
||||
|
||||
4. `src_safe_in_window`: Even between the atomic store and
|
||||
the buffered inc, the collector cannot free src.
|
||||
|
||||
5. `lockLevel_injective`: All lock levels are distinct (well-defined total order).
|
||||
|
||||
6. `global_level_min`: The global lock has the lowest level.
|
||||
|
||||
7. `lockInc_level_strict_mono`, `lockDec_level_strict_mono`:
|
||||
Stripe locks are strictly ordered by index.
|
||||
|
||||
8. `no_deadlock_from_total_order`: A 2-thread deadlock cycle is impossible
|
||||
when both threads acquire locks in ascending level order.
|
||||
|
||||
Together these establish that YRC's write barrier protocol
|
||||
(atomic store → buffer inc → buffer dec) is safe under concurrent
|
||||
collection, and the locking discipline prevents deadlock.
|
||||
|
||||
## What is NOT proved: Completeness (liveness)
|
||||
|
||||
This proof covers **safety** (no use-after-free) and **deadlock-freedom**,
|
||||
but does NOT prove **completeness** — that all garbage cycles are eventually
|
||||
collected.
|
||||
|
||||
Completeness depends on the trial deletion algorithm (Bacon 2001) correctly
|
||||
identifying closed cycles. Specifically it requires proving:
|
||||
|
||||
1. After `mergePendingRoots`, merged RCs equal logical RCs
|
||||
(buffered inc/dec exactly compensate graph changes since last merge).
|
||||
2. `markGray` subtracts exactly the internal (heap→heap) edge count from
|
||||
each node's merged RC, yielding `trialRC(x) = externalRefCount(x)`.
|
||||
3. `scan` correctly partitions: nodes with `trialRC ≥ 0` are rescued by
|
||||
`scanBlack`; nodes with `trialRC < 0` remain white.
|
||||
4. White nodes form closed subgraphs with zero external refs → garbage.
|
||||
|
||||
These properties follow from the well-known Bacon trial-deletion algorithm
|
||||
and are assumed here rather than re-proved. The YRC-specific contribution
|
||||
(buffered RCs, striped queues, concurrent mutators) is what our safety
|
||||
proof covers — showing that concurrency does not break the preconditions
|
||||
that trial deletion relies on (physical graph consistency, eventual RC
|
||||
consistency after merge).
|
||||
|
||||
Reference: D.F. Bacon and V.T. Rajan, "Concurrent Cycle Collection in
|
||||
Reference Counted Systems", ECOOP 2001.
|
||||
-/
|
||||
98
tests/yrc/tyrc_cas_race.nim
Normal file
98
tests/yrc/tyrc_cas_race.nim
Normal file
@@ -0,0 +1,98 @@
|
||||
discard """
|
||||
cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
|
||||
output: "ok"
|
||||
valgrind: "leaks"
|
||||
disabled: "windows"
|
||||
disabled: "freebsd"
|
||||
disabled: "openbsd"
|
||||
"""
|
||||
|
||||
# Test concurrent traversal and mutation of a shared cyclic list under YRC.
|
||||
# Multiple threads race to replace nodes using a lock for synchronization.
|
||||
# This exercises YRC's write barrier and cycle collection under contention.
|
||||
|
||||
import std/locks
|
||||
|
||||
type
|
||||
Node = ref object
|
||||
value: int
|
||||
next: Node
|
||||
|
||||
proc newCycle(start, count: int): Node =
|
||||
result = Node(value: start)
|
||||
var cur = result
|
||||
for i in 1..<count:
|
||||
cur.next = Node(value: start + i)
|
||||
cur = cur.next
|
||||
cur.next = result # close the cycle
|
||||
|
||||
proc sumCycle(head: Node; count: int): int =
|
||||
var cur = head
|
||||
for i in 0..<count:
|
||||
result += cur.value
|
||||
cur = cur.next
|
||||
|
||||
const
|
||||
NumThreads = 4
|
||||
CycleLen = 6
|
||||
Iterations = 50
|
||||
|
||||
var
|
||||
shared: Node
|
||||
sharedLock: Lock
|
||||
threads: array[NumThreads, Thread[int]]
|
||||
wins: array[NumThreads, int]
|
||||
|
||||
proc worker(id: int) {.thread.} =
|
||||
{.cast(gcsafe).}:
|
||||
for iter in 0..<Iterations:
|
||||
# Under the lock, walk the shared list and replace a node's next pointer
|
||||
withLock sharedLock:
|
||||
var cur = shared
|
||||
if cur == nil: continue
|
||||
for step in 0..<CycleLen:
|
||||
let nxt = cur.next
|
||||
if nxt == nil: break
|
||||
# Replace cur.next with a fresh node that points to nxt.next
|
||||
let replacement = Node(value: id * 1000 + iter, next: nxt.next)
|
||||
cur.next = replacement
|
||||
wins[id] += 1
|
||||
cur = cur.next
|
||||
if cur == nil: break
|
||||
|
||||
# Outside the lock, create a local cycle to exercise the collector
|
||||
let local = newCycle(id * 100 + iter, 3)
|
||||
discard sumCycle(local, 3)
|
||||
|
||||
# Create initial shared cyclic list: 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 0
|
||||
initLock(sharedLock)
|
||||
shared = newCycle(0, CycleLen)
|
||||
|
||||
for i in 0..<NumThreads:
|
||||
createThread(threads[i], worker, i)
|
||||
|
||||
for i in 0..<NumThreads:
|
||||
joinThread(threads[i])
|
||||
|
||||
# Verify: the list is still traversable (no crashes, no dangling pointers).
|
||||
var totalWins = 0
|
||||
for i in 0..<NumThreads:
|
||||
totalWins += wins[i]
|
||||
|
||||
# Walk the list to verify it's still a valid cycle (or chain)
|
||||
var cur = shared
|
||||
var seen = 0
|
||||
var maxSteps = CycleLen * 3 # generous bound
|
||||
while cur != nil and seen < maxSteps:
|
||||
seen += 1
|
||||
cur = cur.next
|
||||
if cur == shared: break # completed the cycle
|
||||
|
||||
shared = nil
|
||||
GC_fullCollect()
|
||||
deinitLock(sharedLock)
|
||||
|
||||
if totalWins > 0 and seen > 0:
|
||||
echo "ok"
|
||||
else:
|
||||
echo "FAIL: wins=", totalWins, " seen=", seen
|
||||
74
tests/yrc/tyrc_shared_cycle.nim
Normal file
74
tests/yrc/tyrc_shared_cycle.nim
Normal file
@@ -0,0 +1,74 @@
|
||||
discard """
|
||||
cmd: "nim c --mm:yrc -d:useMalloc --threads:on $file"
|
||||
output: "ok"
|
||||
valgrind: "leaks"
|
||||
disabled: "windows"
|
||||
disabled: "freebsd"
|
||||
disabled: "openbsd"
|
||||
"""
|
||||
|
||||
# Test sharing a cyclic list between threads under YRC.
|
||||
|
||||
type
|
||||
Node = ref object
|
||||
value: int
|
||||
next: Node
|
||||
|
||||
proc newCycle(start, count: int): Node =
|
||||
## Create a cyclic linked list: start -> start+1 -> ... -> start+count-1 -> start
|
||||
result = Node(value: start)
|
||||
var cur = result
|
||||
for i in 1..<count:
|
||||
cur.next = Node(value: start + i)
|
||||
cur = cur.next
|
||||
cur.next = result # close the cycle
|
||||
|
||||
proc sumCycle(head: Node; count: int): int =
|
||||
var cur = head
|
||||
for i in 0..<count:
|
||||
result += cur.value
|
||||
cur = cur.next
|
||||
|
||||
const
|
||||
NumThreads = 4
|
||||
NodesPerCycle = 5
|
||||
|
||||
var
|
||||
shared: Node
|
||||
threads: array[NumThreads, Thread[int]]
|
||||
results: array[NumThreads, int]
|
||||
|
||||
proc worker(id: int) {.thread.} =
|
||||
# Each thread reads the shared cycle and computes a sum.
|
||||
# Also creates its own local cycle to exercise the collector.
|
||||
{.cast(gcsafe).}:
|
||||
let local = newCycle(id * 100, NodesPerCycle)
|
||||
let localSum = sumCycle(local, NodesPerCycle)
|
||||
|
||||
let sharedSum = sumCycle(shared, NodesPerCycle)
|
||||
results[id] = sharedSum + localSum
|
||||
|
||||
# Create a shared cyclic list: 0 -> 1 -> 2 -> 3 -> 4 -> 0
|
||||
shared = newCycle(0, NodesPerCycle)
|
||||
let expectedSharedSum = 0 + 1 + 2 + 3 + 4 # = 10
|
||||
|
||||
for i in 0..<NumThreads:
|
||||
createThread(threads[i], worker, i)
|
||||
|
||||
for i in 0..<NumThreads:
|
||||
joinThread(threads[i])
|
||||
|
||||
var allOk = true
|
||||
for i in 0..<NumThreads:
|
||||
let expectedLocal = i * 100 * NodesPerCycle + (NodesPerCycle * (NodesPerCycle - 1) div 2)
|
||||
# sum of id*100, id*100+1, ..., id*100+4
|
||||
let expected = expectedSharedSum + expectedLocal
|
||||
if results[i] != expected:
|
||||
echo "FAIL thread ", i, ": got ", results[i], " expected ", expected
|
||||
allOk = false
|
||||
|
||||
shared = nil # drop the shared cycle, collector should reclaim it
|
||||
GC_fullCollect()
|
||||
|
||||
if allOk:
|
||||
echo "ok"
|
||||
Reference in New Issue
Block a user