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.

Dynamically typed array languages such as Python, APL, and Matlab lift scalar operations to arrays and replicate scalars to fit applications. We present a mechanism for automatically inferring map and replicate operations in a statically-typed language in a way that resembles the programming experience of a dynamically-typed language while preserving the static typing guarantees. Our type system—which supports parametric polymorphism, higher-order functions, and top-level let-generalization—makes use of integer linear programming in order to find the minimum number of operations needed to elaborate to a well-typed program. We argue that the inference system provides useful and unsurprising guarantees to the programmer. We demonstrate important theoretical properties of the mechanism and report on the implementation of the mechanism in the statically-typed array programming language Futhark.

In many domains, large amounts of time series data are being collected and analyzed in a semi-automatic manner. A prominent approach is the seasonal and trend decomposition using locally estimated scatterplot smoothing (STL) technique, which has been applied extensively in the past. However, STL quickly becomes computationally very expensive when applied to large data sets. In this work, we propose the first parallel implementation for the STL decomposition approach, which is tailored to the specific needs of graphics processing units (GPU). Our experimental evaluation on two global-scale case studies in temperature and vegetation trend analysis exhibits at least three-to-four orders of magnitude speed-up, demonstrating the effectiveness of the overall approach and the immense potential of the implementation in spatio-temporal data analyses. The source code is publicly available at https://github.com/diku-dk/hastl. An artifact that allows the experimental results to be reproduced is available at https://sid.erda.dk/sharelink/hOUrqJJ FfA.