Advancing Automated Analysis of Concurrent Pointer Programs

推进并发指针程序的自动分析

• 批准号: 276397324
• 负责人: Professor Dr. Thomas Noll
• 金额: --
• 依托单位: Informatik 2 - Lehrstuhl Softwaremodellierung und Verifikation
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2015
• 资助国家: 德国
• 起止时间: 2014-12-31 至 2019-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/276397324?language=en
• 关键词: Advancing; Automated; Analysis; Concurrent; Pointer

Many software bugs can be traced back to the erroneous use ofpointers, i.e., references to memory addresses. They constitute anessential concept in modern programming languages, and are usedfor implementing (dynamic) data structures like lists, trees etc., whichare organised in the computer's memory as the so-called heap. Dueto the resulting unbounded state spaces, pointer errors are hard todetect in sequential programs. Concurrency (in the form of threads orprocesses) raises various additional challenges that are handled bycurrent verification techniques only to a limited extent. Based on ourexperience with the graph-based approach to symbolic verification of(sequential) pointer programs, the initial project provided significantcontributions by developing automated and modular techniques foranalysing concurrent threads operating on heap data structures andby integrating logic- and automata-based approaches to heapabstraction. In particular, by introducing the concept of indexes tograph grammars we were able to raise the degree of automation ofshape analyses that deal with relational properties of data structuressuch as balancedness. The goal of the proposed follow-up project isto substantially enhance our framework with regard to the automatedsupport for language inclusion and logical entailment checking, theclasses of dynamic data structures that can be handled, theconcurrent programming features that are supported, and theautomated generation of test cases. To this aim, we will elaborate onthe connection between the graph- and automata-based approachesand further develop the concept of indexed graph grammars.Moreover we will advance the permission-based technique formodular reasoning about concurrent threads to obtain more preciseinformation about heap access patterns, and to cover more generalforms of synchronisation beyond the simple fork-join model. Theoutcome of this research project will be novel techniques, algorithmsand tools to support formal reasoning on relational shape propertiesof concurrent pointer programs. To assess their usability andpracticability, they will be evaluated on case studies such as variousforms of (balanced) lists and trees with related operations, comprisinglock-free concurrent data structures and parallel sorting algorithms.

许多软件错误可以追溯到指针的错误使用，即对内存地址的引用。它们构成了现代编程语言中的一个基本概念，用于实现列表、树等(动态)数据结构，这些数据结构在计算机内存中被组织为所谓的堆。由于产生了无界的状态空间，因此在顺序程序中很难检测到指针错误。并发性(以线程或进程的形式)带来了各种额外的挑战，而当前的验证技术只能在有限的范围内处理这些挑战。基于基于图形的(顺序)指针程序符号验证的经验，最初的项目通过开发自动化和模块化技术来分析堆数据结构上操作的并发线程，并通过集成基于逻辑和自动机的方法来进行堆抽象，从而做出了重大贡献。特别是，通过在图文法中引入索引的概念，我们能够提高形状分析的自动化程度，这些分析处理数据结构的关系属性，如平衡性。提议的后续项目的目标是在以下方面大幅加强我们的框架：对语言包含和逻辑蕴涵检查的自动支持、可处理的动态数据结构类、所支持的并发编程功能以及测试用例的自动生成。为此，我们将阐述基于图的方法和基于自动机的方法之间的联系，并进一步发展索引图文法的概念；此外，我们还将提出基于权限的并发线程模块推理技术，以获得关于堆访问模式的更准确的信息，并涵盖简单的分叉-连接模型之外的更一般的同步形式。该研究项目的成果将是支持并发指针程序关系形状属性的形式化推理的新技术、新算法和新工具。为了评估它们的可用性和实用性，将在案例研究中对它们进行评估，例如各种形式的(平衡)列表和带有相关操作的树，包括无锁并发数据结构和并行排序算法。

项目成果

SL-COMP: Competition of Solvers for Separation Logic

• DOI: 10.1007/978-3-030-17502-3_8
• 发表时间: 2019-04
• 作者: M. Sighireanu;J. A. Pérez;A. Rybalchenko;Nikos Gorogiannis;Radu Iosif;Andrew Reynolds;Cristina Serban;Jens Katelaan;Christoph Matheja;T. Noll;Florian Zuleger;W. Chin;Quang Loc Le;Quang-Trung Ta;T. Le;Thanh-Toan Nguyen;Siau-Cheng Khoo;Michal Cyprian;Adam Rogalewicz;Tomáš Vojnar;C. Enea;Ondřej Lengál;Chong Gao;Zhilin Wu

Graph-Based Shape Analysis Beyond Context-Freeness

超越上下文无关的基于图形的形状分析

• DOI: 10.1007/978-3-319-92970-5_17
• 发表时间: 2018
• 作者: Hannah Arndt;Christina Jansen;Christoph Matheja;Thomas Noll
• 通讯作者: Thomas Noll

Quantitative separation logic: a logic for reasoning about probabilistic pointer programs

• DOI: 10.1145/3290347
• 发表时间: 2018-02
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Kevin Batz;Benjamin Lucien Kaminski;J. Katoen;Christoph Matheja;T. Noll

Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic

符号堆分离逻辑鲁棒性的统一推理

• DOI: 10.1007/978-3-662-54434-1_23
• 发表时间: 2017
• 期刊: ArXiv
• 作者: Christina Jansen;Jens Katelaan;Christoph Matheja;Thomas Noll;Florian Zuleger
• 通讯作者: Florian Zuleger

Let this Graph Be Your Witness! - An Attestor for Verifying Java Pointer Programs

让这张图为你见证吧！

• DOI: 10.1007/978-3-319-96142-2_1
• 发表时间: 2018
• 作者: Hannah Arndt;Christina Jansen;Joost-Pieter Katoen;Christoph Matheja;Thomas Noll
• 通讯作者: Thomas Noll