Verifying Concurrent Pointer Programs
J.-P. Katoen, Th. Noll, J. Heinen, S. Rieger
The incorrect use of pointers is one of the most common sources of software errors. This especially applies to concurrent systems whose nondeterministic behavior rises additional challenges. Proving the correctness of concurrent pointer-manipulating programs with unbounded heap, let alone algorithmically, is a highly non-trivial task. This project attempts to develop automated verification techniques and accompanying tool support for concurrent programs with dynamic thread creation and memory allocation that handle linked data structures which are potentially unbounded in their size. More concretely, two issues are addressed:
J.-P. Katoen, Th. Noll, J. Heinen, S. Rieger
The incorrect use of pointers is one of the most common sources of software errors. This especially applies to concurrent systems whose nondeterministic behavior rises additional challenges. Proving the correctness of concurrent pointer-manipulating programs with unbounded heap, let alone algorithmically, is a highly non-trivial task. This project attempts to develop automated verification techniques and accompanying tool support for concurrent programs with dynamic thread creation and memory allocation that handle linked data structures which are potentially unbounded in their size. More concretely, two issues are addressed:
- In a first phase, we concentrated on (possibly cyclic) singly-linked list data structures. We allow to express correctness properties of programs by combining a simple pointer logic for specifying heap properties with linear-time (LTL) operators for reasoning about system executions. To obtain a finitary representation of the system, we developed a technique which abstracts from non-interrupted sublists in the heap, resulting in a finite-state representation of the data space. In a second abstraction step, using an intermediate Petri-net representation, we also derive a finite-state representation of the control flow, which then allows us to employ standard LTL model checking techniques. Thus our approach stays within the realm of traditional (linear-time) model checking. This facilitates the usage of standard model checkers for validating temporal properties addressing absence of memory leaks, dereferencing of null pointers, dynamic creation of cells, and simple and position-dependent aliasing.
- Next we extended our approach to analyze programs that handle more complex dynamic data structures. We developed a novel abstraction framework that employs graph grammars, more precisely context-free hyperedge replacement grammars, as an intuitive formalism for abstractly modeling dynamic data structures. The key idea is to use the replacement operations which are induced by the grammar rules in two directions. By a backward application of some rule, a subgraph of the heap can be condensed into a single nonterminal edge, thus obtaining an abstraction of the heap. By applying rules in forward direction, certain parts of the heap which have been abstracted before can be concretized again, which avoids the necessity for explicitly defining the effect of pointer-manipulating operations on abstracted parts of the heap. Altogether this method again allows to extend finite-state verification techniques to handle pointer-manipulating programs operating on complex dynamic data structures that are potentially unbounded in their size. We demonstrated how our framework can be employed for analysis and verification purposes by giving its instantiation for binary trees, and by applying this instantiation to the well-known Deutsch-Schorr-Waite traversal algorithm. Our approach is supported by a prototype tool, enabling the quick verification of essential properties such as heap invariants, completeness, and termination.
