Model Checked - MPSC queue + Rework State Machines (#128)

* model checking - 1st try to fix MPSC queue (the model checker crashes with not enough memory :/)

* Give the thread the opportunity to not deadlock on sleep on Mac/with Clang

* whoopsie

* Add impl of Weave MPSC channel in C++ for CDSChecker model checking + comment out fences

* Comment out GEMM tests for syncRoot + Pledges: #97

* don't use sleep, it's can deadlock in the CI ...

* Try get epoch time to avoid mac bugs

* use `getTime` and hope that it's properly implemented on Mac

* State-machine, return to CheckTask to avoid leaving task spawning multitasks in queue (followup #121)

* Don't spinlock for testing, deadlocks ARM and OSX

* Could it be non-mono clock jitter?

* Add some log for MacOS debug

* Race condition between spawning the thread and entering the spinlock in the `isReady` test

* a,d obviously I mess up the function call

Author: mratsim

formal_verification/README.md

@@ -0,0 +1,21 @@
+# Formal Verification
+
+To ensure that Weave synchronization data structures are free of
+concurrency bugs, deadlocks or livelocks they are formally verified via model checking.
+
+The event notifier which parks idle threads and wake them up when receiving tasks
+has been formally implemented verified via TLA+ (Temporal Logic of Action).
+
+TLA+ is an industrial-strength formal specification language, model checker and can plug into proof assistant to prove properties of code.
+It is used at Microsoft and Amazon to validate bug-free distributed protocol or at Intel to ensure that that the memory of a CPU is free of cache-coherency bugs.
+
+Link: https://lamport.azurewebsites.net/tla/tla.html
+
+
+Weave Multi-Producer Single-Consumer queue has been implemented in C++ and run through CDSChecker, a model checking tool for C++11 atomics.
+
+It exhaustively checks all possible thread interleavings to ensure that no path lead to a bug.
+
+Note: Due to CDSChecker running out of "snapshotting memory" (to rollback to a previous program state) when using dlmalloc `mspace` functions, the checks are not complete.
+
+Link: http://plrg.ics.uci.edu/software_page/42-2/