CORE: a framework for the automatic repair of concurrency bugs

Abstract

Desktop computers now contain 2, 4 or even 8 processors. To benefit from them programs must be written to work in parallel. If writing good code is hard, writing good parallel code is much harder. Parallelization adds process communication and synchronization to the list of difficulties faced by programmers. It also adds new kinds of bugs not found in single-threaded code such as deadlocks and data races. In this thesis we develop the CORE (COncurrent REpair) framework. It automatically fixes deadlocks and data races in parallel Java programs. It uses a search-based software engineering approach to mutate and evolve the source code. In these mutants synchronization blocks are added, removed, expanded, shrunk or the synchronization variable is changed. Each potential fix is model checked or run through a thread noising tool that forces different thread interleavings to be explored. Efficiently fixing data races and deadlocks in parallel Java programs is realized by combining two techniques. First, different forms of static and dynamic analyses are brought together to constrain the search space. Second, a genetic algorithm without crossover was implemented that uses both noising and model checking to determine fitness. These techniques are unified in the CORE framework. Different kinds of analysis better constrain the search space of the problem. Intelligent use of noising, model checking and incremental model checking are combined efficiently into a modern framework that help to increase the overall quality of concurrent software. This thesis created three projects within the CORE framework, ARC-OPT, CORE-MC and CORE-IMC. First, static analysis from Chord and dynamic analysis from ConTest with fitness evaluation by thread noising from ConTest were combined in ARC-OPT. Second, JPF was integrated into the framework to analyze the source. Fitness was evaluated by JPF and ConTest. This version was called CORE-MC. Third, function header scanning for in-scope locks and incremental modelling support was added to CORE-MC to create CORE-IMC. Each project builds upon the previous and each was evaluated against a suite of test programs.