Automatic Data Dependence Analysis by Deductive Verification

Parallelization of programs is of essence in the high-performance computing (HPC) area. But parallelization is only correct if certain data dependences can be reliably excluded, for example, read-after-write dependences, where a read access occurs as the subsequent access on a data element after a write access. Data dependence analyses should not merely be correct, but as precise as possible, so as not to miss any opportunity for parallelization. Various dynamic and static analyses were proposed in the HPC community, but, until recently, none based on program logic and deductive verification, even though the latter approach has important advantages, including soundness, precision, and modularity. Previously a proof-of-concept was given that fully automatic dependence analysis based on deductive verification is possible, but it suffered from limitations that rendered it impractical: the restriction to one-dimensional arrays and flat loops and, importantly, it does not differentiate between inter- and intra-iteration data dependences, which often results in a loss of precision. In this paper we lift all three limitations and show that a deductive approach is a competitive alternative to the kinds of dependence analyses used hitherto in HPC. Our axiomatization in a deduction system constitutes the first formalization of the semantics of inter-iteration dependence.