Correctness is Demanding, Performance is Frustrating
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929387195072512 |
|---|---|
| author | Sinkarovs, Artjoms Koopman, Thomas Scholz, Sven-Bodo |
| author_facet | Sinkarovs, Artjoms Koopman, Thomas Scholz, Sven-Bodo |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_10405 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Correctness is Demanding, Performance is Frustrating Sinkarovs, Artjoms Koopman, Thomas Scholz, Sven-Bodo Programming Languages 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. |
| title | Correctness is Demanding, Performance is Frustrating |
| topic | Programming Languages |
| url | https://arxiv.org/abs/2406.10405 |