 NSFPAR ID:
 10299930
 Date Published:
 Journal Name:
 Proceedings of the ACM on Programming Languages
 Volume:
 5
 Issue:
 POPL
 ISSN:
 24751421
 Page Range / eLocation ID:
 1 to 29
 Format(s):
 Medium: X
 Sponsoring Org:
 National Science Foundation
More Like this

Writing concurrent programs is notoriously hard due to scheduling nondeterminism. The most common concurrency bugs are data races, which are accesses to a shared resource that can be executed concurrently. Dynamic datarace prediction is the most standard technique for detecting data races: given an observed, dataracefree trace t, the task is to determine whether t can be reordered to a trace t* that exposes a datarace. Although the problem has received significant practical attention for over three decades, its complexity has remained elusive. In this work, we address this lacuna, identifying sources of intractability and conditions under which the problem is efficiently solvable. Given a trace t of size n over k threads, our main results are as follows. First, we establish a general O(k · n2·(k1) upperbound, as well as an O(nk) upperbound when certain parameters of t are constant. In addition, we show that the problem is NPhard and even W[1]hard parameterized by k, and thus unlikely to be fixedparameter tractable. Second, we study the problem over acyclic communication topologies, such as serverclients hierarchies. We establish an O(k2 · d · n2 · log n) upperbound, where d is the number of shared variables accessed in t. In addition, we show that even for traces with k = 2 threads, the problem has no O(n2ϵ) algorithm under the Orthogonal Vectors conjecture. Since any trace with 2 threads defines an acyclic topology, our upperbound for this case is optimal up to polynomial improvements for up to moderate values of k and d. Finally, motivated by existing heuristics, we study a distancebounded version of the problem, where the task is to expose a data race by a witness trace that is similar to t. We develop an algorithm that works in O(n) time when certain parameters of t are constant.more » « less

Deadlocks are one of the most notorious concurrency bugs, and significant research has focused on detecting them efficiently. Dynamic predictive analyses work by observing concurrent executions, and reason about alternative interleavings that can witness concurrency bugs. Such techniques offer scalability and sound bug reports, and have emerged as an effective approach for concurrency bug detection, such as data races. Effective dynamic deadlock prediction, however, has proven a challenging task, as no deadlock predictor currently meets the requirements of soundness, highprecision, and efficiency.
In this paper, we first formally establish that this tradeoff is unavoidable, by showing that (a) sound and complete deadlock prediction is intractable, in general, and (b) even the seemingly simpler task of determining the presence of potential deadlocks, which often serve as unsound witnesses for actual predictable deadlocks, is intractable. The main contribution of this work is a new class of predictable deadlocks, called sync(hronization)preserving deadlocks. Informally, these are deadlocks that can be predicted by reordering the observed execution while preserving the relative order of conflicting critical sections. We present two algorithms for sound deadlock prediction based on this notion. Our first algorithm SPDOffline detects all syncpreserving deadlocks, with running time that is linear per abstract deadlock pattern, a novel notion also introduced in this work. Our second algorithm SPDOnline predicts all syncpreserving deadlocks that involve two threads in a strictly online fashion, runs in overall linear time, and is better suited for a runtime monitoring setting.
We implemented both our algorithms and evaluated their ability to perform offline and online deadlockprediction on a large dataset of standard benchmarks. Our results indicate that our new notion of syncpreserving deadlocks is highly effective, as (i) it can characterize the vast majority of deadlocks and (ii) it can be detected using an online, sound, complete and highly efficient algorithm.

Happens beforebased dynamic analysis is the goto technique for detecting data races in large scale software projects due to the absence of false positive reports. However, such analyses are expensive since they employ expensive vector clock updates at each event, rendering them usable only for inhouse testing. In this paper, we present a samplingbased, randomized race detector that processes only
constantly many events of the input trace even in the worst case. This is the firstsublinear time (i.e., running ino (n ) time wheren is the length of the trace) dynamic race detection algorithm; previous sampling based approaches like run in linear time (i.e.,O (n )). Our algorithm is a property tester for race detection — it is sound in that it never reports any false positive, and on traces that are far, with respect to hamming distance, from any racefree trace, the algorithm detects an race with high probability. Our experimental evaluation of the algorithm and its comparison with stateoftheart deterministic and sampling based race detectors shows that the algorithm does indeed have significantly low running time, and detects races quite often. 
null (Ed.)Concolic testing combines concrete execution with symbolic execution along the executed path to automatically generate new test inputs that exercise program paths and deliver high code coverage during testing. The GKLEE tool uses this approach to expose data races in CUDA programs written for execution of GPGPUs. In programs employing concurrent dynamic data structures, automatic generation of data structures with appropriate shapes that cause threads to follow selected, possibly divergent, paths is a challenge. Moreover, a single nonconflicting data structure must be generated for multiple threads, that is, a single shape must be found that simultaneously causes all threads to follow their respective chosen paths. When an execution exposes a bug (e.g., a data race), the generated data structure shape helps the programmer understand the cause of the bug. Because GKLEE does not permit pointers that construct dynamic data structures to be made symbolic, it cannot automatically generate data structures of different shapes and must rely on the user to write code that constructs them to exercise desired paths. We have developed DSGEN for automatically generating nonconflicting dynamic data structures with different shapes and integrated it with GKLEE to uncover and facilitate understanding of data races in programs that employ complex concurrent dynamic data structures. In comparison to GKLEE, DSGEN increases the number of races detected from 10 to 25 by automatically generating a total of 1,897 shapes in implementations of four complex concurrent dynamic data structures  BTree, HashArray Mapped Trie, RRBTree, and Skip List.more » « less

We study the problem of measuring errors in nontracepreserving quantum operations, with a focus on their impact on quantum computing. We propose an error metric that efficiently provides an upper bound on the trace distance between the normalized output states from imperfect and ideal operations, while remaining compatible with the diamond distance. As a demonstration of its application, we apply our metric in the analysis of a lossy beam splitter and a nondeterministic conditional signflip gate, two primary nontracepreserving operations in the KnillLaflammeMilburn protocol. We then turn to the leakage errors of neutralatom quantum computers, finding that these errors scale worse than previously anticipated, implying a more stringent faulttolerant threshold. We also assess the quantum Zeno gate's error using our metric. In a broader context, we discuss the potential of our metric to analyze general postselected protocols, where it can be employed to study error propagation and estimate thresholds in faulttolerant quantum computing. The results highlight the critical role of our proposed error metric in understanding and addressing challenges in practical quantum information processing.more » « less