Abstract
Dedicated many-core processors such as GPGPUs, enable programmers to design and implement parallel algorithms to optimize performance. The stream compaction and summed-area table algorithms are two examples where parallel versions have been proposed in the literature with substantial speed ups compared to sequential counterparts.
Since these two algorithms are widely used, their correctness is of the utmost importance, i.e., the algorithms must be functionally correct and their implementations must be memory safe. These algorithms use the parallel prefix sum algorithm internally. In our previous work, we verified two parallel prefix sum algorithms. In this paper, we show how we can reuse a verified sub-function (i.e., prefix sum) to prove more complicated algorithms (i.e., stream compaction and summed area table) in a modular way with less effort. Moreover, we demonstrate that it is feasible in practice to verify larger case studies by building the verification of the complicated algorithm on top of the basic one.
To show the correctness of the algorithms, we use deductive program verification based on permission-based separation logic, which is supported by the program verifier VerCors. To the best of our knowledge, we are the first to verify functional correctness of the parallel stream compaction and summed-area table algorithms for an arbitrary array size, using tool support.
Since these two algorithms are widely used, their correctness is of the utmost importance, i.e., the algorithms must be functionally correct and their implementations must be memory safe. These algorithms use the parallel prefix sum algorithm internally. In our previous work, we verified two parallel prefix sum algorithms. In this paper, we show how we can reuse a verified sub-function (i.e., prefix sum) to prove more complicated algorithms (i.e., stream compaction and summed area table) in a modular way with less effort. Moreover, we demonstrate that it is feasible in practice to verify larger case studies by building the verification of the complicated algorithm on top of the basic one.
To show the correctness of the algorithms, we use deductive program verification based on permission-based separation logic, which is supported by the program verifier VerCors. To the best of our knowledge, we are the first to verify functional correctness of the parallel stream compaction and summed-area table algorithms for an arbitrary array size, using tool support.
| Original language | English |
|---|---|
| Title of host publication | Theoretical Aspects of Computing – ICTAC 2020 |
| Subtitle of host publication | 17th International Colloquium, Macau, China, November 30 – December 4, 2020, Proceedings |
| Editors | Violet Ka I Pun, Volker Stolz, Adenilso Simão |
| Place of Publication | Cham |
| Publisher | Springer |
| Pages | 181-199 |
| Number of pages | 19 |
| ISBN (Electronic) | 978-3-030-64276-1 |
| ISBN (Print) | 978-3-030-64275-4 |
| DOIs | |
| Publication status | Published - 25 Nov 2020 |
| Event | 17th International Colloquium on Theoretical Aspects of Computing, ICTAC 2020 - Virtual Conference, Macau, China Duration: 30 Nov 2020 → 4 Dec 2020 Conference number: 17 https://ictac2020.github.io/ |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 12545 |
| ISSN (Print) | 2512-2010 |
| ISSN (Electronic) | 2512-2029 |
Conference
| Conference | 17th International Colloquium on Theoretical Aspects of Computing, ICTAC 2020 |
|---|---|
| Abbreviated title | ICTAC 2020 |
| Country/Territory | China |
| City | Macau |
| Period | 30/11/20 → 4/12/20 |
| Internet address |
Keywords
- 22/2 OA procedure