Modular relaxed dependencies in weak memory concurrency

DOI10.1007/978-3-030-44914-8_22MaRDI QIDQ5041113zbMATH OpenOpenAlexFDO

Authors

Publication date 13 October 2022

Published in Programming Languages and Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-44914-8_22

zbMATH Keywords

compiler optimisationscompositionalitydenotational semanticsthin-air problemweak memory concurrency

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of compilers and interpreters (68N20) Semantics in the theory of computing (68Q55)

Recommendations

• A promising semantics for relaxed-memory concurrency
• A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
• Studying Operational Models of Relaxed Concurrency

Cites work

• A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
• A denotational semantics for SPARC TSO
• A promising semantics for relaxed-memory concurrency
• Automatically comparing memory consistency models
• Coinductive big-step operational semantics
• Compositional verification of compiler optimisations on relaxed memory
• Domain-Theoretic Foundations of Functional Programming
• scientific article; zbMATH DE number 3988722 (Why is no real title available?)
• scientific article; zbMATH DE number 4119660 (Why is no real title available?)
• Mathematizing C++ concurrency
• Overhauling SC atomics in C11 and OpenCL
• The Java memory model

Cited in

(6)

• Operational semantics with semicommutations
• The decidability of verification under PS 2.0
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• Reasoning about promises in weak memory models with event structures
• Mechanised operational reasoning for C11 programs with relaxed dependencies
• Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL

This page was built for publication: Modular relaxed dependencies in weak memory concurrency

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