Reasoning algebraically about refinement on TSO architectures

DOI10.1007/978-3-319-10882-7_10MaRDI QIDQ2938158zbMATH OpenOpenAlexFDO

Authors Brijesh Dongol, John Derrick, Graeme Smith

Publication date 13 January 2015

Published in Theoretical Aspects of Computing – ICTAC 2014 (Search for Journal in Brave)

Full work available at URL http://eprints.whiterose.ac.uk/113097/1/main.pdf

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Mathematical problems of computer architecture (68M07)

Recommendations

• A high-level semantics for program execution under total store order memory
• A load-buffer semantics for total store ordering
• From total store order to sequential consistency: a practical reduction theorem
• Reasoning about TSO programs using reduction and abstraction
• On the verification problem for weak memory models

Cited in

(7)

• Reasoning about TSO programs using reduction and abstraction
• TSO-to-TSO linearizability is undecidable
• From total store order to sequential consistency: a practical reduction theorem
• A load-buffer semantics for total store ordering
• A high-level semantics for program execution under total store order memory
• Linearizability on hardware weak memory models
• Making Linearizability Compositional for Partially Ordered Executions

This page was built for publication: Reasoning algebraically about refinement on TSO architectures

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