Regression-free Synthesis for Concurrency

Select |




Print


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

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


2014-07-18


Conference Material


International Conference on Computer Aided Verification (CAV)


Vienna, Austria


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.


synthesis for concurrency, Termite, device drivers, termite


http://cavconference.org/


nicta:7896


Cerny, Pavol; Henzinger, Thomas; Radhakrishna, Arjun; Ryzhyk, Leonid; Tarrach, Thorsten. Regression-free Synthesis for Concurrency. In: International Conference on Computer Aided Verification (CAV); Vienna, Austria. 2014-07-18.



Loading citation data...

Citation counts
(Requires subscription to view)