This repository contains specifications and safety proofs of a simple concurrent algorithm that first appeared in the note "Teaching Concurrency" published in the March 2009 issue of ACM SIGACT News: http://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf. In this algorithm, there are N processes and two arrays of length N, x and y. Each process i executes the following sequence of statements:
x[i] := 1;
y[i] := x[(i-1) mod N];
The reads and writes of each x[j] are assumed to be atomic. This algorithm has the property that once all processes have finished, at least one y[j] = 1.
The specification and safety proofs are written in several different languages. My goal is to understand concurrency reasoning in various verification tools, with a long term goal of applying one of the tools to a realistic system. So far, I've written specs and proofs in the following tools:
- PlusCal/TLA+ (https://github.com/tlaplus/tlaplus)
- Dafny (https://github.com/dafny-lang/dafny)
- CIVL/Boogie (https://github.com/boogie-org/boogie)
- mypyvy (https://github.com/wilcoxjay/mypyvy)
- SMT (http://smtlib.cs.uiowa.edu/)
I'd be happy to get feedback on my existing solutions, suggestions on other tools to try, or contributions in other tools.