P. Cousot & R. Cousot, Invariance Proof Methods and Analysis Techniques For Parallel Programs

Patrick Cousot & Radhia Cousot.
Invariance Proof Methods and Analysis Techniques For Parallel Programs.
In A.W. Biermann, G. Guiho & Y. Kodratoff, editors, Automatic Program Construction Techniques, Ch. 12, pages 243--271. Macmillan, New York, 1984.
PDF (1.9 Mo).
Abstract:
   We use discrete state transition systems (Keller [1976], Cousot, P. [1979, 1981]) as abstract models of programs so that our approach is independent of any particular programming language. We use parallel programs with shared variables for illustration purposes.
   Our approach is also independent of the particular class of program properties which is considered. For simplicity, we only consider invariance properties in this paper. Important properties falling under this category are partial correctness, non termination, absence of run-time errors, deadlock freedom, mutual exclusion, etc.
   Since programs are finite descriptions of arbitrary long and sometimes infinite computations, properties of these computations can only be proved using some inductive reasoning. Hence program proof methods rely upon induction principles. For a given class of program properties several different induction principles can be considered. For simplicity, only one basic induction principle will be considered in this paper, which underlies Floyd [1967]'s partial correctness proof method. (A number of different although equivalent induction principles for invariance can be found in Cousot and Cousot [1982].)
   All proof methods which rely upon the same induction principle intuitively look similar, but can be difficult to compare in the abstract. We offer a unified view for comparing them. It consists in showing that the verification conditions involved in any of these methods can be obtained by decomposition of the global inductive hypothesis used in the induction principle into an equivalent set of local inductive hypotheses. Such decompositions can be formalized as connections between lattices (see Cousot and Cousot [1979, 1980b]) and in particular obtained by a cover of the set of states of the program where each local inductive hypothesis holds for a given block of the cover (Cousot[1979]). It is possible to find as many proof methods as such different decompositions. We illustrate only three of them which respectively lead to Floyd [1967], Owicki and Gries [1976], and Lamport [1977, 1980] invariance proof methods. This approach also provides a framework for systematically constructing new sound and complete proof methods based on unexplored induction principles or decompositions (See for example Cousot, R. [1981], Cousot and Cousot [1980a]).
   Static program flow analysis techniques can be used for discovering semantic properties of programs, that is, for discovering properties of the runtime behavior of programs without actually running them. Such analysis methods consist in solving a fixed point system of equations (by elimination or iteration algorithms) associated with the program to be analyzed (Cousot and Cousot [1977]). In the design of such methods the essential part consists in defining correctly the rules for associating the system of equations with the program. We have shown (Cousot and Cousot [1979]) that they can be derived from the verification conditions of a proof method using an approximate decomposition, hence from a basic induction principle. We illustrate this point of view by generalizing Cousot and Cousot [1976] to parallel programs with shared variables. Another example can be found in Cousot and Cousot [1980b] that generalizes Cousot and Halbwachs [1978] to parallel processes communicating by rendez-vous.

\bibitem{CousotCousot84-1}
P.~Cousot and R.~Cousot.
\newblock Invariance Proof Methods and Analysis Techniques For Parallel
Programs.
\newblock In A.W.~Biermann, G.~Guiho and Y.~Kodratoff (Eds),
\emph{Automatic Program Construction Techniques}, Ch.~12, pages 243--271,
Macmillan, New York, NY, U.S.A., 1984.

@incollection{CousotCousot84-1,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Invariance Proof Methods and Analysis Techniques For Parallel
                Programs},
   pages =     {243--271},
   editor =    {Biermann, A{.}W{.} and Guiho, G{.} and Kodratoff, Y{.}},
   chapter =   12,
   booktitle = {Automatic Program Construction Techniques},
   publisher = {Macmillan, New York, New York, United States},
   year =      1984,
}

copyright notice
Last modified: Tuesday, 29-Sep-2015 18:10:43 EDT