A Framework for Proving Correctness of Adjoint Message Passing Programs

Uwe Naumann Laurent Hascoët Chris Hill Paul Hovland Jan Riehme Jean Utke

Proceedings of the 15th European PVM/MPI Users' Group Meeting on Recent Advances in Parallel Virtual Machine and Message Passing Interface (8 pages)

Abstract: Adjoint programs play a central role in modern numerical algorithms such as large-scale sensitivity analysis, parameter tuning, or general nonlinear optimization. They can be generated automatically by compilers. 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. We propose a proof technique that relies on data dependences in partitioned global address space versions of the adjoint message passing program. Assuming that the original program is deadlock-free and deterministic, the transformation rules can be shown to be correct in the sense that the automatically generated adjoint program exhibits the same properties 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.

Keywords: program transformation, automatic differentiation, inverse computation, MPI, message passing

Full text (pdf)


@inproceedings{Naumann2008AFf,
  author = {Naumann, U. and Hasco{\"e}t, L. and Hill, C. and Hovland, P. and Riehme, J. and Utke, J.},
  title = "A Framework for Proving Correctness of Adjoint Message-Passing Programs",
  booktitle = "Proceedings of the 15th European PVM/MPI Users' Group Meeting on Recent
         Advances in Parallel Virtual Machine and Message Passing Interface",
  isbn = "978-3-540-87474-4",
  pages = "316--321",
  location = "Dublin, Ireland",
  doi = "http://dx.doi.org/10.1007/978-3-540-87475-1_44",
  publisher = "Springer-Verlag, Berlin, Heidelberg",
  year = "2008"
}