Formal Derivation of Divide-and-Conquer Programs: A Case Study in the Multidimensional FFT's

Sergei Gorlatch

This paper reports a case study in the development of parallel programs in the Bird-Meertens formalism (BMF), starting from divide-and-conquer algorithm specifications. The contribution of the paper is two-fold: (1) we classify divide-and-conquer algorithms and formally derive a parameterized family of parallel implementations for an important subclass of divide-and-conquer, called DH (distributable homomorphisms); (2) we systematically adjust the mathematical specification of the Fast Fourier Transform (FFT) to the DH format and thereby obtain a generic SPMD program, well suited for implementation under MPI. The target program includes the efficient FFT solutions used in practice -- the binary-exchange and the 2D- and 3D-transpose implementations -- as its special cases.