Abstract:
In certain types of programs, re-ordering their execution can speed them up by optimizing memory accesses and parallelism. However, these re-orderings are constrained by the fact that updates depend on the results of earlier iterations. It is easy to generate and check the validity of simple re-orderings, but more complex cases are beyond the reach of existing tools. For these cases, programmers can hand-write the re-orderings, but we need to be able to automatically verify them to avoid programmer error. We propose two potential methods for verifying their correctness.