THESIS
2014
xiii, 125 pages : illustrations ; 30 cm
Abstract
Shared-memory concurrent programs are pervasive in this multi-core era. In these programs,
programmers use the threads to concurrently access the shared data and use the locks to
synchronize between the threads to guarantee the data integrity or the correctness. Specifying
the synchronization that achieves both the high performance and the correctness is very
challenging. For example, programmers may specify the overly restrictively synchronization,
which often leads to the performance bottleneck because it unnecessarily prevents multiple
threads from concurrently accessing the shared data. On the other hand, programmers may
specify the inadequate synchronization, which leads to concurrency bugs such as data races,
atomicity violations and deadlocks.
This thesis makes two main...[
Read more ]
Shared-memory concurrent programs are pervasive in this multi-core era. In these programs,
programmers use the threads to concurrently access the shared data and use the locks to
synchronize between the threads to guarantee the data integrity or the correctness. Specifying
the synchronization that achieves both the high performance and the correctness is very
challenging. For example, programmers may specify the overly restrictively synchronization,
which often leads to the performance bottleneck because it unnecessarily prevents multiple
threads from concurrently accessing the shared data. On the other hand, programmers may
specify the inadequate synchronization, which leads to concurrency bugs such as data races,
atomicity violations and deadlocks.
This thesis makes two main contributions. The first contribution is the proposal of two
bug fixing techniques Axis and Grail. The manual fixing of the concurrency bugs is challenging
and error-prone, e.g., 39% of the manual fixes are incorrect, because the programmers need to
reason about the huge space of possible thread interleavings. Existing approaches have been
proposed to automatically fix the atomicity violations, one important category of concurrency
bugs. They either do not provide the correctness, e.g., new bugs may be introduced, or greatly
sacrifice the concurrency, due to the imprecise reasoning.
⋅ Axis is the first automatic atomicity violation fixing technique that guarantees the
correctness and besides, it allows more concurrency than existing approaches. The
correctness guarantee and the precise reasoning of the concurrency is enabled by the use
of the well-studied discrete control theory. Under the hood, Axis reduces the problem
of violation fixing to a constraint solving problem and implements the solver based on
the control theory. Our evaluation on 13 subjects shows that our patches commonly
outperform that of existing approaches. With the deadlock-free guarantee, our patches
incur moderate overhead (around 10%), which is a worthwhile cost for correctness.
⋅ Grail is a general fixing algorithm that departs from previous techniques (including Axis)
by simultaneously providing both the correctness and the optimal performance guarantees.
Grail synthesizes bug-free yet fully optimal synchronization. To achieve this, Grail
builds a model of the buggy code that is both contextual, distinguishing among different
runtime configurations to ensure efficiency, and global, accounting for the entire
synchronization behavior of the involved threads to ensure correctness. Evaluation of
Grail on 12 real-world bugs from popular codebases confirms its practical advantages,
especially compared with existing techniques: The Grail patches are mostly 40% more
efficient, and incur only 2% overhead.
The second contribution is the proposal of the fixing of performance bottlenecks caused
by the overly restrictive synchronization. Our proposed approach automatically fine tunes
the existing overly restrictive synchronization to unleash more concurrency for the accesses
of the data structures, while preserving correctness. Our approach is widely applicable and
not limited to special data structure types. Under the hood, it relies on the static analysis of the data structure hierarchy and the side effects to determine the fine-grained synchronization
to use; It also exploits the semantics of collections to optimize the code that uses the
collections. The case studies on five heavily used applications show that our approach brings
the significant speedup, e.g., at least 7%-20% speedup and up to 2X speedup.
Post a Comment