Consequencer

The steady exponential increase in processor performance has reached the inevitable turning point, at which it is no longer feasible to increase the clock speeds of individual processors. To achieve higher performance, processors now contain several cores that work in parallel. Consequently, concurrency has become an important aspect across many areas within computer science, such as algorithms, data structures, programming languages, software engineering, testing, and verification. Concurrent programs consist of several computations or threads that are active at the same time and communicate through some control mechanism, such as locks and shared variables, or message passing. Concurrent programming is difficult: programmers do not only have to guarantee the correctness of the sequential execution of each individual thread, they must also consider nondeterministic interferences from other threads. Due to these complex interactions, considerable resources are spent to repair buggy concurrent software. Testing remains the most used (and often the only known) paradigm in industry to find errors, even though the inherently nondeterministic nature of the concurrent schedules causes errors that manifest rarely and are difficult to reproduce and repair. Testing is not effective in detecting such concurrency errors, as all possible executions of the programs have to be explored explicitly. Consequently, testing needs to be complemented by automated verification tools that enable detection of errors without explicitly (i.e. symbolically) exploring executions. On the other hand, the state of the art for concurrent program verification lags behind that for sequential programs. Here, researchers have successfully explored a wide range of techniques and tools to analyse real-world sequential software. A recently proposed approach for symbolic verification of concurrent programs called sequentialization, consists in translating the concurrent program into an equivalent sequential program so that verification techniques or tools that were originally designed for sequential programs can be reused without any changes. This technique has been successfully used to discover bugs in existing software and has been implemented in several tools (e.g., Corral by Microsoft Research). However, existing sequentialization schemas do not support weak memory models, or distributed programs that use message passing. In this proposal we address these weaknesses and plan the development of automated verification tools that enable detection of errors in concurrent programs in a systematic and symbolic way. More specifically, we will develop the theory, models and algorithms that underpin sequentialization of concurrent programs that use FIFO channels. This will enable us to capture within a single framework (1) concurrent programs that communicate through shared memory, for the variety of (weak) memory models that are implemented in today's computer architectures, and (2) distributed programs which use a message-passing communication style (i.e., the two most commonly used programming models for concurrency). A key deliverable of this project will be a set of automatic code-to-code translators, called ConSequencer, for C programs that use Pthread (for shared variables) and MPI (for distributed programs). This will serve as a concurrency plugin for any program verification tool designed for sequential programs. We will evaluate our solutions on publicly available benchmarks using a range of robust sequential verification tools for the C language.