Formal Verification of Parallel Prefix Sum

Mohsen Safari; Wytse Oortwijn; Sebastiaan Joosten; Marieke Huisman

doi:10.1007/978-3-030-55754-6_10

Formal Verification of Parallel Prefix Sum

Mohsen Safari^*, Wytse Oortwijn, Sebastiaan Joosten, Marieke Huisman

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

14 Citations (Scopus)

141 Downloads (Pure)

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 language	English
Title of host publication	NASA Formal Methods
Subtitle of host publication	12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings
Editors	Ritchie Lee, Susmit Jha, Anastasia Mavridou
Place of Publication	Cham
Publisher	Springer
Pages	170-186
Number of pages	17
ISBN (Electronic)	978-3-030-55754-6
ISBN (Print)	978-3-030-55753-9
DOIs	https://doi.org/10.1007/978-3-030-55754-6_10
Publication status	Published - 10 Aug 2020
Event	12th NASA Formal Methods Symposium, NFM 2020 - Virtual Conference Duration: 11 May 2020 → 15 May 2020 Conference number: 12 https://ti.arc.nasa.gov/events/nfm-2020/

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	12229
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	12th NASA Formal Methods Symposium, NFM 2020
Abbreviated title	NFM 2020
Period	11/05/20 → 15/05/20
Internet address	https://ti.arc.nasa.gov/events/nfm-2020/

Keywords

22/2 OA procedure

Access to Document

10.1007/978-3-030-55754-6_10

ArticleFinal published version, 733 KBLicence: Taverne

Cite this

Safari, M., Oortwijn, W., Joosten, S., & Huisman, M. (2020). Formal Verification of Parallel Prefix Sum. In R. Lee, S. Jha, & A. Mavridou (Eds.), NASA Formal Methods: 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings (pp. 170-186). (Lecture Notes in Computer Science; Vol. 12229). Springer. https://doi.org/10.1007/978-3-030-55754-6_10

@inproceedings{2011650f435f423bac08f00933d628fe,

title = "Formal Verification of Parallel Prefix Sum",

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.",

keywords = "22/2 OA procedure",

author = "Mohsen Safari and Wytse Oortwijn and Sebastiaan Joosten and Marieke Huisman",

year = "2020",

month = aug,

day = "10",

doi = "10.1007/978-3-030-55754-6_10",

language = "English",

isbn = "978-3-030-55753-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "170--186",

editor = "Ritchie Lee and Susmit Jha and Anastasia Mavridou",

booktitle = "NASA Formal Methods",

address = "Germany",

note = "12th NASA Formal Methods Symposium, NFM 2020, NFM 2020 ; Conference date: 11-05-2020 Through 15-05-2020",

url = "https://ti.arc.nasa.gov/events/nfm-2020/",

}

Safari, M, Oortwijn, W, Joosten, S & Huisman, M 2020, Formal Verification of Parallel Prefix Sum. in R Lee, S Jha & A Mavridou (eds), NASA Formal Methods: 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings. Lecture Notes in Computer Science, vol. 12229, Springer, Cham, pp. 170-186, 12th NASA Formal Methods Symposium, NFM 2020, 11/05/20. https://doi.org/10.1007/978-3-030-55754-6_10

Formal Verification of Parallel Prefix Sum. / Safari, Mohsen; Oortwijn, Wytse; Joosten, Sebastiaan et al.
NASA Formal Methods: 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings. ed. / Ritchie Lee; Susmit Jha; Anastasia Mavridou. Cham: Springer, 2020. p. 170-186 (Lecture Notes in Computer Science; Vol. 12229).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Formal Verification of Parallel Prefix Sum

AU - Safari, Mohsen

AU - Oortwijn, Wytse

AU - Joosten, Sebastiaan

AU - Huisman, Marieke

N1 - Conference code: 12

PY - 2020/8/10

Y1 - 2020/8/10

N2 - 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.

AB - 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.

KW - 22/2 OA procedure

U2 - 10.1007/978-3-030-55754-6_10

DO - 10.1007/978-3-030-55754-6_10

M3 - Conference contribution

SN - 978-3-030-55753-9

T3 - Lecture Notes in Computer Science

SP - 170

EP - 186

BT - NASA Formal Methods

A2 - Lee, Ritchie

A2 - Jha, Susmit

A2 - Mavridou, Anastasia

PB - Springer

CY - Cham

T2 - 12th NASA Formal Methods Symposium, NFM 2020

Y2 - 11 May 2020 through 15 May 2020

ER -

Formal Verification of Parallel Prefix Sum

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this