| Title | Locking discipline inference and checking |
| Publication Type | Miscellaneous |
| Year of Publication | 2015 |
| Authors | Ernst MD, Lovato A, Macedonio D, Spoto F, Thaine J |
| Date or Month Published | September |
| 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. The paper also provides two implementations of the formal semantics for the Java language: one based on abstract interpretation and one based on type theory. 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. |
| Downloads | https://homes.cs.washington.edu/~mernst/pubs/locking-inference-checking-... PDF
|
| Citation Key | ErnstLMST2015 |
