Solving Time-Partition Constraints by Farkas' Lemma
Introduction: Since time-partition constraints are similar to space-partition constraints, can we use a similar algorithm to solve them? Unfortunately, the slight difference between the two problems translates into a big technical difference between the two solution methods. Algorithm (Finding a highest-ranked synchronization-free affine partition for a program.) simply solves for C i , c i , C2 , and c2, such that for all ii in Zdl and i2 in Zd2 if
F i i i fi = F 2 i 2 f2
C i i i 4- ci = C 2 i 2 4- c 2 .
The linear inequalities due to the loop bounds are only used in determining if two references share data dependence, and are not used otherwise. To find solutions to the time-partition constraints, we cannot ignore the linear inequalities i -< i'; ignoring them often would allow only the trivial solution of placing all iterations in the same partition. Thus, the algorithm to find solutions to the time-partition constraints must handle both equalities and inequalities.
The general problem we wish to solve is: given a matrix A, find a vector c such that for all vectors x such that Ax > 0, it is the case that c T x > 0. In other words, we are seeking c such that the inner product of c and any coordinates in the polyhedron defined by the inequalities Ax > 0 always yields a nonnegative answer.
This problem is addressed by Farkas' Lemma. Let A be an m x n matrix of reals, and let c be a real, nonzero n-vector. Farkas' lemma says that either the primal system of inequalities
Ax > 0, cT x < 0
has a real-valued solution x, or the dual system
A T y = c, y > 0
has a real-valued solution y, but never both.
The dual system can be handled by using Fourier-Motzk in elimination to project away the variables of y. For each c that has a solution in the dual system, the lemma guarantees that there are no solutions to the primal system. Put another way, we can prove the negation of the primal system, i.e., we can prove that c T x > 0 for all x such that Ax > 0, by finding a solution y to the dual system: A T y = c and y > 0.
Algorithm: Finding a set of legal, maximally independent affine time partition mappings for an outer sequential loop.
INPUT: A loop nest with array accesses.
OUTPUT: A maximal set of linearly independent time-partition mappings.
METHOD: The following steps constitute the algorithm:
1. Find all data-dependent pairs of accesses in a program.
2. For each pair of data-dependent accesses, T\ = ( F i , f i , B i , b i ) in statement si nested in d\ loops and T2 — (F2 , f2, B 2 , b 2 ) in statement s2 nested in d2 loops, let (Ci,Ci) and (C2 , c 2 ) be the (unknown) time-partition mappings of statements si and s 2 , respectively. Recall the time-partition constraints state that
For all ii in Zdl and i2 in Zd2 such that
a) ii - < s i s 2 h,
b) B J i b i > 0,
c) B 2 i 2 b2 > 0, and
d) d ) F 1 i 1 f 1 = F 2 i 2 f 2,
it is the case that C i i i ci < C2 i 2 c 2 .