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.
Chapter PDF
References
Winskel, G.: Event Structure Semantics of CCS and Related Languages. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 561–576. Springer, Heidelberg (1982)
Nielsen, M., Plotkin, G.D., Winskel, G.: Petri Nets, Event Structures and Domains: Part I. Theo. Comp. Sci. 13(1), 85–108 (1981)
van Glabbeek, R.J., Goltz, U.: Refinement of Actions and Equivalence Notions for Concurrent Systems. Acta Informatica 37, 229–327 (2001)
Winskel, G.: Event Structures. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, Springer, Heidelberg (1987)
van Glabbeek, R.J., Plotkin, G.D.: Configuration Structures. In: Proc. 10\(^{\text{th}}\) IEEE Symp. Logics in Computer Science (LICS’95), San Diego, pp. 199–209. IEEE Press, Los Alamitos (1995)
Cenciarelli, P.: Configuration Theories. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 200–215. Springer, Heidelberg (2002)
van Glabbeek, R.J., Plotkin, G.D.: Event Structures for Resolvable Conflicts. In: Fiala, J., Koubek, V., Kratochvíl, J. (eds.) MFCS 2004. LNCS, vol. 3153, pp. 550–561. Springer, Heidelberg (2004)
Gosling, J., et al.: The Java Language Specification, 3rd edn. Addison-Wesley Longman, Amsterdam (2005)
Manson, J., Pugh, W., Adve, S.V.: The Java Memory Model. In: Proc. 32\(^{\text{nd}}\) ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL’05), pp. 378–391. ACM Press, New York (2005)
Winskel, G., Nielsen, M.: Models of Concurrency. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science. Vol. 4: Semantic Modelling, pp. 1–148. Oxford University Press, Oxford (1995)
MacLane, S.: Categories for the Working Mathematician. Springer, New York (1971)
Saraswat, V., et al.: A Theory of Memory Models (2006), http://www.saraswat.org/raofull.pdf
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Cenciarelli, P., Knapp, A., Sibilio, E. (2007). The Java Memory Model: Operationally, Denotationally, Axiomatically. In: De Nicola, R. (eds) Programming Languages and Systems. ESOP 2007. Lecture Notes in Computer Science, vol 4421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71316-6_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-71316-6_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71314-2
Online ISBN: 978-3-540-71316-6
eBook Packages: Computer ScienceComputer Science (R0)