The Java memory model: Operationally, denotationally, axiomatically
P Cenciarelli, A Knapp, E Sibilio - European Symposium on Programming, 2007 - Springer
P Cenciarelli, A Knapp, E Sibilio
European Symposium on Programming, 2007•SpringerA semantics to a small fragment of Java capturing the new memory model (JMM) described
in the Language Specification is given by combining operational, denotational and
axiomatic techniques in a novel semantic framework. The operational steps (specified in the
form of SOS) construct denotational models (configuration structures) and are constrained
by the axioms of a configuration theory. The semantics is proven correct with respect to the
Language Specification and shown to capture many common examples in the JMM …
in the Language Specification is given by combining operational, denotational and
axiomatic techniques in a novel semantic framework. The operational steps (specified in the
form of SOS) construct denotational models (configuration structures) and are constrained
by the axioms of a configuration theory. The semantics is proven correct with respect to the
Language Specification and shown to capture many common examples in the JMM …
Abstract
A semantics to a small fragment of Java capturing the new memory model (JMM) described in the Language Specification is given by combining operational, denotational and axiomatic techniques in a novel semantic framework. The operational steps (specified in the form of SOS) construct denotational models (configuration structures) and are constrained by the axioms of a configuration theory. The semantics is proven correct with respect to the Language Specification and shown to capture many common examples in the JMM literature.
Springer