@article{GorTSE,
author={Sergei Gorlatch},
title={Toward Formally-Based Design of Message Passing Programs},
journal={IEEE Transactions on Software Engineering},
volume=26,
number=3,
year= March 2000,
pages={276--288},
abstract={
We present a methodology for designing message passing programs
with collective operations, such as reduction, scan, gather, etc.
The design process is based on the correctness-preserving
transformation rules, provable in a formal functional framework.
We develop architecture-independent design
rules for composition and decomposition:
e.g., scan followed by reduction is replaced by a single reduction,
and global reduction is decomposed into two faster operations.
The impact of the design rules on the target performance
is estimated\linebreak analytically and tested in the machine experiments.
As a case study, we design two provably correct,
efficient programs in the Message Passing Interface (MPI)
for the famous maximum segment sum problem, starting from an intuitive
but inefficient algorithm specification.
}
Sergei Gorlatch