Strategy Preserving Compilation for Parallel Functional Code

TL;DR

This paper introduces a formally verified translation method from high-level functional code to low-level imperative code for parallel hardware, ensuring correctness and performance portability across GPUs and CPUs.

Contribution

It presents a formal, correctness-guaranteed translation strategy from functional to imperative code, addressing performance portability and preserving parallelization strategies.

Findings

Generated code achieves performance comparable to ad hoc methods.

Translation preserves parallelization strategies and is proven correct.

Applicable to GPUs and multicore CPUs.

Abstract

Graphics Processing Units (GPUs) and other parallel devices are widely available and have the potential for accelerating a wide class of algorithms. However, expert programming skills are required to achieving maximum performance. hese devices expose low-level hardware details through imperative programming interfaces where programmers explicity encode device-specific optimisation strategies. This inevitably results in non-performance-portable programs delivering suboptimal performance on other devices. Functional programming models have recently seen a renaissance in the systems community as they offer possible solutions for tackling the performance portability challenge. Recent work has shown how to automatically choose high-performance parallelisation strategies for a wide range of hardware architectures encoded in a functional representation. However, the translation of such functional representations to the imperative program expected by the hardware interface is typically performed ad hoc with no correctness guarantees and no guarantees to preserve the intended parallelisation strategy. In this paper, we present a formalised strategy-preserving translation from high-level functional code to low-level data race free parallel imperative code. This translation is formulated and proved correct within a language we call Data Parallel Idealised Algol (DPIA), a dialect of Reynolds' Idealised Algol. Performance results on GPUs and a multicore CPU show that the formalised translation process generates low-level code with performance on a par with code generated from ad hoc approaches.