Trustworthy Systems

Regression-free synthesis for concurrency

Authors

Pavol Cerny, Thomas Henzinger, Arjun Radhakrishna, Leonid Ryzhyk and Thorsten Tarrach

University of Colorado Boulder

IST Austria

NICTA

Abstract

While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present a new repair algo- rithm that avoids such regressions. The solution space is given by the program transformations we consider in the repair process. These include reordering of instructions within a thread, inserting atomic sections, and inserting wait-notify mechanisms. The new algorithm, PACES, is an ex- tension of the CEGIS loop. It learns constraints on the space of candi- date solutions, from both positive examples (error-free traces) and coun- terexamples (error traces). From counterexamples, the algorithm learns a constraint necessary to remove them. From positive examples, it learns constraints that are necessary in order to prevent the repair from turn- ing the trace into a counterexample. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs. The tool is able to fix the bugs while avoiding regressions.

BibTeX Entry

  @inproceedings{Cerny_HRRT_14,
    address          = {Vienna, Austria},
    author           = {Cerny, Pavol and Henzinger, Thomas and Radhakrishna, Arjun and Ryzhyk, Leonid and Tarrach, Thorsten},
    booktitle        = { International Conference on Computer Aided Verification},
    keywords         = {synthesis for concurrency, termite, device drivers, termite},
    month            = jul,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7896.pdf},
    title            = {Regression-free Synthesis for Concurrency},
    year             = {2014}
  }

Download