Linearizability on hardware weak memory models

DOI10.1007/s00165-019-00499-8zbMath1451.68030OpenAlexW2989289194WikidataQ126807837 ScholiaQ126807837MaRDI QIDQ782494

Graeme Smith, Kirsten Winter, Robert J. Colvin

Publication date: 27 July 2020

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-019-00499-8

zbMATH Keywords

correctnesslinearizabilityconcurrent objects

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical problems of computer architecture (68M07)

Related Items

Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP

Uses Software

• SPIN
• Line-up

Cites Work

• Abstraction for concurrent objects
• The existence of refinement mappings
• Relating trace refinement and linearizability
• A wide-spectrum language for verification of programs on weak memory models
• Concurrent Library Correctness on the TSO Memory Model
• Reasoning Algebraically About Refinement on TSO Architectures
• Deciding Robustness against Total Store Ordering
• Liveness-Preserving Atomicity Abstraction
• On abstraction and compositionality for weak-memory linearisability
• Show No Weakness: Sequentially Consistent Specifications of TSO Libraries
• A Framework for Correctness Criteria on Weak Memory Models
• Checking and Enforcing Robustness against TSO
• Mathematizing C++ concurrency
• Making Linearizability Compositional for Partially Ordered Executions