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

Jade Alglave, Patrick Cousot

Research output: Contribution to journalArticlepeer-review

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)
Pages (from-to)3-18
Number of pages16
JournalACM SIGPLAN Notices
Volume52
Issue number1
DOIs
StatePublished - Jan 2017

Keywords

  • concurrency
  • distributed and parallel programming
  • in- variance
  • verification
  • weak consistency models

ASJC Scopus subject areas

  • General Computer Science

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