Comments (7)
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/
-
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://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.
Related Issues (20)
- windows aligned_alloc in allocs.nim have different params order compared to docs and malloc.h
- [Request] Optional per-thread startup procedure HOT 1
- `blockUntilAny` equivalent
- GC Boehm Error with more than 8 threads HOT 2
- parallelFor has arguments that do not fit in the parallel tasks data buffer HOT 9
- a plea for an easier to understand error message HOT 3
- Recent Nim makes Weave crash HOT 8
- affinity_posix should get this patch (for Android/Termux)
- @mratsim
- Cache misses (much) worse for page-aligned (e.g. power of two) accesses
- Raytracing example doesnt compile with threads HOT 1
- UX: auto-transform captured seq to ptr UncheckedArray behind the scenes HOT 3
- functions with no arguments fail parsing HOT 1
- Is there a manual or tutorial for weave? HOT 2
- Weave doesn't compile on MacOS with arm64 HOT 2
- Error: undeclared identifier: 'gebb_ukernel_int_x86_AVX512' HOT 2
- Feature Request: Cores as init parameter, respect core perf levels
- Vastly simplify and accelerate memory management. HOT 1
- Use Lnear Congruential Generator to generate work-stealing permutation HOT 1
- randomly "off values" HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from weave.