Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Thu 21 Jan 2021 16:30 - 16:40 at POPL-B - Concurrency (Shared Memory)

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 efforts are made towards efficient techniques for race detection. The most usual 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 W[1]-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.

Thu 21 Jan

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

16:00 - 17:00
Concurrency (Shared Memory)POPL at POPL-B
16:00
10m
Talk
Verifying Observational Robustness Against a C11-style Memory Model
POPL
Roy Margalit Tel Aviv University, Israel, Ori Lahav Tel Aviv University
Link to publication DOI
16:10
10m
Talk
Provably Space Efficient Parallel Functional ProgrammingDistinguished Paper
POPL
Jatin Arora CMU, Sam Westrick Carnegie Mellon University, Umut A. Acar Carnegie Mellon University
Link to publication DOI
16:20
10m
Talk
Modeling and Analyzing Evaluation Cost of CUDA Kernels
POPL
Stefan K. Muller Illinois Institute of Technology, Jan Hoffmann Carnegie Mellon University
Link to publication DOI
16:30
10m
Talk
Optimal Prediction of Synchronization-Preserving Races
POPL
Umang Mathur University of Illinois at Urbana-Champaign, Andreas Pavlogiannis Aarhus University, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print
16:40
10m
Talk
Taming x86-TSO Persistency
POPL
Artem Khyzha Tel Aviv University, Ori Lahav Tel Aviv University
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL