Compositional Proofs of Concurrent Programs

Lawrence C. Paulson, Computer Laboratory, University of Cambridge

Research associates: Tanja Vos (to 17 March 2000), Sidi O. Ehmety

Funded by the EPSRC (1 October 1999 to 16 June 2003).

Grant reference GR/M75440/01. Value £157,756


Proposed Research

Background. UNITY [3] is a formalism for proving the correctness of concurrent systems. It supports a simple model of concurrent programming. There is a single, global state. A program consists of an initial condition and a set of actions. The latter is a collection of guarded atomic commands that are repeatedly executed under some fairness constraint. UNITY includes a small fragment of temporal logic. While primitive compared with TLA [10], it supplies well-understood methods for proving both safety and progress (liveness) properties. UNITY is of enduring interest: introduced in 1988, it is still investigated by many researchers.

UNITY gives a general treatment of concurrent systems, especially those based on shared variables. The original textbook [3] specified commands to be simultaneous assignments to variables. Researchers later realized that any commands could be allowed, provided a command always terminated and that each program included a skip (do nothing) command [16, 17]. UNITY supersedes the ad-hoc formalisms that authors sometimes introduce when verifying concurrent programs. The input language of Murphi, a popular model-checker, is based on UNITY [6].

The Isabelle mechanization regards a program as a triple: the set of program states, the set of allowed initial states, and the set of commands. A command (or action) is a relation on the set of program states. The set of possible finite traces is defined inductively. Predicates on states are identified with sets of states. Similarly, program properties (or specifications) are identified with sets of programs, by analogy with the 'proofs as programs' approach. Identifying program properties with sets allows a smooth formalization of the guarantees operator discussed below.

Safety properties are expressed using the constrains operator co (also called next), which expresses the usual precondition-postcondition relationship. The meaning of F : A co B is that if A holds and some action of program F is executed, then B will hold afterwards. (Recall that specifications are identified with sets of programs; equivalently, co may be regarded as a 3-place relation.) If the postcondition equals the precondition then the property holds forever once established and is called stable. A stable property that holds initially is called invariant.

Progress properties are expressed using the leads-to relation. The meaning of F : A |-> B is that if A holds now then B will hold eventually as program F executes. Leads-to properties depend upon which fairness policy is adopted. Misra [16] describes three: minimal progress, weak fairness and strong fairness. Most work assumes weak fairness, which guarantees that a command will eventually be executed if it is enabled continuously.

UNITY has been mechanized using other tools. HOL-UNITY [1] is impressive. It provides much automation and includes a graphical interface for outlining progress proofs, but it does not address program composition. Coq-UNITY [8] has its own treatment of composition: a program has an additional component defining the set of actions it may be composed with. This treatment seems limited and does not appear to be used by other researchers.

This proposal starts from the notion of the union of two programs: essentially, parallel composition. If F and G are two programs defined over the same state space, then F || G is also a program. Its initial condition is the intersection of those of F and G, while its set of actions is the union of F's and G's actions. Our goal is to derive properties of F || G from the abstract properties of F and G without having to consider the actions of F || G explicitly.

We can reason in this compositional way about safety. If F : A co B and G : A co B then clearly F || G : A co B, since an action of F || G is either an action of F or an action of G, and all those actions take the precondition A to the postcondition B. However, such reasoning does not work for progress. Even if F : A |-> B and G : A |-> B, we cannot expect that F || G : A |-> B because the two programs might interfere with each other. For example, if x is a shared variable, then F might increment x and G might decrement x; each program guarantees that eventually |x| > 10, but F || G does not: it can alternately increment and decrement x forever.

Several researchers have proposed methods for reasoning about compositional systems. Chandy and Sanders [4] base their work on existential and universal properties. A property X is existential provided that if F satisfies X then F || G satisfies X. It is universal provided that if F, G satisfy X then F || G satisfies X. These simple notions allow a compositional approach to progress based upon transient assertions (which are existential) and safety assertions (which are universal), combined using the PSP law.

Chandy and Sanders [4] also introduce guarantees assertions. If F : X guarantees Y, then for all G, if F || G satisfies X, then F || G also satisfies Y. (Here X and Y are program properties: safety, progress, or even other guarantees properties. Such assertions provide a general means of proving safety and progress properties of systems that take F as a component.

The theory outlined above allows reasoning about F || G where the two components cooperate to make progress. Equally important is the case where F makes progress and G does not interfere. Meier and Sanders [12] give a general treatment of non-interference, superseding the work of several previous authors. Central to their approach is the notion of progress set, which generalizes the sufficient conditions of previous non-interference theorems. The literature includes much more in this vein. With the help of mechanical proof tools, this theory can be subjected to formal scrutiny and applied to examples.

Programme and Methodology

UNITY proofs have traditionally been done by hand. Many unstated assumptions make mechanization difficult. For example, if x is a local variable of F, then obviously the only actions of F || G that can modify x are actions of F. All such 'obvious' properties have to be made explicit and given effective proof support.

The very notion of state is problematical. Insisting that a state should be a function from variable names to values is restrictive. Allowing states to remain abstract yields a more elegant formalization, allowing for instance Cartesian product constructions over state spaces. The elegance is marred when we consider variable sharing, particularly the sort that identifies the variables F[i ].out and G.in[i]. We now have the choice between complicating the theory to admit such sharing or forcing states after all to be functions over variables. In the later case, the variable names will become equivalence classes. Both approaches are complicated. A third approach to extending and renaming state variables could be based upon the work of Marques [11]. Determining which approach is best will require experimentation. This is a key task of the proposal, and is independent of the various theories of composition.

The next step is to mechanize the theory of Chandy and Sanders [4], which is the most attractive of the existing theories of composition. One feature that distinguishes their work from many other 'rely-guarantee' models is that assertions refer to the full system, rather than distinguishing the component from its environment. This facilitates the analysis of systems comprising many components. Paulson has already mechanized parts of this theory, but much work remains, and all such work is preliminary until the notion of state (discussed above) is finalized.

The next step is to evaluate the environment by performing some case studies. The first will be the Allocator of Chandy and Charpentier [2]. In this example, several clients request and return resources (represented by tokens), while an allocator attempts to satisfy the requests. Since the design is compositional, the allocator and a typical client are specified separately. Properties of the allocator are proved under the assumption that clients are well-behaved (for instance, they return resources eventually). A typical client is verified under analogous assumptions. Many clients and the allocator can be combined to form a system, which is verified by reasoning about how the components interact. This proof is expressed in terms of the abstract properties of the components and can be performed before the components themselves have been verified.

The Allocator example admits several variations and generalizations. For example, the clients and allocator can communicate via shared variables (instantaneously) or via a network. Such distinctions are important; exhausting these possibilities will take some time. The expertise and mechanical theories derived from the first case study will allow more elaborate ones to be investigated. There are other examples in the literature, but ideally, new examples will be designed in collaboration with the UNITY teams at Caltech or Austin.

Other theories for verifying compositional systems will also be investigated. One possibility is the progress sets of Meier and Sanders [12]; another is Misra's closure properties [15]. More speculatively, another possibility is to apply the mechanical formalisms to Misra's theory of multiprogramming, Seuss [18].

References

[1] Flemming Andersen, Kim Dam Petersen, and Jimmi S. Pettersson. Program verification using HOL-UNITY. In J. Joyce and C. Seger, editors, Higher Order Logic Theorem Proving and Its Applications: HUG '93, LNCS 780, pages 1–15. Springer, 1994.

[2] K. Mani Chandy and Michel Charpentier. An experiment in program composition and proof, 1998. preprint.

[3] K. Mani Chandy and Jayadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.

[4] K. Mani Chandy and Beverly A. Sanders. Reasoning about program composition, 1998. preprint.

[5] Michel Charpentier, Mamoun Filali, Philippe Mauran, Gérard Padiou, and Philippe Quéinnec. Tailoring UNITY to distributed program design. In Rolim [19], pages 820–832.

[6] David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang. Protocol verification as a hardware design aid. In Computer Design: VLSI in Computers and Processors, pages 522–525. IEEE Computer Society Press, October 1992.

[7] Jim Grundy and Malcolm Newey, editors. Theorem Proving in Higher Order Logics: Emerging Trends. Supplementary proceedings, TPHOLs '98. Technical report 98–08, Department of Computer Science, Australian National University, 1998.

[8] Barbara Heyd and Pierre Crégut. A modular coding of UNITY in COQ.In von Wright et al. [20], pages 251–266.

[9] Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In von Wright et al. [20], pages 283–298.

[10] Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.

[11] François Marques. Program composition in COQ-UNITY. In Grundy and Newey [7], pages 95–104.

[12] David Meier and Beverly Sanders. Composing leads-to properties. Technical Report TR 96–013, Department of Computer and Information Science, University of Florida, 1996.

[13] Stephan Merz. Yet another encoding of TLA in Isabelle. Technical report, Institut für Informatik, TU München, 1997.

[14] Jayadev Misra. A family of 2-process mutual exclusion algorithms. February 1990. Notes on UNITY: 13–90.

[15] Jayadev Misra. Closure properties. Sep 1994.

[16] Jayadev Misra. A logic for concurrent programming: Progress. Journal of Computer and Software Engineering, 3(2):273–300, 1995.

[17] Jayadev Misra. A logic for concurrent programming: Safety. Journal of Computer and Software Engineering, 3(2):239–272, 1995.

[18] Jayadev Misra. An object model for multiprogramming. In Rolim [19].

[19] José Rolim, editor. Parallel and Distributed Processing, LNCS 1388, 1998.

[20] J. von Wright, J. Grundy, and J. Harrison, editors. Theorem Proving in Higher Order Logics: TPHOLs '96, LNCS 1125, 1996.


Lawrence C. Paulson