TitleLocking discipline inference and checking
Publication TypeConference Paper
Year of Publication2016
AuthorsErnst MD, Lovato A, Macedonio D, Spoto F, Thaine J
Conference NameICSE 2016, Proceedings of the 38th International Conference on Software Engineering
Pagination1133-1144
Date or Month PublishedMay
Conference LocationAustin, TX, USA
AbstractConcurrency is a requirement for much modern software, but the implementation of multithreaded algorithms comes at the risk of errors such as data races. Programmers can prevent data races by documenting and obeying a locking discipline, which indicates which locks must be held in order to access which data. \par This paper introduces a formal semantics for locking specifications that gives a guarantee of race freedom. A notable difference from most other semantics is that it is in terms of values (which is what the runtime system locks) rather than variables. The paper also shows how to express the formal semantics in two different styles of analysis: abstract interpretation and type theory. We have implemented both analyses, in tools that operate on Java. To the best of our knowledge, these are the first tools that can soundly infer and check a locking discipline for Java. Our experiments compare the implementations with one another and with annotations written by programmers, showing that the ambiguities and unsoundness of previous formulations are a problem in practice.
Downloadshttps://checkerframework.org/ checking implementation https://homes.cs.washington.edu/~mernst/pubs/locking-inference-checking-... PDF
Citation KeyErnstLMST2016