Java Memory Model Examples: Good, Bad and Ugly

David Aspinall, Jaroslav Ševčík

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We review a number of illustrative example programs for the Java Memory Model (JMM), relating them to the original design goals and giving intuitive explanations (which can be made precise). We consider good, bad and ugly examples. The good examples are allowed behaviours in the JMM, showing possibilities for non sequentially consistent executions and reordering optimisations. The bad examples are prohibited behaviours, which are clearly ruled out by the JMM. The ugly examples are most interesting: these are tricky cases which illustrate some problem areas for the current formulation of the memory model, where the anticipated design goals are not met. For some of these we mention possible fixes, drawing on knowledge we gained while formalising the memory model in the theorem prover Isabelle.
Original languageEnglish
Title of host publicationProceedings of Verification and Analysis of Multi-Threaded Java-Like Programs (VAMP 2007)
Number of pages15
Publication statusPublished - 2007

Fingerprint Dive into the research topics of 'Java Memory Model Examples: Good, Bad and Ugly'. Together they form a unique fingerprint.

Cite this