[Testing] Concurrency: Race detection / Model Checking / Formal Verification about weave HOT 7 OPEN

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

from weave.

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:

• http://hpts.ws/papers/2011/sessions_2011/Debugging.pdf
• http://hpts.ws/papers/2011/sessions_2011/amazonbundle.tar.gz
• https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf

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

from weave.

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

from weave.

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

from weave.

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

from weave.

• 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

from weave.

• 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

from weave.