Skip to content

Commit

Permalink
introduce Thread Collider to solve #18 and nim-lang/RFCs#222 and repr…
Browse files Browse the repository at this point in the history
…oduce the spurious livelock/deadlock and multithreaded corruption we have in CI
  • Loading branch information
mratsim committed May 7, 2020
1 parent 4ed3291 commit 0ac8156
Showing 1 changed file with 20 additions and 0 deletions.
20 changes: 20 additions & 0 deletions thread_collider/README.md
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 0ac8156

Please sign in to comment.