Automatic differentiation of parallel loops with formal methods
| Autor: | Jan Hückelheim, Laurent Hascoët |
|---|---|
| Přispěvatelé: | Mathematics and Computer Science Division [ANL] (MCS), Argonne National Laboratory [Lemont] (ANL), Transformations et outils informatiques pour le calcul scientifique (Ecuador), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) |
| Jazyk: | angličtina |
| Rok vydání: | 2022 |
| Předmět: | |
| Zdroj: | PPoPP 2022 / 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming PPoPP 2022 / 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, Apr 2022, Seoul, South Korea. ACM, pp.463-464, ⟨10.1145/3503221.3508442⟩ ICPP 2022-51st International Conference on Parallel Processing ICPP 2022-51st International Conference on Parallel Processing, Aug 2022, Bordeaux, France. ⟨10.1145/3545008.3545089⟩ |
| DOI: | 10.1145/3503221.3508442⟩ |
| Popis: | International audience; This paper presents a novel combination of reverse mode automatic differentiation and formal methods, to enable efficient differentiation of (or backpropagation through) shared-memory parallel loops. Compared to the state of the art, our approach can reduce the need for atomic updates or private data copies during the parallel derivative computation, even in the presence of unstructured or data-dependent data access patterns. This is achieved by gathering information about the memory access patterns from the input program, which is assumed to be correctly parallelized. This information is then used to build a model of assertions in a theorem prover, which can be used to check the safety of shared memory accesses during the parallel derivative loops. We demonstrate this approach on scientific computing benchmarks including a lattice-Boltzmann method (LBM) solver from the Parboil benchmark suite and a Green's function Monte Carlo (GFMC) kernel from the CORAL benchmark suite. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|