Scalable Deductive Verification of Data-Level Parallel Programs
For developers of parallel programs (e.g., GPU kernels), this work reduces verification time and enables verification of larger programs, but the techniques are incremental improvements to existing deductive verification methods.
This paper improves the scalability of deductive verification for data-level parallel programs by introducing techniques for rewriting quantified expressions and reasoning about array aliasing. These techniques, implemented in the VerCors verifier, reduce verification time by an average factor of 9 (up to 150x) on GPU kernels and enable verification of previously unobtainable results.
This paper introduces several techniques that improve the scalability of the deductive verification of data-level programs working on arrays and matrices. First of all, we introduce a technique to rewrite expressions with (nested) quantifiers, so suitable triggers can be generated for these expressions. We have proven this rewrite technique correct in a theorem prover. Second, we make reasoning about potentially overlapping arrays easier, by providing specification constructs to indicate and verify that two arrays are not aliases, or that they are immutable, so they can be modelled as mathematical sequences. All our techniques are implemented in the VerCors program verifier. We illustrate how our techniques improve scalability through a large number of experiments. Using our techniques on a set of typical GPU kernels, we achieve a reduction of verification time by, on average, a factor of 9, with outliers being up to 150 times faster. Additionally, applying these techniques to earlier experiments and an earlier case study of a radio telescope pipeline permitted the verification of results which were previously unobtainable and significantly reduced the verification time.