Verifying Array Properties in Pure Data-Parallel Programs

In functional data-parallel programs, index array computations are separated into sequences of bulk-parallel operators—map, prefix sum, scatter—and used to gather or scatter data array elements, thus determining data array properties. This programming style is problematic for general-purpose verification frameworks (e.g., Dafny, F*, Liquid Haskell), which are flexible and powerful, but require verbose annotations and non-trivial user proofs, making them inaccessible to non-experts. We present a compiler approach to verifying array properties with high automation, aimed at making verification of data-parallel programs more accessible to users without verification expertise. We support a small but powerful predefined set of properties—equivalence, range, injectivity, bijectivity, monotonicity, filtering, partitioning—that enable the compiler to (automatically) reason at a higher level of abstraction. We evaluate our approach on challenging applications with non-linear indexing, including graph algorithms, Cooley-Tukey FFT, filtering, multi-way partitioning, and flattened irregular nested parallel programs that are difficult to verify, such as batch operations on arrays of different sizes.