An operational happens-before memory model

DOI10.1007/S11704-015-4492-4zbMath1403.68028OpenAlexW2208855850MaRDI QIDQ1712426

Xinyu Feng, Yang Zhang

Publication date: 22 January 2019

Published in: Frontiers of Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s11704-015-4492-4

zbMATH Keywords

operational semanticshappens-beforeDRF-guaranteeJMMrelaxed memory model

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Operational semantics of a weak memory model with channel synchronization ⋮ Operational semantics of a weak memory model with channel synchronization

Cites Work

• Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it
• Java and the Java Memory Model — A Unified, Machine-Checked Formalisation
• Formalising Java’s Data Race Free Guarantee
• Generative Operational Semantics for Relaxed Memory Models
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Time, clocks, and the ordering of events in a distributed system
• The Java memory model
• The Java Memory Model: Operationally, Denotationally, Axiomatically

This page was built for publication: An operational happens-before memory model