Tue 19 Jun 2018 15:10 - 15:45 at Grand Ballroom C - Types and Correctness

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 Jun

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:45
Types and CorrectnessARRAY at Grand Ballroom C
14:00
35m
Talk
Parallel Programming with Arrays in Kappa 
ARRAY
Beatrice Åkerblom Stockholm University, Elias Castegren Uppsala University, Tobias Wrigstad Uppsala University
14:35
35m
Talk
Rank Polymorphism Viewed as a Constraint Problem
ARRAY
Justin Slepak Northeastern University, Panagiotis Manolios Northeastern University, Olin Shivers Northeastern University, USA
15:10
35m
Talk
Proving a Core Code for FDM Correct by 2 + dw Tests
ARRAY
Magne Haveraaen University of Bergen, Norway