Cong Quy Trinh: Automated Verification of Data Properties and Linearizability for Heap-Manipulating Programs

Abstract

Software verification is the process of verifying a software application by checking whether it satisfies requirements. Tha automated verification of programs is one of the most challenging problems in software verification. The problem becomes even more challenging when dealing with concurrent programs that dynamically allocate memory on the heap. In this thesis we propose methods for verifying both safety, shape, and linearizability properties of both sequential and concurrent heap-manipulating programs. In short, linearizability means that concurrent operations appear to be executed atomically on a single machine. Such programs induce an infinite-state space in several dimensions: they consist of an unbounded number of concurrent threads, an unbounded number of pointers, they use unbounded dynamically allocated memory, and the domain of data values is unbounded. In addition, we verify linearizability properties of concurrent programs whose linearization points are either fixed or depend on the future execution of the program. In this thesis, we describe three approaches for verifying safety, shape, and linearizability properties.

In the first approach, we present a framework for verifying programs that manipulate dynamic linked data structures, whose correctness depends on ordering relations between data values. Our framework extends that of forest automata, in which the heap is described by a set of tree automata, by adding data constraints that express relationships between data elements associated with cells of the heap. This approach works for verifying safety property of sequential programs.

In the second approach, we present a framework for automatically verifying linearizability of concurrent data structures with an unbounded number of threads. In this framework, non-fixed linearization points (LPs) are handled by asking the user to specify so-called linearization policies, which are mechanisms for assigning LPs to executions. To handle an unbounded number of threads, we use the thread-modular approach which allows to bound the number of considered threads. To handle an unbounded heap, we define an abstraction, which precisely describes the parts of the heap that are visible (reachable) from global variables, and makes a succinct representation of the parts that are local to threads. We have applied the framework to prove linearizability for a wide range of concurrent data structures based on singly-linked lists.

In the third approach, we present a novel shape analysis that can handle heap structures which are more complex than just singly-linked lists, in particular we handle skip lists and arrays of singly linked lists, while at the same time handling an unbounded number of concurrent threads, an unbounded domain of data values (including timestamps), and an unbounded shared heap. Our approach represents a set of heaps by a set of so-called fragments. A fragment is an abstraction of a pair of heap cells that are connected by a pointer field. To the best of our knowledge, our framework is the first that can automatically verify concurrent data structure implementations that employ singly linked lists, skiplists as well as arrays of singly linked lists, at the same time as handling an unbounded number of concurrent threads, an unbounded domain of data values (including timestamps), and an unbounded shared heap.