The Java memory model

DOI10.1145/1040305.1040336MaRDI QIDQ5276162zbMATH OpenOpenAlexFDO

Authors Jeremy Manson, William Pugh, Sarita V. Adve

Publication date 14 July 2017

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

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

zbMATH Keywords

concurrencyJavamemory modelmultithreading

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

Recommendations

• scientific article; zbMATH DE number 1951189
• Generative operational semantics for relaxed memory models
• Java Memory Model-Aware Model Checking
• Java and the Java memory model -- a unified, machine-checked formalisation
• An operational happens-before memory model

Cited in

(43)

• TSO-to-TSO linearizability is undecidable
• An operational happens-before memory model
• The decidability of verification under PS 2.0
• Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations
• A formal hierarchy of weak memory models
• Complete formal specification of the OpenMP memory model
• Memory model sensitive bytecode verification
• Observations on the assured evolution of concurrent Java programs
• Studying Operational Models of Relaxed Concurrency
• Java Memory Model-Aware Model Checking
• Plan B, a buffered memory model for Java
• Dataflow analysis for datarace-free programs
• Static analysis of run-time errors in embedded critical parallel C programs
• scientific article; zbMATH DE number 2089382 (Why is no real title available?)
• Toward a formal semantic framework for deterministic parallel programming
• A Certified Data Race Analysis for a Java-like Language
• CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
• Formalising Java’s Data Race Free Guarantee
• Pervasive Theory of Memory
• scientific article; zbMATH DE number 1949622 (Why is no real title available?)
• scientific article; zbMATH DE number 1951189 (Why is no real title available?)
• scientific article; zbMATH DE number 1746457 (Why is no real title available?)
• Verification of STM on relaxed memory models
• Fences in weak memory models
• Weak atomicity for the x86 memory consistency model
• Initialization problems for Java
• Modular relaxed dependencies in weak memory concurrency
• Unifying Operational Weak Memory Verification: An Axiomatic Approach
• A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs
• Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model
• Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making
• The Java Memory Model: Operationally, Denotationally, Axiomatically
• Operational semantics of a weak memory model with channel synchronization
• Operational semantics of a weak memory model with channel synchronization
• Sound concurrent traces for online monitoring
• Making Linearizability Compositional for Partially Ordered Executions
• Decidability of liveness for concurrent objects on the TSO memory model
• Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
• Opportunistic monitoring of multithreaded programs
• Interpreting knowledge-based programs
• Model checking race-freedom when ``sequential consistency for data-race-free programs is guaranteed
• Locksynth: deriving synchronization code for concurrent data structures with ASP
• Formal verification of a C-like memory model and its uses for verifying program transformations

This page was built for publication: The Java memory model

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