Advancing Automated Analysis of Concurrent Pointer Programs

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

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.