Owicki-Gries reasoning for weak memory models
From MaRDI portal
Publication:3449485
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
- Program verification under weak memory consistency using separation logic
- Unifying Operational Weak Memory Verification: An Axiomatic Approach
- A formal hierarchy of weak memory models
- Verification of Concurrent Programs on Weak Memory Models
- Automating deductive verification for weak-memory programs
Cites work
- scientific article; zbMATH DE number 3614147 (Why is no real title available?)
- A separation logic for fictional sequential consistency
- An axiomatic proof technique for parallel programs
- Common compiler optimisations are invalid in the C11 memory model and what we can do about it
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Mathematizing C++ concurrency
- Parameterized Memory Models and Concurrent Separation Logic
- Verifying properties of parallel programs
Cited in
(24)- Ogre and Pythia: an invariance proof method for weak consistency models
- Unifying Operational Weak Memory Verification: An Axiomatic Approach
- Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
- Verifying visibility-based weak consistency
- Checking robustness between weak transactional consistency models
- Parallelized sequential composition and hardware weak memory models
- Tackling real-life relaxed concurrency with FSL++
- Fences in weak memory models
- Automating deductive verification for weak-memory programs
- Reasoning about promises in weak memory models with event structures
- Observation-based concurrent program logic for relaxed memory consistency models
- Thread-modular analysis of release-acquire concurrency
- Mechanised operational reasoning for C11 programs with relaxed dependencies
- Program verification under weak memory consistency using separation logic
- A load-buffer semantics for total store ordering
- Reasoning about optimistic concurrency using a program logic for history
- A fine-grained semantics for arrays and pointers under weak memory models
- scientific article; zbMATH DE number 7327945 (Why is no real title available?)
- Making Linearizability Compositional for Partially Ordered Executions
- Operational Reasoning for Concurrent Caml Programs and Weak Memory Models
- Verifying concurrent memory reclamation algorithms with grace
- Robustness Against Transactional Causal Consistency.
- Rely-guarantee reasoning for causally consistent shared memory
- Compositional reasoning for non-multicopy atomic architectures
This page was built for publication: Owicki-Gries reasoning for weak memory models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3449485)
