A Proof Theory for Loop-Parallelizing Transformations

Abstract

The microprocessor industry has embraced multicore architectures as the new dominant design paradigm. Harnessing the full power of such computers requires writing multithreaded programs, but regardless of whether one is writing a program from scratch or porting an existing single-threaded program, concurrency is hard to implement correctly and often reduces the legibility and maintainability of the source code. Single-threaded programs are easier to write, understand, and verify.

Parallelizing compilers offer one solution by automatically transforming sequential programs into parallel programs. Assisting the programmer with challenging tasks like this (or other optimizations), however, causes compilers to be highly complex. This leads to bugs that add unexpected behaviors to compiled programs in ways that are very difficult to test. Formal compiler verification adds a rigorous mathematical proof of correctness to a compiler, which provides high assurance that successfully compiled programs preserve the behaviors of the source program such that bugs are not introduced. However, no parallelizing compiler has been formally verified.

We lay the groundwork for verified parallelizing compilers by developing a general theory to prove the soundness of parallelizing transformations. Using this theory, we prove the soundness of a framework of small, generic transformations that compose together to build optimizations that are correct by construction. We demonstrate it by implementing several classic and cutting-edge loop-parallelizing optimizations: DOALL, DOACROSS, and Decoupled Software Pipelining. Two of our main contributions are the development and proof of a general parallelizing transformation and a transformation that coinductively folds a transformation over a potentially nonterminating loop, which we compose together to parallelize loops. Our third contribution is an exploration of the theory behind the correctness of parallelization, where we consider the preservation of nondeterminism and develop bisimulation-based proof techniques. Our proofs have been mechanically checked by the Coq Proof Assistant.