The parallelization of sequential programs is a tedious and error-prone task; the incorrect use of synchronization primitives may yield a program that produces different results than the original code, or even different results in different runs. This paper proposes an alternative approach that borrows concepts from program verification to generate a parallel program guaranteed to produce the same result as the sequential version.

The core idea is that, in addition to potential parallelization points, the programmer provides a specification of the sequential program behavior and a proof (an annotation of the program with crucial assertions) that the program meets this specification. The specification is expressed in a class of separation logic formulas called symbolic heaps, which describe both logical conditions and the shape of data structures, and, in particular, which parts of the data do not overlap. From this and the proof, a symbolic analysis determines program points where synchronization primitives are to be inserted, based on various inference queries supported by automated separation logic provers.

The paper introduces the technique for the more casual reader using examples. The main part then provides the technical background for the expert, in particular the details of the analysis and the proof of its soundness. The paper demonstrates in a fascinating fashion how automated proving techniques find their way into compilation technology. Thus, the task of the programmer may gradually shift from writing low-level code to providing high-level specifications.