We develop a static deadlock analysis for commercial Android Java applications, of sizes in the tens of millions of LOC, under active development at a major tech company. The analysis runs primarily at code-review time, on only the modified code and its dependents; we aim at reporting to developers in under 15 minutes.
To detect deadlocks in this setting, we first model the real language as an abstract language with balanced re-entrant locks, nondeterministic iteration and branching, and non-recursive procedure calls. We show that the existence of a deadlock in this abstract language is equivalent to a certain condition over the sets of so-called \emph{critical pairs} of each program thread; these record, for all possible executions of the thread, which locks are currently held at the point when a fresh lock is acquired. Since the critical pairs of any program thread is finite and computable, the deadlock detection problem for our language is decidable, and in NP.
We then leverage these results to develop an open-source implementation of our analysis adapted to deal with real Java code. The core of the implementation is an algorithm which computes critical pairs in a compositional, abstract interpretation style, running in quasi-exponential time. Our analyser is built in the INFER verification framework and has been in industrial deployment for over two years; it has seen over two hundred fixed deadlock reports with a report fix rate of approximately 54%.
Thu 18 NovDisplayed time zone: Hobart change
21:00 - 22:00 | |||
21:00 20mTalk | Learning Domain-Specific Edit Operations from Model Repositories with Frequent Subgraph Mining Research Papers Christof Tinnes Saarland University, Timo Kehrer Humboldt University of Berlin, Mitchell Joblin Siemens AG, Uwe Hohenstein Siemens AG, Andreas Biesdorf Siemens AG, Sven Apel Saarland University | ||
21:20 20mTalk | Unsupervised Labeling and Extraction of Phrase-based Concepts in Vulnerability Descriptions Research Papers Sofonias Yitagesu Tianjin University, Zhenchang Xing Australian National University, Xiaowang Zhang Tianjin University, Zhiyong Feng Tianjin University, Xiaohong Li TianJin University, Linyi Han Tianjin University | ||
21:40 20mTalk | A Compositional Deadlock Detector for Android Java Research Papers James Brotherston , Paul Brunet University College London, Nikos Gorogiannis Facebook, Max Kanovich University College London |