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

DOI10.1145/3009837.3009883MaRDI QIDQ5370841zbMATH OpenOpenAlexFDO

Authors Jade Alglave, Patrick Cousot

Publication date 20 October 2017

Published in Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://discovery.ucl.ac.uk/id/eprint/1550683/

zbMATH Keywords

concurrencydistributed and parallel programminginvarianceverificationweak consistency models

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 3902009
• Owicki-Gries reasoning for weak memory models
• scientific article; zbMATH DE number 2102714
• The complexity of weak consistency
• scientific article; zbMATH DE number 3956417

Cited in

(8)

• Checking robustness between weak transactional consistency models
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• scientific article; zbMATH DE number 7327945 (Why is no real title available?)
• Robustness Against Transactional Causal Consistency.
• Reasoning about promises in weak memory models with event structures
• A fine-grained semantics for arrays and pointers under weak memory models
• Rely-guarantee reasoning for causally consistent shared memory
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL

This page was built for publication: Ogre and Pythia: an invariance proof method for weak consistency models

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5370841)