Advancing Automated Analysis of Concurrent Pointer Programs

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

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.