Creative Commons Attribution 4.0 license (CC BY 4.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.24
URN: urn:nbn:de:0030-drops-167333
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16733/
Lammich, Peter
Refinement of Parallel Algorithms down to LLVM
| pdf-format: |
|
Abstract
We present a stepwise refinement approach to develop verified parallel algorithms, down to efficient LLVM code. The resulting algorithms' performance is competitive with their counterparts implemented in C/C++. Our approach is backwards compatible with the Isabelle Refinement Framework, such that existing sequential formalizations can easily be adapted or re-used. As case study, we verify a parallel quicksort algorithm, and show that it performs on par with its C++ implementation, and is competitive to state-of-the-art parallel sorting algorithms.
BibTeX - Entry
@InProceedings{lammich:LIPIcs.ITP.2022.24,
author = {Lammich, Peter},
title = {{Refinement of Parallel Algorithms down to LLVM}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {24:1--24:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16733},
URN = {urn:nbn:de:0030-drops-167333},
doi = {10.4230/LIPIcs.ITP.2022.24},
annote = {Keywords: Isabelle, Concurrent Separation Logic, Parallel Sorting, LLVM}
}
| Keywords: | Isabelle, Concurrent Separation Logic, Parallel Sorting, LLVM | |
| Seminar: | 13th International Conference on Interactive Theorem Proving (ITP 2022) | |
| Issue date: | 2022 | |
| Date of publication: | 03.08.2022 | |
| Supplementary Material: | Software (Isabelle Formalization): https://www21.in.tum.de/~lammich/isabelle_llvm_par/ |
