Informatics Report Series


Report   

EDI-INF-RR-0958


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Formalising Java's Data-Race-Free Guarantee
Authors: David Aspinall ; Jaroslav Sevcik
Date: 2007
Publication Title:TPHOLs 2007 (LNCS)
Publisher:Springer
Publication Type:Conference Paper Publication Status:Submitted
Volume No:4732 Page Nos:22-37
DOI:10.1007/978-3-540-74591-4_4 ISBN/ISSN:978-3-540-74590-7
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh