Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Akl, S. The Design and Analysis of Parallel Algorithms. Prentice-Hall Inc., Englewood Cliffs, NJ, 1989.
Batcher, K. Sorting networks and their applications. In AFIPS Spring Joint Computing Conference (1968), vol. 32, pp. 307–314.
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.
Dowd, M., Perl, Y., Rudolph, L., and Saks, M. The periodic balanced sorting network. Journal of the ACM 36, 4 (October 1989), 738–757.
Gibbons, A., and Rytter, W. Efficient Parallel Algorithms. Cambridge University Press, Cambridge, 1988.
Jones, G., and Sheeran, M. Collecting butterflies. Tech. Rep. PRG-91, Oxford University, Programming Research Group, February 1991.
Leighton, F. Introduction to Parallel Algorithms and Architectures: Arrays, Trees, Hypercubes. Morgan Kaufmann, San Mateo, CA, 1990.
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.).
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.
Smith, D. R., and Lowry, M. R. Algorithm theories and design tactics. Science of Computer Programming 14, 2–3 (October 1990), 305–321.
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.
Smith, D. R. Constructing specification morphisms. Tech. Rep. KES.U.92.1, Kestrel Institute, January 1992. to appear in Journal of Symbolic Computation, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1993 Kluwer Academic Publishers
About this chapter
Cite this chapter
Smith, D.R. (1993). Derivation of Parallel Sorting Algorithms. In: Paige, R., Reif, J., Watcher, R. (eds) Parallel Algorithm Derivation and Program Transformation. The Springer International Series In Engineering and Computer Science, vol 231. Springer, Boston, MA. https://doi.org/10.1007/978-0-585-27330-3_2
Download citation
DOI: https://doi.org/10.1007/978-0-585-27330-3_2
Publisher Name: Springer, Boston, MA
Print ISBN: 978-0-7923-9362-7
Online ISBN: 978-0-585-27330-3
eBook Packages: Springer Book Archive