[Testing] Concurrency: Race detection / Model Checking / Formal Verification #18

mratsim · 2019-11-21T10:21:31Z

While Weave is currently doing a very good job at restricting shared writable state to channels, and specifically trySend and tryRecv 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 (b8ac8d6)

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)

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

https://iris-project.org/

TLA+

https://www.learntla.com/introduction/example/

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

The text was updated successfully, but these errors were encountered:

mratsim · 2019-12-15T23:35:03Z

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

mratsim · 2019-12-16T01:47:09Z

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/
- https://stackoverflow.com/questions/22147090/ltl-ctl-or-tla-for-modelling-for-my-model-detailed-description-inside
- 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/

Others

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://kilthub.cmu.edu/articles/Overview_of_ComFoRT_A_Model_Checking_Reasoning_Framework/6575960/files/12062606.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:

State Machine in Isabelle: https://hal.inria.fr/hal-01556227/document
Using PlusCalc2 (PhD Thesis): https://www.semanticscholar.org/paper/Formal-Verification-of-Distributed-Algorithms-using-Akhtar/d793eef1cb4003651eb715bc9e4c2b1915882ba3

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

mratsim · 2020-01-20T11:37:36Z

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

mratsim · 2020-05-06T23:26:44Z

Recent:
Dynamic Race Detection for C++11
https://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2017/POPL.pdf

mratsim · 2020-05-07T01:41:00Z

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

…oduce the spurious livelock/deadlock and multithreaded corruption we have in CI

mratsim · 2020-05-08T13:44:43Z

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

mratsim · 2021-02-04T22:43:34Z

Compiler Correctness for Concurrency: from concurrent separation logic to shared-memory assembly language
Santiago Cuellar, Nick Giannarakis, Jean-Marie Madiot, William Mansky, Lennart Beringer, Qinxiang Cao, and Andrew W. Appel
https://www.cs.princeton.edu/~appel/papers/ccc.pdf

mratsim added help wanted 👥 Extra attention is needed Testing 🛂 labels Nov 21, 2019

mratsim changed the title ~~[Testing] Concurrency: ensuring correctness of the channels implementation~~ [Testing] Concurrency: Race detection / Model Checking / Formal Verification Dec 15, 2019

mratsim added concurrency 💥 deadlock/livelock 💀 🔒 labels Dec 22, 2019

mratsim mentioned this issue Apr 26, 2020

Fuzzing #120

Open

mratsim mentioned this issue May 7, 2020

Correct-by-construction Nim programs nim-lang/RFCs#222

Open

mratsim added a commit that referenced this issue May 7, 2020

introduce Thread Collider to solve #18 and nim-lang/RFCs#222 and repr…

0ac8156

…oduce the spurious livelock/deadlock and multithreaded corruption we have in CI

mratsim mentioned this issue May 9, 2020

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

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Testing] Concurrency: Race detection / Model Checking / Formal Verification #18

[Testing] Concurrency: Race detection / Model Checking / Formal Verification #18

[Testing] Concurrency: Race detection / Model Checking / Formal Verification #18

[Testing] Concurrency: Race detection / Model Checking / Formal Verification #18

Comments

Sanitizers

valgrind --tool:helgrind build/mybinary

LLVM ThreadSanitizer

Libraries

Relacy Race Detector

Chess

Landslide

Do-it-yourself

Model Checking and Formal verification

VCC

Iris

TLA+

Spin

Resources

Others

`valgrind --tool:helgrind build/mybinary`