{"id":548,"date":"2022-03-08T17:00:41","date_gmt":"2022-03-08T17:00:41","guid":{"rendered":"https:\/\/fde.cat\/index.php\/2022\/03\/08\/an-open-source-compositional-deadlock-detector-for-android-java\/"},"modified":"2022-03-08T17:00:41","modified_gmt":"2022-03-08T17:00:41","slug":"an-open-source-compositional-deadlock-detector-for-android-java","status":"publish","type":"post","link":"https:\/\/fde.cat\/index.php\/2022\/03\/08\/an-open-source-compositional-deadlock-detector-for-android-java\/","title":{"rendered":"An open source compositional deadlock detector for Android Java"},"content":{"rendered":"

What the research is:<\/span><\/h2>\n

We\u2019ve developed a new static analyzer<\/a> that catches deadlocks in Java code for Android without ever running the code. What distinguishes our analyzer from past research is its ability to analyze revisions in codebases with hundreds of millions of lines of code.<\/span><\/p>\n

We have deployed our analyzer in Meta\u2019s continuous integration system, where it scans every commit to the Android app family. In the last two years, developers have actioned over 200 fixes in response to deadlock reports, at a fix rate of around 54 percent.<\/span><\/p>\n

Our analyzer is open source and forms part of the<\/span> Infer static analysis framework<\/span><\/a>.<\/span><\/p>\n

How it works:<\/span><\/h2>\n

We used abstract interpretation techniques to design our analyzer. For each method, the analyzer computes a summary of how the method behaves in terms of lock acquisition and release, as well as whether the method will run on the main thread or on a background thread. This is done in a compositional manner: Each method is summarized once, at most, and its summary is used in the summarization of its callers, ensuring predictable high performance.<\/span><\/p>\n

The central part of the summary is the set of critical pairs<\/span> of the method. A critical pair (A,B) records the following fact: The method tries to acquire lock B, and at that time, it\u2019s already holding precisely locks in set A. This data, computed across all methods, is enough to let us answer the question of whether a deadlock is possible between two concurrent methods.<\/span><\/p>\n

To be fast and efficient, our tool avoids analyzing all source files in an app. Instead, it first processes all methods in the revision\u2019s modified files. Then, based on that data, it applies a heuristic that locates methods outside the revision that could potentially deadlock with one of the methods in the revision. It is this heuristic that enables our analysis to scale.<\/span><\/p>\n

In our <\/span>paper<\/span><\/a>, we also prove that our analysis is sound and complete for an abstract programming language that has only non-deterministic control. In other words, in this language, we can find all the deadlocks without false positives.<\/span><\/p>\n

<\/h2>\n

Why it matters:<\/span><\/h2>\n

A deadlock is typically an unrecoverable error. Deadlocks are also very difficult bugs to diagnose because thread scheduling is essentially non-deterministic and, thus, a test might need to run thousands or millions of times in order to exhibit the problem.<\/span><\/p>\n

Detecting deadlocks statically, without running or even building the code is, therefore, extremely valuable. Our approach achieves this goal while also making the analyzer sufficiently scalable so that it can be deployed on the massive codebases at Meta.<\/span><\/p>\n

Read the full paper<\/span><\/h2>\n

A compositional deadlock detector for Android Java<\/span><\/a><\/p>\n

Acknowledgements<\/span><\/h2>\n

Additional thanks to the co-authors of this research, James Brotherston, Paul Brunet, and Max Kanovich, all at University College London (UCL).<\/span><\/p>\n

The post An open source compositional deadlock detector for Android Java<\/a> appeared first on Engineering at Meta<\/a>.<\/p>\n

Engineering at Meta<\/p>","protected":false},"excerpt":{"rendered":"

What the research is: We\u2019ve developed a new static analyzer that catches deadlocks in Java code for Android without ever running the code. What distinguishes our analyzer from past research is its ability to analyze revisions in codebases with hundreds of millions of lines of code. We have deployed our analyzer in Meta\u2019s continuous integration… Continue reading An open source compositional deadlock detector for Android Java<\/span><\/a><\/p>\n","protected":false},"author":0,"featured_media":0,"comment_status":"","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"spay_email":"","footnotes":""},"categories":[7],"tags":[],"class_list":["post-548","post","type-post","status-publish","format-standard","hentry","category-technology","entry"],"jetpack_featured_media_url":"","jetpack-related-posts":[{"id":170,"url":"https:\/\/fde.cat\/index.php\/2020\/12\/14\/infer-powering-microsofts-infer-a-new-static-analyzer-for-c\/","url_meta":{"origin":548,"position":0},"title":"Infer powering Microsoft\u2019s Infer#, a new static analyzer for C#","date":"December 14, 2020","format":false,"excerpt":"What it is: Infer# brings the Infer static analysis platform to developers who use Microsoft\u2019s C# programming language. It can already detect null-pointer dereference and resource leak bugs, thanks to bi-abduction analysis. Detection of race conditions based on RacerD analysis is also in the works. Infer# has been used to\u2026","rel":"","context":"In "External"","img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":656,"url":"https:\/\/fde.cat\/index.php\/2022\/11\/22\/retrofitting-null-safety-onto-java-at-meta\/","url_meta":{"origin":548,"position":1},"title":"Retrofitting null-safety onto Java at Meta","date":"November 22, 2022","format":false,"excerpt":"We developed a new static analysis tool called Nullsafe that is used at Meta to detect NullPointerException (NPE) errors in Java code. Interoperability with legacy code and gradual deployment model were key to Nullsafe\u2019s wide adoption and allowed us to recover some null-safety properties in the context of an otherwise\u2026","rel":"","context":"In "Technology"","img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":480,"url":"https:\/\/fde.cat\/index.php\/2021\/09\/29\/open-sourcing-mariana-trench-analyzing-android-and-java-app-security-in-depth\/","url_meta":{"origin":548,"position":2},"title":"Open-sourcing Mariana Trench: Analyzing Android and Java app security in depth","date":"September 29, 2021","format":false,"excerpt":"We\u2019re sharing details about Mariana Trench (MT), a tool we use to spot and prevent security and privacy bugs in Android and Java applications. As part of our effort to help scale security through building automation, we recently open-sourced MT to support security engineers at Facebook and across the industry.\u00a0\u2026","rel":"","context":"In "Technology"","img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":286,"url":"https:\/\/fde.cat\/index.php\/2021\/08\/31\/sre-weekly-issue-262\/","url_meta":{"origin":548,"position":3},"title":"SRE Weekly Issue #262","date":"August 31, 2021","format":false,"excerpt":"View on sreweekly.com A message from our sponsor, StackHawk: Join the Secure Coding Summit to hear from industry-leading AppSec and DevSecOps practitioners, analysts, and visionaries as they share their best pro tips to level up your code security. http:\/\/sthwk.com\/secure-code-summit Articles The Prerequisites for Chaos Engineering Chaos Engineering isn\u2019t adding chaos\u2026","rel":"","context":"In "SRE"","img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":492,"url":"https:\/\/fde.cat\/index.php\/2021\/10\/20\/facebook-engineers-receive-2021-ieee-computer-society-cybersecurity-award-for-static-analysis-tools\/","url_meta":{"origin":548,"position":4},"title":"Facebook engineers receive 2021 IEEE Computer Society Cybersecurity Award for static analysis tools","date":"October 20, 2021","format":false,"excerpt":"Until recently, static analysis tools weren\u2019t seen by our industry as a reliable element of securing code at scale. After nearly a decade of investing in refining these systems, I\u2019m so proud to celebrate our engineering teams today for being awarded the IEEE Computer Society\u2019s Cybersecurity Award for Practice for\u2026","rel":"","context":"In "Technology"","img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]},{"id":728,"url":"https:\/\/fde.cat\/index.php\/2023\/06\/27\/meta-developer-tools-working-at-scale\/","url_meta":{"origin":548,"position":5},"title":"Meta developer tools: Working at scale","date":"June 27, 2023","format":false,"excerpt":"Every day, thousands of developers at Meta are working in repositories with millions of files. Those developers need tools that help them at every stage of the workflow while working at extreme scale. In this article we\u2019ll go through a few of the tools in the development process. And, as\u2026","rel":"","context":"In "Technology"","img":{"alt_text":"","src":"","width":0,"height":0},"classes":[]}],"_links":{"self":[{"href":"https:\/\/fde.cat\/index.php\/wp-json\/wp\/v2\/posts\/548","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/fde.cat\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/fde.cat\/index.php\/wp-json\/wp\/v2\/types\/post"}],"replies":[{"embeddable":true,"href":"https:\/\/fde.cat\/index.php\/wp-json\/wp\/v2\/comments?post=548"}],"version-history":[{"count":0,"href":"https:\/\/fde.cat\/index.php\/wp-json\/wp\/v2\/posts\/548\/revisions"}],"wp:attachment":[{"href":"https:\/\/fde.cat\/index.php\/wp-json\/wp\/v2\/media?parent=548"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/fde.cat\/index.php\/wp-json\/wp\/v2\/categories?post=548"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/fde.cat\/index.php\/wp-json\/wp\/v2\/tags?post=548"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}