concurrency; verification; error explanation; data mining
en
Abstract:
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.