tr-announce April 2008

tr-announce@lists.rwth-aachen.de

1 participants
1 discussions

2008-06: A Framework for Proving Correctness of Adjoint Message Passing Programs

by Peter Schneider-Kamp

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.

16 years, 5 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce April 2008