Relaxed memory models

DOI10.1145/1480881.1480930MaRDI QIDQ5261535zbMATH OpenOpenAlexFDO

Authors Gérard Boudol, Gustavo Petri

Publication date 3 July 2015

Published in Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

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

zbMATH Keywords

operational semanticsmemory models

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Recommendations

• Generative operational semantics for relaxed memory models
• An operational happens-before memory model
• Relationships between memory models
• A calculus for relaxed memory
• A model of memory dynamics
• scientific article; zbMATH DE number 1728265
• A formal hierarchy of weak memory models

Cited in

(23)

• A promising semantics for relaxed-memory concurrency
• Context-bounded analysis of TSO systems
• Operational semantics of a weak memory model with channel synchronization
• A denotational semantics for SPARC TSO
• Operational semantics of a weak memory model with channel synchronization
• Parallelized sequential composition and hardware weak memory models
• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• Verification of STM on relaxed memory models
• Operational semantics with semicommutations
• Observation-based concurrent program logic for relaxed memory consistency models
• Brookes is relaxed, almost!
• Relaxed operational semantics of concurrent programming languages
• Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
• A denotational semantics for SPARC TSO
• Verified software toolchain (invited talk)
• A calculus for relaxed memory
• Programmer-centric memory consistency modelling
• Studying Operational Models of Relaxed Concurrency
• An axiomatic specification for sequential memory models
• A formal hierarchy of weak memory models
• Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
• An operational happens-before memory model
• Generative operational semantics for relaxed memory models

This page was built for publication: Relaxed memory models

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