(PLDI 2021) When Threads Meet Events: Efficient and Precise Static Race Detection with Origins
Data races are among the worst bugs in software in that they exhibit non-deterministic symptoms and are notoriously difficult to detect. The problem is exacerbated by interactions between threads and events in real-world software. We present a novel static technique, O2, to detect data races in large complex multithreaded and event-driven software. O2 is powered by “origins”, an abstraction that unifies threads and events by treating them as entry points of code paths attributed with data pointers. Origins in most cases are inferred automatically through static analysis, but can be also specified by developers. More importantly, origins provide an efficient way to precisely reason about shared memory and pointer aliases.
We have implemented O2 for both C/C++ and JVM applications and applied it to a wide range of open source software. O2 has found new races in every single real-world code base we have evaluated with, including Linux kernel, Redis, OVS, Memcached, Hadoop, Tomcat, ZooKeeper and Firefox Android apps. Moreover, O2 scales to millions of lines of code in a few minutes, on average 70x faster (up to 568x) compared to existing static analysis tools, and reduces 77% false positives. Moreover, O2 outperforms the state-of-the-art static race detection tool, RacerD, by the similar performance and 6x less reported false positives on average. At the time of writing, O2 has revealed more than 40 unique previously unknown races that have been confirmed or fixed by developers.
Wed 15 JunDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 16:50
|(PLDI 2020) Inductive Sequentialization of Asynchronous Programs|
|(PLDI 2021) When Threads Meet Events: Efficient and Precise Static Race Detection with Origins|
|(POPL 2021) Optimal Prediction of Synchronization-Preserving Races|
|(POPL 2022) Visibility Reasoning for Concurrent Snapshot Algorithms|