Derivation of Parallel Programs: Two Examples
Edgar Knapp · 1990
We give two examples of how concurrent programs can be derived from their specifications much like sequential ones. As a formal framework for our research we use the UNITY formalism due to Chandy and Misra. Starting from an initial UNITY specification we proceed in a series of strengthening steps until the specification is restrictive enough to be translated directly into UNITY code. The programs we obtain this way satisfy Reynold's Conditions in that each atomic action mentions at most one shared variable, and are therefore easily implemented on a variety of architectures. 0 Contents 0 Introduction 1 1 Parallel Linear Search 3 1.0 Problem Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.1 Design of a Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 The Program . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2 Asynchronous Fixpoint Computation 8 2.0 Problem Specification . . . . . . . . . . . . . . ....