Formal Verification of Parallel Prefix Sum

Mohsen Safari, Wytse Oortwijn, Sebastiaan J. C. Joosten, Marieke Huisman

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

3 Citations (Scopus)

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.
Original languageEnglish
Title of host publicationNASA Formal Methods - 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings
EditorsRitchie Lee, Susmit Jha, Anastasia Mavridou
PublisherSpringer Singapore
Pages170-186
Number of pages17
ISBN (Electronic)978-3-030-55754-6
ISBN (Print)978-3-030-55753-9
DOIs
Publication statusPublished - 10 Aug 2020
Event12th NASA Formal Methods Symposium, NFM 2020 - Virtual Conference
Duration: 11 May 202015 May 2020
Conference number: 12
https://ti.arc.nasa.gov/events/nfm-2020/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume12229

Conference

Conference12th NASA Formal Methods Symposium, NFM 2020
Abbreviated titleNFM 2020
Period11/05/2015/05/20
Internet address

Fingerprint Dive into the research topics of 'Formal Verification of Parallel Prefix Sum'. Together they form a unique fingerprint.

Cite this