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.