Ogre and Pythia: an invariance proof method for weak consistency models
2017
We design an invariance proof method for concurrent programs parameterised by a weak consistency model. The calculational design of the invariance proof method is by abstract interpretation of a truly parallel analytic semantics. This generalises the methods by Lamport and Owicki-Gries for sequential consistency. We use cat as an example of language to write consistency specifications of both concurrent programs and machine architectures.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
62
References
22
Citations
NaN
KQI