Correctness-preserving transformations for the design of parallel programs
This paper is about how to design correct computer programs. In particular it concerns formal methods for the construction and verification of parallel algorithms. We develop the theoretical foundations of a language and a programming methodology for designing parallel algorithms and illustrate the methodology by presenting a concrete program derivation. The goal of the methodology is to define a mapping of a program specification into a concurrent programming language. The methodology is developed in the context of the Unity formalism.
We put special emphasis on derivation of parallel algorithms that are correct with respect to some high-level program specification. The issue of efficiency in the sense of execution time and space is outside the scope of the present paper.
Unable to display preview. Download preview PDF.
- 1.K. R. Apt and E. R. Olderog. Proof rules and transformations dealing with fairness. Science of Computer Programming, 3:65–100, 1983.Google Scholar
- 2.BP Innovation Centre and Edinburgh Portable Compilers Ltd. B-Tool Version 1.1, Reference Manual, 1991.Google Scholar
- 3.N. Brown. Correctness-Preserving Transformations for the Design of Parallel Program. In Internal note, 1994. full version.Google Scholar
- 4.N. Brown. A Sound Mapping from Abstract Algorithms to Occam Programs. In H.R. Arabnia, editor, Transputer Research and Applications Conference. IOS Press, October 1994. pages 218,231.Google Scholar
- 5.N. Brown and D. Méry. A proof environment for concurrent programs. In J. C. P. Woodcock, editor, FME'93: Industrial-Strength Formal Methods, pages 196–215. IFAD, Springer-Verlag, 1993. LNCS 670.Google Scholar
- 6.K. M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988.Google Scholar
- 7.K.M. Chandy and S. Taylor. An Introduction to Parallel Programming. Jones and Bartlett, 1992.Google Scholar
- 8.E. Knapp. An Exercise in the Formal Derivation of Parallel Programs: Maximum Flows in Graphs. Transactions On Programming Languages and Systems, 12(2):203–223, 1990.Google Scholar
- 10.J. Misra. Specification structuring. Internal report, Department of Computer Sciences, The University of Texas at Austin, March 1990.Google Scholar
- 12.B.A. Sanders. Eliminating the Substitution Axiom from UNITY Logic. Formal Aspects of Computing, 3:189–205, 1991.Google Scholar
- 13.Scientific Computing Associates inc, 246 Church Street, Suite 307 New Haven, CT 06510 USA. Original LINDA C-Linda Reference manual, 1990.Google Scholar