Correctness is Demanding, Performance is Frustrating
Abstract
In this paper we demonstrate a technique for developing high performance applications with strong correctness guarantees. We use a theorem prover to derive a high-level specification of the application that includes correctness invariants of our choice. After that, within the same theorem prover, we implement an extraction of the specified application into a high-performance language of our choice. Concretely, we are using Agda to specify a framework for automatic differentiation (reverse mode) that is focused on index-safe tensors. This framework comes with an optimiser for tensor expressions and the ability to translate these expressions into SaC and C. We specify a canonical convolutional neural network within the proposed framework, compute the derivatives needed for the training phase and then demonstrate that the generated code matches the performance of hand-written code when running on a multi-core machine.
Cite
@article{arxiv.2406.10405,
title = {Correctness is Demanding, Performance is Frustrating},
author = {Artjoms Sinkarovs and Thomas Koopman and Sven-Bodo Scholz},
journal= {arXiv preprint arXiv:2406.10405},
year = {2024}
}