Derivation of Parallel Sorting Algorithms
Parallel algorithms can be derived from formal problem specifications by applying a sequence of transformations that embody information about algorithms, data structures, and optimization techniques. The KIDS system provides automated support for this approach to algorithm design. This paper carries through the salient parts of a formal derivation for a well-known parallel sorting algorithm — Batcher’s Even-Odd sort. The main difficulty lies in building up the problem domain theory within which the algorithm is inferred.
KeywordsOutput Condition Parallel Algorithm Composition Operator Algorithm Design Sorting Algorithm
Unable to display preview. Download preview PDF.
- Batcher, K. Sorting networks and their applications. In AFIPS Spring Joint Computing Conference (1968), vol. 32, pp. 307–314.Google Scholar
- Blaine, L., and Goldberg, A. DTRE — a semi-automatic transformation system. In Constructing Programs from Specifications, B. Möller, Ed. North-Holland, Amsterdam, 1991, pp. 165–204.Google Scholar
- Dowd, M., Perl, Y., Rudolph, L., and Saks, M. The periodic balanced sorting network. Journal of the ACM 36, 4 (October 1989), 738–757.Google Scholar
- Jones, G., and Sheeran, M. Collecting butterflies. Tech. Rep. PRG-91, Oxford University, Programming Research Group, February 1991.Google Scholar
- Leighton, F. Introduction to Parallel Algorithms and Architectures: Arrays, Trees, Hypercubes. Morgan Kaufmann, San Mateo, CA, 1990.Google Scholar
- Smith, D. R. Top-down synthesis of divide-and-conquer algorithms. Artificial Intelligence 21, 1 (September 1985), 43–96. (Reprinted in Readings in Artificial Intelligence and Software Engineering, C. Rich and R. Waters, Eds., Los Altos, CA, Morgan Kaufmann, 1986.).Google Scholar
- Smith, D. R. KIDS — a semi-automatic program development system. IEEE Transactions on Software Engineering Special Issue on Formal Methods in Software Engineering 16, 9 (September 1990), 1024–1043.Google Scholar
- Smith, D. R., and Lowry, M. R. Algorithm theories and design tactics. Science of Computer Programming 14, 2–3 (October 1990), 305–321.Google Scholar
- Smith, D. R. Structure and design of problem reduction generators. In Constructing Programs from Specifications, B. Möller, Ed. North-Holland, Amsterdam, 1991, pp. 91–124.Google Scholar
- Smith, D. R. Constructing specification morphisms. Tech. Rep. KES.U.92.1, Kestrel Institute, January 1992. to appear in Journal of Symbolic Computation, 1993.Google Scholar