Relating trace refinement and linearizability

DOI10.1007/s00165-017-0418-2zbMath1377.68151OpenAlexW2588661182MaRDI QIDQ1688548

Kirsten Winter, Graeme Smith

Publication date: 8 January 2018

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

Full work available at URL: https://doi.org/10.1007/s00165-017-0418-2

zbMATH Keywords

correctnesslinearizabilityconcurrencytrace refinement

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (1)

Linearizability on hardware weak memory models

Uses Software

• Rodin
• Z

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Abstraction for concurrent objects
• A scalable lock-free stack algorithm
• The existence of refinement mappings
• Tractable Refinement Checking for Concurrent Objects
• A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
• Liveness-Preserving Atomicity Abstraction
• A Framework for Correctness Criteria on Weak Memory Models

This page was built for publication: Relating trace refinement and linearizability