Compositional reasoning for non-multicopy atomic architectures

DOI10.1145/3574137MaRDI QIDQ6610380zbMATH OpenFDO

Authors Nicholas Coughlin, Kirsten Winter, Graeme Smith

Publication date 25 September 2024

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

Full work available at URL https://doi.org/10.1145/3574137

zbMATH Keywords

non-multicopy atomicityrely/guarantee reasoningverificationweak memory models

Mathematics Subject Classification ID

Computer science (68-XX)

Cites work

• A load-buffer semantics for total store ordering
• A Marriage of Rely/Guarantee and Separation Logic
• A promising semantics for relaxed-memory concurrency
• A separation logic for a promising semantics
• A wide-spectrum language for verification of programs on weak memory models
• An axiomatic basis for computer programming
• Concrete semantics. With Isabelle/HOL
• Dafny: an automatic program verifier for functional correctness
• scientific article; zbMATH DE number 3485178 (Why is no real title available?)
• scientific article; zbMATH DE number 6876104 (Why is no real title available?)
• scientific article; zbMATH DE number 194642 (Why is no real title available?)
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Library abstraction for C/C++ concurrency
• Local rely-guarantee reasoning
• Mathematizing C++ concurrency
• Myths about the mutual exclusion problem
• Owicki-Gries reasoning for weak memory models
• Parallelized sequential composition and hardware weak memory models
• Relational thread-modular abstract interpretation under relaxed memory models
• The Rely-Guarantee method for verifying shared variable concurrent programs

Cited in

(1)

• Rely-guarantee reasoning for causally consistent shared memory

This page was built for publication: Compositional reasoning for non-multicopy atomic architectures

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