Making Linearizability Compositional for Partially Ordered Executions
From MaRDI portal
Publication:6104493
DOI10.1007/978-3-319-98938-9_7zbMath1514.68164arXiv1802.01866OpenAlexW2887304561MaRDI QIDQ6104493
Heike Wehrheim, Brijesh Dongol, John Derrick, Simon Doherty
Publication date: 28 June 2023
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1802.01866
Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Related Items (2)
Verifying correctness of persistent concurrent data structures ⋮ Linearizability on hardware weak memory models
Cites Work
- Abstraction for concurrent objects
- On interprocess communication. I: Basic formalism
- Stateless model checking for TSO and PSO
- Proving linearizability using forward simulations
- A separation logic for a promising semantics
- Automating deductive verification for weak-memory programs
- A Program Logic for C11 Memory Fences
- Overhauling SC atomics in C11 and OpenCL
- Taming release-acquire consistency
- Concurrent Library Correctness on the TSO Memory Model
- Library abstraction for C/C++ concurrency
- Reasoning Algebraically About Refinement on TSO Architectures
- A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
- Tackling Real-Life Relaxed Concurrency with FSL++
- On abstraction and compositionality for weak-memory linearisability
- Owicki-Gries Reasoning for Weak Memory Models
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Show No Weakness: Sequentially Consistent Specifications of TSO Libraries
- Causal memory: definitions, implementation, and programming
- The Java memory model
- A promising semantics for relaxed-memory concurrency
- Mathematizing C++ concurrency
- Formal Techniques for Networked and Distributed Systems – FORTE 2004
This page was built for publication: Making Linearizability Compositional for Partially Ordered Executions
