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

处理器性能的稳定指数增长已经到达了不可避免的转折点，在这个转折点上，提高单个处理器的时钟速度不再可行。为了获得更高的性能，处理器现在包含多个并行工作的核心。因此，并发性已经成为计算机科学中许多领域的一个重要方面，如算法、数据结构、编程语言、软件工程、测试和验证。并发程序由几个同时活动的计算或线程组成，并通过某种控制机制进行通信，如锁和共享变量或消息传递。并发编程是困难的：程序员不仅必须保证每个单独线程的顺序执行的正确性，他们还必须考虑来自其他线程的不确定性干扰。由于这些复杂的交互，需要花费大量的资源来修复有错误的并发软件。测试仍然是工业中最常用的(通常也是唯一已知的)发现错误的范例，即使并发调度固有的不确定性导致很少出现并且难以再现和修复的错误。测试在检测此类并发错误方面并不有效，因为必须明确地探索程序的所有可能的执行。因此，测试需要由自动化验证工具来补充，该工具能够在不显式地(即，象征性地)探索执行的情况下检测错误。另一方面，并发程序验证的现状落后于顺序程序的验证。在这方面，研究人员已经成功地探索了大量的技术和工具来分析真实世界的顺序软件。最近提出的一种称为序列化的并发程序符号验证方法，在于将并发程序转换为等价的顺序程序，使得最初为顺序程序设计的验证技术或工具可以在不做任何改变的情况下被重用。该技术已成功地用于发现现有软件中的错误，并已在几个工具中实现(例如，Microsoft Research的Corral)。然而，现有的序列化模式不支持弱存储模型，或使用消息传递的分布式程序。在这个提案中，我们解决了这些弱点，并计划开发自动化验证工具，使之能够以系统和符号的方式检测并发程序中的错误。更具体地说，我们将开发支持使用FIFO通道的并发程序的序列化的理论、模型和算法。这将使我们能够在单个框架内捕获(1)通过共享内存通信的并发程序，适用于当今计算机体系结构中实现的各种(弱)内存模型，以及(2)使用消息传递通信风格的分布式程序(即，两种最常用的并发编程模型)。该项目的一个关键交付成果将是一组自动代码到代码转换器，称为ConSequencer，用于使用P线程(用于共享变量)和MPI(用于分布式程序)的C程序。这将作为任何为顺序程序设计的程序验证工具的并发插件。我们将使用一系列面向C语言的健壮的顺序验证工具，在公开可用的基准测试上评估我们的解决方案。

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.