Formal verification of parallel prefix sum
Authors:
- Safari, Mohsen
- Oortwijn, Wytse
- Joosten, Sebastiaan
- Huisman, Marieke
Published in: NASA Formal Methods Symposium pp 170–186
Abstract:
With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.
In this paper, we use deductive program verification based on permission-based separation logic, as supported by VerCors, to show correctness of the two most frequently used parallel in-place prefix sum algorithms for an arbitrary array size. Interestingly, the correctness proof for the second algorithm reuses the auxiliary lemmas that we needed to create the first proof. To the best of our knowledge, this paper is the first tool-supported verification of functional correctness of the two parallel in-place prefix sum algorithms which does not make any assumption about the size of the input array.
BibTeX entry:
@inproceedings{Safari20,
abstract = {With the advent of dedicated hardware for multicore programming, parallel algorithms have become omnipresent. For example, various algorithms have been proposed for the parallel computation of a prefix sum in the literature. As the prefix sum is a basic building block for many other multicore algorithms, such as sorting, its correctness is of utmost importance. This means, the algorithm should be functionally correct, and the implementation should be thread and memory safe.
In this paper, we use deductive program verification based on permission-based separation logic, as supported by VerCors, to show correctness of the two most frequently used parallel in-place prefix sum algorithms for an arbitrary array size. Interestingly, the correctness proof for the second algorithm reuses the auxiliary lemmas that we needed to create the first proof. To the best of our knowledge, this paper is the first tool-supported verification of functional correctness of the two parallel in-place prefix sum algorithms which does not make any assumption about the size of the input array.},
author = {Safari, Mohsen and Oortwijn, Wytse and Joosten, Sebastiaan and Huisman, Marieke},
bdsk-url-1 = {https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/465636/Safari2020_Chapter_FormalVerificationOfParallelPr.pdf?sequence=4},
booktitle = {NASA Formal Methods Symposium},
date-added = {2021-09-18 14:47:12 -0400},
date-modified = {2021-09-18 15:28:09 -0400},
month = {Aug},
organization = {Springer, Cham},
pages = {170--186},
title = {Formal verification of parallel prefix sum},
url = {https://www.research-collection.ethz.ch/bitstream/handle/20.500.11850/465636/Safari2020_Chapter_FormalVerificationOfParallelPr.pdf?sequence=4},
year = {2020}
}