Blogs (9) >>
SPLASH 2016
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Thu 3 Nov 2016 11:45 - 12:10 at Matterhorn 1 - Concurrency Analysis and Model Checking Chair(s): Thomas Gross

We present RDIT, a novel dynamic technique to detect data races in multithreaded programs with incomplete trace information, i.e., in the presence of missing events. RDIT is both precise and maximal: it does not report any false alarms and it detects a maximal set of true traces from the observed incomplete trace. RDIT is underpinned by a sound BarrierPair model that abstracts away the missing events by capturing the invocation data of their enclosing methods. By making the least conservative abstraction that a missing method introduces synchronization only when it has a memory address in scope that overlaps with other events or other missing methods, and by formulating maximal thread causality as logical constraints, RDIT guarantees to precisely detect races with maximal capability. RDIT has been applied in seven real-world large concurrent systems and has detected dozens of true races with zero false alarms. Comparatively, existing algorithms such as Happens-Before, Causal- Precedes, and Maximal-Causality which are known to be precise all report many false alarms when missing synchronizations.

Thu 3 Nov

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10
Concurrency Analysis and Model CheckingOOPSLA at Matterhorn 1
Chair(s): Thomas Gross ETH Zurich
10:30
25m
Talk
Directed Synthesis of Failing Concurrent Executions
OOPSLA
Malavika Samak Indian Institute of Science, Bangalore, Omer Tripp IBM Research, USA, Murali Krishna Ramanathan Indian Institute of Science, Bangalore
DOI Media Attached
10:55
25m
Talk
Maximal Causality Reduction for TSO and PSO
OOPSLA
Shiyou Huang Texas A&M University, Jeff Huang Texas A&M University
DOI
11:20
25m
Talk
Stateless Model Checking with Data-Race Preemption Points
OOPSLA
Ben Blum Carnegie Mellon University, Garth Gibson Carnegie Mellon University
DOI Pre-print Media Attached
11:45
25m
Talk
Precise and Maximal Race Detection from Incomplete Traces
OOPSLA
Jeff Huang Texas A&M University, Arun Krishnakumar Rajagopalan Texas A&M University
DOI Media Attached