A Framework for Correctness Criteria on Weak Memory Models

DOI10.1007/978-3-319-19249-9_12zbMath1427.68166OpenAlexW2246674664MaRDI QIDQ5206951

Graeme Smith, John Derrick

Publication date: 19 December 2019

Published in: FM 2015: Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-19249-9_12

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (2)

Relating trace refinement and linearizability ⋮ Linearizability on hardware weak memory models

Cites Work

• Unnamed Item
• Abstraction for concurrent objects
• Concurrent Library Correctness on the TSO Memory Model
• The future(s) of shared data structures
• A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Counting networks
• Show No Weakness: Sequentially Consistent Specifications of TSO Libraries

This page was built for publication: A Framework for Correctness Criteria on Weak Memory Models