Dynamic Probabilistic Inference of Atomic Sets
(English)Manuscript (preprint) (Other academic)
Concurrent programs often ensure the consistency of their data structures through synchronization. Because control-centric synchronization primitives, such as locks, are disconnected from the consistency invariants of the data structures, a compiler cannot check and and enforce these invariants - making it hard to detect bugs caused by incorrect synchronization. Moreover, a consistency bug may be the result of some unlikely schedule and therefore not show up in program testing. In contrast, data-centric synchronization adds annotations to data structures, defining sets of fields that must be accessed atomically. A compiler can check such annotations for consistency, detect deadlock, and automatically add primitives to prevent data races. However, annotating existing code is time consuming and error prone because it requires understanding the concurrency semantics implemented in the code. We propose a novel algorithm, called BAIT, for deriving such annotations automatically from observed program executions using Bayesian probabilistic inference. The algorithm produces atomic set, unit of work, and alias annotations for atomic-set based synchronization. Using our implementation of the algorithm, we have derived annotations for large code bases, for example the Java collections framework, in a matter of seconds. A comparison of the inferred annotations against manually converted programs, and two case studies on large, widely-used programs, show that our implementation derives detailed annotations of high quality.
atomic sets, data-centric synchronization, bayesian inference
Research subject Computer Science
IdentifiersURN: urn:nbn:se:kth:diva-152241OAI: oai:DiVA.org:kth-152241DiVA: diva2:749498
QS 20142014-09-242014-09-242014-09-29Bibliographically approved