We present Symbiosis: a concurrency debugging technique based on novel differential schedule projections (DSPs). A DSP shows the small set of memory operations and data-flows responsible for a failure, as well as a reordering of those elements that avoids the failure. To build a DSP, Symbiosis first generates a full, failing, multithreaded schedule via thread path profiling and symbolic constraint solving. Symbiosis selectively reorders events in the failing schedule to produce a non-failing, alternate schedule. A DSP reports the ordering and data-flow differences between the failing and non-failing schedules. Our evaluation on buggy real-world software and benchmarks shows that, in practical time, Symbiosis generates DSPs that both isolate the small fraction of event orders and data-flows responsible for the failure, and show which event reorderings prevent failing. In our experiments, DSPs contain 81% fewer events and 96% less data-flows than the full failure-inducing schedules. Moreover, by allowing developers to focus on only a few events (up to 5 in our test cases), DSPs reduce the amount of time required to find a valid fix.
Wed 17 JunDisplayed time zone: Tijuana, Baja California change
16:00 - 17:40 | Synthesis IIResearch Papers at PLDI Main BLUE (Portland 254-255) Chair(s): Işıl Dillig University of Texas, Austin | ||
16:00 25mTalk | Concurrency Debugging with Differential Schedule Projections Research Papers Nuno Machado INESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Brandon Lucia Carnegie Mellon University, Luís Rodrigues Universidade de Lisboa, Instituto Superior Técnico, INESC-ID Media Attached | ||
16:25 25mTalk | Synthesis of Machine Code from Semantics Research Papers Venkatesh Srinivasan University of Wisconsin - Madison, Thomas Reps University of Wisconsin - Madison and Grammatech Inc. Media Attached | ||
16:50 25mTalk | Synthesis of ranking functions using extremal counterexamples Research Papers Laure Gonnord University of Lyon & LIP, France, David Monniaux CNRS, VERIMAG, Gabriel Radanne Université Denis Diderot Paris 7, PPS Media Attached | ||
17:15 25mTalk | Type-and-Example-Directed Program Synthesis Research Papers Media Attached |