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
PublisherAssociation for Computing Machinery
Pages3-18
Number of pages16
VolumePart F125683
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

Other

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

Fingerprint

Invariance
Semantics
Specifications

Keywords

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

ASJC Scopus subject areas

  • Software

Cite this

Alglave, J., & Cousot, P. (2017). Ogre and pythia: An invariance proof method for weak consistency models. In POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Vol. Part F125683, pp. 3-18). Association for Computing Machinery. https://doi.org/10.1145/3009837.3009883

Ogre and pythia : An invariance proof method for weak consistency models. / Alglave, Jade; Cousot, Patrick.

POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Vol. Part F125683 Association for Computing Machinery, 2017. p. 3-18.

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

Alglave, J & Cousot, P 2017, Ogre and pythia: An invariance proof method for weak consistency models. in POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. vol. Part F125683, Association for Computing Machinery, pp. 3-18, 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 1/15/17. https://doi.org/10.1145/3009837.3009883
Alglave J, Cousot P. Ogre and pythia: An invariance proof method for weak consistency models. In POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Vol. Part F125683. Association for Computing Machinery. 2017. p. 3-18 https://doi.org/10.1145/3009837.3009883
Alglave, Jade ; Cousot, Patrick. / Ogre and pythia : An invariance proof method for weak consistency models. POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. Vol. Part F125683 Association for Computing Machinery, 2017. pp. 3-18
@inproceedings{9398d131ea1e42f5a5374e2d7920a796,
title = "Ogre and pythia: An invariance proof method for weak consistency models",
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.",
keywords = "Concurrency, Distributed and parallel programming, Invariance, Verification, Weak consistency models",
author = "Jade Alglave and Patrick Cousot",
year = "2017",
month = "1",
day = "1",
doi = "10.1145/3009837.3009883",
language = "English (US)",
volume = "Part F125683",
pages = "3--18",
booktitle = "POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages",
publisher = "Association for Computing Machinery",

}

TY - GEN

T1 - Ogre and pythia

T2 - An invariance proof method for weak consistency models

AU - Alglave, Jade

AU - Cousot, Patrick

PY - 2017/1/1

Y1 - 2017/1/1

N2 - 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.

AB - 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.

KW - Concurrency

KW - Distributed and parallel programming

KW - Invariance

KW - Verification

KW - Weak consistency models

UR - http://www.scopus.com/inward/record.url?scp=85015334167&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85015334167&partnerID=8YFLogxK

U2 - 10.1145/3009837.3009883

DO - 10.1145/3009837.3009883

M3 - Conference contribution

VL - Part F125683

SP - 3

EP - 18

BT - POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages

PB - Association for Computing Machinery

ER -