Proving a Core Code for FDM Correct by 2 + dw Tests
Software correctness in general is a hard problem, and especially so for high performance computing (HPC). One problem being that array layout and traversal may depend on array size and hardware properties (cache size, core count, etc), making verification almost specific to every execution of the software. Can one of the reasons for the difficulties be that we are focussing too much on specific instances and low level detail, and not enough on abstraction and generic code? There exists several meta-theorems for generic code, one promising correctness by testing of minimal data sets, another free theorems.
Here we present three generic array algorithms which can form the core when implementing explicit solvers for finite difference methods (FDM). Knowing the size for the computational grid, the first two generic algorithms requires one test each to ensure correctness. The third requires $dw$ tests, where $d$ is the number of dimensions, e.g., 3, and $w$ is the width of the difference operator, e.g., 3 or 5. This verification is fast enough to be an integral part of a simulation run, which typically will have hundreds of calls with these parameter combinations.
Generic implementations also provide free theorems, which gives rise to optimisation rules for the FDM code.
We illustrate this on a 3D Burgers’ solver using these generic core codes implemented for CPU and GPU.
Tue 19 JunDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:45 | |||
14:00 35mTalk | Parallel Programming with Arrays in Kappa ARRAY Beatrice Åkerblom Stockholm University, Elias Castegren Uppsala University, Tobias Wrigstad Uppsala University | ||
14:35 35mTalk | Rank Polymorphism Viewed as a Constraint Problem ARRAY Justin Slepak Northeastern University, Panagiotis Manolios Northeastern University, Olin Shivers Northeastern University, USA | ||
15:10 35mTalk | Proving a Core Code for FDM Correct by 2 + dw Tests ARRAY Magne Haveraaen University of Bergen, Norway |