The Java memory model
From MaRDI portal
Publication:5276162
DOI10.1145/1040305.1040336zbMath1369.68079OpenAlexW2091085450MaRDI QIDQ5276162
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
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of programming languages (68N15)
Related Items (28)
Modular Relaxed Dependencies in Weak Memory Concurrency ⋮ TSO-to-TSO linearizability is undecidable ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ A Certified Data Race Analysis for a Java-like Language ⋮ CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types ⋮ Sound concurrent traces for online monitoring ⋮ Making Linearizability Compositional for Partially Ordered Executions ⋮ Decidability of liveness for concurrent objects on the TSO memory model ⋮ An operational happens-before memory model ⋮ A formal hierarchy of weak memory models ⋮ Verification of STM on relaxed memory models ⋮ Fences in weak memory models ⋮ Weak atomicity for the x86 memory consistency model ⋮ Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language ⋮ Complete formal specification of the OpenMP memory model ⋮ Dataflow Analysis for Datarace-Free Programs ⋮ Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs ⋮ The decidability of verification under PS 2.0 ⋮ Memory model sensitive bytecode verification ⋮ Formal verification of a C-like memory model and its uses for verifying program transformations ⋮ Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations ⋮ A Sound and Complete Shared-Variable Concurrency Model for Multi-threaded Java Programs ⋮ Operational semantics of a weak memory model with channel synchronization ⋮ Operational semantics of a weak memory model with channel synchronization ⋮ Static Analysis Via Abstract Interpretation of the Happens-Before Memory Model ⋮ Toward a Formal Semantic Framework for Deterministic Parallel Programming ⋮ Studying Operational Models of Relaxed Concurrency ⋮ Observations on the assured evolution of concurrent Java programs
This page was built for publication: The Java memory model
