Reasoning about promises in weak memory models with event structures

DOI10.1007/978-3-031-27481-7_17zbMath1529.68181arXiv2211.16330MaRDI QIDQ6174540

Lara Bargmann, Heike Wehrheim, 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

zbMATH Keywords

promisesevent structuresweak memory modelsincorrectness logic

Mathematics Subject Classification ID

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

Cites Work

• Unnamed Item
• Unnamed Item
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• An axiomatic proof technique for parallel programs
• Flow models of distributed computations: Three equivalent semantics for CCS
• Parallel product of event structures
• Well-behaved flow event structures for parallel composition and action refinement
• A separation logic for a promising semantics
• A Program Logic for C11 Memory Fences
• Reverse Hoare Logic
• Owicki-Gries Reasoning for Weak Memory Models
• Modular Relaxed Dependencies in Weak Memory Concurrency
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Ogre and Pythia: an invariance proof method for weak consistency models
• A promising semantics for relaxed-memory concurrency
• Mathematizing C++ concurrency
• An axiomatic basis for computer programming
• Parallelized sequential composition and hardware weak memory models

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