Symbolic Computation Group

David R. Cheriton School of Computer Science
University of Waterloo, Waterloo, Ontario, Canada

Friday, June 12, 2026, at the University of Waterloo
Lifting Compiler Reasoning via Data-Parallel Operators
Cosmin Oancea, Associate Professor, DIKU, University of Copenhagen

Abstract:

High-level data-parallel languages typically organize the computation as a nested composition of second-order array combinators, such as map, reduce, prefix sum, scatter (parallel write). The thesis is that the richer semantics of these combinators enables raising the level of abstraction at which the compiler reasons, yielding simpler, more scalable or more effective program analysis and transformation.

This talk demonstrates this hypothesis for several instance analyses integrated in the Futhark compiler. We present a solution to the challenging problem of reverse-mode automatic differentiation (R-AD), which is rooted in two key ideas: (1) By differentiating parallel constructs using specialized rules built on their richer semantics, we generate code that is often significantly more efficient in both space and time than low-level alternatives. (2) We address the parallel bottlenecks associated with the use of "tape" in traditional R-AD systems by eliminating the tape entirely through strategic scope-level re-execution. Our technique preserves work asymptotics, unlocks aggressive optimizations, and enables straightforward navigation of space-time tradeoffs via loop stripmining or flattening nested parallelism.

As time permits, the talk will highlight recent and ongoing work on (i) verifying properties of index arrays, in a way that is more accessible to non-experts than related solutions, and (ii) using scheduling languages to allow non-expert users to guide the compiler in the process of aggressive optimization of performance-critical computations.

 

Last modified on Friday, 05 June 2026, at 20:18 hours.