Plan B, a buffered memory model for Java

DOI10.1145/2429069.2429110MaRDI QIDQ2931808zbMATH OpenOpenAlexFDO

Authors Delphine Demange, Vincent Laporte, Lei Zhao, Suresh Jagannathan, David Pichardie, Jan Vitek

Publication date 27 November 2014

Published in Proceedings of the 40th 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/2429069.2429110

zbMATH Keywords

concurrencyJavamemory modelverified compilation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• The Java memory model
• scientific article; zbMATH DE number 1951189
• Memory model sensitive bytecode verification
• Java and the Java memory model -- a unified, machine-checked formalisation
• Generative operational semantics for relaxed memory models

Cited in

(5)

• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Memory model sensitive bytecode verification
• A denotational semantics for SPARC TSO
• Operational semantics of a weak memory model with channel synchronization
• Operational semantics of a weak memory model with channel synchronization

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Plan B, a buffered memory model for Java

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