Wed 17 Jun 2015 16:00 - 16:25 at PLDI Main BLUE (Portland 254-255) - Synthesis II Chair(s): Isil Dillig

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.

PLDI 2015 Artifact Evaluated Badge

Conference Day
Wed 17 Jun

Displayed time zone: Tijuana, Baja California change

16:00 - 17:40
Synthesis IIResearch Papers at PLDI Main BLUE (Portland 254-255)
Chair(s): Isil DilligUniversity of Texas, Austin
16:00
25m
Talk
Concurrency Debugging with Differential Schedule Projections
Research Papers
Nuno MachadoINESC-ID / Instituto Superior Técnico, Universidade de Lisboa, Brandon LuciaCarnegie Mellon University, Luís RodriguesUniversidade de Lisboa, Instituto Superior Técnico, INESC-ID
Media Attached
16:25
25m
Talk
Synthesis of Machine Code from Semantics
Research Papers
Venkatesh SrinivasanUniversity of Wisconsin - Madison, Thomas RepsUniversity of Wisconsin - Madison and Grammatech Inc.
Media Attached
16:50
25m
Talk
Synthesis of ranking functions using extremal counterexamples
Research Papers
Laure GonnordUniversity of Lyon & LIP, France, David MonniauxCNRS, VERIMAG, Gabriel RadanneUniversité Denis Diderot Paris 7, PPS
Media Attached
17:15
25m
Talk
Type-and-Example-Directed Program Synthesis
Research Papers
Peter-Michael OseraUniversity of Pennsylvania, Steve Zdancewic
Media Attached