Unifying Operational Weak Memory Verification: An Axiomatic Approach

DOI10.1145/3545117MaRDI QIDQ5056374zbMATH OpenOpenAlexWikidataFDO

Authors Simon Doherty, Sadegh Dalvandi, Brijesh Dongol, Heike Wehrheim

Publication date 8 December 2022

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/3545117

zbMATH Keywords

axiom hierarchyHoare logicOwicki-Gries reasoningverificationweak memory models

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Program verification under weak memory consistency using separation logic
• A formal hierarchy of weak memory models
• Owicki-Gries reasoning for weak memory models
• Automating deductive verification for weak-memory programs
• Software verification for weak memory via program transformation

Cites work

• A load-buffer semantics for total store ordering
• A program logic for C11 memory fences
• A promising semantics for relaxed-memory concurrency
• A separation logic for a promising semantics
• Algebras of modal operators and partial correctness
• An axiomatic basis for computer programming
• An axiomatic proof technique for parallel programs
• Automatically comparing memory consistency models
• Automating deductive verification for weak-memory programs
• Concurrent Kleene algebra and its foundations
• Concurrent Library Correctness on the TSO Memory Model
• Context-bounded analysis of TSO systems
• Convolution as a Unifying Concept
• Effective abstractions for verification under relaxed memory models
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• scientific article; zbMATH DE number 3562484 (Why is no real title available?)
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• Library abstraction for C/C++ concurrency
• Mathematizing C++ concurrency
• Modular relaxed dependencies in weak memory concurrency
• Ogre and Pythia: an invariance proof method for weak consistency models
• Owicki-Gries reasoning for weak memory models
• Software verification for weak memory via program transformation
• Stateless model checking for TSO and PSO
• Stateless model checking for TSO and PSO
• Tackling real-life relaxed concurrency with FSL++
• The Java memory model
• Verification of sequential and concurrent programs
• Verifying correctness of persistent concurrent data structures: a sound and complete method

Cited in

(16)

• A wide-spectrum language for verification of programs on weak memory models
• Program verification under weak memory consistency using separation logic
• Automating deductive verification for weak-memory programs
• A formal hierarchy of weak memory models
• Verification of Concurrent Programs on Weak Memory Models
• Owicki-Gries reasoning for weak memory models
• Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
• Software verification for weak memory via program transformation
• Correct Hardware Design and Verification Methods
• Reasoning about promises in weak memory models with event structures
• A fine-grained semantics for arrays and pointers under weak memory models
• Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
• Rely-guarantee reasoning for causally consistent shared memory
• An ACL2 mechanization of an axiomatic framework for weak memory
• Mechanised operational reasoning for C11 programs with relaxed dependencies
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL

Describes a project that uses

Uses Software

• Line-up
• SPIN

This page was built for publication: Unifying Operational Weak Memory Verification: An Axiomatic Approach

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