Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms

Mohsen Safari, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computing - ICTAC 2020 - 17th International Colloquium, Macau, China, November 30 - December 4, 2020, Proceedings
EditorsViolet Ka I Pun, Volker Stolz, Adenilso Simão
PublisherSpringer Singapore
Pages181-199
Number of pages19
ISBN (Electronic)978-3-030-64276-1
ISBN (Print)978-3-030-64275-4
DOIs
Publication statusPublished - 25 Nov 2020
Event17th International Colloquium on Theoretical Aspects of Computing, ICTAC 2020 - Virtual Conference, Macau, China
Duration: 30 Nov 20204 Dec 2020
Conference number: 17
https://ictac2020.github.io/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12545

Conference

Conference17th International Colloquium on Theoretical Aspects of Computing, ICTAC 2020
Abbreviated titleICTAC 2020
CountryChina
CityMacau
Period30/11/204/12/20
Internet address

Fingerprint Dive into the research topics of 'Formal Verification of Parallel Stream Compaction and Summed-Area Table Algorithms'. Together they form a unique fingerprint.

Cite this