CONSEQUENCER: Sequentialization-based Verification of Concurrent Programs with FIFO channels

点击翻译按钮获取中文摘要

The steady exponential increase in processor performance has reached the inevitable turning point, at which it is no longer feasible toincrease the clock speeds of individual processors. To achievehigher performance, processors now contain several cores that work in parallel.Consequently, concurrency has become an important aspect across manyareas within computer science, such as algorithms, data structures, programminglanguages, software engineering, testing, and verification.Concurrent programs consist of several computations or threads that areactive at the same time and communicate through some control mechanism, such aslocks and shared variables, or message passing. Concurrent programming is difficult:programmers do not only have to guarantee the correctnessof the sequential execution of each individual thread, they must also considernondeterministic interferences from other threads. Due to these complexinteractions, considerable resources are spent to repair buggy concurrentsoftware.Testing remains the most used (and often the only known) paradigm in industry to find errors,even though the inherently nondeterministic nature of the concurrentschedules causes errors that manifest rarely and are difficult to reproduce and repair.Testing is not effective in detecting such concurrency errors, as allpossible executions of the programs have to be explored explicitly.Consequently, testing needs to be complemented by automated verification tools thatenable 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 andtools 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 thatverification techniques or tools that were originally designed forsequential programs can be reused without any changes.This technique has been successfully used to discover bugs in existing softwareand 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.