# Fast, Sound and Effectively Complete Dynamic Race Prediction

## TL;DR

This paper introduces M2, a novel polynomial-time algorithm for dynamic data race prediction in lock-based concurrent programs that is both sound and complete for two-process traces, outperforming existing methods.

## Contribution

The paper presents M2, the first sound and complete polynomial-time algorithm for dynamic race prediction in two-process traces, with effective partial completeness for more processes.

## Key findings

- M2 detects all races in two-process traces.
- The tool reports thousands of races with at most one miss.
- Running times are comparable or better than existing methods.

## Abstract

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 consecutively. 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 many 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 conditions for detecting completeness dynamically in cases of more than two processes. We make an experimental evaluation of our algorithm on a standard set of benchmarks taken from recent literature on the topic. Our tool soundly reports thousands of races and misses at most one race in the whole benchmark set. In addition, our technique detects all racy memory locations of the benchmark set. 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.