Про аналіз коректності автотьюнінгу програм з використанням техніки переписувальних правил

Abstract

У роботі запропоновано підхід до перевірки коректності оптимізаційних перетворень паралельних програм, що виконуються автотьюнером. Автотьюнер розглядається як еволюційна дискретна динамічна система й перевірка коректності зводиться до перевірки властивості еквівалентності за результатом представлень вихідної і оптимізованої версій програм у формальній моделі автотьюнінгу. Цю перевірку у часткових випадках можна виконати автоматично за вихідним кодом за допомогою техніки переписувальних правил.

В работе представлен подход к проверке корректности оптимизационных преобразований параллельных программ, выполняемых автотьюнером. Автотьюнер рассматривается как эволюционная дискретная динамическая система, а проверка корректности сводится к проверке свойству эквивалентности по результату интерпретаций исходной и оптимизированной программ в формальной модели автотьюнинга. Эту проверку в частных случаях можно выполнять автоматически по исходному коду программы с помощью техники переписывающих правил.

Article presents an approach to correctness validation of autotuning optimizational transformations. Autotuner is considered as dynamic discrete system and validation is reduced to verification of characteristic of equivalence by result of representation of initial and optimized program versions in autotuning formal model. In partial cases this validation can be done automatically using source code and rewriting rules technique.