Details

Данная работа посвящена применению метода проверки модели к задаче автонастройки параметров программ, исполняемых на графическом процессоре. В отличие от эмпирических автотюнеров и методов машинного обучения, формальная верификация позволяет искать оптимальные значения параметров запуска без доступа к целевому оборудованию и с формальными гарантиями оптимальности найденной конфигурации. Задачи, решённые в ходе работы: • Разработать формальные модели вычислительного конвейера GPU на языке PlusCal/TLA+ для двух классов вычислительных задач --- суммирования чётных элементов и поиска минимального элемента массива. • Разработать транслятор формальных моделей с языка Promela на язык PlusCal для возможности переиспользования существующих SPIN-моделей. • Подобрать оптимальные параметры автонастройки разработанных моделей с использованием верификаторов TLC и Apalache. • Провести анализ результатов трансляции и верификации. В результате работы разработаны две формальные модели вычислительного конвейера GPU (SUM и MIN), реализован транслятор подмножества Promela в подмножество PlusCal на C++17, проведено шесть вычислительных экспериментов с верификаторами TLC и Apalache. Оптимальные конфигурации, найденные двумя методами (прямой перебор и бисекция), полно- стью совпадают: для модели SUM --- (WG∗ , TS∗ ) = (4, 4) при минимальном времени T ∗ = 15 тактов модельного времени; для модели MIN --- (4, 2) при T ∗ = 10. Потенциал автонастройки составил 13 % для модели SUM и 60 % для MIN. Сопоставление с предшествующими исследованиями на платформе SPIN показало полное совпадение оптимальных конфигураций, что подтверждает корректность автоматической трансляции и эквивалентность платформ TLA+ и SPIN для рассматриваемого класса задач. Эмпирическая оценка символьного верификатора Apalache выявила границы его применимости для моделей с многочисленными параллельными процессами и многомерным состоянием: SMT-решатель Z3 возвращает UNKNOWN на глубине 32 шагов после часа работы, тогда как явный верификатор TLC выполняет полную верификацию за 9 секунд. Для достижения данных результатов в работе использовались следующие информационные технологии и программное обеспечение: язык спецификаций TLA+ и алгоритмический язык PlusCal; явный верификатор TLC (версия 2.19) из состава TLA+ Toolbox (версия 1.7.4); символьный верификатор Apalache (версия 0.57.1) с SMT-решателем Z3; язык моделирования Promela; генераторы лексических и синтаксических анализаторов flex и bison; язык C++ (стандарт C++17); система вёрстки LATEX для подготовки текста работы.

The work is devoted to applying the model checking method to the problem of autotuning parameters of programs executed on a graphics processing unit. In contrast to empirical autotuners and machine learning methods, formal verification allows searching for optimal parameter values without access to the target hardware, and provides formal guarantees of optimality of the found configuration. The research set the following goals: • To develop formal models of a GPU computational pipeline in the PlusCal/TLA+ language for two classes of computational tasks --- summation of even elements and search for the minimum element of an array. • To develop a translator of formal models from Promela to PlusCal for reuse of existing SPIN models. • To find optimal autotuning parameters for the developed models using the TLC and Apalache verifiers. • To analyse the results of translation and verification. As a result of the work, two formal models of a GPU computational pipeline (SUM and MIN) were developed, a translator of a Promela subset into a PlusCal subset was implemented in C++17, and six computational experiments with the TLC and Apalache verifiers were conducted. The optimal configurations found by the two methods (direct enumeration and bisection) coincide completely: for the SUM model --- (WG∗ , TS∗ ) = (4, 4) with the minimum execution time T ∗ = 15 ticks of model time; for the MIN model --- (4, 2) with T ∗ = 10. The autotuning potential amounted to 13 % for the SUM model and 60 % for MIN. Comparison with previous research on the SPIN platform showed complete agreement of the optimal configurations, which confirms the correctness of the automatic translation and the equivalence of the TLA+ and SPIN platforms for the considered class of problems. The empirical evaluation of the symbolic verifier Apalache revealed the limits of its applicability for models with many parallel processes and multidimensional state: the Z3 SMT solver returns UNKNOWN at depth 32 after one hour of running, whereas the explicit verifier TLC performs full verification in 9 seconds. To achieve these results, the following information technologies and software were used: the TLA+ specification language and the PlusCal algorithmic language; the explicit verifier TLC (version 2.19) from the TLA+ Toolbox (version 1.7.4); the symbolic verifier Apalache (version 0.57.1) with the Z3 SMT solver; the Promela modelling language; the lexical and syntactic analyser generators flex and bison; the C++ programming language (C++17 standard); the LATEX typesetting system for preparing the text of the work.