| Title | Locking discipline inference and checking |
| Publication Type | Conference Paper |
| Year of Publication | 2016 |
| Authors | Ernst MD, Lovato A, Macedonio D, Spoto F, Thaine J |
| Conference Name | ICSE 2016, Proceedings of the 38th International Conference on Software Engineering |
| Pagination | 1133-1144 |
| Date or Month Published | May |
| Conference Location | Austin, TX, USA |
| Abstract | Concurrency 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. |
| Downloads | https://checkerframework.org/ checking implementation
https://homes.cs.washington.edu/~mernst/pubs/locking-inference-checking-... PDF
|
| Citation Key | ErnstLMST2016 |
