96 research outputs found
Dynamic Data-Race Detection Through the Fine-Grained Lens
No full textData races are among the most common bugs in concurrency. The standard approach to data-race detection is via dynamic analyses, which work over executions of concurrent programs, instead of the program source code. The rich literature on the topic has created various notions of dynamic data races, which are known to be detected efficiently when certain parameters (e.g., number of threads) are small. However, the fine-grained complexity of all these notions of races has remained elusive, making it impossible to characterize their trade-offs between precision and efficiency.
In this work we establish several fine-grained separations between many popular notions of dynamic data races. The input is an execution trace σ with events, threads and ℒ locks. Our main results are as follows. First, we show that happens-before HB races can be detected in O(⋅ min(, ℒ)) time, improving over the standard O(⋅ ) bound when ℒ = o(). Moreover, we show that even reporting an HB race that involves a read access is hard for 2-orthogonal vectors (2-OV). This is the first rigorous proof of the conjectured quadratic lower-bound in detecting HB races. Second, we show that the recently introduced synchronization-preserving races are hard to detect for 3-OV and thus have a cubic lower bound, when = Ω(). This establishes a complexity separation from HB races which are known to be strictly less expressive. Third, we show that lock-cover races are hard for 2-OV, and thus have a quadratic lower-bound, even when = 2 and ℒ = ω(log ). The similar notion of lock-set races is known to be detectable in O(⋅ ℒ) time, and thus we achieve a complexity separation between the two. Moreover, we show that lock-set races become hitting-set (HS)-hard when ℒ = Θ(), and thus also have a quadratic lower bound, when the input is sufficiently complex. To our knowledge, this is the first work that characterizes the complexity of well-established dynamic race-detection techniques, allowing for a rigorous comparison between them
Algorithmic advances in dynamic analysis for detecting concurrency bugs
No full textConcurrency is an indispensable programming paradigm and multi-threaded programs form the bedrock of most modern software applications. Multi-threaded programs, however, are also the most tricky to get right. Despite rigorous in-house testing, concurrency issues like data races, race conditions, deadlocks and atomicity violations incessantly find there way into production-level software. In the past, errors arising due to complex concurrency bugs in software have led to catastrophic loss of human lives and money. Tackling concurrency bugs, and in particular, efficiently detecting such bugs, has, therefore, been the center of attention in computer science research for several decades now.
Dynamic analysis techniques, in particular, have emerged as the de facto standard for detecting concurrency bugs. Such techniques, examine execution traces of programs, with an aim to detect concurrency bugs at runtime. This thesis advances the state-of-the art in dynamic analysis for detecting concurrency bugs. We propose several algorithms for improving the precision, recall and efficiency of existing techniques for dynamically detecting concurrency bugs like data races and atomicity violations. We also investigate several complexity-theoretic questions establishing precise complexity bounds on several questions arising in dynamic concurrency bug detection.
We first consider the problem of detecting data races dynamically. Most popular techniques for dynamic race detection are either based on a principle of lockset violations, or on the happens-before partial order. While these techniques are usually employed at runtime, for detecting data races on-the-fly, there are many scenarios when executions can be, or need to be analyzed for concurrency bugs in an offline setting. Since executions can be extremely large, they are often stored in a compressed format to ease their warehousing. In this thesis, we study the problem of detecting data races when the analysis needs to be performed over an execution that has been compressed using a grammar-based compression scheme. We show how to detect data races efficiently in such a setting, without needing to decompress the (potentially) exponentially succinct compressed format.
We next study the problem of dynamic race prediction, which asks if one can infer the presence of data races beyond those present in a single trace observed by monitoring a program while it is executing. Existing race detectors report false alarms, miss a lot of real races, or do not scale beyond small execution traces. We propose several algorithms that offer a good balance of scalability and predictive power, while being sound (no false positives). We also study the problem from a complexity-theoretic point of view and identify upper and lower bounds, both in the general setting and in settings when the observed execution trace satisfies special properties.
Next, we consider the problem of dynamically detecting atomicity violations. This thesis proposes a linear time vector-clock algorithm for a well-studied notion of atomicity, called conflict serializability, for which the only known algorithms ran in cubic time.
The algorithms proposed in this thesis have been implemented and evaluated against large benchmark suites to evaluate their effectiveness. The techniques developed in this thesis are backed by strong theoretical foundations that ensure that our algorithms are scalable, sound and have high predictive power, making them applicable for analyzing modern software systems.Submission published under a 24 month embargo labeled 'U of I Access', the embargo will last until 2023-12-01The student, Umang Mathur, accepted the attached license on 2021-07-16 at 17:21.The student, Umang Mathur, submitted this Dissertation for approval on 2021-07-16 at 17:26.This Dissertation was approved for publication on 2021-07-19 at 11:23.DSpace SAF Submission Ingestion Package generated from Vireo submission #16995 on 2022-04-06 at 17:16:10Made available in DSpace on 2022-04-29T21:41:39Z (GMT). No. of bitstreams: 2
MATHUR-DISSERTATION-2021.pdf: 1409268 bytes, checksum: 38100bbe811f8c0e68527926131094c6 (MD5)
LICENSE.txt: 4209 bytes, checksum: 1fcc77be006b05f4869e0be361ec7fcc (MD5)
Previous issue date: 2021-07-19Embargo set by: Seth Robbins for item 123299
Lift date: 2024-04-29T21:41:44Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemEmbargo set by: Seth Robbins for item 123299
Lift date: 2024-04-29T21:42:24Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemEmbargo set by: Seth Robbins for item 123299
Lift date: 2024-04-29T21:43:01Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemEmbargo set by: Seth Robbins for item 123299
Lift date: 2024-04-29T21:44:44Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemEmbargo set by: Seth Robbins for item 123299
Lift date: 2024-04-29T21:46:25Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemEmbargo set by: Seth Robbins for item 123299
Lift date: 2024-04-29T21:47:53Z
Reason: Author requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemAuthor requested U of Illinois access only (OA after 2yrs) in Vireo ETD systemU of I Onl
Optimistic Prediction of Synchronization-Reversal Data Races (ICSE'24)
No full text<p>Dynamic data race detection has emerged as a key technique for ensuring reliability of concurrent software in practice. However, dynamic approaches can often miss data races owing to non-determinism in the thread scheduler. Predictive race detection techniques cater to this shortcoming by inferring alternate executions that may expose data races without re-executing the underlying program. More formally, the dynamic data race prediction problem asks, given a trace of an execution of a concurrent program, can be correctly reordered to expose a data race? Existing state-of-the art techniques for data race prediction either do not scale to executions arising from real world concurrent software, or only expose a limited class of data races, such as those that can be exposed without reversing the order of synchronization operations.</p>
<p><br>In general, exposing data races by reasoning about synchronization reversals is an intractable problem. In this work, we identify a class of data races, called Optimistic Sync(hronization)-Reversal races that can be detected in a tractable manner and often include non-trivial data races that cannot be exposed by prior tractable techniques. We also propose a sound algorithm OSR for detecting all optimistic sync-reversal data races in overall quadratic time, and show that the algorithm is optimal by establishing a matching lower bound. Our experiments demonstrate the effectiveness of OSR— on our extensive suite of benchmarks, OSR reports the largest number of data races, and is scales well to large execution traces. </p>
<p> </p>
<p>We thank reviewers from ICSE'24 artifact evaluation for their suggestions and comments.</p>
Optimistic Prediction of Synchronization-Reversal Data Races (ICSE'24)
No full text<p>Dynamic data race detection has emerged as a key technique for ensuring reliability of concurrent software in practice. However, dynamic approaches can often miss data races owing to non-determinism in the thread scheduler. Predictive race detection techniques cater to this shortcoming by inferring alternate executions that may expose data races without re-executing the underlying program. More formally, the dynamic data race prediction problem asks, given a trace of an execution of a concurrent program, can be correctly reordered to expose a data race? Existing state-of-the art techniques for data race prediction either do not scale to executions arising from real world concurrent software, or only expose a limited class of data races, such as those that can be exposed without reversing the order of synchronization operations.</p>
<p><br>In general, exposing data races by reasoning about synchronization reversals is an intractable problem. In this work, we identify a class of data races, called Optimistic Sync(hronization)-Reversal races that can be detected in a tractable manner and often include non-trivial data races that cannot be exposed by prior tractable techniques. We also propose a sound algorithm OSR for detecting all optimistic sync-reversal data races in overall quadratic time, and show that the algorithm is optimal by establishing a matching lower bound. Our experiments demonstrate the effectiveness of OSR— on our extensive suite of benchmarks, OSR reports the largest number of data races, and is scales well to large execution traces.</p>
A Decidable Fragment of Second Order Logic With Applications to Synthesis
No full textWe propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an exists^*forall^* quantifier prefix (over variables, functions and relations) making EQSMT conducive for modeling synthesis problems. Moreover, EQSMT allows reasoning using a combination of background theories provided that they have a decidable satisfiability problem for the exists^*forall^* FO-fragment (e.g., linear arithmetic). Our decision procedure reduces the satisfiability of EQSMT formulae to satisfiability queries of exists^*forall^* formulae of each individual background theory, allowing us to use existing efficient SMT solvers supporting exists^*forall^* reasoning for these theories; hence our procedure can be seen as effectively quantified SMT (EQSMT) reasoning
Benchmark programs for "Atomicity Checking in Linear Time using Vector Clocks"
No full textMulti-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software.
A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially.
We consider the well studied notion of conflict serializability for dynamically checking atomicity.
Existing algorithms detect violations of conflict serializability by detecting cycles in a graph of transactions observed in a given execution.
The size of such a graph can be as large as the size of the trace making the analysis not scalable.
In this paper, we present AeroDrome, a novel single pass linear time algorithm that detects violations of conflict serializability using vector clocks. Experiments show that AeroDrome scales to traces with a large number of events with significant speedup.</p
Artifact for "Atomicity Checking in Linear Time using Vector Clocks"
No full textMulti-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software.
A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially.
We consider the well studied notion of conflict serializability for dynamically checking atomicity.
Existing algorithms detect violations of conflict serializability by detecting cycles in a graph of transactions observed in a given execution.
The size of such a graph can be as large as the size of the trace making the analysis not scalable.
In this paper, we present AeroDrome, a novel single pass linear time algorithm that detects violations of conflict serializability using vector clocks. Experiments show that AeroDrome scales to traces with a large number of events with significant speedup.</p
Artifact for "Atomicity Checking in Linear Time using Vector Clocks"
No full textMulti-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software.
A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially.
We consider the well studied notion of conflict serializability for dynamically checking atomicity.
Existing algorithms detect violations of conflict serializability by detecting cycles in a graph of transactions observed in a given execution.
The size of such a graph can be as large as the size of the trace making the analysis not scalable.
In this paper, we present AeroDrome, a novel single pass linear time algorithm that detects violations of conflict serializability using vector clocks. Experiments show that AeroDrome scales to traces with a large number of events with significant speedup.</p
Artifact for "Atomicity Checking in Linear Time using Vector Clocks"
No full textMulti-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software.
A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially.
We consider the well studied notion of conflict serializability for dynamically checking atomicity.
Existing algorithms detect violations of conflict serializability by detecting cycles in a graph of transactions observed in a given execution.
The size of such a graph can be as large as the size of the trace making the analysis not scalable.
In this paper, we present AeroDrome, a novel single pass linear time algorithm that detects violations of conflict serializability using vector clocks. Experiments show that AeroDrome scales to traces with a large number of events with significant speedup.</p
Benchmark programs for "Atomicity Checking in Linear Time using Vector Clocks"
No full textMulti-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of software.
A non-interference property like atomicity can reduce this interleaving space by ensuring that any execution is equivalent to an execution where all atomic blocks are executed serially.
We consider the well studied notion of conflict serializability for dynamically checking atomicity.
Existing algorithms detect violations of conflict serializability by detecting cycles in a graph of transactions observed in a given execution.
The size of such a graph can be as large as the size of the trace making the analysis not scalable.
In this paper, we present AeroDrome, a novel single pass linear time algorithm that detects violations of conflict serializability using vector clocks. Experiments show that AeroDrome scales to traces with a large number of events with significant speedup.</p
- …
