UCL Discovery
UCL home » Library Services » Electronic resources » UCL Discovery

A Compositional Deadlock Detector for Android Java

Brotherston, J; Brunet, P; Gorogiannis, N; Kanovich, M; (2022) A Compositional Deadlock Detector for Android Java. In: Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering. Association for Computing Machinery (ACM) (In press). Green open access

[thumbnail of deadlocks_final.pdf]
deadlocks_final.pdf - Published Version

Download (475kB) | Preview


We develop a static deadlock analysis for commercial Android Java applications, of sizes in the tens of millions of LoC, under active development at Facebook. 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 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 ∼54%.

Type: Proceedings paper
Title: A Compositional Deadlock Detector for Android Java
Event: Automated Software Engineering
Open access status: An open access version is available from UCL Discovery
Publisher version: https://dl.acm.org/conference/ase
Language: English
Additional information: This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions.
Keywords: deadlocks, concurrency, program analysis
UCL classification: UCL
UCL > Provost and Vice Provost Offices > UCL BEAMS
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science
UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science
URI: https://discovery.ucl.ac.uk/id/eprint/10140070
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item