On a Fixpoint Semantics and the Design of Proof Rules for Fair ParallelPrograms
Charanjit S. Jutla, Josyula R. Rao · 1992
In this paper, we present a predicate transformer approach to the semantics of parallel programs. The meaning of a program is given by two components - a predicate transformer wlt characterizing the progress properties of the program and a predicate transformer wsafe concerned with safety properties. We illustrate the utility of our semantics by developing a simple and powerful framework for the systematic design of proof rules for progress for a range of fairness assumptions including pure nondeterminism, unconditional fairness, minimal progress, weak fairness and strong fairness. Beginning with an intuitive branching time temporal logic (CTL*) formula characterizing progress for the fairness notion being considered, we obtain a simple fixpoint characterization of wlt. We use this fixpoint characterization to extract a simple UNITY-like proof rule for proving progress under the aforementioned fairness constraint. A key feature of our framework is that by merely checking a set of simple conditions, the soundness and completeness of the proof rule is easily guaranteed. It is to be noted that unlike previous work on proof rules for fairness, our meta-theoretic arguments are conducted without resorting to any complicated machinery such as ordinals. Further, the UNITY-like formulation of the proof rule enables one to use the UNITY theory of progress when designing programs based on different notions of fairness. The fixpoint characterizations of wlt for the fairness constraints share a common structure - they are all expressed in terms of a simpler predicate transformer, called the generalized weakest precondition (gwp). We motivate a notion of completeness for progress under fairness constraints and show that it is subject to the same assumptions and constraints as Hoare triples. We define a simple notion of program composition and show that for all notions of fairness considered (excepting strong fairness) gwp and wsafe are compositional. Finally, we show that two programs have the same predicate transformer semantics (in terms of wlt and wsafe) iff they agree on all formulae of a fair version of the full branching time logic CTL* without stuttering. This means that two semantically equivalent programs agree on a rich class of properties.