Owicki-Gries Reasoning for Weak Memory Models

DOI10.1007/978-3-662-47666-6_25zbMath1440.68046OpenAlexW1430872261MaRDI QIDQ3449485

Viktor Vafeiadis, Ori Lahav

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

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Verifying Visibility-Based Weak Consistency ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models ⋮ Thread-modular analysis of release-acquire concurrency ⋮ Unnamed Item ⋮ Parallelized sequential composition and hardware weak memory models ⋮ Making Linearizability Compositional for Partially Ordered Executions ⋮ Reasoning about promises in weak memory models with event structures ⋮ A fine-grained semantics for arrays and pointers under weak memory models ⋮ Tackling Real-Life Relaxed Concurrency with FSL++ ⋮ Robustness Against Transactional Causal Consistency. ⋮ Checking robustness between weak transactional consistency models ⋮ Unnamed Item

Cites Work

• Unnamed Item
• An axiomatic proof technique for parallel programs
• A Separation Logic for Fictional Sequential Consistency
• Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it
• Parameterized Memory Models and Concurrent Separation Logic
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Verifying properties of parallel programs
• Mathematizing C++ concurrency

This page was built for publication: Owicki-Gries Reasoning for Weak Memory Models