diff --git a/.gitmodules b/.gitmodules index 363c3a8..d944500 100644 --- a/.gitmodules +++ b/.gitmodules @@ -16,3 +16,6 @@ [submodule "benchmarks/vendor/mkl-dnn"] path = benchmarks/vendor/mkl-dnn url = https://github.com/intel/mkl-dnn +[submodule "thread_collider/greenlet"] + path = thread_collider/greenlet + url = https://github.com/treeform/greenlet diff --git a/tests/README.md b/tests/README.md new file mode 100644 index 0000000..a15c129 --- /dev/null +++ b/tests/README.md @@ -0,0 +1,60 @@ +# Testing + +Tests are done at the end of Weave files in an `when isMainModule` block +and also by running the benchmarks and ensuring: +- no deadlocks or livelocks +- ensuring correct result + +## Debugging tools + +Weave has intentionally a very restricted set of cross-thread synchronization data structures. +Data races can only appear in them, those are the `cross_thread_com` folder and includes: +- 3 kinds of channels to transfer tasks, steal requests, and result (==Future) between threads +- An event notifier to wake up sleeping threads (formally verified! which also uncovered a deadlock bug in glibc) +- Pledges (~Promises that can have delayed tasks triggered on fulfillment) +- Scoped barriers (to await all tasks and descendant tasks in a scope) + +Some useful commands + +### LLVM ThreadSanitizer + +https://clang.llvm.org/docs/ThreadSanitizer.html + +``` +nim c -r -d:danger --passC:"-fsanitize=thread" --passL:"-fsanitize=thread" --debugger:native --cc:clang --outdir:build weave/cross_thread_com/channels_spsc_single_ptr.nim +``` + +### Valgrind Helgrind + +https://valgrind.org/docs/manual/hg-manual.html + +``` +nim c -r -d:danger --debugger:native --cc:clang --outdir:build weave/cross_thread_com/channels_spsc_single_ptr.nim +valgrind --tool=helgrind build/channels_spsc_single_ptr +``` + +### Valgrind Data Race Detection + +https://valgrind.org/docs/manual/drd-manual.html + +``` +nim c -r -d:danger --debugger:native --cc:clang --outdir:build weave/cross_thread_com/channels_spsc_single_ptr.nim +valgrind --tool=drd build/channels_spsc_single_ptr +``` + +## Formal verification + +Formal verification is the most powerful tool to prove that an concurrent data structure or a synchronization primitive has a sound design. +An example using TLA (Temporal logic of Action) is available in the formal_verification folder. + +See Leslie Lamport page on TLA, usage and use-cases: https://lamport.azurewebsites.net/tla/tla.html + +However while proving design is sound is great, we also need to prove that the implementation is bug-free. +This needs a model-checking tool that is aware of C11/C++11 memory model (i.e. relaxed, acquire, release) atomics and fences. + +This is planned. + +## Research + +Research into data race detection, sanitiziers, model checking and formal verification for concurrency +is gathered here: https://github.com/mratsim/weave/issues/18 diff --git a/thread_collider/README.md b/thread_collider/README.md new file mode 100644 index 0000000..6121c52 --- /dev/null +++ b/thread_collider/README.md @@ -0,0 +1,20 @@ +# Thread Collider + +Thread Collider is a [formal verification](https://en.wikipedia.org/wiki/Formal_verification) tool +to highlight concurrency bugs in Nim multithreaded programs and data structures. + +It uses [Model Checking](https://en.wikipedia.org/wiki/Model_checking) techniques to exhaustively investigate +all possible interleavings (if it has enough time) of your threads and variable states +and ensure that your assumptions, represented by asserts or liveness properties (no deadlocks/livelocks), +holds in a concurrent environment. + +Thread Collider has been designed with the C11/C++11 memory model in my mind. It is aware of relaxed memory semantics +and can detect races that involve atomic variables and fences that involves relaxed, acquire and release synchronization semantics. + +## References + +- RFC: Correct-by-Construction Nim programs\ + https://github.com/nim-lang/RFCs/issues/222 + +- \[Testing\] Concurrency: Race detection / Model Checking / Formal Verification\ + https://github.com/mratsim/weave/issues/18 diff --git a/thread_collider/collider_common.nim b/thread_collider/collider_common.nim new file mode 100644 index 0000000..4c6fa25 --- /dev/null +++ b/thread_collider/collider_common.nim @@ -0,0 +1,46 @@ +# Thread Collider +# Copyright (c) 2020 Mamy André-Ratsimbazafy +# Licensed and distributed under either of +# * MIT license (license terms in the root directory or at http://opensource.org/licenses/MIT). +# * Apache v2 license (license terms in the root directory or at http://www.apache.org/licenses/LICENSE-2.0). +# at your option. This file may not be copied, modified, or distributed except according to those terms. + +static: doAssert defined(i386) or defined(amd64), "Thread Collider requires an x86 or x86_64 CPU at the moment." + # Constrained by Greenlet/Fibers that are only x86. + +# Common types +# ---------------------------------------------------------------------------------- + +type + ThreadID* = distinct int8 + +# ThreadID +# ---------------------------------------------------------------------------------- + +const MaxThreads* {.intdefine.} = 4 +static: doAssert MaxThreads <= high(int8) + +var thread_count: ThreadID + +proc inc(tid: var ThreadID){.borrow.} +proc `$`*(tid: ThreadID): string {.borrow.} + +proc genUniqueThreadID*(): ThreadID = + result = thread_count + thread_count.inc() + +# Compiler reordering barrier +# ---------------------------------------------------------------------------------- +# This prevents the compiler for reordering instructions +# which locks and non-relaxed atomics do (and function calls so we could use non-inline functions) + +const someGcc = defined(gcc) or defined(llvm_gcc) or defined(clang) +const someVcc = defined(vcc) or defined(clang_cl) + +when someVcc: + proc compilerReorderingBarrier*(){.importc: "_ReadWriteBarrier", header: "".} +elif someGcc or defined(tcc): + proc compilerReorderingBarrier*(){.inline.} = + {.emit: """asm volatile("" ::: "memory");""".} +else: + {.error: "Unsupported compiler".} diff --git a/thread_collider/greenlet b/thread_collider/greenlet new file mode 160000 index 0000000..aed081c --- /dev/null +++ b/thread_collider/greenlet @@ -0,0 +1 @@ +Subproject commit aed081c38be407fa94cb3e05028c989722c4611d diff --git a/thread_collider/modeling/Vector_Clock.png b/thread_collider/modeling/Vector_Clock.png new file mode 100644 index 0000000..1b61d63 Binary files /dev/null and b/thread_collider/modeling/Vector_Clock.png differ diff --git a/thread_collider/modeling/colliders.nim b/thread_collider/modeling/colliders.nim new file mode 100644 index 0000000..68198b2 --- /dev/null +++ b/thread_collider/modeling/colliders.nim @@ -0,0 +1,28 @@ +# Thread Collider +# Copyright (c) 2020 Mamy André-Ratsimbazafy +# Licensed and distributed under either of +# * MIT license (license terms in the root directory or at http://opensource.org/licenses/MIT). +# * Apache v2 license (license terms in the root directory or at http://www.apache.org/licenses/LICENSE-2.0). +# at your option. This file may not be copied, modified, or distributed except according to those terms. + +import + ../[shadow, collider_common] + +# Collider +# ---------------------------------------------------------------------------------- +# +# Note: those types are held in a global with the lifetime of the whole programs +# and should never be collected, in particular on fiber context switch + +type + Collider* = object + ## The Global Collider context + dag: DAG + scheduler: Scheduler + + Scheduler = object + threadpool: seq[ShadowThread] + + + ExecutionContext = object + diff --git a/thread_collider/modeling/directed_acyclic_graphs.nim b/thread_collider/modeling/directed_acyclic_graphs.nim new file mode 100644 index 0000000..a7b4c13 --- /dev/null +++ b/thread_collider/modeling/directed_acyclic_graphs.nim @@ -0,0 +1,13 @@ +# Thread Collider +# Copyright (c) 2020 Mamy André-Ratsimbazafy +# Licensed and distributed under either of +# * MIT license (license terms in the root directory or at http://opensource.org/licenses/MIT). +# * Apache v2 license (license terms in the root directory or at http://www.apache.org/licenses/LICENSE-2.0). +# at your option. This file may not be copied, modified, or distributed except according to those terms. + +# Directed Acyclic Graph +# ---------------------------------------------------------------------------------- + +type + DAG = object + # A direct acyclic graph of operations/events/instructions from the execution traces diff --git a/thread_collider/modeling/events.nim b/thread_collider/modeling/events.nim new file mode 100644 index 0000000..ac84bfa --- /dev/null +++ b/thread_collider/modeling/events.nim @@ -0,0 +1,43 @@ +# Thread Collider +# Copyright (c) 2020 Mamy André-Ratsimbazafy +# Licensed and distributed under either of +# * MIT license (license terms in the root directory or at http://opensource.org/licenses/MIT). +# * Apache v2 license (license terms in the root directory or at http://www.apache.org/licenses/LICENSE-2.0). +# at your option. This file may not be copied, modified, or distributed except according to those terms. + +type + EventKind* = enum + eAtomic + eFence + eLock + eCondVar + eThread + eFutex + + TransitionKind* = enum + tRead + tWrite + tFence + tLock + tFutex + tReleaseSequenceFixup + + Relation = enum + ## Formal model of C/C++11 memory model Batty et al, 2011 + SequencedBefore + ReadsFrom + SynchronizeWith + HappensBefore + SequentialConsistency + ModificationOrder + + AtomicEventKind* = enum + AtomicRead + AtomicWrite + + ReadEvent = object + reorderedLoad*: ReorderedLoad + ## Handle reordered relaxed atomics + + Event = object + loc: tuple[filename: string, line: int, column: int] diff --git a/thread_collider/modeling/reordered_loads.nim b/thread_collider/modeling/reordered_loads.nim new file mode 100644 index 0000000..56ee3cb --- /dev/null +++ b/thread_collider/modeling/reordered_loads.nim @@ -0,0 +1,72 @@ +# Thread Collider +# Copyright (c) 2020 Mamy André-Ratsimbazafy +# Licensed and distributed under either of +# * MIT license (license terms in the root directory or at http://opensource.org/licenses/MIT). +# * Apache v2 license (license terms in the root directory or at http://www.apache.org/licenses/LICENSE-2.0). +# at your option. This file may not be copied, modified, or distributed except according to those terms. + +import + ./vector_clocks + +# Reordered loads +# ---------------------------------------------------------------------------------- +# +# +# Motivating example +# ```Nim +# var x {.noInit.}, y {.noInit.}: Atomic[int32] +# x.store(0, moRelaxed) +# y.store(0, moRelaxed) +# +# proc threadA() = +# let r1 = y.load(moRelaxed) +# x.store(1, moRelaxed) +# echo "r1 = ", r1 +# +# proc threadA() = +# let r2 = x.load(moRelaxed) +# y.store(1, moRelaxed) +# echo "r2 = ", r2 +# +# spawn threadA() +# spawn threadB() +# ``` +# +# It is possible to have r1 = 1 and r2 = 1 for this program, +# contrary to first intuition. +# +# I.e. we can see that before setting one of x or y to 1 +# a load at least must have happened, and so those load should be 0. +# +# However, under a relaxed memory model, given that those load-store +# are on different variables, the compiler can reorder the program to: +# +# ```Nim +# var x {.noInit.}, y {.noInit.}: Atomic[int32] +# x.store(0, moRelaxed) +# y.store(0, moRelaxed) +# +# proc threadA() = +# x.store(1, moRelaxed) +# let r1 = y.load(moRelaxed) +# echo "r1 = ", r1 +# +# proc threadA() = +# y.store(1, moRelaxed) +# let r2 = x.load(moRelaxed) +# echo "r2 = ", r2 +# +# spawn threadA() +# spawn threadB() +# ``` +# +# And so we need to introduce a read from reordered loads + +type + ReorderedValue = object + value: uint64 + expiry: VectorClock + srcThread: ThreadID + + ReorderedLoad* = ref object + rv: ReorderedValue diff --git a/thread_collider/modeling/vector_clocks.nim b/thread_collider/modeling/vector_clocks.nim new file mode 100644 index 0000000..823da7d --- /dev/null +++ b/thread_collider/modeling/vector_clocks.nim @@ -0,0 +1,251 @@ +# Thread Collider +# Copyright (c) 2020 Mamy André-Ratsimbazafy +# Licensed and distributed under either of +# * MIT license (license terms in the root directory or at http://opensource.org/licenses/MIT). +# * Apache v2 license (license terms in the root directory or at http://www.apache.org/licenses/LICENSE-2.0). +# at your option. This file may not be copied, modified, or distributed except according to those terms. + +import + std/tables, + ../collider_common + +# Vector Clocks +# ---------------------------------------------------------------------------------- + +# Vector Clocks is an algorithm for generating +# a partial ordering of events in a distributed system +# and detecting causality violations. +# +# They are an evolution of Lamport's Timestamps described +# - Time, Clocks and the Ordering of Events in a Distributed System +# Leslie Lamport, 1978 +# https://amturing.acm.org/p558-lamport.pdf +# +# - Timestamps in Message-Passing Systems That Preserve the Partial Ordering +# Colin J Fidge, 1988 +# https://zoo.cs.yale.edu/classes/cs426/2012/lab/bib/fidge88timestamps.pdf +# +# - Virtual Time and Global States of Distributed Systems +# Friedemann Mattern, 1988 +# https://www.vs.inf.ethz.ch/publ/papers/VirtTimeGlobStates.pdf +# +# - Distributed Testing of Concurrent Systems: Vector Clocks to the Rescue +# Hernàn Ponce-de-Léon, Stefan Haar, and Delphine Longuet, 2014 +# http://www.lsv.fr/Publis/PAPERS/PDF/PHL-ictac14.pdf +# +# - Encoded Vector Clock: Using Primes to Characterize Causalityin Distributed Systems +# Ajay D. Kshemkalyani, Ashfaq Khokhar, Min Shen +# https://www.cs.uic.edu/~ajayk/ext/icdcn18_paper19.pdf +# +# - Resettable Encoded Vector Clock for Causality Analysis +# with an Application to Dynamic Race Detection +# Tommasso Pozzetti, 2017 +# https://webthesis.biblio.polito.it/12434/1/tesi.pdf +# +# Via a vector of 1 timestamp you can answer the following questions on event ordering / causality: +# - happensBefore? +# - concurrent? +# - impossible? +# +# Logical instructions +# - increment the threadlocal timestamp to represent one thread moving ahead +# - and/or merging two vector clocks to represent 2 threads synchronizing. +# +# However classic VectorClocks are quite bulky. +# They would require seq[TimeStamp] at least (if threads are initialized at once before +# any "interesting" concurrency event) +# or Table[ThreadID, Timestamp] if we want a generic race detection tool that can +# work with threads spawned at any time. +# But Table hashing and the required pointer dereference is an overhead that might prove quite high +# given how many states have to be checked in a concurrent system, +# in particular multi-producer multi-consumer data structures +# +# Furthermore using `seq` or `Table` means involving the GC which is a potential source of +# bugs when working with fibers. +# +# Unfortunately: +# - Encoded Vector Clock have an issue with timestamp growth which is exponential, and may require dynamic allocation +# - Resettable Encoded Vector Clock have an "horizon" of past event beyond which they cannot detect races +# +# So we recreate our own seq ad impose a (configurable) compile-time size to avoid dynamic allocation + +type + Timestamp* = distinct int64 + + CausalOrdering* = enum + ## The ordering relation of 2 distributed events + ## according to their Vector Clock. + ## + ## 2 events are concurrent when their observed timestamps are in "conflict" + ## And we can't deduce a total ordering. + Identical + HappenedBefore + HappenedAfter + Concurrent + + VectorClock* = object + ## A vector clock tracks the partial ordering of event in a distributed system. + ## 2 clocks can be compared to check if + ## - 1 event must have happened before the other + ## - They could happen concurrently + ## - They violate the laws of causality + ## + ## The length is the number of processes/threads tracked + ## The array of known local timestamps is indexed by the threadID (< len) + localTS: array[MaxThreads, Timestamp] + len: int8 + +proc inc(time: var Timestamp){.borrow.} +proc `$`*(time: Timestamp): string {.borrow.} +proc `<`*(a, b: Timestamp): bool {.borrow.} +proc `==`*(a, b: Timestamp): bool {.borrow.} + +proc init*(clock: var VectorClock) {.inline.} = + ## Initialize a vector clock + zeroMem(clock.addr, sizeof(clock)) + +func tick*(clock: var VectorClock, tid: ThreadID) {.inline.}= + ## Local tick in thread `tid` + if int8(tid) > clock.len: + clock.len = int8(tid) + 1 + clock.localTS[tid.int].inc() + +func synchronize*(a: var VectorClock, b: VectorClock) {.inline.}= + ## Synchronize clock `a` with clock `b` + if b.len > a.len: + a.len = b.len + for i in 0 ..< a.len: + if a.localTS[i] < b.localTS[i]: + a.localTS[i] = b.localTS[i] + +func causality*(a, b: VectorClock): CausalOrdering = + ## Returns the causal order between 2 vector clocks + + result = Identical + for i in 0 ..< MaxThreads: + let tsA = a.localTS[i] + let tsB = b.localTS[i] + + if tsA == tsB: + continue + elif tsA < tsB: + if result == HappenedAfter: + return Concurrent + result = HappenedBefore + else: + if result == HappenedBefore: + return Concurrent + result = HappenedAfter + # return Identical + +# -------------------------------------------------------------------------------- +# Sanity checks + +when isMainModule: + import random + + proc clock[N: static int](a: array[N, int]): VectorClock = + static: doAssert N <= MaxThreads + result.len = N.int8 + for i in 0 ..< N: + result.localTS[i] = TimeStamp(a[i]) + + proc randomClock(rng: var Rand, N: static int): VectorClock = + static: doAssert N <= MaxThreads + result.len = N.int8 + for i in 0 ..< N: + result.localTS[i] = TimeStamp(rng.rand(high(int))) + + proc causality[N: static int](a, b: array[N, int]): CausalOrdering = + clock(a).causality(clock(b)) + + proc test_causality() = + # From https://en.wikipedia.org/wiki/Vector_clock#/media/File:Vector_Clock.svg + + doAssert causality([0, 0, 0], [0, 0, 1]) == HappenedBefore + doAssert causality([0, 0, 1], [0, 1, 1]) == HappenedBefore + doAssert causality([0, 1, 1], [0, 2, 1]) == HappenedBefore + doAssert causality([0, 2, 1], [1, 2, 1]) == HappenedBefore + doAssert causality([1, 2, 1], [2, 2, 1]) == HappenedBefore + + doAssert causality([0, 2, 1], [0, 3, 1]) == HappenedBefore + doAssert causality([0, 3, 1], [0, 3, 2]) == HappenedBefore + doAssert causality([2, 2, 1], [2, 4, 1]) == HappenedBefore + doAssert causality([0, 3, 1], [2, 4, 1]) == HappenedBefore + + doAssert causality([0, 3, 2], [0, 3, 3]) == HappenedBefore + doAssert causality([2, 4, 1], [2, 5, 1]) == HappenedBefore + doAssert causality([0, 3, 3], [3, 3, 3]) == HappenedBefore + doAssert causality([2, 5, 1], [2, 5, 4]) == HappenedBefore + doAssert causality([0, 3, 3], [2, 5, 4]) == HappenedBefore + + doAssert causality([2, 5, 4], [2, 5, 5]) == HappenedBefore + doAssert causality([3, 3, 3], [4, 5, 5]) == HappenedBefore + doAssert causality([2, 5, 5], [4, 5, 5]) == HappenedBefore + + echo "Causality tests - Happened before - SUCCESS" + + # -------------------------------------------------------- + + doAssert causality([0, 3, 1], [1, 2, 1]) == Concurrent + doAssert causality([0, 3, 1], [2, 2, 1]) == Concurrent + doAssert causality([1, 2, 1], [0, 3, 1]) == Concurrent + doAssert causality([2, 2, 1], [0, 3, 1]) == Concurrent + + doAssert causality([2, 4, 1], [0, 3, 2]) == Concurrent + doAssert causality([2, 5, 1], [0, 3, 2]) == Concurrent + doAssert causality([2, 4, 1], [0, 3, 3]) == Concurrent + doAssert causality([2, 5, 1], [0, 3, 3]) == Concurrent + + doAssert causality([3, 3, 3], [2, 5, 4]) == Concurrent + doAssert causality([3, 3, 3], [2, 5, 5]) == Concurrent + + doAssert causality([3, 3, 3], [2, 4, 1]) == Concurrent + doAssert causality([3, 3, 3], [2, 5, 1]) == Concurrent + + doAssert causality([0, 3, 2], [1, 2, 1]) == Concurrent + doAssert causality([0, 3, 2], [2, 2, 1]) == Concurrent + doAssert causality([2, 2, 1], [0, 3, 3]) == Concurrent + + echo "Causality tests - Concurrency - SUCCESS" + + proc test_invariants(numTests: int) = + var rng = initRand(seed = numTests) + for _ in 0 ..< numTests: + let + A = rng.randomClock(3) + B = rng.randomClock(3) + C = rng.randomClock(3) + + let rel_A_B = causality(A, B) + let rel_B_C = causality(B, C) + let rel_A_C = causality(A, C) + + if rel_A_B == Identical: + # Transitivity + doAssert rel_B_C == rel_A_C + elif rel_A_B == HappenedBefore: + if rel_B_C == HappenedBefore: + # Transitivity + doAssert rel_A_C == HappenedBefore + elif rel_A_B == HappenedAfter: + if rel_B_C == HappenedAfter: + # Transitivity + doAssert rel_A_C == HappenedAfter + + let rel_B_A = causality(B, A) + + case rel_A_B + of Identical: + doAssert rel_B_A == Identical + of HappenedBefore: + doAssert rel_B_A == HappenedAfter + of HappenedAfter: + doAssert rel_B_A == HappenedBefore + of Concurrent: + doAssert rel_B_A == Concurrent + + echo "Invariants tests - Transitivity & Commutativity - SUCCESS" + + test_causality() + test_invariants(10000) diff --git a/thread_collider/shadow.nim b/thread_collider/shadow.nim new file mode 100644 index 0000000..3be5070 --- /dev/null +++ b/thread_collider/shadow.nim @@ -0,0 +1,14 @@ +# Thread Collider +# Copyright (c) 2020 Mamy André-Ratsimbazafy +# Licensed and distributed under either of +# * MIT license (license terms in the root directory or at http://opensource.org/licenses/MIT). +# * Apache v2 license (license terms in the root directory or at http://www.apache.org/licenses/LICENSE-2.0). +# at your option. This file may not be copied, modified, or distributed except according to those terms. + +import + shadow/shadow_atomics + shadow/shadow_threads + +export + shadow_atomics, + shadow_threads diff --git a/thread_collider/shadow/shadow_atomics.nim b/thread_collider/shadow/shadow_atomics.nim new file mode 100644 index 0000000..76a8f7b --- /dev/null +++ b/thread_collider/shadow/shadow_atomics.nim @@ -0,0 +1,41 @@ +# Thread Collider +# Copyright (c) 2020 Mamy André-Ratsimbazafy +# Licensed and distributed under either of +# * MIT license (license terms in the root directory or at http://opensource.org/licenses/MIT). +# * Apache v2 license (license terms in the root directory or at http://www.apache.org/licenses/LICENSE-2.0). +# at your option. This file may not be copied, modified, or distributed except according to those terms. + +# Common types +# ---------------------------------------------------------------------------------- + +type + MemoryOrder* = enum + ## Specifies how non-atomic operations can be reordered around atomic + ## operations. + + moRelaxed + ## No ordering constraints. Only the atomicity and ordering against + ## other atomic operations is guaranteed. + + # moConsume + # ## This ordering is currently discouraged as it's semantics are + # ## being revised. Acquire operations should be preferred. + + moAcquire + ## When applied to a load operation, no reads or writes in the + ## current thread can be reordered before this operation. + + moRelease + ## When applied to a store operation, no reads or writes in the + ## current thread can be reorderd after this operation. + + moAcquireRelease + ## When applied to a read-modify-write operation, this behaves like + ## both an acquire and a release operation. + + moSequentiallyConsistent + ## Behaves like Acquire when applied to load, like Release when + ## applied to a store and like AcquireRelease when applied to a + ## read-modify-write operation. + ## Also guarantees that all threads observe the same total ordering + ## with other moSequentiallyConsistent operations. diff --git a/thread_collider/shadow/shadow_threads.nim b/thread_collider/shadow/shadow_threads.nim new file mode 100644 index 0000000..a95261c --- /dev/null +++ b/thread_collider/shadow/shadow_threads.nim @@ -0,0 +1,54 @@ +# Thread Collider +# Copyright (c) 2020 Mamy André-Ratsimbazafy +# Licensed and distributed under either of +# * MIT license (license terms in the root directory or at http://opensource.org/licenses/MIT). +# * Apache v2 license (license terms in the root directory or at http://www.apache.org/licenses/LICENSE-2.0). +# at your option. This file may not be copied, modified, or distributed except according to those terms. + +import ../greenlet/src/greenlet + +# Shadow threads +# ----------------------------------------------- +# We replace Nim threads by our own "threads" with the same interface + +static: doAssert not compileOption("threads"), "Thread Collider requires --threads:off to replace Nim threads" + +type + ThreadState* = enum + ## Thread state, used for reporting stack traces of interleaved thread status + # Disabled # Never scheduled + Idle # Schedulable but previous "step" was another thread + Running # Schedulable and previous step was this thread + Parked # Thread is waiting on a lock or condition variable + Terminated # Thread has been joined + + Thread*[TArg] = object + ## A Thread handle + + # Nim compat + when TArg is void: + dataFn: proc () {.nimcall, gcsafe.} + else: + dataFn: proc (m: TArg) {.nimcall, gcsafe.} + data: TArg + + # Collider + shadow: ShadowThread + + ShadowThread* = ptr object + ## Collider Metadata for athread + + # Collider + fiber*: Greenlet # A fiber to simulate a Nim Thread + id*: int # A thread unique ID + next*: Event # The next "interesting" event (lock, atomic load, fence, ...) + state*: State # The thread state + +proc createThread*[TArg](t: var Thread[TArg], + tp: proc (arg: TArg) {.thread, nimcall.}, + param: TArg) = + ## Creates a new thread `t` and starts its execution. + ## + ## Entry point is the proc `tp`. `param` is passed to `tp`. + ## `TArg` can be ``void`` if you + ## don't need to pass any data to the thread.