An approach to correctness of data parallel algorithms

Abstract

The design of data parallel algorithms for fine-grained SIMD machines is a fundamental domain in today computer science. High standards in the specification and resolution of problems have been achieved in the sequential case. It seems reasonable to apply the same level of quality to data parallel programs. It appears that most of the data parallel problems can be specified in terms of post and preconditions. These conditions characterize the overall state of the fine-grained processors in the initial and final states. In this paper: We present an axiomatic system to prove correctness of data parallel algorithms on fine-grained SIMD machines. We specify some data parallel problems like tree sum, radix sorting, and dynamic memory allocation. With this set of axioms we prove the correctness of programs solving the above problems. It seems that the framework to deal with data parallel problems is quite different from the other one dealing with problems of parallelism with multiple threads of control, like those solvable in CSP.