Debugging is time-consuming: bug reports rarely provide sufficient information to reproduce the reported failure, so developers turn into detectives searching for an explanation of how the bug occurred. We introduced execution synthesis, a technique that combines reverse static analysis with forward symbolic execution to automate this process and find program inputs and thread schedules that cause a program to exhibit the symptoms shown in a bug report. We leverage the insight that, to fix a bug, developers need not reproduce the exact same execution that failed in the field, but any execution that leads to the same failure state is sufficient. Execution synthesis requires no runtime tracing or program modifications, thus incurring no runtime overhead.

Debugging real systems is hard, requires deep knowledge of the code, and is time-consuming. Bug reports rarely provide sufficient information, thus forcing developers to turn into detectives searching for an explanation of how the program could have arrived at the reported failure point. Using a combination of static analysis and symbolic execution, it “synthesizes” a thread schedule and various required  program inputs that cause the bug to manifest. The synthesized execution can be played back deterministically in a regular debugger, like gdb. This is particularly useful in debugging concurrency bugs.

Our technique requires no runtime tracing or program modifications, thus incurring no runtime overhead and being practical for use in production systems. We evaluate ESD— a debugger based on execution synthesis—on popular software (e.g., the SQLite database, ghttpd Web server, HawkNL network library, UNIX utilities): starting from mere bug reports, ESD reproduces on its own several real concurrency and memory safety bugs in less than three minutes.

Links