Verifying Array Properties in Pure Data-Parallel Programs

In functional data-parallel programs, index array computations are separated (fissioned) into sequences of bulkparallel operators—map, prefix sum, scatter—and used to gather or scatter data array elements, thus determiningdata 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 userproofs, making them inaccessible to non-experts. We present a compiler approach to verifying array propertieswith high automation, aimed at making verification of data-parallel programs more accessible to users withoutverification expertise. We support a small but powerful predefined set of properties—equivalences, ranges,injectivity, bijectivity, monotonicity, filtering, partitioning—that enable the compiler to (automatically) reasonat 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 nestedparallel programs that are difficult to verify, such as batch operations on arrays of different sizes.