Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 10:35 - 10:57 at Sala II - Concurrency Chair(s): Ori Lahav

RacerD is a static race detector that has been proven to be effective in engineering practice: it has seen thousands of data races fixed by developers before reaching production, and has supported the migration of Facebook’s Android app from a single-threaded to a multi-threaded architecture. We prove a True Positives Theorem stating that under certain assumptions, which reflect the way that product code (but not infrastructure code) uses concurrency, an idealized theoretical version of the analysis never reports a false positive. We also provide an empirical evaluation of an implementation of this analysis, versus the original RacerD.

The theorem was motivated in the first case by the desire to understand the observation from production that RacerD was providing remarkably accurate signal to developers, and then the theorem guided further analyzer design decisions. Technically, our result can be seen as saying that the analysis computes an under-approximation of an over-approximation, which is the reverse of the more usual (over of under) situation in static analysis. We suggest that theorems of this variety might be generally useful in designing static analyses for bug catching.

Slides (tpt-popl19.pdf)1.49MiB

Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change

10:35 - 12:03: ConcurrencyResearch Papers at Sala II
Chair(s): Ori LahavTel Aviv University
10:35 - 10:57
A True Positives Theorem for a Static Race Detector
Research Papers
Nikos Gorogiannis, Peter W. O'HearnFacebook and University College London, Ilya SergeyYale-NUS College and National University of Singapore
Link to publication DOI Pre-print Media Attached File Attached
10:57 - 11:19
Decoupling Lock-Free Data Structures from Memory Reclamation for Static Analysis
Research Papers
Link to publication DOI Pre-print Media Attached File Attached
11:19 - 11:41
Pretend Synchrony: Synchronous Verification of Asynchronous Distributed Programs
Research Papers
Klaus v. GleissenthallUniversity of California at San Diego, USA, Rami Gökhan KıcıUniversity of California at San Diego, USA, Alexander Bakst, Deian StefanUniversity of California San Diego, Ranjit JhalaUniversity of California, San Diego
Link to publication DOI Media Attached
11:41 - 12:03
Weak-Consistency Specification via Visibility Relaxation
Research Papers
Michael EmmiSRI International, Constantin EneaUniversité Paris Diderot
Link to publication DOI Media Attached File Attached