Mostly Automated Formal Verification of Loop Dependencies with Applications to Distributed Stencil Algorithms

The class of stencil programs involves repeatedly updating elements of arrays according to fixed patterns, referred to as stencils. Stencil problems are ubiquitous in scientific computing and are used as an ingredient to solve more involved problems. Their high regularity allows massive parallelizat...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2019-02, Vol.62 (2), p.193-213
Main Authors: Grégoire, Thomas, Chlipala, Adam
Format: Article
Language:English
Subjects:
Algorithms
Artificial Intelligence
Automation
Computer Science
Dependence
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Nested loops
Parallel processing
Programming languages
Robustness (mathematics)
State of the art
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The class of stencil programs involves repeatedly updating elements of arrays according to fixed patterns, referred to as stencils. Stencil problems are ubiquitous in scientific computing and are used as an ingredient to solve more involved problems. Their high regularity allows massive parallelization. Two important challenges in designing such algorithms are cache efficiency and minimizing the number of communication steps between nodes. In this paper, we introduce a mathematical framework for a crucial aspect of formal verification of both sequential and distributed stencil algorithms, and we describe its Coq implementation. We present a domain-specific embedded programming language with support for automating the most tedious steps of proofs that nested loops respect dependencies, applicable to sequential and distributed examples. Finally, we evaluate the robustness of our library by proving the dependency-correctness of some real-world stencil algorithms, including a state-of-the-art cache-oblivious sequential algorithm, as well as two optimized distributed kernels.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-018-9451-y