Formal verification of parallel prefix sum and stream compaction algorithms in CUDA

Mohsen Safari*, Marieke Huisman

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

5 Citations (Scopus)
192 Downloads (Pure)

Abstract

GPUs are an important part of any High Performance Computing (HPC) architecture. To make optimal use of the specifics of a GPU architecture, we need programming models that naturally support the parallel execution model of a GPU. CUDA and OpenCL are two widely used examples of such programming models. Furthermore, we also need to redesign algorithms such that they adhere to this parallel programming model, and we need to be able to prove the correctness of these redesigned algorithms. In this paper we study two examples of such parallelized algorithms, and we discuss how to prove their correctness (data race freedom and (partial) functional correctness) using the VerCors program verifier. First of all, we prove the correctness of two parallel algorithms solving the prefix sum problem. Second, we show how such a prefix sum algorithm is used as a basic block in a stream compaction algorithm, and we prove correctness of this stream compaction algorithm, taking advantage of the earlier correctness proof for the prefix sum algorithm. The proofs as described in this paper are developed over the CUDA implementations of these algorithms. In earlier work, we had already shown correctness of a more high-level version of the algorithm. This paper discusses how we add support to reason about CUDA programs in VerCors, and it then shows how we can redo the verification at the level of the CUDA code. We also discuss some practical challenges that we had to address to prove correctness of the actual CUDA-level verifications.

Original languageEnglish
Pages (from-to)81-98
Number of pages18
JournalTheoretical computer science
Volume912
Early online date2 Mar 2022
DOIs
Publication statusPublished - 12 Apr 2022

Keywords

  • CUDA
  • Deductive verification
  • GPU verification
  • Prefix sum
  • Separation logic
  • Stream compaction
  • UT-Hybrid-D

Fingerprint

Dive into the research topics of 'Formal verification of parallel prefix sum and stream compaction algorithms in CUDA'. Together they form a unique fingerprint.

Cite this