Ogre and pythia: An invariance proof method for weak consistency models

Jade Alglave, Patrick Cousot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationPOPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
EditorsAndrew D. Gordon, Giuseppe Castagna
PublisherAssociation for Computing Machinery
Pages3-18
Number of pages16
ISBN (Electronic)9781450346603
DOIs
StatePublished - Jan 1 2017
Event44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 - Paris, France
Duration: Jan 15 2017Jan 21 2017

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Other

Other44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017
Country/TerritoryFrance
CityParis
Period1/15/171/21/17

Keywords

  • Concurrency
  • Distributed and parallel programming
  • Invariance
  • Verification
  • Weak consistency models

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Ogre and pythia: An invariance proof method for weak consistency models'. Together they form a unique fingerprint.

Cite this