Mechanical certification of systolic algorithms (Q1123588)

The common practice in designing systolic algorithms is to finish with a description of interconnection network, flows of data and behaviour of every processing element. The proof of the correctness of the result is usually omitted. The problem of proving correctness of algorithms amounts to proving that the correct data arrives at the correct place at the correct time so as to produce the expected result. The paper reviewed presents one possible approach to accomplish it using Boyer-Moore theorem power (see \textit{R. S. Boyer} and \textit{J. S. Moore} [A computational logic (Academic Press, New York) (1979; Zbl 0448.68020)]). Particularly, the authors propose the methodology involving the following steps i) uncover recurrence equations from presentations (i.e. from functions that define the functionality of the processing elements and the communication paths), ii) solve the recurrence equations using input schedules as initial conditions to obtain a closed form solution (i.e. to find the values on all the input ports and accumulators in terms of the data fed from the external world), iii) prove that the array meets the output schedule from the closed form solution and they show how to carry out the second and the third steps using Boyer-Moore theorem prover. The whole process is explained in details by proving correctness of a systolic algorithm for a dynamic programming problem.