Owicki-Gries reasoning for weak memory models
DOI10.1007/978-3-662-47666-6_25zbMATH Open1440.68046OpenAlexW1430872261MaRDI QIDQ3449485FDOQ3449485
Authors: Ori Lahav, Viktor Vafeiadis 
Publication date: 4 November 2015
Published in: Automata, Languages, and Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-662-47666-6_25
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
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
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Verifying properties of parallel programs
- An axiomatic proof technique for parallel programs
- Mathematizing C++ concurrency
- Title not available (Why is that?)
- Common compiler optimisations are invalid in the C11 memory model and what we can do about it
- Parameterized Memory Models and Concurrent Separation Logic
- A separation logic for fictional sequential consistency
Cited In (24)
- 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++
- Reasoning about promises in weak memory models with event structures
- Automating deductive verification for weak-memory programs
- Fences in weak memory models
- Mechanised operational reasoning for C11 programs with relaxed dependencies
- Observation-based concurrent program logic for relaxed memory consistency models
- Thread-modular analysis of release-acquire concurrency
- 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
- Title not available (Why is that?)
- 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
- Ogre and Pythia: an invariance proof method for weak consistency models
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)
