Alglave, J;
Cousot, P;
(2017)
Ogre and Pythia: An Invariance Proof Method for Weak Consistency Models.
In: Castagna, G and Gordon, AD, (eds.)
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages.
(pp. pp. 3-18).
ACM: New York, USA.
Preview |
Text
Alglave_Ogre_Pythia_Invariance.pdf - Accepted Version Download (1MB) | Preview |
Abstract
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.
| Type: | Proceedings paper |
|---|---|
| Title: | Ogre and Pythia: An Invariance Proof Method for Weak Consistency Models |
| Event: | POPL 2017: 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 15-21 January 2017, Paris, France |
| ISBN-13: | 9781450346603 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1145/3009837.3009883 |
| Publisher version: | https://doi.org/10.1145/3093333.3009883 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | concurrency, distributed and parallel programming, invariance, verification, weak consistency models |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/1550683 |
Archive Staff Only
 |
View Item |
