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.
The Java Memory Model: Operationally, Denotationally, Axiomatically / Cenciarelli, Pietro; Alexander, Knapp; Eleonora, Sibilio. - LNCS 4421:(2007), pp. 329-346. (Intervento presentato al convegno 16th European Symposium on Programming, ESOP tenutosi a Braga (Portugal) nel March 2007) [10.1007/978-3-540-71316-6_23].
The Java Memory Model: Operationally, Denotationally, Axiomatically
CENCIARELLI, Pietro;
2007
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
