The following technical report is available from http://aib.informatik.rwth-aachen.de:
A Framework for Proving Correctness of Adjoint Message Passing Programs Uwe Naumann, Laurent Hascoet, Chris Hill, Paul Hovland, Jan Riehme, Jean Utke AIB 2008-06
Adjoint programs play a central role in modern numerical algorithms such as large-scale sensitivity analysis, parameter tuning, and general nonlinear optimization. They can be generated automatically by compilers. In such cases, the data flow of the original program needs to be reversed. If message passing is used, then any communication needs to be reversed, too. Crucial properties of the original program such as deadlock-freeness and determinism must be preserved in the adjoint code. A formalism for proving the correctness of compiler-generated adjoints is required but has been missing so far, to the best of our knowledge.
To rectify this situation, we propose a proof technique that relies on data dependences in partitioned global address space versions of the adjoint message-passing program. If the original program is deadlock-free, the transformation rules can be shown to be correct in the sense that the automatically generated adjoint program is also deadlock free while implementing the mathematical mapping from given independent inputs onto their corresponding adjoints correctly. As an example we discuss asynchronous unbuffered send/receive using MPI.