Concurrent-programs
ACL2 proofs establishing the fairness of the Bakery Algorithm and the
coherence of the German Cache Protocol.
Subtopics
- Bakery-algorithm
- This set of books shows how one can use stuttering trace containment
with fairness constraints to verify concurrent protocols. We apply the method
here to prove the correctness of an implementation of the Bakery algorithm.
The implementation is interesting in the sense that it depends critically on
fair selection of processes to ensure absence of deadlock. We show how the
requisite notions can be formalized as generic theories and used in the proof
of refinements.
- German-protocol
- An ACL2 proof of coherence of the German Cache Protocol. The
protocol is translated directly into ACL2 from the murphy code provided in
ccp.m. The proof involves formalizing coherence and strengthening the property
into an inductive invariant.
