UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Ogre and Pythia: An Invariance Proof Method for Weak Consistency Models

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. Green open access

[img]
Preview
Text
Alglave_Ogre_Pythia_Invariance.pdf - ["content_typename_Accepted version" not defined]

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 > Provost and Vice Provost Offices
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: http://discovery.ucl.ac.uk/id/eprint/1550683
Downloads since deposit
104Downloads
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item