[Back]

M. Tabaei Befrouei:
"Effective Error Explanation Techniques for Concurrent Software";
Supervisor, Reviewer: G. Weissenbacher, T. Eiter, R. Majumdar; Informationssysteme, 2016; oral examination: 2016-12-06.

Concurrency bugs are among the most difficult software bugs to detect
and diagnose. This is mainly due to the inherent inability of humans
to comprehend concurrently executing computations and to foresee the
possible interleavings that they can entail. In concurrent programs,
interactions between concurrent computations and the order of program
events can vary across executions. This nondeterminism may result in
erroneous and undesired program behavior whose root cause is difficult
to analyze. Facing the challenge of debugging concurrent programs,
this dissertation proposes effective concurrency bug explanation
techniques to assist programmers in understanding the cause of failure
in concurrent programs. Our techniques which do not rely on any
characteristics specific to one type of bug, provide general
frameworks for explaining bugs both in shared memory multithreaded
programs and message passing concurrent systems.

In devising our dynamic techniques for bug explanation, we follow two
different approaches, namely anomaly detection and slicing. Our
anomaly detection techniques are based on statistical analysis and
pattern mining. These techniques adapt a standard pattern mining algorithm
called sequential pattern mining to extract anomalies from datasets of
failing and passing execution traces. Anomalies in the form of
sequences of events reveal the problematic or unexpected order between
concurrent events which may cause a failure. To address scalability
issues of the standard sequential pattern mining algorithm in
extracting anomalies, we propose three different approximation methods
according to the problem setting. The first technique
under-approximates anomalies by limiting them to sequences of events
which occur consecutively in traces. The second technique makes the
pattern mining problem more tractable by shortening the length of the
traces via partitioning them into subtraces. The third technique is
based on a novel abstraction technique for improving the scalability
of the pattern mining algorithm. This technique reduces the length and
the number of distinct events in traces while preserving the ordering
information between the events of original traces including context
switches which are crucial for understanding concurrency bugs. The bug
patterns extracted by this technique not only reveal the problematic
interleavings but also the context in which the bug occurred.

In a completely different approach, we use a proof-based technique to
construct semantics-aware slices from failing traces. This technique
analyzes a single symbolic execution trace to isolate a slice
comprising a code fragment and schedule causing a concurrency bug as
well as annotations that describe the erroneous program states. Our
slicing technique, in fact, generalizes existing interpolation-based
frameworks for sequential bug explanation to a concurrency setting.
We evaluate the efficiency and effectiveness of our proposed
techniques on benchmarks covering a broad range of real-world
concurrency bugs. Moreover, we compare the strengths and limitations
of the anomaly detection techniques with the proof-based slicing technique.

debugging, concurrent programming, verification

http://publik.tuwien.ac.at/files/publik_257531.pdf

Project Head Georg Weissenbacher:
Heisenbugs: Auffindung und Erklärung