[WIP] Thread Collider: Race detection / Formal Verification of Nim concurrent programs

.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

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

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

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: "<intrin.h>".}
+elif someGcc or defined(tcc):
+  proc compilerReorderingBarrier*(){.inline.} =
+    {.emit: """asm volatile("" ::: "memory");""".}
+else:
+  {.error: "Unsupported compiler".}

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
+

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

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]

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