Formal Techniques for Development and Auto-tuning of Parallel Programs

The paper presents formal algebra-algorithmic models for parallel program design and auto-tuning aimed to achieve the highest degree of computation performance. Parallel programs are modeled in terms of high-level schemes represented in Glushkov’s system of algorithmic algebra and a concept of a transition system implemented in the term rewriting technique. The optimization techniques (the methods of asynchronous loop computations and choosing the optimal strategy of indexed data structures traversal) are proposed for auto-tuning. The evaluation of the performance impact of corresponding code transformations is given. The models of parallel program execution and auto-tuning are developed. As the structure and logic of tuned programs can be changed, an approach to verification of correctness of optimization transformations of parallel code performed by an auto-tuner is developed. In some partial cases, this validation can be automated and implemented by checking defined source code characteristics using rewriting rules framework, so correctness verification is reduced to checking equivalence by result property. The developed methods are demonstrated on the examples of optimization of parallel Brownian motion simulation and weather forecasting programs. The multiprocessor speedup for the Brownian motion simulation program was close to the theoretical limit, and the improvement of the overall execution time for the meteorological forecasting program exceeded 13%. The developed formal models and software methods are effective means of achieving the main goal of increasing the multiprocessor speedup of parallel programs as well as of verification of the correctness of the applied code transformations.