AN APPROACH TO CORRECTNESS OF DATA-PARALLEL ALGORITHMS

The design of data parallel algorithms for fine-grain machines is a fu ndamental domain in today's computer science. High standards in the sp ecification and resolution of problems have been achieved in the seque ntial case. It seems reasonable to apply the same level of quality to data parallel programs. It appears that most data parallel problems ca n be specified in terms of pre- and postconditions. These conditions c haracterize the overall state of the fine-grain processors in the init ial and final states. In this paper: We present an axiomatic system to prove correctness of data parallel algorithms on single-instruction m ultiple-data (SIMD) machines. We specify some data parallel problems l ike tree sum, root finding, radix sorting, and dynamic memory allocati on. With this set of axioms we prove the correctness of programs solvi ng the problems above. It seems that the framework for data parallel p roblems is quite different from those for problems of parallelism with multiple threads of control, like those solvable in Communicating Seq uential Processes (CSP). (C) 1994 Academic Press. Inc.