Relating trace refinement and linearizability

DOI10.1007/S00165-017-0418-2MaRDI QIDQ1688548zbMATH OpenOpenAlexFDO

Authors Graeme Smith, Kirsten Winter

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

concurrencycorrectnesslinearizabilitytrace refinement

Mathematics Subject Classification ID

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

Recommendations

• Strict linearizability and abstract atomicity
• Proving Linearizability Via Non-atomic Refinement
• Using refinement calculus techniques to prove linearizability
• Linearizability on hardware weak memory models
• Model-checking of correctness conditions for concurrent objects

Cites work

• scientific article; zbMATH DE number 42431 (Why is no real title available?)
• scientific article; zbMATH DE number 45231 (Why is no real title available?)
• A framework for correctness criteria on weak memory models
• A scalable lock-free stack algorithm
• A sound and complete proof technique for linearizability of concurrent data structures
• Abstraction for concurrent objects
• Action refinement.
• Liveness-Preserving Atomicity Abstraction
• Modeling in Event B. System and software engineering.
• The existence of refinement mappings
• Tractable refinement checking for concurrent objects

Cited in

(6)

• Strict linearizability and abstract atomicity
• Interleaving-tree based fine-grained linearizability fault localization
• Using refinement calculus techniques to prove linearizability
• Putting strong linearizability in context: preserving hyperproperties in programs that use concurrent objects
• Tractable refinement checking for concurrent objects
• Linearizability on hardware weak memory models

Describes a project that uses

Uses Software

• Z
• Rodin

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1688548)