权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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

CONSEQUENCER：具有 FIFO 通道的并发程序的基于序列化的验证

基本信息

批准号：
EP/M008991/1
负责人：
Gennaro Parlato
金额：
$ 12.61万
依托单位：
University of Southampton
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2015
资助国家：
英国
起止时间：
2015 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FM008991%2F1
关键词：
CONSEQUENCER Sequentialization based Verification Concurrent

项目摘要

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.

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

项目成果

期刊论文数量（10）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Concurrent Program Verification with Lazy Sequentialization and Interval Analysis

使用惰性序列化和区间分析进行并发程序验证

DOI：
发表时间：
2017
期刊：
影响因子：
0
作者：
Nguyen T L
通讯作者：
Nguyen T L

Bounded Verification of Multi-threaded Programs via Lazy Sequentialization

DOI：
10.1145/3478536
发表时间：
2021-12
期刊：
ACM Transactions on Programming Languages and Systems (TOPLAS)
影响因子：
0
作者：
Omar Inverso;Ermenegildo Tomasco;B. Fischer;Salvatore La Torre;G. Parlato
通讯作者：
Omar Inverso;Ermenegildo Tomasco;B. Fischer;Salvatore La Torre;G. Parlato

VeriSmart 2.0: Swarm-Based Bug-Finding for Multi-threaded Programs with Lazy-CSeq

VeriSmart 2.0：使用 Lazy-CSeq 进行基于群的多线程程序错误查找

DOI：
10.1109/ase.2019.00124
发表时间：
2019
期刊：
影响因子：
0
作者：
Fischer B
通讯作者：
Fischer B

Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings

系统构建和分析的工具和算法 - 第 21 届国际会议，TACAS 2015，作为欧洲软件理论与实践联合会议的一部分举行，ETAPS 2015，英国伦敦，2015 年 4 月 11-18 日，会议记录

DOI：
10.1007/978-3-662-46681-0_45
发表时间：
2015
期刊：
影响因子：
0
作者：
Nguyen T
通讯作者：
Nguyen T

Parallel bug-finding in concurrent programs via reduced interleaving instances

DOI：
10.1109/ase.2017.8115686
发表时间：
2017-10
期刊：
2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE)
影响因子：
0
作者：
Truc L. Nguyen;P. Schrammel;B. Fischer;S. L. Torre;G. Parlato
通讯作者：
Truc L. Nguyen;P. Schrammel;B. Fischer;S. L. Torre;G. Parlato