We provide the offence tool for weak memory models, which places either lock-based or lock-free synchronisation in an x86 or Power program to ensure its stability, i.e. that the program has no executions but SC ones.
The tool is based on our CAV 2011 paper, called Stability in Weak Memory Models. See here for the long version of the paper with proofs, and the Coq development.
News
January 2011 the 24th: Release of offence 1.00.
Offence
You will find here the sources of the tool, as well as a documentation.
Experiments
We provide here the details of our experiments:- Soundness experiments, i.e. offence restores SC.
- Timing of the synchronisation constructs introduced by offence.
- B-cumulativity of lwsync.
Advertisement
