FEVS: A Functional Equivalence Verification Suite for High-Performance Scientific Computing |
| |
Authors: | Stephen F Siegel Timothy K Zirkel |
| |
Institution: | (1) 11 Dubiel Drive, Worcester, Massachusetts 01609, USA;(2) 79 Kenwood Ave, Newton, Massachusetts 02459, USA;(3) 15737 Cadoz Drive, Austin, Texas 78728, USA;(4) Kineret St. 14/16, 44201 Kfar-Saba, Israel |
| |
Abstract: | Scientific computing poses many challenges to formal verification, including the facts that typical programs: (1) are numerically-intensive,
(2) are highly-optimized (often by hand), and (3) often employ parallelism in complex ways. Another challenge is specifying
correctness. One approach is to provide a very simple, sequential version of an algorithm together with the optimized (possibly
parallel) version. The goal is to show the two versions are functionally equivalent, or provide useful feedback when they
are not. We present a new verification suite consisting of pairs of programs of this form. The suite can be used to evaluate
and compare tools that verify functional equivalence. The programs are all in C and the parallel versions use the Message
Passing Interface. They are simpler than codes used in practice, but are representative of real coding patterns (e.g., manager-worker
parallelism, loop tiling) and present realistic challenges to current verification tools. The suite includes solvers for the
1-d and 2-d diffusion equations, Jacobi iteration schemes, Gaussian elimination, and N-body simulation. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|