Formal Validation of Data-Parallel Programs: The Assertional Approach

Luc Bouge, David Cachera

In this talk, we specifically address the validation of Alpha programs, as specified by Quinton and Rajopadhye, IRISA, Rennes, France. Alpha programs are made of a set of recurrence equations, one for each variable. A rich set of transformations has been developped for them, including changes of basis to separate time and space components. But little has been done to prove abstract properties of such programs, especially partial properties of their functional behavior. We do not consider here properties which may depend on a particular scheduling of the program.

We present here a framework to prove input/output properties {p} S {q}. It is based on the search for a program invariant, very much as in the proof of a while-loop in Hoare's logic. Our main result is the completeness of the method: for any valid property, there exists an invariant to prove it. In fact, this invariant is nothing but the logical encoding of all data-flow dependencies specified by the program. Its external from is actually exactly the same as the program text, up to a suitable interpretation of the ``='' sign. Of course, a property may also be proved using weaker ad-hoc invariants.

Using this approach sets up a firm foundation for all kinds of ``handwaving'' manipulations found in the literature about Alpha programs. It is especially crucial when the properties under study cannot be expressed as another Alpha program: non-linear indexing of arrays, induction arguments, etc.

@TECHREPORT{LIP:RR95-08,
        AUTHOR             = {Luc Bougé and  David Cachera},
        INSTITUTION        = {LIP, ENS Lyon, France},
        NUMBER             = {RR96-32},
        TITLE              = {A logical framework for proving Alpha programs},
        TYPE               = {Research Report},
        YEAR               = {1996},
	URL                = {ftp://ftp.ens-lyon.fr/pub/LIP/Rapports/RR/RR96/RR96-32.ps.Z}
}