CodePlexProject Hosting for Open Source Software

For the verification of sequential programs there exists a generic verification methodology based on Hoare-logics. The user annotates a program p with precondition A and postcondition B. If it is possible to derive the Hoare-triple ({A}, p, {B}) in the calculus of Hoare-logics we can conclude that any execution of p in a program state that satisfies A can only yield a program state that satisfies B. It is common to express the precondition and postcondition as assertions on the program state. The verification of a Hoare-triple can then be performed by translating the Hoare-triple to verification-conditions based on a weakest-precondition-style axiomatization of the Hoare-logics. The notable thing is that you can derive Hoare-triples for large programs by applying the rule for sequential composition. This allows you to view any program of arbitrary length as a relation on the program state.

Going from a sequential to a concurrent system, we have to change our way of thinking and, in particular, our way of specifying correctness of the system in a fundamental way. The one notable difference between sequential and concurrent programs is that the semantics of program-execution are extended with the concept of parallel composition:

p_1 || p_2 || ... || p_n

Instead of arguing about a single program we now want to talk about n programs running concurrently (e.g. all the threads in a multi-processor system). In this context, "running concurrently" means that the semantics of the composed system is characterized by the fact that at any given transition exactly one of the component programs p_i performs a single step. In the following we give a brief introduction on how the original sequential Hoare-logics are extended to concurrent systems. We begin with an overview on the original effort by Susan Owicki and David Gries and then discuss the rely-guarantee method. Finally, we consider the verification methodology implemented by VCC and relate it to the two previous methods. We do not try to go into absolute detail here, but instead try to give an intuition for the differences between the verification methods. Detail information can be gotten from the corresponding papers.

p_1: x = x + 1 || p_2 : x = x + 2

Here, we have two programs p_1 and p_2 which each consist of only a single assignment statement. Intuitively, we can see that for the whole system p = p_1 || p_2 the Hoare-triple

({x == *a*}, p, {x == *a* + 3})

is valid for all *a*. However, there are two different computations of the system that lead to this final result.

Since in a concurrent system the steps of the programs in a parallel composition may be interleaved arbitrarily there may be more than one well-defined computation for a given program (opposed to the sequential case where there always is only a single well-defined computation for any given program). Thus, in a concurrent setting, validity of a Hoare-triple ({A}, p, {B}) means that for all computations of p, any computation that starts from a program state satisfying A may only reach a program state satisfying B.

With the notion of validity of a Hoare-triple in a concurrent setting, we still need a calculus that allows us to derive that a concurrent Hoare-triple is valid. Such a calculus can be described by inference rules that describe the valid Hoare-triples we can derive by looking at one single step of the machine at a time as well as the rules for the compositional language constructs, sequential and parallel composition. The good thing is that each step of the concurrent machine is just a step of one of its sequential programs. Thus, we already have the inference rules for the valid Hoare-triples on single steps of the concurrent machine from the sequential case. Essentially, we have all the rules we need apart from a rule for deriving valid Hoare-triples for the parallel composition.

In order to prove that a concurrent Hoare triple is valid, we need to prove that all interleavings of the concurrent program fulfill the Hoare-triple. That means, we either have to derive the Hoare-triple for each of the interleavings or we need some kind of clever trick that makes checking all interleavings easier. In the case of Owicki-Gries, the clever trick consists of annotating intermediate conditions on all points where the sequential component may be interleaved by other components of the concurrent system. Then, two things remain to be done: We have to verify correctness of the sequential component programs with respect to the Hoare-triples we get from the annotations, and, further, we have to check that the intermediate assertions do not invalidate each other for all possible interleavings. This is called the interference-freedom-check.

({A1}, p_1, {B1}) is valid and ({A2}, p_2, {B2}) is valid and the proofs of both components are interference-free ----------------------------------------------------------------------------------------------------------------------------------- ({A1 /\ A2}, p_1 || p_2 , {B1 /\ B2}) is valid

Let us consider some annotations for our previous example:

p_1: {x == *a* \/ x == *a* + 2} =: {A1} x = x + 1 {x == *a* + 1 \/ x == *a* + 3} =: {B1} p_2: {x == *a* \/ x == *a* + 1} =: {A2} x = x + 2 {x == *a* + 2 \/ x == *a* + 3} =: {B2}

In this example it is easy to see that the annotated assertions indeed form valid Hoare-triples with their corresponding instruction. Now, we just need to show for all intermediate assertions that they are not invalidated by other component processes' steps, i.e.

({A1 /\ A2}, p_2, {A1}) is valid ({B1 /\ A2}, p_2, {B1}) is valid and ({A2 /\ A1}, p_1, {A2}) is valid ({B2 /\ A1}, p_1, {B2}) is valid

We can see that, for larger systems the number of interference checks quickly gets very large.

Formal Aspects of Computing Vol. 9 Nr. 2, March 1997, Springer London

http://www.springerlink.com/content/pw138twh343x5466/

Last edited Sep 5, 2009 at 9:35 AM by MarkHillebrand, version 3