Building on the unity experience: compositionality, fairness and probability in parallelism
Josyula R. Rao · 1992
The UNITY methodology marks an important milestone in research on program verification. The methodology shows how a simple programming notation and a small set of carefully engineered operators can be used to reason effectively about a wide range of parallel programs. The goal of this dissertation is to explore and understand the limitations of this approach by: (a) clearly formulating and tackling existing problems of parallelism using the machinery of UNITY (b) increasing the applicability of UNITY by extending and generalizing the notation and logic, and (c) developing useful abstractions and paradigms for program design. We summarize our contributions below. In designing a system of processes, it is desirable to have a guarantee that the progress made by each individual process is inherited by the system. Using semantic arguments, we derive such a guarantee in terms of restrictions on inter-process interactions. Our restrictions form the basis of a compositional methodology for parallel program design and provide a rigorous justification for including certain features in parallel programming languages. Changing the nature of the fairness assumption in UNITY affects the progress properties that can be proven of UNITY programs. We propose a framework for the systematic design of proof rules for proving progress under fairness assumptions ranging from pure nondeterminism to strong fairness. Proofs of soundness and relative completeness of the synthesized rules follow by checking a set of simple conditions. Unlike existing work, our proofs do not use ordinals. Of late, programmers have started using probabilistic transitions in designing simple and efficient algorithms for problems that may not have a deterministic solution. We generalize UNITY to permit probabilistic transitions and develop a UNITY-like theory to design probabilistic parallel programs. We illustrate our theory with examples from random walks and mutual exclusion. We propose a new paradigm for the design of probabilistic parallel programs called eventual determinism. The paradigm provides a means of combining probabilistic and deterministic algorithms to take advantage of both. The proofs of such algorithms use the probabilistic generalization of UNITY. We illustrate the paradigm with examples from conflict-resolution and self-stabilization. Our investigations and results reaffirm the promise of UNITY: it provides a versatile medium for posing and solving many of the diverse problems of parallelism.