Rely-guarantee reasoning for causally consistent shared memory
From MaRDI portal
Publication:6535633
DOI10.1007/978-3-031-37706-8_11zbMATH Open1547.68123MaRDI QIDQ6535633FDOQ6535633
Authors: Ori Lahav, Brijesh Dongol, Heike Wehrheim 
Publication date: 1 February 2024
Recommendations
- On rely-guarantee reasoning
- Generalised rely-guarantee concurrency: an algebraic foundation
- Local rely-guarantee reasoning
- The Rely-Guarantee method for verifying shared variable concurrent programs
- Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)
Cites Work
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Myths about the mutual exclusion problem
- Causal memory: definitions, implementation, and programming
- Views, compositional reasoning for concurrent programs
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- An axiomatic proof technique for parallel programs
- Tentative steps toward a development method for interfering programs
- A calculus of durations
- A Marriage of Rely/Guarantee and Separation Logic
- The Rely-Guarantee method for verifying shared variable concurrent programs
- Verification of sequential and concurrent programs
- Owicki-Gries reasoning for weak memory models
- A separation logic for a promising semantics
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Ogre and Pythia: an invariance proof method for weak consistency models
- A promising semantics for relaxed-memory concurrency
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- A complete axiom system for propositional interval temporal logic with infinite time
- On verifying causal consistency
- Reasoning about vectors using an SMT theory of sequences
- Taming release-acquire consistency
- The benefits of duality in verifying concurrent programs under TSO
- Title not available (Why is that?)
- A load-buffer semantics for total store ordering
- Unifying Operational Weak Memory Verification: An Axiomatic Approach
- Compositional reasoning for non-multicopy atomic architectures
Cited In (1)
This page was built for publication: Rely-guarantee reasoning for causally consistent shared memory
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6535633)
