Write a Blog >>
Thu 23 Jan 2020 11:45 - 12:07 at Ile de France II (IDF II) - Dynamic Program Analysis Chair(s): Peter Thiemann

Writing concurrent programs is highly error-prone due to the nondeterminism in interprocess communication. The most reliable indicators of errors in concurrency are data races, which are accesses to a shared resource that can be executed concurrently. We study the problem of predicting data races in lock-based concurrent programs. The input consists of a concurrent trace t, and the task is to determine all pairs of events of t that constitute a data race. The problem lies at the heart of concurrent verification and has been extensively studied for over three decades. However, existing polynomial-time sound techniques are highly incomplete and can miss simple races.

In this work we develop M2: a new polynomial-time algorithm for this problem, which has no false positives. In addition, our algorithm is complete for input traces that consist of two processes, i.e., it provably detects all races in the trace. We also develop sufficient criteria for detecting completeness dynamically in cases of more than two processes. We make an experimental evaluation of our algorithm on a challenging set of benchmarks taken from recent literature on the topic. Our algorithm soundly reports hundreds of real races, many of which are missed by existing methods. In addition, using our dynamic completeness criteria, M2 concludes that it has detected all races in the benchmark set, hence the reports are both sound and complete. Finally, its running times are comparable, and often smaller than the theoretically fastest, yet highly incomplete, existing methods. To our knowledge, M2 is the first sound algorithm that achieves such a level of performance on both running time and completeness of the reported races.

(main.pdf)446KiB

Thu 23 Jan

Displayed time zone: Saskatchewan, Central America change

11:45 - 12:30
Dynamic Program AnalysisResearch Papers at Ile de France II (IDF II)
Chair(s): Peter Thiemann University of Freiburg, Germany
11:45
22m
Talk
Fast, Sound, and Effectively Complete Dynamic Race Prediction
Research Papers
Andreas Pavlogiannis Aarhus University
Link to publication DOI Media Attached File Attached
12:07
22m
Talk
Detecting Floating-Point Errors via Atomic Conditions
Research Papers
Daming Zou Peking University, Muhan Zeng Peking University, Yingfei Xiong Peking University, Zhoulai Fu IT University of Copenhagen, Denmark, Lu Zhang Peking University, Zhendong Su ETH Zurich
Link to publication DOI Media Attached File Attached