- Abstract:
-
We present a formalisation of the data race free guarantee provided by Java, as captured by the semi-formal Java Memory Model. The data race free (DRF) guarantee says that all programs which are correctly synchronised (free of data races) can only have sequentially consistent behaviours, so they can be understood intuitively by programmers. By formalising this in a theorem prover, we have achieved three main aims. First, we have made the definitions and proofs precise, leading to a better understanding. Our analysis found several hidden inconsistencies and missing details. Second, once we built a formal definition, we could explore variations and investigate their impact in the proof with the aim of simplifying the JMM; we found that not all of the conditions in the JMM definition are necessary for the DRF guarantee. This allows us to suggest a quick fix to the serious bug discovered by Cenciarelli et al (2007) without invalidating the DRF guarantee. Finally, the formal definition provides a basis to test concrete examples, and investigate JMM-aware logics for concurrent programs in future work.
- Links To Paper
- 1st Link
- Bibtex format
- @InProceedings{EDI-INF-RR-0958,
- author = {
David Aspinall
and Jaroslav Sevcik
},
- title = {Formalising Java's Data-Race-Free Guarantee},
- book title = {TPHOLs 2007 (LNCS)},
- publisher = {Springer},
- year = 2007,
- volume = {4732},
- pages = {22-37},
- doi = {10.1007/978-3-540-74591-4_4},
- url = {http://groups.inf.ed.ac.uk/request/jmmform.pdf},
- }
|