Open mratsim opened 4 years ago
Some more tools: Loom https://github.com/tokio-rs/loom
The paper it is based on: CDSChecker Checking COncurrent Data Structure written in C/C++ atomics
DataRaceBench, a benchmark of race detection tools https://github.com/LLNL/dataracebench For Helgrind, ThreadSanitizer, Archer, and Intel Inspector.
Microsoft overview: https://docs.microsoft.com/en-us/archive/msdn-magazine/2008/june/tools-and-techniques-to-identify-concurrency-issues
5 data race detection tools (for Java?): https://www.cs.uic.edu/~jalowibd/uploads/06561640_DataRace.pdf
5 others with algorithms details (java as well): https://onlinelibrary.wiley.com/doi/full/10.4218/etrij.17.0115.1027
Rex algorithm for race detction: https://drops.dagstuhl.de/opus/volltexte/2017/7272/pdf/LIPIcs-ECOOP-2017-15.pdf
Something somewhat related but for users not for the runtime: Race detection of Futures: https://arxiv.org/pdf/1901.00622.pdf
And regarding formal verification:
TLA+ was written by Leslie Lamport of the Lamport Queue and Byzantine General fame i.e. anything distributed or concurrent traces back to his foundational work. It has been used successfully at Amazon, Microsoft and Dropbox for large scale distributed system proof:
tutorial: https://lamport.azurewebsites.net/tla/hyperbook.html
comments: http://lamport.azurewebsites.net/tla/industrial-use.html
PlusCalc is an imperative language that compiles to TLA+ and seems simple to use: https://rix0r.nl/essays/2015/08/25/model-checking-for-the-working-man-mf/
Alloy meets TLA: https://arxiv.org/pdf/1603.03599.pdf
Model checking Parallel Software: http://www.refactorium.com/formal_methods/How-to-prove-that-your-parallel-code-works/
Book "Specifying System" by Leslie Lamport: http://lamport.azurewebsites.net/tla/book.html
Interesting discussion on type-theory-based prover like Coq vs set theory (Zermelo Fraenkel) based like TLA: https://news.ycombinator.com/item?id=10649128 And link to translating C to TLA+ to verify concurrent C programs: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/MLBHB-ftscs15.pdf
TLA series https://pron.github.io/posts/tlaplus_part1
https://members.loria.fr/SMerz/talks/argentina2005/slides.pdf
Semaphores in TLA+: http://herbrete.vvv.enseirb-matmeca.fr/IF311/lecture03.xhtml
Reader-Writer lock: http://jonaschapuis.com/2018/11/formal-verification-of-a-reader-writer-lock-with-tla/
state machine in TLA+: https://lamport.azurewebsites.net/video/video2-script.pdf
FDR is a model checker specialized in communicating sequential processes: http://www.cs.ox.ac.uk/projects/fdr/
Roméo tackles Petri Nets: http://romeo.rts-software.org/
Upaal is specialized on finite-state machine with a time component like real-time embedded systems and communication protocols: http://www.uppaal.org/
CADP by Inria looks interesting but not public except for academics http://cadp.inria.fr/
Interesting thread with lots of references of formal verification for industrial use (with lives on the line) : https://www.researchgate.net/post/Can_anyone_suggest_tool_chains_to_incorporate_formal_methods_in_the_development_of_industrial_railway_signalling_application
https://tools.clearsy.com/ and https://www.methode-b.com/ (lots of French) And in English: https://www3.hhu.de/stups/prob/index.php/Main_Page
Comparison of 10 formal models to prove that an automatic train scheduling system is deadlock-free: https://arxiv.org/abs/1803.10324
While focused on GUI for TLA, this thesis introduction clearly explain the different approach to model checking via Temporal logic, i.e. linear vs branching and the application domains (network protocol, hardware,....) https://pdfs.semanticscholar.org/edea/1923936e095b994aeee3958c07e1db59b2e1.pdf
https://www.researchgate.net/publication/220756135_User-Friendly_GUI_in_Software_Model_Checking
A formal verification of web service atomic transaction protocol using Upaal and TLA+ (atomic web transaction which are probably much more complex than the deadlock I have in the event notifier/Backoff mechanism #43 #28) https://www.it.uu.se/research/group/darts/papers/texts/rvs10.pdf
Verifying Abstract State Machines, event system and pubsub via BOGOR/BIR: https://arxiv.org/abs/1404.2155
https://cpachecker.sosy-lab.org/
https://www.cs.cmu.edu/~aldrich/courses/654-sp05/handouts/model-checking-3.pdf
https://news.ycombinator.com/item?id=14731308 https://news.ycombinator.com/item?id=10220264
TLA, Alloy, B: https://groups.google.com/forum/m/#!topic/tlaplus/C7Rmka3iSGE
Amazon spec in TLA Alloy:
Formal verification of Distributed algorithms:
Expressive and efficient bounded model checking for concurrent software (PhD Thesis): https://ssvlab.github.io/esbmc/papers/phd_thesis_morse.pdf, https://github.com/esbmc/esbmc
(French) Vérification par model-checking de programmes concurrents paramétrés sur des modèles mémoires faibles : https://www.lri.fr/~conchon/FIIL/phd_david_declerck
Another one-based on LLVM IR:
Whoop: https://pdeligia.github.io/lib/papers/whoop_ase15.pdf Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers, Deligiannis et al
Recent: Dynamic Race Detection for C++11 https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf
PhD Thesis by the author of landslide
Practical Concurrency testing\ Ben Blum, 2018\ http://reports-archive.adm.cs.cmu.edu/anon/2018/CMU-CS-18-128.pdf
Practical systematic concurrency testing for concurrent and distributed software\ Paul Thomson, 2016\ https://spiral.imperial.ac.uk/bitstream/10044/1/55908/1/Thomson-P-2017-PhD-Thesis.pdf
Optimal stateless model checking under the release-acquire semantics\ Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Tuan Phong Ngo, 2018\ https://dl.acm.org/doi/10.1145/3276505
Effective Stateless Model Checking for C/C++ Concurrency\ Michalis Kokologiannakis, Ori Lahav, Konstantinos Sagonas, Viktor Vafeiadis, 2018 https://plv.mpi-sws.org/rcmc/paper.pdf
Model Checking for Weakly Consistent Libraries\ Michalis Kokologiannakis, Azalea Raad, Viktor Vafeiadis, 2019\ http://www.soundandcomplete.org/papers/PLDI2019/GenMC.pdf
Optimal Stateless Model Checking for Reads-FromEquivalence under Sequential Consistency\ Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lang, Tuan Phong Ngo, Konstantinos Sagonas, 2019\ http://user.it.uu.se/~kostis/Papers/oopsla19-final.pdf
Stateless Model Checking for TSO and PSO\ Parosh Aziz Abdulla, Stavros Aronis, Mohamed Faouzi Atig,Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas, 2015\ https://link.springer.com/content/pdf/10.1007%2F978-3-662-46681-0_28.pdf https://github.com/nidhugg/nidhugg
Quasi-Optimal Partial Order Reduction\ Huyen T.T. Nguyen, César Rodriguez, Marcelo Sousa,Camille Coti, and Laure Petrucci, 2018\ https://arxiv.org/pdf/1802.03950.pdf\ https://github.com/cesaro/dpu
While Weave is currently doing a very good job at restricting shared writable state to channels, and specifically
trySend
andtryRecv
routines, we need tooling and tests to detect races and concurrent heisenbugs.Unfortunately it is apparently a NP-hard problem. The issue is that to ease debugging we need to reliable trigger the bug to ensure it is fixed. However threads interleaving is non-deterministic and we can't ask people to use our own deterministic fork of Windows, Linux or Mac.
Also allocating and free-ing memory willy-nilly from lots of threads might also overwhelm the allocator in use or maybe trigger bugs (if we use Nim allocator), so it's probably better to never free memory for testing to avoid allocator bugs/slowness (https://github.com/mratsim/weave/commit/b8ac8d64ca07eb47a926f3f70b96e94fe930cf08)
There are a couple approaches that can be taken with varying order of impracticality.
Sanitizers
This category only requires recompiling with extra flags, sometimes just
--debugger:native
. While they can detect the presence of bugs, I don't think they can prove the absence of one.valgrind --tool:helgrind build/mybinary
http://valgrind.org/docs/manual/hg-manual.html
POSIX-only, with debugger:native it will mention the Nim lines that are potentially racy. It slows down the code a lot.
Also there is some noise on memset, memcpy (not sure if it also happens if you never free memory)
![DeepinScreenshot_select-area_20191120231347](https://user-images.githubusercontent.com/22738317/69325486-85324980-0c4a-11ea-936d-ee8e90861e88.png)
LLVM ThreadSanitizer
Compile with clang with
-fsanitize=thread
Libraries
Libraries can exhaustively tests all kind of thread interleaving provided a test scenario, say MPSC queue with 2 producers and 1 consumers. We however have to assume that being bug free for 2 producers mean being bug-free for N (which has been proved for some MPSC queue implementations).
Important: Library used should ideally support C++11 memory model and/or ensure correctness on weak memory model architecture (i.e. everything not x86 like ARM? PowerPC, MIPS)
Relacy Race Detector
We can switch Nim atomics to Relacy atomics via templates and recompile.
Chess
Microsoft, Windows-only
Landslide
https://github.com/bblum/landslide https://www.pdl.cmu.edu/Landslide/index.shtml
See extensive PhD Thesis at the bottom
Do-it-yourself
The blog post for MultithreadedTC a verifier for the JVM explains in-depth how it is architected: via an internal metronome clock that sync all threads and then at synchronization points test all combinations of thread interleaving.
http://www.cs.umd.edu/projects/PL/multithreadedtc/overview.html
Model Checking and Formal verification
This is heavyweight and requires either using a foreign language or a lot of annotation and constraints in the source code, in exchange it provides mathematical guarantees of correctness:
VCC
Annotate C code and it will be passed to Z3
Iris
TLA+
Spin
Resources
PhD Thesis, Ben Blum
Practical Concurrency Testing or: How I Learned to Stop Worrying and Love the Exponential Explosion
http://reports-archive.adm.cs.cmu.edu/anon/2018/CMU-CS-18-128.pdf