Logical Inference Techniques for Loop Parallelization

This paper presents a fully automatic approach to loop paralleliza-tion that integrates the use of static and run-time analysis and thus overcomes many known difficulties such as nonlinear and indi-rect array indexing and complex control flow. Our hybrid analysis framework validates the parallelization transformation by verify-ing the independence of the loop’s memory references. To this end it represents array references using the USR (uniform set repre-sentation) language and expresses the independence condition as an equation, S = ∅, where S is a set expression representing ar-ray indexes. Using a language instead of an array-abstraction rep-resentation for S results in a smaller number of conservative ap-proximations but exhibits a potentially-high runtime cost. To alle-viate this cost we introduce a language translation F from the USR set-expression language to an equally rich language of predicates (F(S) ⇒ S = ∅). Loop parallelization is then validated using a novel logic inference algorithm that factorizes the obtained com-plex predicates (F(S)) into a sequence of sufficient-independence conditions that are evaluated first statically and, when needed, dy-namically, in increasing order of their estimated complexities. We evaluate our automated solution on 26 benchmarks from PERFECT-CLUB and SPEC suites and show that our approach is effective in parallelizing large, complex loops and obtains much better full pro-gram speedups than the Intel and IBM Fortran compilers