Formalising Java’s Data Race Free Guarantee

David Aspinall, Jaroslav Ševčík

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

Abstract / Description of output

We formalise the data race free (DRF) guarantee provided by Java, as captured by the semi-formal Java Memory Model (JMM) [1] and published in the Java Language Specification [2].The DRF guarantee says that all programs which are correctly synchronised (i.e., free of data races) can only have sequentially consistent behaviours. Such programs can be understood intuitively by programmers. Formalisation has achieved three aims. First, we made definitions and proofs precise, leading to a better understanding; our analysis found several hidden inconsistencies and missing details. Second, the formalisation lets us explore variations and investigate their impact in the proof with the aim of simplifying the model; we found that not all of the anticipated conditions in the JMM definition were actually necessary for the DRF guarantee. This allows us to suggest a quick fix to a recently discovered serious bug [3] without invalidating the DRF guarantee. Finally, the formal definition provides a basis to test concrete examples, and opens the way for future work on JMM-aware logics for concurrent programs.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007. Proceedings
EditorsKlaus Schneider, Jens Brandt
PublisherSpringer
Pages22-37
Number of pages16
ISBN (Electronic)978-3-540-74591-4
ISBN (Print)978-3-540-74590-7
DOIs
Publication statusPublished - 2007

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume4732

Fingerprint

Dive into the research topics of 'Formalising Java’s Data Race Free Guarantee'. Together they form a unique fingerprint.

Cite this