A Methodology for Designing Proof Rules for Fair Parallel Programs

Abstract

We propose a methodology for designing sound and complete proof systems for proving progress properties of parallel programs under various fairness assumptions. Our methodology begins with a branching time temporal logic formula (CTL*) formula that expresses progress under a fairness assumption. The next step obtains an equivalent fixpoint characterization of this CTL* formula in the μ-calculus. The final step uses the fixpoint characterizations to extract proof systems for proving progress under the fairness constraint. The methodology guarantees that the proof rules so obtained are sound and relatively complete in the sense of Cook.