Reasoning about promises in weak memory models with event structures

DOI10.1007/978-3-031-27481-7_17MaRDI QIDQ6174540zbMATH OpenFDO

Authors Heike Wehrheim, Lara Bargmann, Brijesh Dongol

Publication date 17 August 2023

Published in Formal Methods (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2211.16330, https://openresearch.surrey.ac.uk/view/delivery/44SUR_INST/12180650930002346/13180650920002346

zbMATH Keywords

event structuresincorrectness logicpromisesweak memory models

Mathematics Subject Classification ID

Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Modern processors such as ARMv8 and RISC-V allow executions in which independent instructions within a process may be reordered. To cope with such phenomena, so called promising semantics have been developed, which permit threads to read values that have not yet been written. Each promise is a speculative update that is later validated (fulfilled) by an actual write. Promising semantics are operational, providing a pathway for developing proof calculi. In this paper, we develop an incorrectness-style logic, resulting in a framework for reasoning about state reachability. Like incorrectness logic, our assertions are underapproximating, since the set of all valid promises are not known at the start of execution. Our logic uses event structures as assertions to compactly represent the ordering among events such as promised and fulfilled writes. We prove soundness and completeness of our proof calculus and demonstrate its applicability by proving reachability properties of standard weak memory litmus tests.

Recommendations

• A promising semantics for relaxed-memory concurrency
• A separation logic for a promising semantics
• A wide-spectrum language for verification of programs on weak memory models
• The decidability of verification under PS 2.0
• On the verification problem for weak memory models

Cites work

• A program logic for C11 memory fences
• A promising semantics for relaxed-memory concurrency
• A separation logic for a promising semantics
• An axiomatic basis for computer programming
• An axiomatic proof technique for parallel programs
• Flow models of distributed computations: Three equivalent semantics for CCS
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 3995041 (Why is no real title available?)
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• 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
• Parallel product of event structures
• Parallelized sequential composition and hardware weak memory models
• Reverse Hoare logic
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Well-behaved flow event structures for parallel composition and action refinement

This page was built for publication: Reasoning about promises in weak memory models with event structures

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