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 (1)
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
