Rely-guarantee reasoning for causally consistent shared memory
From MaRDI portal
Publication:6535633
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)
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
Cites work
- scientific article; zbMATH DE number 7327945 (Why is no real title available?)
- A Marriage of Rely/Guarantee and Separation Logic
- A calculus of durations
- A complete axiom system for propositional interval temporal logic with infinite time
- A load-buffer semantics for total store ordering
- A promising semantics for relaxed-memory concurrency
- A separation logic for a promising semantics
- An axiomatic proof technique for parallel programs
- Causal memory: definitions, implementation, and programming
- Compositional reasoning for non-multicopy atomic architectures
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Iris from the ground up: a modular foundation for higher-order concurrent separation logic
- Myths about the mutual exclusion problem
- Ogre and Pythia: an invariance proof method for weak consistency models
- On verifying causal consistency
- Owicki-Gries reasoning for weak memory models
- RGITL: a temporal logic framework for compositional reasoning about interleaved programs
- Reasoning about vectors using an SMT theory of sequences
- Taming release-acquire consistency
- Tentative steps toward a development method for interfering programs
- The Rely-Guarantee method for verifying shared variable concurrent programs
- The benefits of duality in verifying concurrent programs under TSO
- Unifying Operational Weak Memory Verification: An Axiomatic Approach
- Verification of sequential and concurrent programs
- Views, compositional reasoning for concurrent programs
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)
