for i in range(0, n):

b[i + 1] = g(a[i]);

a[i - 1] = f(b[i - 4]);

First, the synthesizer should figure out that the problem is under-constrained. It should report that the following values are undefined:

a[0..2] = ??

b[0] = ??

a[n] = ??

If, as suggested by the synthesizer, I refined the program to be consistent:

a[0..2] = 0

b[0] = 0

a[n] = 0

for i in range(0, n):

b[i + 1] = g(a[i]);

a[i - 1] = f(b[i - 4]);

I'd like to get:

a[0] = 0

a[1] = 0

a[2] = 0

b[0] = 0

b[1] = g(a[0])

b[2] = g(a[1])

b[3] = g(a[2])

for (int i = 3; i < n - 1; i++) {

a[i] = f(b[i - 3]);

b[i + 1] = g(a[i])

a[n] = 0

Note that the synthesizer performed loop peeling -- it figured out to do loop peeling to emit assignments for b[1], b[2], and b[3]. Furthermore, it reordered the assignments in the loop and performed loop skewing -- it changed the indices of the assignments, such as from a[i - 1] to a[i], to ensure an array value is written before it is read.

Milind and I just worked out most of the theory for this today. You can think of it as a generalization of attribute grammar synthesis to loop code. Basically, if we assume the input code is singly assigned -- array values should have one unique value -- this is a matter of unrolling the intermediate steps of the loop, scheduling their dependency graph, and reconstructing the Von Neumann-friendly loop. The weekend may be busy :)

A fun question is whether a functional program could declaratively handle the above. For example, it could expand the for loop into a dependency graph and then use demand-driven evaluation. However, there are two problems. First, the interpretation of indices would have to change: my code correctly skewed the loop indices to make sure "a[i - 1]" and "b[i - 4]" are never negative. Second, the loop would be unsafe: in my approach, the synthesizer can statically check that the array is fully defined. Either way, traditional functional languages force programmers to explicitly handle these (arguably) low-level loop details. Go synthesis!

## 2 comments:

Hello Leo,

This very much looks like Systems of Uniform Recurrence Equations (SUREs) from Karp, Miller and Winograd ("The Organizations of Computations for Uniform Recurrence Equations", 1967).

The questions of schedulability/liveness and parallelization are not at all trivial. I think that you may be interested in a survey paper from Alain Darte, "Understanding loops: the influence of the decomposition of Karp, Miller, and Winograd" (MEMOCODE 2010).

I'd be very interested if you tried to put this kind of data-flow-like ideas in FTL. Old languages, like Alpha, tried to leverage such principles, without much long-term success I guess.

Cool, looking forward to reading it :)

I agree that these ideas are old. This is pretty analogous to attribute grammar synthesis, which is essentially trying to find a triply-nested loop, and also came out of the same era :)

I think two big things have changed since the early days. First, our understanding of loops -- e.g., the polyhedral model -- has improved. That means we can ask powerful questions about concrete code instances and transformations. Second, our ability to synthesize -- search over code -- has improved, both due to hardware and algorithm (e.g., SAT/SMT) advances. In this case, we can flip a polyhedral loop transform checker into a polyhedral code synthesizer, among other things. These are significant: the best paper from PLDI last year, if you dig to work from the 60s on SETL, is actually fairly similar situation.

Thanks again!

Post a Comment