Authors

Abstract

The accompanying poster to this short paper presents acombination of reverse mode AD and formal methods to enable efficient differentiation of (or backpropagation through)shared-memory parallel code. Compared to the state of theart, our approach can more often avoid the need for atomicupdates or private data copies during the parallel derivative computation, even in the presence of unstructured ordata-dependent data access patterns. This is achieved bygathering information about the memory access patternsfrom the input program, which is assumed to be correctlyparallelized. This information is then used to build a model ofassertions in a theorem prover, which can be used to checkthe safety of shared memory accesses during the parallelderivative computation