tgoop.com/plcomp/83
Last Update:
https://hal.archives-ouvertes.fr/hal-03000244/document
https://github.com/Ekdohibs/PolyGen
https://www.youtube.com/watch?v=MJ_NjnIqM38
Courant, Leroy, [2021] "Verified Code Generation for the Polyhedral Model"
Полиэдральная (называемая также политопной) модель используется в качестве промежуточного представления как для императивных вложенных циклов (другое название - "гнезда циклов", т.е. конструкции из императивных команд и for-образных циклов) так и декларативных матричных/тензорных DSL. Основная идея - рассматривать оптимизацию и параллелизацию итеративных вычислений как преобразования политопов (обобщение геометрического понятия многогранника на произвольное число измерений). Полиэдральный оптимизатор должен уметь конструировать полиэдральное представление из кода, производить собственно оптимизации и преобразовывать результат снова в код.
В статье рассматривается, конструируется и верифицируется только последняя часть этого процесса, т.е. верифицированный кодогенератор из уже оптимизированного полиэдрального IR, и только для последовательного кода. За основу взят алгоритм "сканирования полиэдров" из Bastoul, [2004] "Code generation in the polyhedral model is easier than you think", используемый в GCC. Для верификации использован Coq и гибридная OCaml/Coq библиотека верифицированных полиэдральных операций VPL. Примечательна она использованием "апостериорной" верификации - оптимизированные алгоритмы на Окамле вместе с результатом своей работы также выдают небольшие Farkas-сертификаты корректности, которые в свою очередь проверяются уже верифицированными функциями на Coq.
Как задаются полиэдральная модель и исходное представление? Делается упрощение, что все формулы, используемые в качестве индексов для массивов и граничных условий для циклов - аффинные выражения от переменных (однородные полиномы степени 1). Для каждой инструкции определяется политоп, внутри каждой точки которого она должна быть исполнена, дополнительно инструкции упорядочиваются при помощи так называемого расписания (schedule) выполнения. Оптимизация заключается в трансформации расписания с сохранением зависимостей по данным.
Исходное полиэдральное представление Poly параметризовано набором примитивных инструкций (присваивание, арифметические операции и т.д.), для которых задана абстрактная семантика а-ля Хоар - бинарные отношения состояний памяти до и после выполнения инструкции. Сама программа моделируется как набор четверок из итерируемой примитивной инструкции, ограничивающего политопа, функции расписания итерации и функции преобразования, вычисляющей индексы для инструкции - этот последний компонент для полиэдральных моделей нестандартен, обычно преобразования выполняются над самими инструкциями.
Сама кодогенерация разбивается на четыре прохода. Первым идет schedule elimination. Используется алгоритм из Bastoul [2004] - разворачивание расписания в политоп более высокой размерности, то есть, добавляются переменные, принимающие соответствующие значения функции расписания. Недостаток этого алгоритма именно в том, что за счет увеличения количества использованных переменных он замедляет последующую кодогенерацию.
Затем идёт abstract loop decomposition - генерирование циклов сканированием политопа по каждому измерению. Для этого взят алгоритм из Quillere, Rajopadhye, Wilde, [2000] "Generation of efficient nested loops from polyhedra". Используется дополнительное IR PolyLoop, где добавляются новые команды - guard и loop, транслируемые в конечном коде в динамические проверки и императивные циклы. Политоп "сканируется" методом Фурье-Моцкина (так как благодаря принятому ограничению для выражений достаточно арифметики Пресбургера) и раскладывается в комбинации вышеупомянутых команд. Важный момент на этом этапе - взаимное упорядочивание циклов, получаемых из нескольких политопов.
#codegen #coq #polyhedral #verification
BY PLComp
Share with your friend now:
tgoop.com/plcomp/83