Статьи по современным легковесным методам порождения кода
Destination-Driven Code Generation
https://pdfs.semanticscholar.org/dcb8/8719880e1f76ad71fb1c5aebb118e2ecfe71.pdf
One-pass Code Generation in V8
https://github.com/eatonphil/one-pass-code-generation-in-v8/blob/master/One-pass%20Code%20Generation%20in%20V8.pdf
HotpathVM: An Effective JIT Compiler for Resource-constrained Devices
https://static.usenix.org/events/vee06/full_papers/p144-gal.pdf
#codegen
Destination-Driven Code Generation
https://pdfs.semanticscholar.org/dcb8/8719880e1f76ad71fb1c5aebb118e2ecfe71.pdf
One-pass Code Generation in V8
https://github.com/eatonphil/one-pass-code-generation-in-v8/blob/master/One-pass%20Code%20Generation%20in%20V8.pdf
HotpathVM: An Effective JIT Compiler for Resource-constrained Devices
https://static.usenix.org/events/vee06/full_papers/p144-gal.pdf
#codegen
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
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
👍18
За этим следует оптимизационный шаг constraint elimination. Предыдущий проход, декомпозиция, создает большое количество избыточных guard-команд, что упрощает верификацию алгоритма, но снижает быстродействие получаемого кода, поэтому данный этап нацелен на их стирание. Тут используется еще одно IR - PolyLoopSimpl, куда добавлен примитив simplify, минимизирующий политоп по заданному ограничению.
Последний шаг - трансляция программы в AST Loop, состоящее из классических команд типа if и for, которое и является результатом работы кодогенератора. Основная задача на этом этапе - трансляция loop-команд.
Полученный кодогенератор (фактически, аналог CLooG) может быть экстрагирован в Окамл и позволяет получать модели императивных программ из полиэдрального представления, впрочем, работающего фронтенда у него нет, так что представления нужно расписывать вручную.
Формализация на Coq (около 8 тысяч строк) потребовала реализовать небольшую библиотеку для линейной алгебры, операции для работы над политопами, а также описать семантику промежуточных представлений и доказать соответствующие теоремы о корректности трансляции в Loop. Как правило, верификация компиляторных проходов делается либо через доказательства сохранения семантики, либо методом валидации трансляции. В статье использована их комбинация - валидация для полиэдральных операций и доказательства для семантик всех проходов кодогенератора. Здесь заметно, что статья является продолжением линии французских работ по (в том числе верифицированным) полиэдральным методам - дается ряд ссылок на предшественников.
В заключении дан обзор методов полиэдральной кодогенерации, упомянуты применения для верификации нейросетей. Также сообщается о найденной потенциальной ошибке, связанной с упорядочиванием трёх и более политопов в алгоритме генерации циклов Quillere [2000]. Авторы выражают желание в будущем заняться верификацией непосредственно оптимизаций и реализовать генерацию С кода из Loop AST, как шаг к добавлению полиэдрального оптимизатора в CompCert. Основная потенциальная проблема - переход от арифметики произвольной точности к операциям с переполнениям.
#codegen #coq #polyhedral #verification
Последний шаг - трансляция программы в AST Loop, состоящее из классических команд типа if и for, которое и является результатом работы кодогенератора. Основная задача на этом этапе - трансляция loop-команд.
Полученный кодогенератор (фактически, аналог CLooG) может быть экстрагирован в Окамл и позволяет получать модели императивных программ из полиэдрального представления, впрочем, работающего фронтенда у него нет, так что представления нужно расписывать вручную.
Формализация на Coq (около 8 тысяч строк) потребовала реализовать небольшую библиотеку для линейной алгебры, операции для работы над политопами, а также описать семантику промежуточных представлений и доказать соответствующие теоремы о корректности трансляции в Loop. Как правило, верификация компиляторных проходов делается либо через доказательства сохранения семантики, либо методом валидации трансляции. В статье использована их комбинация - валидация для полиэдральных операций и доказательства для семантик всех проходов кодогенератора. Здесь заметно, что статья является продолжением линии французских работ по (в том числе верифицированным) полиэдральным методам - дается ряд ссылок на предшественников.
В заключении дан обзор методов полиэдральной кодогенерации, упомянуты применения для верификации нейросетей. Также сообщается о найденной потенциальной ошибке, связанной с упорядочиванием трёх и более политопов в алгоритме генерации циклов Quillere [2000]. Авторы выражают желание в будущем заняться верификацией непосредственно оптимизаций и реализовать генерацию С кода из Loop AST, как шаг к добавлению полиэдрального оптимизатора в CompCert. Основная потенциальная проблема - переход от арифметики произвольной точности к операциям с переполнениям.
#codegen #coq #polyhedral #verification
👍19