Verifying Concurrent List­Manipulating Programs by LTL Model Checking Joost­Pieter Katoen and Thomas Noll and Stefan Rieger RWTH Aachen University Software Modeling and Verification Group 52056 Aachen, Germany {katoen,noll,rieger}@cs.rwth-aachen.de Abstract We present a novel approach to the verification of concurrent pointer­manipulating programs which operate on singly­linked lists. By abstracting from chains (i.e., non­interrupted sublists) in the heap, we obtain a finite­state representation of all possible executions of a given program. The combination of a simple pointer logic for expressing heap properties and of temporal operators then allows us to employ standard LTL model checking techniques. The usability of this approach is demonstrated by establishing correctness properties of a producer/consumer system and of a concurrent garbage collector. Keywords: Software Model Checking, Abstraction, Heap Verification, Shape Analysis, LTL, Lists, Pointer Programs 1 Introduction Techniques for the verification of elementary properties of concurrent pointer programs are indispensable. Programming with pointers is error­prone with potential pitfalls such as dereferencing null pointers and the creation of memory leaks. Pointer programming becomes even more vulnerable in a concurrent setting where data structures such as linked lists and trees are manipulated and inspected by several threads. This paper presents a model­checking approach to the verification of concurrent programs that manipulate singly­linked lists. Existing approaches either make use of non­standard logics, advanced model­checking procedures or extended versions of Hoare logics with accompanying deduction techniques (see Sct. 6 about related work). In contrast, the approach advocated in this paper stays within the realm of traditional (linear­time) model checking. This facilitates the usage of standard (LTL) 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. Our approach is illustrated by considering a simple concurrent programming language that besides the usual control structures offers primitives for pointer manipulation, cell creation and destruction, and (guarded) atomic regions that allow concurrency control constructs such as test­and­set primitives and monitors. An operational semantics is provided in terms of labeled transition systems in which states are equipped with a graph structure representing the current list configuration. List abstraction exploits a variant of summary nodes [45] that represent more than M chained list cells where constant M is directly obtained from the formula to be checked. Each configuration is shown to have a canonical representation (up to isomorphism). The abstract semantics of any concurrent program in our language is finite, obtained in a fully mechanized manner, and keeps the minimal "distance" between program variables and summary nodes invariant. Over­approximation oc- Katoen and Noll and Rieger curs in a very controlled manner; only assignments may yield nondeterminism as variables may get "too close" to summary nodes. Properties are expressed in a first­order linear­time temporal logic (LTL) that is enriched with assertions on singly­linked lists such as reachability of cells, aliasing, and freshness of cells. Our logic is similar in spirit to NTL [19,20] and ETL [49]. Opposed to NTL, we avoid the use of temporal operators inside quantification. In this way, involved mechanisms to keep track of the identities of individual cells are not needed. As a result, standard LTL model checking algorithms can be employed. The differences with ETL are more of a technical nature. ETL has a three­valued interpretation, whereas our logical interpretation is a standard binary one. Moreover, ETL­formulas are translated in first­order logic with transitive closure for the evaluation on a trace, whereas in our case traces are generated by labeled transition systems and used in standard LTL model checking. The feasibility of our approach is shown by considering the verification of a simple concurrent garbage collection program. Furthermore a prototypical tool is currently under development for experimenting with real­life examples. Please note that due to space constraints most of the proofs could not be included in this paper. 2 A List­Manipulating Programming Language Given a universe PV of program variables, we define the set of list­manipulating programs (LM­programs) to be given by the following grammar (where vi, v PV ): LMP ::= var v1, ..., vk(Stmt1 ... Stmtl) Stmt ::= skip | signal | v := PExp | v := PExp | Stmt; Stmt | if BExp then Stmt else Stmt fi | while BExp do Stmt od | new(PExp) | del(PExp) | BExp : Stmt PExp ::= nil | v | v | &v BExp ::= tt | ff | PExp = PExp | BExp BExp | BExp V () := {v1, ..., vk} denotes the set of variables for LMP. var x, y, z( while tt do tt : if x = nil then new(y); x := y else new(y); y := y fi od while tt do x = nil : z := x; x := x; del(z) od ) Fig. 1. Producer/Consumer An LM­program thus consists of a declaration of global program variables and a series of statements to be executed in parallel. Each of these statements can either be a pointer assignment, a sequence of statements, a control structure, or a special statement such as signal which sets a global signal flag that can be tested in the logic, new/del for dynamic creation or deletion of objects at runtime (possibly leading to an unbounded number of allocated heap cells) and guarded atomic regions. If the Boolean guard g in g : s is true, s is executed atomically, i.e., with no interference by other processes. If g is evaluated to false, the process is blocked (until g becomes true). Pointer expressions comprise the special constant nil denoting an undefined 2 Katoen and Noll and Rieger pointer value, a program variable, the dereferencing or referencing of a program variable. Note that for simplicity we do not allow arbitrary dereferencing depths; those can be emulated using a sequence of assignments within an atomic region. Example 2.1 Figure 1 shows an LM­program implementing a producer inserting objects and a consumer deleting objects at the end (pointed to by y) and beginning (pointed to by x) of a queue, respectively. If the queue is empty the consumer cannot proceed due to the guard x = nil until the producer has inserted at least one object. Insertion and deletion are executed atomically to prevent interferences. Definition 2.2 A heap configuration of a program LMP is a tuple = (N, A, , F) with a set of nodes N V (), a set of abstract nodes A N \ PV , a successor function : N Nnil (where Nnil := N {nil}), and a set of flags F {err, dl, leak, signal, new}. Let : 2N 2N with (X) := {n N | k N, n X : k(n) = n} be the transitive closure of , i.e. all nodes reachable from a node in X (and X itself). Thus the nodes represent both the dynamic objects created and deleted at runtime and the static program variables (which cannot be deleted). Edges, as formalized by the ­function, encode the points­to information of a specific program state. The set A of abstract nodes will later be used for our abstraction technique and will be empty throughout the current section. Finally the flags give special information about a state, e.g., whether a runtime error or memory leak occurred, a new node was created, or the signal bit has been set using the signal command. To ensure the finiteness of our abstraction we will automatically delete those heap nodes that are not reachable from the program variables. This is accomplished by the following garbage collection mapping. Whenever it removes an unreachable node, it sets the leak flag indicating a potential memory leak. Definition 2.3 For = (N, A, , F) we define := (N, A N, N, F {leak | (N \ N) = }) where N = (PV ). denotes the set of all garbage­free heap configurations, i.e., : = , and c denotes the set of all concrete configurations, i.e., those with A = . From now on we will always assume garbage freeness when mentioning heap configurations. This enforces a bound on the maximal number of incoming edges for a node (essentially the number of program variables). Definition 2.4 Let = (N, , , F) c. Then we define the semantics of pointer expressions [[ ]] : PExp Nnil by 1 : [[nil ]] := nil [[v ]] := (v) [[v ]] := ([[v ]]) [[&v ]] := v The semantics of Boolean expressions [[ ]] : BExp B is standard and strict 2 . Note that Def. 2.2 implies that (nil) = and so [[ ]] can indeed yield undefined results for both pointer and Boolean expressions. Definition 2.5 For = var v1, ..., vk : (s1 ... sl) LMP the concrete operational semantics is given by a transition system Tc = (Q, q0, lab, ) with a set of states 1 denotes a partial function and the undefined value. 2 One undefined operand yields an undefined expression. 3 Katoen and Noll and Rieger Q c × Stmt({ }Stmt) where Stmt = Stmt {}Stmt {}, an initial state q0 = ((N0, , 0, ), s1 ... sl) where N0 and 0 represent the "input heap", a labeling lab : Q c with (, s) Q : lab((, s)) = , and a transition relation Q×Q. In the following we will use the abbreviations ^F for F \ {signal, new, leak} and noerr for {err, dl} F = . err and dl will denote pointer error and deadlock states. Most transition rules are straightforward, thus here we will only consider some interesting examples. [[g ]] = 1 , s , s noerr , g : s , s (1) , s , s s = noerr , s , s , s , noerr , s , (2) j s.t. , sj , s j i = j : s i s.t. si = s i noerr , s1 ... sk , s1 ... s j ... sk (3) j s.t. , sj , s j j : sj = noerr , s1 ... sk dl, (4) , ... , ... (5) [[ ]] = noerr (N, A, , F), v := (N, A, [v/[[ ]]], ^F), (6) noerr (N, A, , F), new(v) (N {nnew}, A, [v/nnew], ^F {new}), (7) [[ ]] N \ PV noerr (N, A, , F), del() (N \ {[[ ]]}, A, [[[ ]]/, -1 ([[ ]])/nil], ^F), (8) Some remarks on the transition rules are in order. The leak, signal, and new flags are reset after each transition; they are only activated in the state directly following the corresponding "event". Regarding the concurrency rules we need to take care of the special semantics of the atomic regions. If a process is executing such a statement it must not be interrupted, and therefore the corresponding state is marked with (rule 1). The interleaving rule 3 excludes that any other than process j is in an atomic region. If no process can proceed (all are blocked) we reach the special deadlock state (rule 4). If all processes are terminated or an error or deadlock state is reached the program loops to ensure that all paths in the transition system are infinite (rule 5). The treatment of assignments (rule 6) and the new statement (rule 7) is again straightforward, we though have to keep in mind in the first case that runtime errors might occur (dereferencing of nil pointers) and that garbage may be generated. Rule 8 handles the deletion of nodes. Please note that the next­pointers of the predecessors of the deleted node are set to nil (mainly to avoid case distinctions for undefined expressions in the semantics). We conclude that for the producer/consumer example (Fig. 1) the state space 4 Katoen and Noll and Rieger becomes infinite when applying the operational semantics as defined above. 3 State­Space Abstraction As we have seen in the previous section the state space of LM­programs can get infinite even for simple example programs making standard verification methods inapplicable. To tackle the problem we use abstraction techniques to generate an abstract transition system that incorporates the behavior of the concrete one, i.e., whose runs cover all concrete ones. This approach is correct but generally incomplete: although we can conclude from the satisfaction of a property in the abstract state space its validity in the concrete case, the inverse is impossible though. But since the abstraction is parameterized via a global constant M N we can refine the abstraction depending on our needs. For a given M > 0 we set M := {0, 1, ..., M, }, where represents all values greater than M. Chain Abstraction The main idea of our abstraction is to summarize subgraphs of a configuration into summary nodes [45], which will be exactly those contained in the A­component of a heap configuration. Summary nodes (also called abstract nodes) are not allowed to represent arbitrary structures but only so­called chains, i.e., non­interrupted lists. Our abstraction is based on [18,19] with the difference that nodes are either truly abstract or concrete, thus recording node multiplicities is not necessary. Definition 3.1 Let = (N, A, , F) be a configuration. A nonempty set of nodes C N is called a chain if either * |C| = 1 and C PV or * C PV = and there exists a bijection : {1, ..., |C|} C such that ((i)) = (i + 1) for i {1, ..., |C|} and i {2, ..., |C|} : |-1((i))| = 1. For a given chain C we will use the abbreviations C := (1), and C := (|C|). A chain is called maximal if no superset C C is a chain. Thus a chain is a sequence of pointer­connected nodes without interference of other incoming edges or a singleton set containing a program variable. It follows that the abstraction of chains preserves the graph structure. We will now introduce a type of functions, called abstraction morphisms, that is based on this concept. Definition 3.2 Let i = (Ni, Ai, i, Fi) , i {1, 2} be two heap configurations. An abstraction morphism h : N1 N2 satisfies for all v PV N1 and ni, n i Ni: 1. h(v) = v 2. h-1(n2) is a chain in N1 3. 2(n2) = n 2 1( ----- h-1(n2)) = ----- h-1(n 2) 4. 1(n1) = n 1 h(n1) = h(n 1) 2(h(n1)) = h(n 1) 5. n2 A2 h-1(n2) A1 = |h-1(n2)| > M 6. F1 = F2 We write h : 1 2 to denote that the abstraction morphism h abstracts 1 to 2 and 2 1 h : 1 2. 5 Katoen and Noll and Rieger Abstraction morphisms abstract from concrete chains with minimal length M +1 (cond. 2 and 5). The preservation of the graph structure is enforced by conditions 3 and 4. Program variables, being special nodes, remain untouched (cond. 1). Example 3.3 Figure 2 shows an abstraction morphism for M = 1. The dashed lines represent the mapping, and the black nodes denote the resulting abstract nodes. Note that for M = 2 the nodes 3 and 4 could not be projected onto the same abstract node (condition 5 of Def. 3.2). The chain {3, 4} cannot be extended by node 5, since this node has two incoming edges which is only allowed for the first node of a chain. Although in this example the source configuration is concrete, this is of course not necessary by definition. x 1 2 3 4 5 6 7 8 9 x 1 2 Fig. 2. An Abstraction Morphism An important property of abstraction morphisms is their surjectivity. If, in addition a morphism is injective it becomes an isomorphism. Isomorphic configurations cannot be distinguished except for node naming, the graph structure is the same. Canonical Configurations Previously we have defined how configurations can be abstracted. It remains the problem that there can be different abstractions of a given source configuration. For this reason we need a normal form that implies uniqueness. In the following we define this normal form, assuming = (N, A, , F) . Definition 3.4 (i) Let Nj := {n N | v PV : k(v) = n, k < j} be the set of nodes with a distance of at least j from the variable nodes. Analogously Nj := N \Nj+1. (ii) A configuration is called canonical if N2 A = and for all maximal 3 chains C N3 either |C| = 1 or |C| M C A = . The set of all canonical configurations is denoted by . The notion of canonical configurations is quite intuitive: maximal chains are collapsed where possible but only up to a distance of three from variable nodes. The latter condition ensures that pointer expressions always evaluate to concrete nodes, which will simplify the definition of the abstract LMP semantics. The abstraction morphism in Fig. 2 yields a canonical configuration, as can be easily verified. Theorem 3.5 (Existence) For every with N2 A = there exists a such that . It is easy to construct a morphism yielding a canonical configuration. It has to collapse maximal chains that are larger than M or contain abstract nodes, if they are sufficiently distant from the variable nodes. In the following we will call this morphism h. The precise definition does not matter as states the following theorem. 3 Here we refer to maximality in N3. 6 Katoen and Noll and Rieger Theorem 3.6 (Uniqueness) Let and 1, 2 such that h1 : 1 and h2 : 2 are two abstraction morphisms. Then 1 and 2 are isomorphic. The proof of the uniqueness had to be omitted here. The consequence of these results is the appropriateness of canonical configurations as a normal form. The abstract semantics will operate on such configurations. Abstract Semantics of List­Manipulating Programs As already mentioned, our goal is to guarantee the correctness of our abstraction approach. This can be achieved by ensuring that every concrete execution of a given system can be "simulated" by an abstract computation, which necessarily introduces nondeterministic behavior on the abstract side. Regarding the expression semantics nothing needs to be modified: in a canonical configuration, abstract nodes have a distance greater than two from the variable nodes such that every pointer expression refers to a concrete node. The expression semantics can therefore be chosen identical to the concrete case (Def. 2.4), now interpreted on canonical configurations. Definition 3.7 Given a program = var v1, ..., vk : (s1 ... sl) LMP, its abstract operational semantics is defined by the labeled transition system Ta = (Q, [q0]=, lab, ) with state set Q /= × Stmt({ }Stmt), initial state q0 as in Def. 2.5, labeling function lab : Q where (K, s) Q : lab((K, s)) = K, and transition relation as specified by the following rules (we focus on the assignments, since the other rules are analogous to the concrete case, but operating on isomorphism congruence classes). / V () noerr [(N, A, , F)]=, v := [h((N, A, [v/[[ ]]], ^F))]=, (1) s.t. h((N, A, [v/[[w ]]], ^F)) [[w ]] = nil noerr [(N, A, , F)]=, v := w [ ]=, (2) [[v ]] = nil [[ ]] = noerr [(N, A, , F)]=, v := [h((N, A, [(v)/[[ ]]], ^F))]=, (3) [[ ]] = [[ ]] = noerr []=, := [err]=, (4) In Fig. 3 the semantic rules are visualized for an example configuration. In rule 2 there might be the necessity for both abstraction and concretion. The execution of the assignment and the following abstraction via h yields an intermediate configuration which is generally not canonical since the variable v could now be too close to an abstract node. Therefore we have to find a canonical configuration that is at least as concrete as and related by an abstraction morphism to it. There might be more than one solution, thus this rule is nondeterministic (indicated by the dashed arrows), but remains the only source of nondeterminism. In rules 1 and 3 the distance to an abstract node is not reduced, but the opposite case can occur: just imagine an assignment of the form y := nil. If y points into a list whose head is referred to by another variable, we possibly increase the distance from that variable to abstract nodes. The execution of the assignment 7 KatoenandNollandRieger (1) v = w (analogously: v = nil, v = &w) w v assign x w v GC x w v abstract x w v x (2) v = w w v assign x w v GC x w v abstract x w v x w v x w v x concretize (3) v = w (analogously: v = w, v = &w) w v assign x w v GC x w v x abstract w v x Fig. 3. Exemplary visualization of the abstract semantics (M = 3) 8 Katoen and Noll and Rieger x y x y x y x y yxyx p c p c p c pc p c p c Fig. 4. Producer/Consumer: Abstract State Space (M = 1) therefore potentially yields a non­canonical configuration and we have to re­abstract to determine the corresponding canonical configuration. According to Thm. 3.6 the result is unique and thus these steps are deterministic. Example 3.8 Figure 4 shows the finite abstract state space of the producer/consumer program from Fig. 1 for M = 1. The p­ and c­transitions each summarize several producer/consumer steps. The dashed transitions are nondeterministic steps, since the abstract node, visualized in black color, represents at least two nodes in a chain. If now the consumer deletes one node from the beginning of the queue the distance of x to the abstract node becomes two and thus we need to concretize the graph to obtain a canonical configuration. For this we distinguish two cases: either the abstract node represents exactly two nodes, then we reach the graph to the right, or it represents more than two, in which case we stay in the same state since the abstract node still represents more than one concrete node. Theorem 3.9 (Finiteness) For every LMP, Ta is finite. The idea of the proof is to establish a bound on the number of nodes of canonical configurations for a given number of program variables. Theorem 3.10 (Correctness of the Abstraction) Let LMP. For every transition in Tc there exists a corresponding abstract transition in Ta such that the heaps are related by abstraction morphisms. The proof of the correctness theorem has been omitted due to space constraints. 4 A Logic for Concurrent List­Manipulating Programs In the previous sections we have defined our programming language for concurrent pointer manipulation and both its concrete and abstract semantics. In this section we will present a logic which will allow us to reason about heap configurations and program behavior. In the following LV denotes a set of logical variables, where we always assume that LV PV = . Pointer Logic Pointer logic deals with single configurations and is employed to express graph properties as well as to inspect the special flags of heap configurations (see Def. 2.2). 9 Katoen and Noll and Rieger Definition 4.1 The set PL of Pointer Logic formulas is given by the grammar NExp ::= nil | v ( PV ) | x ( LV ) | NExp Atomic ::= tt | ff | err | dl | leak | signal | new | NExp = NExp | NExp ; NExp PL ::= Atomic | PL | PL PL | x : PL Later on we will use the logical operations , , , and (defined as usual) as abbreviations. Note that in contrast to pointer expressions in LM­programs our logic supports dereferencing operations of arbitrary depth. The special operation ; expresses the reachability of heap objects. Definition 4.2 Let : LV N be a variable valuation and c a concrete heap configuration. Then we define [[ ]] : NExp Nnil by: [[nil ]] := nil [[v ]] := v for v PV [[x ]] := (x) for x LV [[ ]] := ([[ ]]) for NExp Note the semantic difference with respect to the programming language. In navigation expressions a variable v is interpreted by itself and not by the node it is referencing. This avoids the necessity of the referencing operator &. Definition 4.3 The (concrete) satisfaction relation |= for PL­formulas is given as follows 4 (for = (N, , , F)): , |= f iff f F, where f {err, dl, leak, signal, new} , |= 1 = 2 iff [[1 ]] = [[2 ]] = , |= 1 ; 2 iff [[i ]] = [[2 ]] ([[1 ]]) , |= x : iff n N : , [x/n] |= Temporal Pointer Logic Pointer Logic enables us to express properties of single configurations. However it cannot be used to specify (ongoing) computations, i.e., configuration sequences. To this aim we will now extend this logic by temporal operators. Definition 4.4 The set TPL of Temporal Pointer Logic formulas is given as follows: TPL ::= PL | TPL | TPL TPL | X TPL | TPL U TPL For TPL we use the abbreviations F := ttU and G := F. Moreover V () LV denotes the set of (bound or free) logical variables occurring in . Note that it is not possible to nest quantifiers and temporal operators. To do so it would be necessary to keep track of the object identities between states, which is difficult in the presence of abstract nodes. In addition it would blow up the state space and exclude the use of standard model checking algorithms. To the best of our knowledge the only approach to support this idea is the one in [18,19,20]; other works in the area such as [46] consider only shapes of the heap. This results in a loss 4 For , , tt and ff the semantics is standard and therefore omitted. 10 Katoen and Noll and Rieger of expressivity, e.g., a property like x : new(x) F del(x) which states that every produced object will eventually be consumed cannot be formulated. Nonetheless we can specify many interesting properties. Example 4.5 For our producer/consumer system from Fig. 1 it holds true: 1. F(dl err) (never deadlock or pointer errors) 2. GF new (new objects are created infinitely often) 3. G((x = nil y = nil) (x ; y v : (v = y x ; v))) (whenever the queue is not empty, the object y points to is reachable from x and between x and this object lies a chain) More general correctness properties are: 4. F x = y (x and y will eventually become aliases) 5. G(z : (x ; z y ; z)) (x and y always point to disjoint parts of the heap) 6. G(y : (x ; y (z : (y ; z z ; y)))) (x always points to a non­cyclic list) 7. FG(leak) (only finitely often a memory leak can occur) 8. G(y : (x ; y (z : (z ; y x ; z)))) (x always points to a chain) As mentioned before, TPL specifies computation paths. The set of possible paths is represented by a transition system. Definition 4.6 Let T = (Q, q0, lab, ) be a (concrete) transition system with lab : Q c. A path in T is an infinite sequence of states = 012... Q such that i i+1 for all i N. Then for PL we have |= ( PL) iff : LV Nlab(0) s.t. lab(0), |=PL For the temporal operators the semantics is identical to the one of LTL. We write T |= iff |= for all paths {q0}Q in T. Reasoning about Abstract Computations As expected the concrete semantics is straightforward. When we switch to abstract configurations, however, we run into several complications since logical variables can be bound to both concrete and abstract nodes. In the latter case we have to record which concrete node, represented by the summary node, it is bound to. This could lead to undefinedness of Pointer Logic formulas. This problem occurs mainly in direct comparisons of the form = . To tackle this problem we choose the global precision constant M in dependence of the formula as follows. If TPL is the formula to check, then we assume from now on that M xV () {j + 1 | j x occurs in }. Due to the presence of abstract nodes it is not sufficient anymore to evaluate logical variables by simple variable­to­node mappings. Additionally we must record the offset of a variable referring to an abstract node and the distance between variables pointing to the same abstract node. This leads to the concept of abstract valuations. 11 Katoen and Noll and Rieger Given and TPL, an abstract valuation is of the form = (, o, ), where : V () N maps logical variables to (abstract) nodes, o : V () M denotes the offset for an abstract node, and : V () V () M is a "distance matrix" for the logical variables with potentially undefined entries. is only defined if both arguments are mapped onto the same entity, and o is only different from 1 if the corresponding variable is mapped onto an abstract node. The set of all such valuations will be denoted by Val,. Using this concept one can define a function d, : NExp × NExp {0, 1, } measuring the "distance" of pointer expressions, where distance here means either 0 if the expressions are mapped onto the same (concrete) entity, 1 if the the first case does not hold but the second argument is reachable from the first or if neither is the case. The presence of abstract nodes plays a vital role in the abstract semantics. Without the global constraint for M we would not be able to resolve all possible cases of abstract valuations, a third truth value would thus become necessary. The distance function is required for the case that both variables are mapped onto an abstract node with offset . With the help of the distance function the abstract semantics of PL and TPL is straightforward. Definition 4.7 Let = (N, A, , F) and = (, o, ) Val,. The satisfaction relation |= for PL­formulas on canonical configurations is then given as follows (omitting the trivial cases): , |= f iff f F, where f {err, dl, leak, signal, new} , |= 1 = 2 iff d,(1, 2) = 0 , |= 1 ; 2 iff d,(1, 2) {0, 1} , |= x : iff n N, off M, dist : V () M s.t. , ([x/n], o[x/off ], [x/dist]) |= Let T = (Q, q0, lab, ) be an abstract transition system with lab : Q /= and Q a path in it. Then |= PL iff for lab(0) there exists an Val, s.t. , |=PL . Temporal operators and Boolean connectives are treated in the standard way. We write T |= iff |= for all paths {q0}Q in T. The following theorem states that the abstract semantics of TPL and of the programming language is correct, i.e., that the validity of a formula under the abstract interpretation implies the validity under the concrete one. The converse though does not hold. Theorem 4.8 Let LMP and TPL. If Ta |= then Tc |= . Proof. It suffices to show for all PL and c the proposition: : LV N s.t. , |= Val, s.t. h(), |= () Note that the ­direction is sufficient for correctness, the ­direction though is trivial. In the proof the choice of the global constant M (depending on the formula) plays a central role. Imagine for example a property "the heap contains at least five objects different from program variables". To formulate this property we need at least five different logical variables and the constraint on M implies that M 5. For smaller M it can happen that a formula that is satisfied in the abstract case, does 12 Katoen and Noll and Rieger not hold in all concrete configurations associated with the abstract one. E.g. for M = 1 and a graph with one abstract node our example property would be satisfied; in the corresponding concrete graph where the abstract node is represented by two concrete nodes not necessarily. With () we can infer from Thm. 3.10 the validity of the claim, since TPL does not allow path quantifiers. By construction of the abstract PL­semantics it is intuitively clear that () holds. 2 Model Checking Temporal Pointer Logic Because of the two­stage approach in defining the logic, we can reduce the TPL model checking problem to an LTL model checking problem, which can efficiently be verified by existing model checkers. Algorithm 1 Let T = (Q, q0, lab, ) be the abstract transition system generated by a program LMP and TPL the formula to verify. Let := { PL | maximal subformula of } = {1, ..., r}. Define a "traditional" transition system T = (Q, q0, lab , ) where lab : Q 2AP with AP = {pi | i {1, ..., r}} such that pi lab (q) lab(q) |= i. Now solve the LTL model checking problem T |=? LTL [1/p1, ..., r/pr]. The idea is thus to replace all (maximal) PL­subformulas by atomic propositions to obtain an LTL­formula. To do so we first have to evaluate the PL­formulas on the transition system and to change its labeling from configurations to atomic propositions, where each atomic proposition represents the truth value of the corresponding PL­subformula on the given configuration. The correctness of this approach is clear. Limitations Due to the nondeterminism in the abstract semantics caused by the presence of abstract nodes we may obtain false negatives. This means that in the abstract transition system there may exist computations which do not correspond to concrete ones and on which the property to verify does not hold. Consider a program creating a list (pointed to by v) with M + 3 elements and then deleting again M + 3 elements. The property to verify is XF(v = nil), i.e. that the list becomes empty. It is obvious that due to the presence of an abstract node after the construction of the list in the abstract semantics there is a path that retains that abstract node and thus the list never becomes empty (see Def. 3.7, rule 2). In the concrete case however the formula is satisfied. Due to the overapproximation and the LTL approach false positives though cannot occur. This means that the successful verification of a property in the abstract case implies the correctness in the concrete case. False negatives can only occur in cases where information on the precise number of objects is necessary. 5 Application: Concurrent Garbage Collection In this section we will show we will employ our approach to find counterexamples of a concurrent garbage collection algorithm. More concretely we will consider a socalled mark­and­sweep collector, which maintains a bit for each object in the heap to record its reachability status. Here we model this information as an additional heap component, a (partial) function r : N B which indicates whether the 13 Katoen and Noll and Rieger collector considers a node to be reachable (1) or not (0). This component is made accessible to the garbage collector program using the additional constructs * reset Stmt, which resets the reachability value of every node to 0, * mark() Stmt where PExp, which sets the reachability information of the node [[ ]] to 1, and * r() BExp where PExp tests whether the reachability bit of [[ ]] is set. We refrain from giving the formal details of the extended syntax and semantics of LM­programs; these are straightforward to formalize. The only modification we would like to mention explicitly is an adaptation of the automatic garbage collection procedure (cf. Def. 2.3), which is activated after the execution of every LMstatement which potentially causes nodes to become unreachable (we refer to the derivation rules in Def. 2.5). To ensure the finiteness of our abstraction, we still have to use it. However, we will adapt the handling of the leak flag such that it will be set only if the garbage collector considers an unreachable node n to be reachable, i.e., if r(n) = 1. Formally this means that for an extended configuration ^ = (N, A, , F, r) we define ^:= (N, A N, N, F {leak | n (N \ N) : r(n) = 1}, r N) with N = (PV ). Using these concepts we can now proceed by describing how a concurrent garbage collector can be added to a given LM­program, called a mutator. For = var v1, . . . , vk : (s1 . . . sl) LMP, we define := var v1, . . . , vk, t : (s1 . . . sl c) with garbage collector c as in Fig. 5. while tt do reset; with v PV do t := v; while t = nil do if r(t) then t := nil else mark(t); t := t fi od od; signal od Fig. 5. A naive garbage collector Thus the garbage collector is running concurrently with the mutator. It executes an infinite loop, starting by resetting the reachability bit of every node in the heap. Using the auxiliary variable t, it then marks every reachable node, beginning with the roots of the heap which are accessible by the program variables. Here the statement with v PV do s od is a meta construct which is expanded to s[v/v1]; s[v/v2]; ...; s[v/vk] for PV = {v1, . . . , vk}. Whenever it encounters a node which has already been marked (if statement), it continues with the next program variable to avoid redundant assignments. Finally it employs the signaling mechanism of our programming language to indicate that now the actual collection phase would start, i.e., that all nodes whose reachability bit is 0 would be removed. Note, however, that we are still using our automatic garbage collection procedure such that we can guarantee that in every configuration of the system, all nodes are reachable. In other words, whenever the signal occurs there should not exist any unmarked node in the heap. This observation is the key idea for specifying the soundness of the garbage collector c as a safety property in TPL. Here we assume that the underlying Pointer Logic (cf. Def. 4.1) is extended by atomic propositions of the form r() which allow us test the reachability information of the node to which the navigation expression refers: G(signal x : r(x)) 14 Katoen and Noll and Rieger x x 0 0 0 x 1 1 0 x 1 1 0 t x 1 1 0 x 1 1 0 x 1 1 0 x 1 0 x 1 0 x 1 0 t y t y t yt C: reset C+ M: y := x M: x := y M: y := nil M: y := nilC: t := t "leak""signal" C+C: signal Fig. 6. Possible erroneous run of garbage collector and mutator Another important issue is the completeness of the garbage collector, which means that every node which has become unreachable in the course of the computation, will eventually be removed. This, however, cannot be directly expressed for two reasons. First, verifying this property would require to keep track of the identity of objects between different configurations, which in turn involves the nesting of quantifiers and temporal operators. This is not supported by our logic. Second, our automatic garbage collection procedure immediately removes nodes that have become unreachable. What we can formulate instead, however, is a safety property which comes very close to the actual completeness. It expresses that a node which has become unreachable will never be marked by the garbage collector. Employing the modified handling of the leak flag, this property can simply be formulated as G leak Note that this formalization is only justified since the garbage collector is monotonic in the following sense: once a node has been marked, its reachability information will not be reset before the collection signal occurs. Moreover completeness can only be expected (just as the above soundness property) if it is guaranteed that the mutator does not modify the reachability bits. The example computation in Fig. 6 shows that the above garbage collector violates both of these requirements. Here the mutator program is assumed to be of the form y := x; x := y; y := nil; y := nil; it simply discards the second node of the list whose head is referenced by x (assuming that this node exists). Here C and M stand for operations of the collector and the mutator, respectively, which are either concretely given or summarized by a "+" sign. The bits labeling the nodes indicate the reachability information as set by the collector. The computation shows that the collector is neither correct nor complete. In the final step involving the signal flag, the reachability value 0 of the list's tail node means that it would be removed by the collector although it is reachable. Two steps earlier, the leak flag indicates that garbage has automatically been deleted which has been marked as reachable by the collector. Both of these problems are caused by the uncontrolled interaction between the mutator and the collector; they can be avoided by placing the body of the collector loop in an atomic region. 6 Related Work Related work on the topic of analyzing pointer­manipulating programs can be classified into the following (often overlapping) categories. 15 Katoen and Noll and Rieger Predicate abstraction abstracts the state space of the program by evaluating it under a number of given predicates. This yields a Boolean program which conservatively simulates all potential executions [25]. Successful software model checkers such as BLAST [28] and SLAM [3] are based on this approach. There are several papers that use classical predicate abstraction for pointer analysis [2,14]. In particular, [15,16] study concurrent garbage collection using predicate abstraction. Shape analysis is a static analysis framework that represents recursive data structures of unbounded size by finite structures, called "shape graphs". The idea is to apply to the heap the same abstraction that is applied to the program's states in predicate abstraction: it is defined in terms of equivalence classes of heap objects that are induced by a finite set of predicates on those objects. The usual approach is to formalize shape graphs by three­valued logical structures [46]. This approach has been implemented TVLA [34] and in BLAST [5] which makes use of TVLA. Recent developments comprise the development of adaptive methods which automatically adjust to the data structures that occur in the given program [31,35,48], demand­driven techniques [5,27], efficiency improvements [33], and interprocedural shape analysis [26,30,43,44]. It is often argued that the application of predicate abstraction to pointer structures does not work well because it is difficult to find predicates which abstract heap structures in an appropriate and compact way [5]. This claim is substantiated by the results in [36] which investigates the application of both predicate abstraction and shape analysis to programs operating on singly­linked lists, employing a similar abstraction as ours: elements on unshared list segments are summarized. It is shown that standard predicate abstraction requires an exponential number of predicates in comparison to the number of predicates in shape analysis. Also [41] considers both techniques, but in a very restricted programming­language setting which only supports single assignments. Regular model checking is a framework for unified verification of infinite­state systems based on automata theory. It represents states using words (trees) over a finite alphabet and sets of states using finite (tree) automata [10]. Like in our approach, singly­linked lists are also considered in [8,9], but only safety and termination properties are verified. Dataflow analysis is a technique for gathering information about certain aspects of a program using its control flow graph. This approach is generally efficient but restricted to rather shallow properties of programs such as aliasing relations [17,39], points­to information [47,51], or pointer range analysis [50]. Hoare­style approaches: first­order reasoning typically breaks down when it comes to prove properties of pointer­manipulating programs. The main reason is that it is impossible to express an invariant of all members of a data structure in first­order logic. The latter has to be extended therefore to support the definition of a reachability predicate [1,12,22,32,37,38]. However such deductive techniques usually involve user interaction, or otherwise only restricted properties such as dereferencing of nil pointers or aliasing effects can be analyzed. Separation logic has been proposed as an extension to Hoare logic that permits local reasoning about linked structures, supporting features to support modular correctness proofs for pointer­manipulating programs [40,42]. It has been employed for termination proofs of heap­manipulating programs [4], for interprocedural shape 16 Katoen and Noll and Rieger analysis [24], for handling abstract data types [7], and for verifying garbage collection algorithms [6]. However most of the work on separation logic focuses on verifying programs manually. In summary, many of the characterizing features of our approach are already present in earlier papers: the restriction to singly­linked lists without data fields, the introduction of abstract entities which represent a potentially unbounded number of heap cells (called "summary nodes" in [13]); see e.g. [2,9,36], and the observation that, in this setting, the number of sharing points in heap structures is bounded by the number of program variables [9,36]. However none of these combines the strengths of our approach which supports concurrent programs with dynamic memory allocation and destructive updates such that arbitrary (cyclic) linked lists can be constructed, integrates both abstraction and model checking in a fully automated way, supports a linear­time logic in which both safety and liveness properties can be expressed, and which allows to use standard LTL model checkers. In comparison, many of the existing approaches suffer from the poor programming environment, the exclusion of cyclic data structures, the requirement of user interaction, or the restriction to safety properties. Notable exceptions are [2], which also offers liveness properties but requires user­defined ranking functions, [20], which employs extended tableau­based techniques for model checking, and [49], which has a non­standard interpretation. 7 Conclusions and Future Work We have presented a framework for the verification of concurrent pointer­manipulating programs with unbounded heap size and destructive updates. The correctness properties are specified using temporal pointer logic which is essentially pointer logic for expressing heap properties enriched with temporal operators. Instead of requiring dedicated algorithms, the TPL model checking problem is reduced to an LTL model checking problem that can be verified effectively with a broad variety of existing model checkers. The tradeoff is the restriction to list­like data structures as well as the limitation in expressiveness of the logic because object identities are not tracked between configurations. Currently we are implementing our method to verify more realistic examples in the future. In particular we will extend the analysis of concurrent garbage collectors by defining a "hardest mutator", i.e., a general mutator program which is capable of simulating the behavior of any other mutator. This will enable us to establish the correctness of garbage collectors independent of the concrete mutator. Furthermore due to the extensive use of concurrency, state space reduction and optimization techniques such as partial order reduction [21,23] will have to be employed and integrated in the implementation. We also plan to extend our framework with dynamic (unbounded) creation of threads. Another interesting aspect could be the combination of existing finite­state modeling languages like Promela [29] and pointer manipulation. Finally in the long run we have plans to increase the expressivity of the logic as well as to generalize our approach to richer data structures, for which new abstractions will be necessary. Moreover an automata­theoretic approach to defining a storeless semantics, as it is studied in [11] for a (concrete) semantics for pointer programs seems promising. 17 Katoen and Noll and Rieger References [1] T. Amtoft, S. Bandhakavi, and A. Banerjee. A logic for information flow in object­oriented programs. In POPL '06, pages 91­102. ACM Press, 2006. [2] I. Balaban, A. Pnueli, and L. D. Zuck. Shape analysis by predicate abstraction. In VMCAI '05, volume 3385 of LNCS, pages 164­180. Springer­Verlag, 2005. [3] T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL '02, pages 1­3. ACM Press, 2002. [4] J. Berdine, B. Cook, D. Distefano, and P. W. O'Hearn. Automatic termination proofs for programs with shape­shifting heaps. In CAV '06, volume 4144 of LNCS, pages 386­400. Springer­Verlag, 2006. [5] D. Beyer, T. A. Henzinger, and G. Th´eoduloz. Lazy shape analysis. In CAV '06, volume 4144 of LNCS, pages 532­546. Springer­Verlag, 2006. [6] L. Birkedal, N. Torp-Smith, and J. C. Reynolds. Local reasoning about a copying garbage collector. In POPL '04, pages 220­231. ACM Press, 2004. [7] R. Bornat, C. Calcagno, P. O'Hearn, and M. Parkinson. Permission accounting in separation logic. In POPL '05, pages 259­270. ACM Press, 2005. [8] A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In CAV '06, volume 4144 of LNCS, pages 517­531. Springer­Verlag, 2006. [9] A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying programs with dynamic 1­selectorlinked list structures in regular model checking. In TACAS '05, volume 3440 of LNCS 3440, pages 13­29. Springer­Verlag, 2005. [10] A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract regular tree model checking of complex dynamic data structures. In SAS '06, volume 4134 of LNCS, pages 52­70. Springer­Verlag, 2006. [11] M. Bozga, R. Iosif, and Y. Lakhnech. Storeless semantics and alias logic. ACM SIGPLAN Not., 38(10):55­65, 2003. [12] M. Bozga, R. Iosif, and Y. Lakhnech. On logics of aliasing. In SAS '04, volume 3148 of LNCS, pages 344­360. Springer­Verlag, 2004. [13] D. R. Chase, M. Wegman, and F. K. Zadeck. Analysis of pointers and structures. In PLDI '90, pages 296­310. ACM Press, 1990. [14] D. Dams and K. S. Namjoshi. Shape analysis through predicate abstraction and model checking. In VMCAI '03, volume 2575 of LNCS, pages 310­323. Springer­Verlag, 2003. [15] S. Das and D. L. Dill. Successive approximation of abstract transition relations. In LICS '01, pages 51­58. IEEE, 2001. [16] S. Das, D. L. Dill, and S. Park. Experience with predicate abstraction. In N. Halbwachs and D. Peled, editors, CAV '99, volume 1633 of LNCS, pages 160­171. Springer­Verlag, 1999. [17] A. Deutsch. Interprocedural may­alias analysis for pointers: beyond k­limiting. In PLDI '94, pages 230­241. ACM Press, 1994. [18] D. Distefano. On Model Checking the Dynamics of Object­Based Software: a Foundational Approach. PhD thesis, Univ. of Twente, 2003. [19] D. Distefano, J.-P. Katoen, and A. Rensink. Who is pointing when to whom? ­ on the automated verification of linked list structures. In FSTTCS '04, volume 3328 of LNCS, pages 250­262. SpringerVerlag, 2004. [20] D. Distefano, J.-P. Katoen, and A. Rensink. Safety and liveness in concurrent pointer programs. In FMCO '06, volume 4111 of LNCS, pages 280­312. Springer­Verlag, 2006. [21] C. Flanagan and P. Godefroid. Dynamic partial­order reduction for model checking software. In POPL '05, pages 110­121. ACM Press, 2005. [22] P. Fradet, R. Gaugne, and D. L. M´etayer. Static detection of pointer errors: an axiomatisation and a checking algorithm. In ESOP '96, volume 1058 of LNCS, pages 125­140. Springer­Verlag, 1996. [23] P. Godefroid. Partial­Order Methods for the Verification of Concurrent Systems: An Approach to the State­Explosion Problem, volume 1032 of LNCS. Springer­Verlag, 1996. [24] A. Gotsman, J. Berdine, and B. Cook. Interprocedural shape analysis with separated heap abstractions. In SAS '06, volume 4134 of LNCS, pages 240­260. Springer­Verlag, 2006. 18 Katoen and Noll and Rieger [25] S. Graf and H. Sa¨idi. Construction of abstract state graphs with PVS. In CAV '97, volume 1254 of LNCS, pages 72­83. Springer­Verlag, 1997. [26] B. Hackett and R. Rugina. Region­based shape analysis with tracked locations. In POPL '05, pages 310­323. ACM Press, 2005. [27] N. Heintze and O. Tardieu. Demand­driven pointer analysis. ACM SIGPLAN Not., 36(5):24­34, 2001. [28] T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with BLAST. In SPIN '03, volume 2648 of LNCS, pages 235­239. Springer­Verlag, 2003. [29] G. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison­Wesley, 2003. [30] B. Jeannet, A. Loginov, T. W. Reps, and S. Sagiv. A relational approach to interprocedural shape analysis. In SAS '04, volume 3148 of LNCS, pages 246­264. Springer­Verlag, 2004. [31] O. Lee, H. Yang, and K. Yi. Automatic verification of pointer programs using grammar-based shape analysis. In ESOP '05, volume 3444 of LNCS, pages 124­140. Springer­Verlag, 2005. [32] T. Lev-Ami, N. Immerman, T. W. Reps, S. Sagiv, S. Srivastava, and G. Yorsh. Simulating reachability using first­order logic with applications to verification of linked data structures. In CADE '05, volume 3632 of LNCS, pages 99­115. Springer­Verlag, 2005. [33] T. Lev-Ami, N. Immerman, and S. Sagiv. Abstraction for shape analysis with fast and precise transformers. In CAV '06, volume 4144 of LNCS, pages 547­561. Springer­Verlag, 2006. [34] T. Lev-Ami and S. Sagiv. TVLA: A system for implementing static analyses. In SAS '00, volume 1824 of LNCS, pages 280­302. Springer­Verlag, 2000. [35] A. Loginov, T. W. Reps, and S. Sagiv. Abstraction refinement via inductive learning. In CAV '05, volume 3576 of LNCS, pages 519­533. Springer­Verlag, 2005. [36] R. Manevich, E. Yahav, G. Ramalingam, and M. Sagiv. Predicate abstraction and canonical abstraction for singly­linked lists. In VMCAI '05, volume 3385 of LNCS, pages 181­198. Springer­Verlag, 2005. [37] A. Mller and M. I. Schwartzbach. The pointer assertion logic engine. In PLDI '01, pages 221­231. ACM Press, 2001. [38] G. Nelson. Verifying reachability invariants of linked structures. In POPL '83, pages 38­47. ACM Press, 1983. [39] E. M. Nystrom, H.-S. Kim, and W. mei W. Hwu. Bottom­up and top­down context­sensitive summarybased pointer analysis. In SAS '04, volume 3148 of LNCS, pages 165­180. Springer­Verlag, 2004. [40] P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In POPL '04, pages 268­280. ACM Press, 2004. [41] A. Podelski and T. Wies. Boolean heaps. In SAS '05, volume 3672 of LNCS, pages 268­283. SpringerVerlag, 2005. [42] J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS '02, pages 55­74. IEEE Computer Society, 2002. [43] N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm. A semantics for procedure local heaps and its abstractions. In POPL '05, pages 296­309. ACM Press, 2005. [44] N. Rinetzky, M. Sagiv, and E. Yahav. Interprocedural shape analysis for cutpoint­free programs. In SAS '05, volume 3672 of LNCS, pages 284­302. Springer­Verlag, 2005. [45] M. Sagiv, T. Reps, and R. Wilhelm. Solving shape­analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst., 20(1):1­50, 1998. [46] M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3­valued logic. ACM Trans. Program. Lang. Syst., 24(3):217­298, 2002. [47] J. Whaley and M. S. Lam. An efficient inclusion­based points­to analysis for strictly­typed languages. In SAS '02, volume 2477 of LNCS, pages 180­195. Springer­Verlag, 2002. [48] E. Yahav and G. Ramalingam. Verifying safety properties using separation and heterogeneous abstractions. In PLDI '04, pages 25­34. ACM Press, 2004. [49] E. Yahav, T. Reps, M. Sagiv, and R. Wilhelm. Verifying temporal heap properties specified via evolution logic. In ESOP '03, volume 2618 of LNCS, pages 204­222. Springer­Verlag, 2003. [50] S. H. Yong and S. Horwitz. Pointer­range analysis. In SAS '04, volume 3148 of LNCS, pages 133­148. Springer­Verlag, 2004. [51] J. Zhu and S. Calman. Symbolic pointer analysis revisited. In PLDI '04, pages 145­157. ACM Press, 2004. 19