Trace-based analysis of concurrent programs

• Applicants: Professor Dr. Martin Sulzmann, Ph.D.; Professor Dr. Peter Thiemann
• Subject Area: Theoretical Computer Science ; Software Engineering and Programming Languages
• Term: since 2015
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 281466659

Trace-based algorithms for the dynamic prediction of data races and deadlocks cannot be efficient, sound, and complete at the same time. We will develop verified prediction algorithms that scale to realistic programs while retaining a good compromise of being mostly sound and almost complete. That is, these algorithms shall run in almost linear time in the size of the trace, report few false positives and few false negatives, and come with formal statements and proofs of their properties. In particular, we aim for algorithms that guarantee *either* no false positives, *or* no false negatives, *or* no false positives under conditions like limits on the numbers of threads or adherence to certain locking protocols. The formal statements provide characterizations of reported false positive/negatives and conditions under which they can be avoided. We will explore a range of analysis aspects that have been neglected in previous work: new combinations of analysis methods based on happens-before relations and lock sets; methods that address concurrency features beyond simple locks (e.g., buffered communication); programmer assistance via detailed diagnostic information and heuristics for program repair; dealing correctly with potentially inaccurately recorded traces.

• DFG Programme: Research Grants