TY - JOUR

T1 - Optimal prediction of synchronization-preserving races

AU - Mathur, Umang

AU - Pavlogiannis, Andreas

AU - Viswanathan, Mahesh

N1 - Funding Information:
We thank anonymous reviewers for their constructive feedback on an earlier draft of this manuscript. Umang Mathur is partially supported by a Google PhD Fellowship. Mahesh Viswanathan is partially supported by grants NSF SHF 1901069 and NSF CCF 2007428.
Publisher Copyright:
© 2021 Owner/Author.

PY - 2021/1

Y1 - 2021/1

N2 - Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce. The most common concurrency errors are (data) races, which occur when memory-conflicting actions are executed concurrently. Consequently, considerable effort has been made towards developing efficient techniques for race detection. The most common approach is dynamic race prediction: given an observed, race-free trace σ of a concurrent program, the task is to decide whether events of σ can be correctly reordered to a trace σ∗ that witnesses a race hidden in σ. In this work we introduce the notion of sync(hronization)-preserving races. A sync-preserving race occurs in σ when there is a witness σ∗ in which synchronization operations (e.g., acquisition and release of locks) appear in the same order as in σ. This is a broad definition that strictly subsumes the famous notion of happens-before races. Our main results are as follows. First, we develop a sound and complete algorithm for predicting sync-preserving races. For moderate values of parameters like the number of threads, the algorithm runs in Õ(N) time and space, where N is the length of the trace σ. Second, we show that the problem has a ω(N/log2 N) space lower bound, and thus our algorithm is essentially time and space optimal. Third, we show that predicting races with even just a single reversal of two sync operations is NP-complete and even W1-hard when parameterized by the number of threads. Thus, sync-preservation characterizes exactly the tractability boundary of race prediction, and our algorithm is nearly optimal for the tractable side. Our experiments show that our algorithm is fast in practice, while sync-preservation characterizes races often missed by state-of-the-art methods.

AB - Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce. The most common concurrency errors are (data) races, which occur when memory-conflicting actions are executed concurrently. Consequently, considerable effort has been made towards developing efficient techniques for race detection. The most common approach is dynamic race prediction: given an observed, race-free trace σ of a concurrent program, the task is to decide whether events of σ can be correctly reordered to a trace σ∗ that witnesses a race hidden in σ. In this work we introduce the notion of sync(hronization)-preserving races. A sync-preserving race occurs in σ when there is a witness σ∗ in which synchronization operations (e.g., acquisition and release of locks) appear in the same order as in σ. This is a broad definition that strictly subsumes the famous notion of happens-before races. Our main results are as follows. First, we develop a sound and complete algorithm for predicting sync-preserving races. For moderate values of parameters like the number of threads, the algorithm runs in Õ(N) time and space, where N is the length of the trace σ. Second, we show that the problem has a ω(N/log2 N) space lower bound, and thus our algorithm is essentially time and space optimal. Third, we show that predicting races with even just a single reversal of two sync operations is NP-complete and even W1-hard when parameterized by the number of threads. Thus, sync-preservation characterizes exactly the tractability boundary of race prediction, and our algorithm is nearly optimal for the tractable side. Our experiments show that our algorithm is fast in practice, while sync-preservation characterizes races often missed by state-of-the-art methods.

KW - complexity

KW - concurrency

KW - dynamic analysis

KW - race detection

UR - http://www.scopus.com/inward/record.url?scp=85099035795&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85099035795&partnerID=8YFLogxK

U2 - 10.1145/3434317

DO - 10.1145/3434317

M3 - Article

AN - SCOPUS:85099035795

VL - 5

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

SN - 2475-1421

IS - POPL

M1 - 36

ER -