To develop Weave I took a poor man's Ada/Spark approach: `preCondition`, `postCondition`, `ascertain` [templates](https://github.com/mratsim/weave/blob/9f0c384f/weave/instrumentation/contracts.nim#L93-L103) (names cleverly chosen to not conflict with `requires` and `ensure`). Those also report the thread that triggered the logic bug and gives lineinfo, wrong value and expected value details. This has been invaluable for debugging stuff like parent task being missing. In particular Nim templates and macro tend to eat stacktraces and Weave code transformations being a heavy user of macros, lots of traces disappear.
The second thing is to embrace the rise of the State Machines. I hope that one day I can formally verify the state machines produced by [Synthesis](https://github.com/mratsim/Synthesis) but even then, having a self contained piece of code with the corresponding visual control flow / event triggers has been very useful to investigate livelocks, a situation where codepaths are mutually depending on each others (an hypothetical example would 2 threads sending the same task to each other repeatedly never actually working on it). The third has been to actually use formal verification via [TLA+](https://lamport.azurewebsites.net/tla/tla.html) proving that my algorithm (a 2-phase commit algorithm to be able to put a thread to sleep) was deadlock-free and so that the deadlocks I had on Linux (and not Windows or Mac) were due to an implementation bug in Glibc and Musl and that they went away when I used Futexes instead of locks+condition variables: see investigation at [https://github.com/mratsim/weave/issues/56](https://github.com/mratsim/weave/issues/56) Disclaimer: this is a teaser for my talk at NimConf on debugging multithreading and proving that your concurrency is correct.
