Тем не менее несколько моментов вызывают вопросы, если не к подходу в целом, то к его реализации в JastAdd.
Во-первых, как упоминалось ранее, отношения (Relations) задаются "внешним" по отношению к дереву образом, и авторы для этого используют обычный императивный код на Java, да ещё и опирающийся на неявные, генерируемые фреймворком методы. Мне такой способ не кажется декларативным и особо высокоуровневым.
Во-вторых, несмотря на то, что дерево разбора превращается в направленный граф общего вида, возможность реализации Control Flow Analysis и Data Flow Analysis остаётся под вопросом. Возможно, этому мешают ограничения на неизменяемость графа, связанные с мемоизацией (в свою очередь, необходимой для эффективной работы алгоритмов). В частности, это накладывает ограничения на построение отношений между "обычными" и узлами в NTA.
В любом случае, для прояснения деталей предлагаемого подхода читателю предлагается ознакомиться со статьёй, благо, она достаточно проста для понимания. Механизм Relational RAGs весьма мощный и универсальный – его полезно иметь в виду при реализации самых разных аспектов работы с языками программирования, не только статического анализа. 😊
#dsl #rag #static #analysis
Во-первых, как упоминалось ранее, отношения (Relations) задаются "внешним" по отношению к дереву образом, и авторы для этого используют обычный императивный код на Java, да ещё и опирающийся на неявные, генерируемые фреймворком методы. Мне такой способ не кажется декларативным и особо высокоуровневым.
Во-вторых, несмотря на то, что дерево разбора превращается в направленный граф общего вида, возможность реализации Control Flow Analysis и Data Flow Analysis остаётся под вопросом. Возможно, этому мешают ограничения на неизменяемость графа, связанные с мемоизацией (в свою очередь, необходимой для эффективной работы алгоритмов). В частности, это накладывает ограничения на построение отношений между "обычными" и узлами в NTA.
В любом случае, для прояснения деталей предлагаемого подхода читателю предлагается ознакомиться со статьёй, благо, она достаточно проста для понимания. Механизм Relational RAGs весьма мощный и универсальный – его полезно иметь в виду при реализации самых разных аспектов работы с языками программирования, не только статического анализа. 😊
#dsl #rag #static #analysis
👍11
https://arxiv.org/pdf/1304.3390.pdf
Quipper: A Scalable Quantum Programming Language
Как нетрудно догадаться, статья посвящена языку для квантовых вычислений. Квантовые вычисления — тема популярная, но сложная, чтобы в ней разобраться, нужно читать что-то более основательное. Вероятно, учебник квантовой механики для начала. При этом, даже если квантовая электродинамика сама по себе и не нужна, придётся выучить как минимум нотацию и семантику бра- и кет-векторов. 😊
Поэтому посмотрим на сам Quipper как язык: в чём его особенности и трудности, и как они решаются.
Технически, Quipper реализован в виде eDSL на Haskell. Вполне ожидаемо, монадический eDSL. Впрочем, лично мне кажется, для описания квантовых алгоритмов в виде circuits (схем) могли бы больше подойти Arrows (стрелки) — если на самом деле они не подходят, то интересно почему?
Помимо монад, Quipper полагается и на более продвинутые фичи Haskell и GHC, в частности, творчески использует Template Haskell чтобы автоматически преобразовывать "классические" функции подходящего вида в соответствующие квантовые схемы, получая оракулов для квантовых алгоритмов.
И тем не менее, кое-чего авторам не хватило:
> In particular, Haskell lacks two features that would be useful for Quipper: linear types and dependent types.
По такому поводу авторы выдвинули идею переделать Quipper в самостоятельный язык со своим собственным компилятором и системой типов. Но можно просто подождать ещё пару лет. А вы говорите, что зависимые типы никому не нужны. 😊
Так или иначе, Quipper разрабатывался как язык, не зависящий от конкретной реализации квантового компьютера, позволяя как тестировать полученные программы на симуляторе (или рисовать в виде диаграмм), так и переносить между разными физическими квантовыми компьютерами. Это достигается использованием общепринятой абстрактной модели QRAM machine, подразумевающей наличие квантового вычислительного устройства в виде сопроцессора, управляемого классическим компьютером. Что определяет следующую особенность программ на Quipper — в их жизненном цикле 3 стадии: 1. компиляция из исходного текста (Haskell) в программу, запускаемую на классической части квантового компьютера; 2. запуск этой программы для подготовки квантовой схемы и её запуска на квантовом сопроцессоре; 3. выполнение квантовой схемы на квантовом сопроцессоре. И на разных стадиях доступны совершенно разные языковые возможности и типы данных.
При написании и компиляции Quipper-программ, по сути, доступна вся мощь языка Haskell. Для формирования программы, работающей на следующем этапе, можно использовать любые средства и любые данные каких угодно типов, в частности, читать файлы, базы данных или запрашивать что-то по сети.
При запуске полученной программы на классической машине, управляющей квантовым компьютером, тоже доступен широкий диапазон данных. В первую очередь, можно сконфигурировать программу параметрами доступного квантового компьютера — количеством кубитов, таймингами и т.п. Во-вторых, можно сконфигурировать размерность и статические данные решаемой задачи, что повлияет на размеры генерируемых квантовых схем.
В конечном итоге, квантовая схема, очевидно, может оперировать только квантовыми данными (кубитами), используя только доступные квантовые операции (гейты).
При этом, квантовые схемы, производимые Quipper — первого порядка, т.е. сами не могут оперировать квантовыми схемами как значениями (не могут создавать и применять замыкания, говоря "классическим" языком). Так что несмотря на то, что Quipper является функциональным языком с поддержкой функций высшего порядка ("наследуя" эти возможности из Haskell), к моменту формирования конечного квантового контура все структуры высшего порядка "схлопываются".
Вся эта схема работы здорово напоминает про staged metaprogramming и модальные системы типов — возможно, это могло бы стать ещё одной фичей квантового языка программирования. 😊
#dsl #haskell #quipper #quantumcomputing
Quipper: A Scalable Quantum Programming Language
Как нетрудно догадаться, статья посвящена языку для квантовых вычислений. Квантовые вычисления — тема популярная, но сложная, чтобы в ней разобраться, нужно читать что-то более основательное. Вероятно, учебник квантовой механики для начала. При этом, даже если квантовая электродинамика сама по себе и не нужна, придётся выучить как минимум нотацию и семантику бра- и кет-векторов. 😊
Поэтому посмотрим на сам Quipper как язык: в чём его особенности и трудности, и как они решаются.
Технически, Quipper реализован в виде eDSL на Haskell. Вполне ожидаемо, монадический eDSL. Впрочем, лично мне кажется, для описания квантовых алгоритмов в виде circuits (схем) могли бы больше подойти Arrows (стрелки) — если на самом деле они не подходят, то интересно почему?
Помимо монад, Quipper полагается и на более продвинутые фичи Haskell и GHC, в частности, творчески использует Template Haskell чтобы автоматически преобразовывать "классические" функции подходящего вида в соответствующие квантовые схемы, получая оракулов для квантовых алгоритмов.
И тем не менее, кое-чего авторам не хватило:
> In particular, Haskell lacks two features that would be useful for Quipper: linear types and dependent types.
По такому поводу авторы выдвинули идею переделать Quipper в самостоятельный язык со своим собственным компилятором и системой типов. Но можно просто подождать ещё пару лет. А вы говорите, что зависимые типы никому не нужны. 😊
Так или иначе, Quipper разрабатывался как язык, не зависящий от конкретной реализации квантового компьютера, позволяя как тестировать полученные программы на симуляторе (или рисовать в виде диаграмм), так и переносить между разными физическими квантовыми компьютерами. Это достигается использованием общепринятой абстрактной модели QRAM machine, подразумевающей наличие квантового вычислительного устройства в виде сопроцессора, управляемого классическим компьютером. Что определяет следующую особенность программ на Quipper — в их жизненном цикле 3 стадии: 1. компиляция из исходного текста (Haskell) в программу, запускаемую на классической части квантового компьютера; 2. запуск этой программы для подготовки квантовой схемы и её запуска на квантовом сопроцессоре; 3. выполнение квантовой схемы на квантовом сопроцессоре. И на разных стадиях доступны совершенно разные языковые возможности и типы данных.
При написании и компиляции Quipper-программ, по сути, доступна вся мощь языка Haskell. Для формирования программы, работающей на следующем этапе, можно использовать любые средства и любые данные каких угодно типов, в частности, читать файлы, базы данных или запрашивать что-то по сети.
При запуске полученной программы на классической машине, управляющей квантовым компьютером, тоже доступен широкий диапазон данных. В первую очередь, можно сконфигурировать программу параметрами доступного квантового компьютера — количеством кубитов, таймингами и т.п. Во-вторых, можно сконфигурировать размерность и статические данные решаемой задачи, что повлияет на размеры генерируемых квантовых схем.
В конечном итоге, квантовая схема, очевидно, может оперировать только квантовыми данными (кубитами), используя только доступные квантовые операции (гейты).
При этом, квантовые схемы, производимые Quipper — первого порядка, т.е. сами не могут оперировать квантовыми схемами как значениями (не могут создавать и применять замыкания, говоря "классическим" языком). Так что несмотря на то, что Quipper является функциональным языком с поддержкой функций высшего порядка ("наследуя" эти возможности из Haskell), к моменту формирования конечного квантового контура все структуры высшего порядка "схлопываются".
Вся эта схема работы здорово напоминает про staged metaprogramming и модальные системы типов — возможно, это могло бы стать ещё одной фичей квантового языка программирования. 😊
#dsl #haskell #quipper #quantumcomputing
👍14
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
Вводная трехчасовая лекция о перспективных направлениях в области компиляции для спецпроцессоров и аппаратных ускорителей
https://www.youtube.com/watch?v=1m8oAQCTSeY
#dsl #smt #autotuning #superoptimization #egraph
https://www.youtube.com/watch?v=1m8oAQCTSeY
#dsl #smt #autotuning #superoptimization #egraph
YouTube
Создание компиляторов для спецпроцессоров. Пётр Советов (МИРЭА)
Запись лекции «Перспективные технологии создания компиляторов для спецпроцессоров» Петра Советова, известного российского специалиста по DSL-компиляторам.
Социально-образовательный проект Samsung Innovation Campus:
https://innovationcampus.ru
Социально-образовательный проект Samsung Innovation Campus:
https://innovationcampus.ru
👍28
На днях, и даже в одно и то же время, прошли два ежегодных российских мероприятия, в том числе и на темы языков и компиляторов. Это -- Национальный Суперкомпьютерный Форум (НСКФ) и Открытая конференция ИСП РАН.
По НСКФ доступны тезисы докладов: https://2021.nscf.ru/nauchno-prakticheskaya-konferenciya/tezisy-dokladov/
В телеграм-канале Открытой конференции есть ссылки на видеозаписи докладов: https://t.me/ispras/390
Я выбрал по одному докладу с каждого мероприятия и далее расскажу, чем эти доклады меня привлекли.
На НСКФ меня более всего заинтересовал доклад "Теории имен А.Питтса и М.Габбая и детерминированное параллельное объектно-ориентированное программирование имеют общую основу" от Климова А. В. и Адамовича А. И.
Этот доклад основан на статье "Адамович А. И., Климов А. В. О теориях имен и ссылок в формальных языках и последствиях для функционального и объектно-ориентированного программирования //Научный сервис в сети Интернет. – 2021. – Т. 23. – С. 3-21.". Статья, кстати говоря, доступна онлайн: https://keldysh.ru/abrau/2021/theses/30.pdf
Авторы рассматривают фундаментальные вопросы формализации понятий имен и ссылок, а также пытаются определить промежуточный класс языков между функциональными (широкие возможности анализа и трансформации программ) и объектно-ориентированными (производительная обработка сложных структур данных).
Оригинальные результаты в этой статье не приведены, но привлечение внимания к работам по номинальным техникам от А. Pitts и его коллег, считаю полезным.
Добавлю, что исследования авторов станут понятнее, если посмотреть их более раннюю статью "Подход к построению системы детерминированного параллельного программирования на основе монотонных объектов": https://pat.keldysh.ru/~anklimov/papers/2019-Adamovich_Klimov--An_Approach_to_Construction_of_a_Deterministic_Parallel_Programming_System--Vestnik_SibGUTI--submitted-revised.pdf
На Открытой конференции ИСП РАН было много интересных докладов и я надеюсь, что к некоторым из них мы еще на PLComp вернемся. Я выделил для себя доклад "Статический анализ, динамическое формирование и кооперативная векторизация программ для гибридных many-core процессоров", моего бывшего коллеги Владимира Роганова. Выбор доклада, разумеется, субъективный, поскольку в разработке инструментального ПО процессора, о котором рассказывает Владимир, я принимал активное участие несколько лет назад.
Так или иначе, мне кажется, полезно и интересно узнать, какие необычные и непростые задачи стоят перед разработчиками компиляторов/симуляторов/ассемблеров/... спецчипов с гетерогенной и массово-параллельной архитектурой. К примеру — JIT-распараллеливание на уровне множеств ядер или вопросы написания кода для VLIW-ускорителя c неоднородным доступом к ресурсам.
P.S. Непосредственно перед Владимиром выступал я, но тема моего доклада уже совсем экзотическая :)
#conf
По НСКФ доступны тезисы докладов: https://2021.nscf.ru/nauchno-prakticheskaya-konferenciya/tezisy-dokladov/
В телеграм-канале Открытой конференции есть ссылки на видеозаписи докладов: https://t.me/ispras/390
Я выбрал по одному докладу с каждого мероприятия и далее расскажу, чем эти доклады меня привлекли.
На НСКФ меня более всего заинтересовал доклад "Теории имен А.Питтса и М.Габбая и детерминированное параллельное объектно-ориентированное программирование имеют общую основу" от Климова А. В. и Адамовича А. И.
Этот доклад основан на статье "Адамович А. И., Климов А. В. О теориях имен и ссылок в формальных языках и последствиях для функционального и объектно-ориентированного программирования //Научный сервис в сети Интернет. – 2021. – Т. 23. – С. 3-21.". Статья, кстати говоря, доступна онлайн: https://keldysh.ru/abrau/2021/theses/30.pdf
Авторы рассматривают фундаментальные вопросы формализации понятий имен и ссылок, а также пытаются определить промежуточный класс языков между функциональными (широкие возможности анализа и трансформации программ) и объектно-ориентированными (производительная обработка сложных структур данных).
Оригинальные результаты в этой статье не приведены, но привлечение внимания к работам по номинальным техникам от А. Pitts и его коллег, считаю полезным.
Добавлю, что исследования авторов станут понятнее, если посмотреть их более раннюю статью "Подход к построению системы детерминированного параллельного программирования на основе монотонных объектов": https://pat.keldysh.ru/~anklimov/papers/2019-Adamovich_Klimov--An_Approach_to_Construction_of_a_Deterministic_Parallel_Programming_System--Vestnik_SibGUTI--submitted-revised.pdf
На Открытой конференции ИСП РАН было много интересных докладов и я надеюсь, что к некоторым из них мы еще на PLComp вернемся. Я выделил для себя доклад "Статический анализ, динамическое формирование и кооперативная векторизация программ для гибридных many-core процессоров", моего бывшего коллеги Владимира Роганова. Выбор доклада, разумеется, субъективный, поскольку в разработке инструментального ПО процессора, о котором рассказывает Владимир, я принимал активное участие несколько лет назад.
Так или иначе, мне кажется, полезно и интересно узнать, какие необычные и непростые задачи стоят перед разработчиками компиляторов/симуляторов/ассемблеров/... спецчипов с гетерогенной и массово-параллельной архитектурой. К примеру — JIT-распараллеливание на уровне множеств ядер или вопросы написания кода для VLIW-ускорителя c неоднородным доступом к ресурсам.
P.S. Непосредственно перед Владимиром выступал я, но тема моего доклада уже совсем экзотическая :)
#conf
👍37
https://arxiv.org/abs/2001.10490
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Sebastian Ullrich, Leonardo de Moura
Большинство систем интерактивного доказательства теорем разрабатываются с прицелом на формализацию математики. Включая возможность использования специфической математической нотации, разработанной для некоторой теории. Такой как 𝛴, 𝛱 или ∫, которые используются не только в математическом анализе, но и в теории категорий, например. Характерная особенность приведённых обозначений, как и многих других — "захват переменных" аналогично тому, как переменные захватываются кванторами в логике и лямбда-абстракцией в лямбда-исчислении. При этом, поскольку системы интерактивного доказательства строятся поверх того или иного варианта лямбда-исчисления, математическую нотацию придётся выражать именно через лямбды, и как-то с ними взаимодействовать.
В этот момент возникает вопрос "гигиены": мы не хотим, чтобы переменные перепутались и были связаны с неправильной лямбда-абстракцией, ообенно "невидимой" лямбдой, которая была автоматически сгенерирована в процессе трансляции другой нотации. Вопрос дополнительно осложняется естественным "инженерным" требованием: поскольку многие обозначения используют одинаковый синтаксис связывания переменных, мы хотели бы описать этот синтаксис и его семантику один раз, и просто переиспользовать во всех подходящих случаях. Примерами переиспользования синтаксиса связывания переменных могут служить те же нотации для сумм и произведений: 𝛴 и 𝛱.
Статья демонстрирует как можно решить эту задачу при помощи типизированной системы макросов и несложного алгоритма, обеспечивающего гигиену. Само собой, за простоту приходится чем-то заплатить. В данном случае — ограниченной применимостью, поскольку алгоритм полагается на определённые свойства языка программирования. Наиболее существенное из них: выполнение программы осуществляется "построчно", по одному выражению верхнего уровня за раз, в порядке их записи в файле. Новую нотацию (на самом деле, любой макрос) могут использовать только выражения, записанные ниже определения макроса. И некоторые другие упрощающие предположения. Такое поведение часто встречается в системах интерактивного доказательства теорем, но сильно ограничивает применимость в языках программирования общего назначения. Для таких языков придётся пользоваться намного более сложным алгоритмом гигиены, как, например, в Racket.
Кроме того, в статье рассматриваются вопросы интеграции макро-системы и систем "уточнения" (elaboration) и type-driven expansion, плюс реализация тактик в виде гигиенических макросов, чего до сих пор не встречалось в системах интерактивных доказательств.
В итоге, несмотря на очевидную направленность на системы интерактивного доказательства, статья является отличным введением в проблематику, связанную с макросами, обеспечением гигиены, типизацией макросов, декларативным и императивным заданием макросов. Рекомендую всем читателям, ещё не знакомым, но интересующимся вопросами создания макро-систем в языках программирования.
#macros #lean #elaboration #proofassistants
Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages
Sebastian Ullrich, Leonardo de Moura
Большинство систем интерактивного доказательства теорем разрабатываются с прицелом на формализацию математики. Включая возможность использования специфической математической нотации, разработанной для некоторой теории. Такой как 𝛴, 𝛱 или ∫, которые используются не только в математическом анализе, но и в теории категорий, например. Характерная особенность приведённых обозначений, как и многих других — "захват переменных" аналогично тому, как переменные захватываются кванторами в логике и лямбда-абстракцией в лямбда-исчислении. При этом, поскольку системы интерактивного доказательства строятся поверх того или иного варианта лямбда-исчисления, математическую нотацию придётся выражать именно через лямбды, и как-то с ними взаимодействовать.
В этот момент возникает вопрос "гигиены": мы не хотим, чтобы переменные перепутались и были связаны с неправильной лямбда-абстракцией, ообенно "невидимой" лямбдой, которая была автоматически сгенерирована в процессе трансляции другой нотации. Вопрос дополнительно осложняется естественным "инженерным" требованием: поскольку многие обозначения используют одинаковый синтаксис связывания переменных, мы хотели бы описать этот синтаксис и его семантику один раз, и просто переиспользовать во всех подходящих случаях. Примерами переиспользования синтаксиса связывания переменных могут служить те же нотации для сумм и произведений: 𝛴 и 𝛱.
Статья демонстрирует как можно решить эту задачу при помощи типизированной системы макросов и несложного алгоритма, обеспечивающего гигиену. Само собой, за простоту приходится чем-то заплатить. В данном случае — ограниченной применимостью, поскольку алгоритм полагается на определённые свойства языка программирования. Наиболее существенное из них: выполнение программы осуществляется "построчно", по одному выражению верхнего уровня за раз, в порядке их записи в файле. Новую нотацию (на самом деле, любой макрос) могут использовать только выражения, записанные ниже определения макроса. И некоторые другие упрощающие предположения. Такое поведение часто встречается в системах интерактивного доказательства теорем, но сильно ограничивает применимость в языках программирования общего назначения. Для таких языков придётся пользоваться намного более сложным алгоритмом гигиены, как, например, в Racket.
Кроме того, в статье рассматриваются вопросы интеграции макро-системы и систем "уточнения" (elaboration) и type-driven expansion, плюс реализация тактик в виде гигиенических макросов, чего до сих пор не встречалось в системах интерактивных доказательств.
В итоге, несмотря на очевидную направленность на системы интерактивного доказательства, статья является отличным введением в проблематику, связанную с макросами, обеспечением гигиены, типизацией макросов, декларативным и императивным заданием макросов. Рекомендую всем читателям, ещё не знакомым, но интересующимся вопросами создания макро-систем в языках программирования.
#macros #lean #elaboration #proofassistants
👍46
https://arxiv.org/pdf/1810.07951.pdf
Don't Unroll Adjoint: Differentiating SSA-form Programs
Michael J Innes, 2019
https://proceedings.neurips.cc/paper/2020/file/9332c513ef44b682e9347822c2e457ac-Paper.pdf
Instead of Rewriting Foreign Code for Machine Learning, Automatically Synthesize Fast Gradients
William S. Moses and Valentin Churavy, NeurIPS 2020
Обе статьи посвящены (обратному aka reverse-mode) автоматическому (или алгоритмическому) дифференцированию функций, представленных в форме Single Static Assignment aka SSA. И тем не менее, они описывают существенно различные подходы.
Первая статья даёт краткое введение в обратное дифференцирование и распространённый подход на основе Wengert Lists. Чтобы перейти к SSA форме, к Wengert Lists необходимо добавить метки, условные и безусловные переходы и фи-узлы (φ nodes). Соответственно, статья вводит правила дифференцирования этих управляющих конструкций (control flow constructs). Дополнительно вводятся правила дифференцирования для чтения и записи в ячейки памяти, поскольку основной прицел статьи — императивные языки (и Julia в особенности). Забавно, что на практике (на текущий момент) основанная на описанном подходе библиотека Zygote не поддерживает деструктивную модификацию массивов, несмотря на её (библиотеки) широкое использование, в особенности во фреймворке для машинного обучения Flux. 😊
Несмотря на использование SSA-формы, первая статья подразумевает сравнительно высокоуровневое представление, близкое к исходному языку, до проведения оптимизаций. Вторая же статья рассматривает внедрение автоматического дифференцирования непосредственно в фреймворк LLVM в виде одного из проходов компиляции, выполняемого над низкоуровневым SSA-представлением, не зависящим от исходного языка и прошедшего ряд оптимизаций. Поэтому основное внимание она уделяет низкоуровневым аспектам: теневой памяти (shadow memory), кешам, обработке указателей, в том числе — вызовам функций по указателю, и переиспользованию информации с других проходов, таких как type-based alias analysis.
Стремление проводить автоматическое дифференцирование настолько низкоуровневого представления продиктовано двумя соображениями. Во-первых, немедленная применимость к большому количеству промышленных языков — C, C++, Rust, Julia — без каких-либо изменений в самом языке. Во-вторых, оптимизация исходного кода может сильно упростить и ускорить порождаемый код расчёта градиента функции, в некоторых случаях — понизить сложность с квадратичной до линейной после применения loop-invariant code motion к исходному коду.
Для подтверждения ускорения, авторы провели замеры производительности и сравнения с традиционными подходами на задачах ADBench от Microsoft и нескольких сторонних реализациях численного решателя дифференциальных уравнений. Результаты и графики приведены в статье. 😊
В любом случае, обе работы полагаются на "классические компиляторные техники", такие как dataflow analysis, alias analysis, abstract interpretation, и оптимизации. И потому представляют собой интереснейшее расширение "поля деятельности компиляторщиков" в сравнительно новую, но стремительно набирающую популярность, область.
Don't Unroll Adjoint: Differentiating SSA-form Programs
Michael J Innes, 2019
https://proceedings.neurips.cc/paper/2020/file/9332c513ef44b682e9347822c2e457ac-Paper.pdf
Instead of Rewriting Foreign Code for Machine Learning, Automatically Synthesize Fast Gradients
William S. Moses and Valentin Churavy, NeurIPS 2020
Обе статьи посвящены (обратному aka reverse-mode) автоматическому (или алгоритмическому) дифференцированию функций, представленных в форме Single Static Assignment aka SSA. И тем не менее, они описывают существенно различные подходы.
Первая статья даёт краткое введение в обратное дифференцирование и распространённый подход на основе Wengert Lists. Чтобы перейти к SSA форме, к Wengert Lists необходимо добавить метки, условные и безусловные переходы и фи-узлы (φ nodes). Соответственно, статья вводит правила дифференцирования этих управляющих конструкций (control flow constructs). Дополнительно вводятся правила дифференцирования для чтения и записи в ячейки памяти, поскольку основной прицел статьи — императивные языки (и Julia в особенности). Забавно, что на практике (на текущий момент) основанная на описанном подходе библиотека Zygote не поддерживает деструктивную модификацию массивов, несмотря на её (библиотеки) широкое использование, в особенности во фреймворке для машинного обучения Flux. 😊
Несмотря на использование SSA-формы, первая статья подразумевает сравнительно высокоуровневое представление, близкое к исходному языку, до проведения оптимизаций. Вторая же статья рассматривает внедрение автоматического дифференцирования непосредственно в фреймворк LLVM в виде одного из проходов компиляции, выполняемого над низкоуровневым SSA-представлением, не зависящим от исходного языка и прошедшего ряд оптимизаций. Поэтому основное внимание она уделяет низкоуровневым аспектам: теневой памяти (shadow memory), кешам, обработке указателей, в том числе — вызовам функций по указателю, и переиспользованию информации с других проходов, таких как type-based alias analysis.
Стремление проводить автоматическое дифференцирование настолько низкоуровневого представления продиктовано двумя соображениями. Во-первых, немедленная применимость к большому количеству промышленных языков — C, C++, Rust, Julia — без каких-либо изменений в самом языке. Во-вторых, оптимизация исходного кода может сильно упростить и ускорить порождаемый код расчёта градиента функции, в некоторых случаях — понизить сложность с квадратичной до линейной после применения loop-invariant code motion к исходному коду.
Для подтверждения ускорения, авторы провели замеры производительности и сравнения с традиционными подходами на задачах ADBench от Microsoft и нескольких сторонних реализациях численного решателя дифференциальных уравнений. Результаты и графики приведены в статье. 😊
В любом случае, обе работы полагаются на "классические компиляторные техники", такие как dataflow analysis, alias analysis, abstract interpretation, и оптимизации. И потому представляют собой интереснейшее расширение "поля деятельности компиляторщиков" в сравнительно новую, но стремительно набирающую популярность, область.
👍70
Первая часть цикла докладов об автоматизации программирования в СССР доступна на youtube.
Цель — напомнить о хорошо забытых идеях и алгоритмах, не вдаваясь в подробности биографий их авторов и детали устройства вычислительных машин.
Цикл состоит из четырех частей:
1. Программирующие программы (50-е годы).
2. Трансляторы (60-70-е годы).
3. Метавычисления.
4. Синтез программ.
Кстати, идея доклада возникла случайно. Для планируемой к изданию энциклопедии «Истории отечественного программирования» нужны были статьи. Ко мне обратились поздно и я написал обзорную заметку, текстом которой был не очень доволен. Увы, проект энциклопедии так, похоже, и не состоялся. Но ссылки интернет хранит: https://rcc.msu.ru/ru/enciklopediya-istoriya-otechestvennogo-programmirovaniya
К счастью, материал не пропал, а был серьезно развит и переработан для выступления на C++ Russia (спасибо Тимуру Сафину за приглашение выступить!).
https://youtube.com/watch?v=0bTdplAlGYg
P.S. На днях на C++ Russia состоится несколько компиляторных докладов с уклоном в LLVM. Я для себя выделил этот доклад: https://cppconf.ru/talks/595fef990d9342c1b34179bff9c057ab/
Цель — напомнить о хорошо забытых идеях и алгоритмах, не вдаваясь в подробности биографий их авторов и детали устройства вычислительных машин.
Цикл состоит из четырех частей:
1. Программирующие программы (50-е годы).
2. Трансляторы (60-70-е годы).
3. Метавычисления.
4. Синтез программ.
Кстати, идея доклада возникла случайно. Для планируемой к изданию энциклопедии «Истории отечественного программирования» нужны были статьи. Ко мне обратились поздно и я написал обзорную заметку, текстом которой был не очень доволен. Увы, проект энциклопедии так, похоже, и не состоялся. Но ссылки интернет хранит: https://rcc.msu.ru/ru/enciklopediya-istoriya-otechestvennogo-programmirovaniya
К счастью, материал не пропал, а был серьезно развит и переработан для выступления на C++ Russia (спасибо Тимуру Сафину за приглашение выступить!).
https://youtube.com/watch?v=0bTdplAlGYg
P.S. На днях на C++ Russia состоится несколько компиляторных докладов с уклоном в LLVM. Я для себя выделил этот доклад: https://cppconf.ru/talks/595fef990d9342c1b34179bff9c057ab/
👍99
Эта небольшая заметка посвящена нескольким новостям по нашей тематике.
Во-первых, хочу напомнить, что в июне прошла конференция PLDI 2022 и многие из представленных там работ имеют компиляторную тематику. Вот программа конференции: https://pldi22.sigplan.org/program/program-pldi-2022/
Во-вторых, давайте поговорим о весьма достойных книгах, которые официально только готовятся к печати и выйдут в 2022-2023 гг.
Нас ждет третье издание классики Engineering a Compiler. Второе издание вышло в 2012 году и мне, увы, пока не удалось установить, в чем же особенности нового издания. Судя по всему, новая версия знаменитого учебника выйдет в этом сентябре: https://www.amazon.com/Engineering-Compiler-Keith-D-Cooper/dp/0128154128
В феврале 2023 года выйдет Essentials of Compilation в издательстве MIT: https://mitpress.mit.edu/books/essentials-compilation Материал в разных редакциях давно уже публиковался на github: https://github.com/IUCompilerCourse/Essentials-of-Compilation
Еще одна довольно известная онлайн-книга скоро будет напечатана. Речь об SSA Book. Официально она теперь называется SSA-based Compiler Design: https://link.springer.com/book/9783030805142 Ждем ее ближе к февралю 2023 года.
Наконец, упомяну о настоящем "долгострое": новой версии классики Programming Languages: An Interpreter-Based Approach" от Samuel Kamin. Новый автор и известный компьютерный ученый, Norman Ramsey, работал над своей версией еще, кажется, с 2005 года. На протяжении многих лет черновые варианты учебника адресно рассылались отдельным профессорам в разных университетах. И, вот, наконец, в этом октябре книга под официальным названием Programming Languages Build, Prove, and Compare будет напечатана: https://www.cambridge.org/ru/academic/subjects/computer-science/programming-languages-and-applied-logic/programming-languages-build-prove-and-compare
Во-первых, хочу напомнить, что в июне прошла конференция PLDI 2022 и многие из представленных там работ имеют компиляторную тематику. Вот программа конференции: https://pldi22.sigplan.org/program/program-pldi-2022/
Во-вторых, давайте поговорим о весьма достойных книгах, которые официально только готовятся к печати и выйдут в 2022-2023 гг.
Нас ждет третье издание классики Engineering a Compiler. Второе издание вышло в 2012 году и мне, увы, пока не удалось установить, в чем же особенности нового издания. Судя по всему, новая версия знаменитого учебника выйдет в этом сентябре: https://www.amazon.com/Engineering-Compiler-Keith-D-Cooper/dp/0128154128
В феврале 2023 года выйдет Essentials of Compilation в издательстве MIT: https://mitpress.mit.edu/books/essentials-compilation Материал в разных редакциях давно уже публиковался на github: https://github.com/IUCompilerCourse/Essentials-of-Compilation
Еще одна довольно известная онлайн-книга скоро будет напечатана. Речь об SSA Book. Официально она теперь называется SSA-based Compiler Design: https://link.springer.com/book/9783030805142 Ждем ее ближе к февралю 2023 года.
Наконец, упомяну о настоящем "долгострое": новой версии классики Programming Languages: An Interpreter-Based Approach" от Samuel Kamin. Новый автор и известный компьютерный ученый, Norman Ramsey, работал над своей версией еще, кажется, с 2005 года. На протяжении многих лет черновые варианты учебника адресно рассылались отдельным профессорам в разных университетах. И, вот, наконец, в этом октябре книга под официальным названием Programming Languages Build, Prove, and Compare будет напечатана: https://www.cambridge.org/ru/academic/subjects/computer-science/programming-languages-and-applied-logic/programming-languages-build-prove-and-compare
👍99
Недавно завершилась конференция C++ Russia 2023 и пришло время подвести некоторые ее итоги. Разумеется, в контексте нашего канала, благо на конференции появилась отдельная секция по компиляторным докладам.
Теперь о двух докладах, на которых я присутствовал в том или ином качестве.
Loop unrolling в деталях Ивана Афансьева. Доклад, как это понятно из названия, посвящен теме раскрутки циклов в компиляторе. Это введение в предмет, более интересное, пожалуй, начинающим. Правда, есть один любопытный нюанс. В завершающей части доклада Иван переходит от игрушечных задач к задаче из своей практической деятельности. Это, совершенно неожиданно, оказывается NP-полная задача о вершинном покрытии графа. Боюсь, что далеко не все начинающие поняли тонкости задачи в процессе доклада. Откуда взялась эта задача? Этот вопрос я и задал Ивану. Тут-то и выяснилось самое интересное. Оказывается, это задача относится к проекту генератора кода для спецпроцессора. Иван решает ее в лоб для малого набора данных (раскручивает циклы, использует векторизацию), а если набор данных велик -- использует ансамбль из эвристических алгоритмов. Достаточно впечатляюще! Здесь я пожалел, что Иван не сделал на эту тему отдельного доклада уже для опытных компиляторщиков.
Автоматизация программирования в СССР. Трансляторы (60–70-е годы). Вторая часть моего доклада. В процессе подготовки от ряда тем пришлось отказаться, поскольку на их изложение времени уже не хватало. В этой части я постарался еще более явно связать древние времена с самыми современными компиляторными подходами и в этом смысле, боюсь, доклад не совсем будет понятен начинающим. Впрочем, возможно я и ошибаюсь, так что предлагаю самостоятельно посмотреть и оценить. За возможность дать ссылку на yt благодарю Тимура Сафина и JUG Ru Group.
https://www.youtube.com/watch?v=Q2ErYDuVAWo
Теперь о двух докладах, на которых я присутствовал в том или ином качестве.
Loop unrolling в деталях Ивана Афансьева. Доклад, как это понятно из названия, посвящен теме раскрутки циклов в компиляторе. Это введение в предмет, более интересное, пожалуй, начинающим. Правда, есть один любопытный нюанс. В завершающей части доклада Иван переходит от игрушечных задач к задаче из своей практической деятельности. Это, совершенно неожиданно, оказывается NP-полная задача о вершинном покрытии графа. Боюсь, что далеко не все начинающие поняли тонкости задачи в процессе доклада. Откуда взялась эта задача? Этот вопрос я и задал Ивану. Тут-то и выяснилось самое интересное. Оказывается, это задача относится к проекту генератора кода для спецпроцессора. Иван решает ее в лоб для малого набора данных (раскручивает циклы, использует векторизацию), а если набор данных велик -- использует ансамбль из эвристических алгоритмов. Достаточно впечатляюще! Здесь я пожалел, что Иван не сделал на эту тему отдельного доклада уже для опытных компиляторщиков.
Автоматизация программирования в СССР. Трансляторы (60–70-е годы). Вторая часть моего доклада. В процессе подготовки от ряда тем пришлось отказаться, поскольку на их изложение времени уже не хватало. В этой части я постарался еще более явно связать древние времена с самыми современными компиляторными подходами и в этом смысле, боюсь, доклад не совсем будет понятен начинающим. Впрочем, возможно я и ошибаюсь, так что предлагаю самостоятельно посмотреть и оценить. За возможность дать ссылку на yt благодарю Тимура Сафина и JUG Ru Group.
https://www.youtube.com/watch?v=Q2ErYDuVAWo
C++ Russia 2026. Конференция для C++ разработчиков
C++ Russia 2026 — конференция для CPP-разработчиков. Несколько десятков технических докладов о современном C++, инструментах, многопоточности и многом другом.
👍64
Прерываю затянувшуюся тишину на нашем канале! Надеюсь, остальные участники PLComp тоже, со временем, активизируются.
Недавно я выступил с двумя компиляторными докладами. Рассказал о том, что мне самому было бы интересно услышать.
Доклад Graph-Based Intermediate Representations: An Overview and Perspectives. Введение и обзор графовых IR. Такие IR диктуют оригинальный взгляд на построение компиляторов в целом. Впрочем, до сих пор эти IR являются, скорее, экзотикой, поэтому доклад будет более интересен специалистам.
Видеозаписи у меня нет, но имеются слайды: https://github.com/true-grue/graph-irs
Доклад В Python есть готовый фронтенд для вашего компилятора. Компиляторные технологии для начинающих в Питоне. О том, как сочетание модуля ast и сопоставления с образцом дает возможность по-новому взглянуть на задачу построения DSL. Кстати, доклад должен быть интересен не только питонистам, ведь примеры (каждый из которых содержит <100 строк кода) включают в себя DSL-компилятор Datalog и компилятор в Wasm.
Видеозапись: https://www.youtube.com/watch?v=h-TzDPL2nDE
Материалы к докладу: https://github.com/true-grue/python-dsls
Недавно я выступил с двумя компиляторными докладами. Рассказал о том, что мне самому было бы интересно услышать.
Доклад Graph-Based Intermediate Representations: An Overview and Perspectives. Введение и обзор графовых IR. Такие IR диктуют оригинальный взгляд на построение компиляторов в целом. Впрочем, до сих пор эти IR являются, скорее, экзотикой, поэтому доклад будет более интересен специалистам.
Видеозаписи у меня нет, но имеются слайды: https://github.com/true-grue/graph-irs
Доклад В Python есть готовый фронтенд для вашего компилятора. Компиляторные технологии для начинающих в Питоне. О том, как сочетание модуля ast и сопоставления с образцом дает возможность по-новому взглянуть на задачу построения DSL. Кстати, доклад должен быть интересен не только питонистам, ведь примеры (каждый из которых содержит <100 строк кода) включают в себя DSL-компилятор Datalog и компилятор в Wasm.
Видеозапись: https://www.youtube.com/watch?v=h-TzDPL2nDE
Материалы к докладу: https://github.com/true-grue/python-dsls
👍35
Видеозапись моего недавнего выступления. Хотя тема и узкоспециальная, все же, предлагаю досмотреть. Мне кажется, во второй-третьей части доклад становится интереснее и для тех компиляторщиков, кому заявленная тематика не близка. Отдельно благодарю представителей компании YADRO за отличные вопросы!
https://www.youtube.com/watch?v=Q6-h6R_e-04
https://www.youtube.com/watch?v=Q6-h6R_e-04
👍28
Коллеги, друзья и единомышленники!
Трудно поверить, но нашему каналу PLComp (Programming Languages & Compilers) уже исполнилось 4 года. За это время мы подготовили почти сотню обзорных заметок, освещающих историю развития компиляторов, структуру современных и перспективных компиляторов, а также смежные темы. Мы искренне надеемся, что наши читатели смогли найти в этих материалах что-то интересное и полезное для себя.
К сожалению, в последние год-два по различным причинам количество новых заметок сократилось, и мы начали задумываться о возможном закрытии проекта. В связи с этим нам бы хотелось задать нашим читателям несколько открытых вопросов:
1. Какие из опубликованных материалов вам запомнились больше всего?
2. Считаете ли вы, что нам стоит продолжить работу над каналом?
3. Какой формат подачи информации кажется вам наиболее подходящим и удобным?
4. Хотели бы вы принять участие в будущих публикациях на PLComp? (лучше ответить личным сообщением)
Мы будем признательны за любые комментарии, идеи и предложения.
Трудно поверить, но нашему каналу PLComp (Programming Languages & Compilers) уже исполнилось 4 года. За это время мы подготовили почти сотню обзорных заметок, освещающих историю развития компиляторов, структуру современных и перспективных компиляторов, а также смежные темы. Мы искренне надеемся, что наши читатели смогли найти в этих материалах что-то интересное и полезное для себя.
К сожалению, в последние год-два по различным причинам количество новых заметок сократилось, и мы начали задумываться о возможном закрытии проекта. В связи с этим нам бы хотелось задать нашим читателям несколько открытых вопросов:
1. Какие из опубликованных материалов вам запомнились больше всего?
2. Считаете ли вы, что нам стоит продолжить работу над каналом?
3. Какой формат подачи информации кажется вам наиболее подходящим и удобным?
4. Хотели бы вы принять участие в будущих публикациях на PLComp? (лучше ответить личным сообщением)
Мы будем признательны за любые комментарии, идеи и предложения.
👍39
📚 Breno Campos, Ferreira Guimarães
"Lazy Evaluation for the Lazy: Automatically Transforming Call-by-Value into Call-by-Need"
Proceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction. February 2023: 239–249
Ленивыми называются такие вычисления, которые программа не производит сразу, а откладывает, пока не потребуется их результат. Если выполнять редкие вычисления лениво, средняя производительность программы может вырасти.
Чтобы понять, какие вычисления выгодно производить лениво, программист делает предположения о сценариях выполнения программы или профилирует её. В языках с поддержкой ленивых вычислений можно просто пометить фрагмент программы как lazy, но во многих, особенно низкоуровневых языках, добиться ленивости сложнее, и это может потребовать существенной модификации кода.
Цель авторов — научить компиляторы находить вычисления, которые предпочтительно сделать ленивыми, не используя аннотирование lazy вручную и даже поддержку ленивости со стороны языка. Для этого они реализовали внутри LLVM специальную profile-guided оптимизацию, делающую вычисление некоторых аргументов функций ленивым. Оптимизация происходит на уровне LLVM IR в SSA форме.
Статья описывает два алгоритма:
1) модификацию Value Slicing, которая строит замыкание для вычисления произвольного значения в SSA IR.
2) Lazification по информации от профилировщика заменяет call-by-value на call-by-need.
Выбор вычислений для lazification и необходимое профилирование программы описаны в более ранней статье:
Chang, Stephen. "Laziness by need." Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013
Авторы добились роста производительности программ на C и C++ от 1% до ~10% за счет увеличения размера на ~10%; тесты включают в себя SPEC CPU 2017.
#optimization #profiling #lazy #llvm
"Lazy Evaluation for the Lazy: Automatically Transforming Call-by-Value into Call-by-Need"
Proceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction. February 2023: 239–249
Ленивыми называются такие вычисления, которые программа не производит сразу, а откладывает, пока не потребуется их результат. Если выполнять редкие вычисления лениво, средняя производительность программы может вырасти.
Чтобы понять, какие вычисления выгодно производить лениво, программист делает предположения о сценариях выполнения программы или профилирует её. В языках с поддержкой ленивых вычислений можно просто пометить фрагмент программы как lazy, но во многих, особенно низкоуровневых языках, добиться ленивости сложнее, и это может потребовать существенной модификации кода.
Цель авторов — научить компиляторы находить вычисления, которые предпочтительно сделать ленивыми, не используя аннотирование lazy вручную и даже поддержку ленивости со стороны языка. Для этого они реализовали внутри LLVM специальную profile-guided оптимизацию, делающую вычисление некоторых аргументов функций ленивым. Оптимизация происходит на уровне LLVM IR в SSA форме.
Статья описывает два алгоритма:
1) модификацию Value Slicing, которая строит замыкание для вычисления произвольного значения в SSA IR.
2) Lazification по информации от профилировщика заменяет call-by-value на call-by-need.
Выбор вычислений для lazification и необходимое профилирование программы описаны в более ранней статье:
Chang, Stephen. "Laziness by need." Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013
Авторы добились роста производительности программ на C и C++ от 1% до ~10% за счет увеличения размера на ~10%; тесты включают в себя SPEC CPU 2017.
#optimization #profiling #lazy #llvm
👍25
Новости PLComp №1, часть 1
📚Статья Flan: An expressive and efficient datalog compiler for program analysis от Supun Abeysinghe, Xhebraj Anxhelo и Tiark Rompf (Purdue)
Реализация компилятора Datalog, который на тестах опережает по производительности известный компилятор Soufflé. Реализация основана на eDSL, что позволяет расширять Datalog с помощью механизмов хост-языка Scala. Для eDSL написан простой интерпретатор, код которого, с помощью Scala LMS (первая проекция Футамуры), транслируется в производительный код на C.
📚Заметки Compiling With Constraints (Mar 18, 2024) от Филипа Цукера (Philip Zucker)
Заметки по очень перспективному подходу к использованию программирования в ограничениях для декларативного описания фаз выбора команд, планирования и распределения регистров. Во многом основано на изучении проекта Unison. Минимум теории, максимум практики в виде примеров кода на Python и MiniZinc.
📚Видео доклада Архитектурно-зависимые оптимизации компилятора LCC для микропроцессоров архитектуры Эльбрус (2024 г.), автор М.И. Нейман-Заде
Доклад посвящён работе оптимизирующего компилятора lcc для процессоров Эльбрус с широким командным словом (VLIW). Компилятор lcc сам по себе структурно схож с традиционными компиляторами, однако особенности целевой платформы накладывают серьезные отпечатки на существующие низкоуровневые оптимизации. В докладе раскрываются аппаратные особенности работы процессоров Эльбрус, их отличия от "традиционных" процессоров, после чего описываются некоторые аппаратно-зависимые оптимизации, характерные для Эльбрусов.
Среди оптимизаций рассказывается про:
* Слияние кода (if-conversion).
* Конвейеризацию циклов (software pipelining с аппаратной поддержкой).
* Динамический разрыв зависимостей.
* Предварительную подкачку данных (улучшенный аналог prefetch).
📚Курс Declarative Program Analysis and Optimization (Spring 2024) от Макса Уилси (Max Willsey, UC Berkley) (если ссылка не работает, попробуйте отключить VPN)
Учебный курс с очень интригующим названием, поскольку декларативный подход к реализации фаз компилятора все еще остается уделом почти исключительно академистов. В курсе речь идет о переписывании термов, стратегическом переписывании, синтезе и верификации систем переписывания, использовании Datalog, о E-графах и насыщении равенствами. Словом, это ультрасовременный университетский курс по специальным вопросам компиляции.
📚Статья Fixing a Bug in PyPy's Incremental GC (2024-03-26)
Починка каждого бага, связанного с GC, это сама по себе уже интересная история,
потому что такие баги обычно нетривиальны. К тому же баг, про который рассказывает автор, приводит к memory corruption и это еще больше усложняет отладку. Поиск стабильного воспроизведения, пошаговая интерактивная отладка в gdb/rr,
написание скриптов для GDB API для упрощения отладки GC и т.д.
(продолжение следует)
#news
📚Статья Flan: An expressive and efficient datalog compiler for program analysis от Supun Abeysinghe, Xhebraj Anxhelo и Tiark Rompf (Purdue)
Реализация компилятора Datalog, который на тестах опережает по производительности известный компилятор Soufflé. Реализация основана на eDSL, что позволяет расширять Datalog с помощью механизмов хост-языка Scala. Для eDSL написан простой интерпретатор, код которого, с помощью Scala LMS (первая проекция Футамуры), транслируется в производительный код на C.
📚Заметки Compiling With Constraints (Mar 18, 2024) от Филипа Цукера (Philip Zucker)
Заметки по очень перспективному подходу к использованию программирования в ограничениях для декларативного описания фаз выбора команд, планирования и распределения регистров. Во многом основано на изучении проекта Unison. Минимум теории, максимум практики в виде примеров кода на Python и MiniZinc.
📚Видео доклада Архитектурно-зависимые оптимизации компилятора LCC для микропроцессоров архитектуры Эльбрус (2024 г.), автор М.И. Нейман-Заде
Доклад посвящён работе оптимизирующего компилятора lcc для процессоров Эльбрус с широким командным словом (VLIW). Компилятор lcc сам по себе структурно схож с традиционными компиляторами, однако особенности целевой платформы накладывают серьезные отпечатки на существующие низкоуровневые оптимизации. В докладе раскрываются аппаратные особенности работы процессоров Эльбрус, их отличия от "традиционных" процессоров, после чего описываются некоторые аппаратно-зависимые оптимизации, характерные для Эльбрусов.
Среди оптимизаций рассказывается про:
* Слияние кода (if-conversion).
* Конвейеризацию циклов (software pipelining с аппаратной поддержкой).
* Динамический разрыв зависимостей.
* Предварительную подкачку данных (улучшенный аналог prefetch).
📚Курс Declarative Program Analysis and Optimization (Spring 2024) от Макса Уилси (Max Willsey, UC Berkley) (если ссылка не работает, попробуйте отключить VPN)
Учебный курс с очень интригующим названием, поскольку декларативный подход к реализации фаз компилятора все еще остается уделом почти исключительно академистов. В курсе речь идет о переписывании термов, стратегическом переписывании, синтезе и верификации систем переписывания, использовании Datalog, о E-графах и насыщении равенствами. Словом, это ультрасовременный университетский курс по специальным вопросам компиляции.
📚Статья Fixing a Bug in PyPy's Incremental GC (2024-03-26)
Починка каждого бага, связанного с GC, это сама по себе уже интересная история,
потому что такие баги обычно нетривиальны. К тому же баг, про который рассказывает автор, приводит к memory corruption и это еще больше усложняет отладку. Поиск стабильного воспроизведения, пошаговая интерактивная отладка в gdb/rr,
написание скриптов для GDB API для упрощения отладки GC и т.д.
(продолжение следует)
#news
👍46
Новости PLComp №1, часть 2
📚Статья Troubleshooting an Intermittent Failure in CI Tests on ARM64 (October 4, 2023)
Тесты для Kong Gateway время от времени падали с синтаксической ошибкой, причем происходило это только на ARM64 и только с включенным компилятором в OpenResty (использует LuaJIT). В ходе исследования бага авторы выяснили причину — некорректная кодогенерация для ARM64, и предложили исправление в основной репозиторий LuaJIT.
Можно отметить, что в обеих статьях использовали отладчик rr. rr позволяет записывать выполнение программы и потом детерминировано его воспроизводить, а также выполнять инструкции в обратном порядке.
📚Видео доклада How Badly Do We Want Correct Compilers? (NDC TechTown 2023)
Доклад известного исследователя Джона Регира (John Regehr). Докладчик, насколько можно заметить, ни разу не произносит слово "CompCert" и сомневается в успешности проектов формально верифицированных компиляторов для популярных ЯП, что, конечно, интригует. Рассматриваются инструменты, в разработке которых принял участие автор доклада: YARPGen, Souper и другие проекты.
📚Заметки Compiling ML models to C for fun (September 19, 2023) и Vectorizing ML models for fun (February 18, 2024), автор Макс Бернштейн (Max Bernstein)
Учебное пособие в двух частях для самых маленьких по разработке DL-компиляторов с примерами на Python. Автор начинает с реализации более производительного варианта библиотеки micrograd и создает компилятор, выдающий представление на C. Во второй части делается переход от скаляров к векторам и осуществляется автовекторизация с помощью выявления скалярных произведений в коде.
📚Видео доклада A Full Employment Theorem for PL Researchers: Domain-Specific Languages от Нейта Фостера (Nate Foster, Cornell) (23 Oct 2023)
Доклад призван воодушевить исследователей в области языков программирования на работу с современными DSL, в первую очередь с теми, которые используются для программирования специализированного "железа". Рассматривается Тьюринг-неполный язык P4 для разбора сетевых пакетов и ставится задача установления эквивалентности двух двоичных парсеров. Для решения задачи используется подход с использованием конечных автоматов, бисимуляции, SMT-решателя и Coq.
📚Видео доклада ægraphs: Acyclic E-graphs for Efficient Optimization in a Production Compiler, автор Chris Fallin (8 июля 2023 г.)
Перенацеливаемый генератор кода Cranelift является, судя по всему, первым промышленным проектом, где широко используются E-графы для решения задачи выбора порядка фаз при компиляции. В Cranelift, как показано в докладе, используется оригинальный упрощенный вариант E-графов -- ациклические E-графы (aegraphs). В предложенную схему на основе aegraphs включены и такие "тяжеловесные" оптимизации, как GVN и LICM.
Над выпуском работали: Пётр Советов, Сергей Бронников, Алексей Маркин
#news
📚Статья Troubleshooting an Intermittent Failure in CI Tests on ARM64 (October 4, 2023)
Тесты для Kong Gateway время от времени падали с синтаксической ошибкой, причем происходило это только на ARM64 и только с включенным компилятором в OpenResty (использует LuaJIT). В ходе исследования бага авторы выяснили причину — некорректная кодогенерация для ARM64, и предложили исправление в основной репозиторий LuaJIT.
Можно отметить, что в обеих статьях использовали отладчик rr. rr позволяет записывать выполнение программы и потом детерминировано его воспроизводить, а также выполнять инструкции в обратном порядке.
📚Видео доклада How Badly Do We Want Correct Compilers? (NDC TechTown 2023)
Доклад известного исследователя Джона Регира (John Regehr). Докладчик, насколько можно заметить, ни разу не произносит слово "CompCert" и сомневается в успешности проектов формально верифицированных компиляторов для популярных ЯП, что, конечно, интригует. Рассматриваются инструменты, в разработке которых принял участие автор доклада: YARPGen, Souper и другие проекты.
📚Заметки Compiling ML models to C for fun (September 19, 2023) и Vectorizing ML models for fun (February 18, 2024), автор Макс Бернштейн (Max Bernstein)
Учебное пособие в двух частях для самых маленьких по разработке DL-компиляторов с примерами на Python. Автор начинает с реализации более производительного варианта библиотеки micrograd и создает компилятор, выдающий представление на C. Во второй части делается переход от скаляров к векторам и осуществляется автовекторизация с помощью выявления скалярных произведений в коде.
📚Видео доклада A Full Employment Theorem for PL Researchers: Domain-Specific Languages от Нейта Фостера (Nate Foster, Cornell) (23 Oct 2023)
Доклад призван воодушевить исследователей в области языков программирования на работу с современными DSL, в первую очередь с теми, которые используются для программирования специализированного "железа". Рассматривается Тьюринг-неполный язык P4 для разбора сетевых пакетов и ставится задача установления эквивалентности двух двоичных парсеров. Для решения задачи используется подход с использованием конечных автоматов, бисимуляции, SMT-решателя и Coq.
📚Видео доклада ægraphs: Acyclic E-graphs for Efficient Optimization in a Production Compiler, автор Chris Fallin (8 июля 2023 г.)
Перенацеливаемый генератор кода Cranelift является, судя по всему, первым промышленным проектом, где широко используются E-графы для решения задачи выбора порядка фаз при компиляции. В Cranelift, как показано в докладе, используется оригинальный упрощенный вариант E-графов -- ациклические E-графы (aegraphs). В предложенную схему на основе aegraphs включены и такие "тяжеловесные" оптимизации, как GVN и LICM.
Над выпуском работали: Пётр Советов, Сергей Бронников, Алексей Маркин
#news
👍35
📚 Пост AI-Powered Fuzzing: Breaking the Bug Hunting Barrier
В 2016 году Google запустила бесплатный сервис для фаззинга открытого ПО OSS-Fuzz. Это произошло после обнародования нескольких критических уязвимостей типа Heartbleed, которые, как обнаружилось, можно было предотвратить, если бы разработчики использовали фаззинг.
Чтобы использовать OSS-Fuzz, разработчик реализует фаззеры для своего проекта и конфигурирует взаимодействие с сервисом. Сервис запускает фаззеры, собирает результаты, приватно сообщает разработчикам о найденных багах, а затем следит за обновлениями чтобы удостовериться, что разработчики смогли исправить баг. Открытые проекты обслуживаются бесплатно, а для закрытого кода можно запустить сервис на своей машине.
В среднем, код проектов, использующих OSS-Fuzz, покрывается не более, чем на 30%, потому что писать фаззеры приходится вручную. Это и трудно, и долго, а разработчики не всегда могут выделить на эту задачу ресурсы. Чтобы помочь разработчикам увеличить покрытие кода фаззерами, в августе 2023 инженеры Google реализовали протокол интеграции OSS-Fuzz с LLM, дабы языковые модели генерировали фаззеры без участия человека.
OSS-Fuzz идентифицирует непокрытые части проекта и формирует запрос к LLM. Запрос включает информацию о непокрытой части проекта. Код фаззера может автоматически уточняться у языковой модели в случае ошибок компиляции или если сгенерированный фаззер не увеличил покрытие кода.
Примеры запросов к LLM и system prompts.
В описании репозитория проекта авторы приводят результаты одного из экспериментов:
- 1300+ бенчмарков из 300 проектов ПО.
- В 160 проектах LLM cумела сгенерировать корректные фаззеры и увеличить покрытие на 10-30%.
К сожалению, неясно, какую LLM использовали для этого эксперимента — заявлена поддержка Vertex AI code-bison и code-bison-32k, Gemini Pro и OpenAI GPT-3.5-turbo и GPT-4.
#llm #fuzzing
В 2016 году Google запустила бесплатный сервис для фаззинга открытого ПО OSS-Fuzz. Это произошло после обнародования нескольких критических уязвимостей типа Heartbleed, которые, как обнаружилось, можно было предотвратить, если бы разработчики использовали фаззинг.
Чтобы использовать OSS-Fuzz, разработчик реализует фаззеры для своего проекта и конфигурирует взаимодействие с сервисом. Сервис запускает фаззеры, собирает результаты, приватно сообщает разработчикам о найденных багах, а затем следит за обновлениями чтобы удостовериться, что разработчики смогли исправить баг. Открытые проекты обслуживаются бесплатно, а для закрытого кода можно запустить сервис на своей машине.
В среднем, код проектов, использующих OSS-Fuzz, покрывается не более, чем на 30%, потому что писать фаззеры приходится вручную. Это и трудно, и долго, а разработчики не всегда могут выделить на эту задачу ресурсы. Чтобы помочь разработчикам увеличить покрытие кода фаззерами, в августе 2023 инженеры Google реализовали протокол интеграции OSS-Fuzz с LLM, дабы языковые модели генерировали фаззеры без участия человека.
OSS-Fuzz идентифицирует непокрытые части проекта и формирует запрос к LLM. Запрос включает информацию о непокрытой части проекта. Код фаззера может автоматически уточняться у языковой модели в случае ошибок компиляции или если сгенерированный фаззер не увеличил покрытие кода.
Примеры запросов к LLM и system prompts.
В описании репозитория проекта авторы приводят результаты одного из экспериментов:
- 1300+ бенчмарков из 300 проектов ПО.
- В 160 проектах LLM cумела сгенерировать корректные фаззеры и увеличить покрытие на 10-30%.
К сожалению, неясно, какую LLM использовали для этого эксперимента — заявлена поддержка Vertex AI code-bison и code-bison-32k, Gemini Pro и OpenAI GPT-3.5-turbo и GPT-4.
#llm #fuzzing
Google Online Security Blog
AI-Powered Fuzzing: Breaking the Bug Hunting Barrier
Dongge Liu, Jonathan Metzman, Oliver Chang, Google Open Source Security Team Since 2016, OSS-Fuzz has been at the forefront of automated v...
👍12
📚 Отчёт Wentao Gao, Van-Thuan Pham, Dongge Liu, Oliver Chang, Toby Murray, and Benjamin I.P. Rubinstein. 2023. Beyond the Coverage Plateau: A Comprehensive Study of Fuzz Blockers (Registered Report). In Proceedings of the 2nd International Fuzzing Workshop (FUZZING ’23), July 17, 2023
Отчёт анализирует некоторые причины проблемы плато, с которой сталкивается Coverage-Guided Greybox Fuzzing (CGF).
CGF это тип фаззинга, который характерен двумя особенностями. Во-первых, фаззер использует общую информацию об архитектуре программы для подбора значимых входов, но не знает её детальной структуры. Во-вторых, фаззер в процессе работы старается максимизировать покрытие кода трассами выполнения.
При CGF фаззер выполняет следующие шаги в цикле, пока не будет достигнут лимит времени:
1. Выбирает вход из накапливаемого множества входов (seed corpus).
2. Мутирует вход, пытаясь достигнуть непокрытых участков кода.
3. Запускает программу на мутированном входе. Если покрытие увеличилось, добавляет вход в seed corpus; при неожиданном поведении программы, например, ошибке времени выполнения, описывает этот случай в отчёте.
Алгоритмы CGF различаются правилами мутации, начальным заполнением seed corpus и другими деталями.
Эксперименты показывают, что современные фаззеры достаточно быстро выходят на плато, при котором покрытие кода перестает расти, сколько бы дополнительного времени ни получил фаззер.
Чтобы понять причины эффекта плато, авторы изучили результаты фаззинга трех популярных библиотек: libPNG, iGraph, OpenSSL с помощью утилиты FuzzIntrospector для cервиса OSS-Fuzz.
(Пример отчёта)
Фаззинг библиотек требует написания программ-оберток (drivers), которые запускают библиотечные функции. Этим занимаются, как правило, сами разработчики библиотек. По мнению авторов, чрезмерно упрощенные обертки являются важной причиной эффекта плато.
Анализ авторов показал, что проблемные ситуации часто возникали независимо от входов: в libPNG все 12 экспериментов показали плато на любых входах, а в iGraph — 9 из 22. Покрытие переставало увеличиваться по следующим причинам:
1. Аргументы функций в обертке зафиксированы. Например, библиотека iGraph поддерживает работу как с ориентированными, так и с неориентированными графами, но существующие обертки вызывали некоторые функции с такими фиксированными аргументами, что под фаззинг попадали только ориентированные графы.
2. Функции вообще не вызываются оберткой:
2.1. Вызываются не все перегрузки.
2.2. Ошибки бы проявились если бы функция была вызвана больше одного раза (например, init-функции).
2.3. Пропущены вызовы, которые могли бы настроить библиотеку на разные конфигурации.
2.4. Пропущены вызовы, добавляющие функциональность (например, установка обработчиков событий).
3. Функции вызываются только в "правильном", ожидаемом порядке, а ошибки проявляются лишь если перемешать вызовы.
4. Наличие объективно недостижимого кода.
Некоторые проблемы в обертке iGraph проявлялись только на определенных входах, которых фаззеры не достигали.
Это были крайние случаи — например, когда размер входного графа превышал предполагаемый лимит.
Неожиданно, но в эксперименте не возникло проблем, связанных с использованием контрольных сумм и магических чисел, хотя это известные проблемы для фаззинга.
Анализ фаззинга OpenSSL, видимо, будет включен в следующую работу.
В качестве решений проблем с обертками авторы предлагают рассмотреть автоматическую генерацию оберток и structure-aware fuzzing, имеющий полную информацию о коде программы.
#fuzzing
Отчёт анализирует некоторые причины проблемы плато, с которой сталкивается Coverage-Guided Greybox Fuzzing (CGF).
CGF это тип фаззинга, который характерен двумя особенностями. Во-первых, фаззер использует общую информацию об архитектуре программы для подбора значимых входов, но не знает её детальной структуры. Во-вторых, фаззер в процессе работы старается максимизировать покрытие кода трассами выполнения.
При CGF фаззер выполняет следующие шаги в цикле, пока не будет достигнут лимит времени:
1. Выбирает вход из накапливаемого множества входов (seed corpus).
2. Мутирует вход, пытаясь достигнуть непокрытых участков кода.
3. Запускает программу на мутированном входе. Если покрытие увеличилось, добавляет вход в seed corpus; при неожиданном поведении программы, например, ошибке времени выполнения, описывает этот случай в отчёте.
Алгоритмы CGF различаются правилами мутации, начальным заполнением seed corpus и другими деталями.
Эксперименты показывают, что современные фаззеры достаточно быстро выходят на плато, при котором покрытие кода перестает расти, сколько бы дополнительного времени ни получил фаззер.
Чтобы понять причины эффекта плато, авторы изучили результаты фаззинга трех популярных библиотек: libPNG, iGraph, OpenSSL с помощью утилиты FuzzIntrospector для cервиса OSS-Fuzz.
(Пример отчёта)
Фаззинг библиотек требует написания программ-оберток (drivers), которые запускают библиотечные функции. Этим занимаются, как правило, сами разработчики библиотек. По мнению авторов, чрезмерно упрощенные обертки являются важной причиной эффекта плато.
Анализ авторов показал, что проблемные ситуации часто возникали независимо от входов: в libPNG все 12 экспериментов показали плато на любых входах, а в iGraph — 9 из 22. Покрытие переставало увеличиваться по следующим причинам:
1. Аргументы функций в обертке зафиксированы. Например, библиотека iGraph поддерживает работу как с ориентированными, так и с неориентированными графами, но существующие обертки вызывали некоторые функции с такими фиксированными аргументами, что под фаззинг попадали только ориентированные графы.
2. Функции вообще не вызываются оберткой:
2.1. Вызываются не все перегрузки.
2.2. Ошибки бы проявились если бы функция была вызвана больше одного раза (например, init-функции).
2.3. Пропущены вызовы, которые могли бы настроить библиотеку на разные конфигурации.
2.4. Пропущены вызовы, добавляющие функциональность (например, установка обработчиков событий).
3. Функции вызываются только в "правильном", ожидаемом порядке, а ошибки проявляются лишь если перемешать вызовы.
4. Наличие объективно недостижимого кода.
Некоторые проблемы в обертке iGraph проявлялись только на определенных входах, которых фаззеры не достигали.
Это были крайние случаи — например, когда размер входного графа превышал предполагаемый лимит.
Неожиданно, но в эксперименте не возникло проблем, связанных с использованием контрольных сумм и магических чисел, хотя это известные проблемы для фаззинга.
Анализ фаззинга OpenSSL, видимо, будет включен в следующую работу.
В качестве решений проблем с обертками авторы предлагают рассмотреть автоматическую генерацию оберток и structure-aware fuzzing, имеющий полную информацию о коде программы.
#fuzzing
ACM Conferences
Beyond the Coverage Plateau: A Comprehensive Study of Fuzz Blockers (Registered Report) | Proceedings of the 2nd International…
👍16
📚 Статья Rocha, Rodrigo CO, et al. "Hybf: A hybrid branch fusion strategy for code size reduction." Proceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction. 2023.
Авторы реализовали для LLVM IR два новых алгоритма слияния ветвей. 70% бенчмарков показали уменьшение размера кода до 4% поверх уже внедренных оптимизаций с пренебрежимо малым эффектом на производительность кода.
Распространенные алгоритмы слияния ветвей ограничены в применении:
- Первоначальная версия алгоритма слияния ветвей [1] работает только для похожих ветвей, содержащих по одному базовому блоку, т.е. для ромбов в графе потока управления.
- Другой алгоритм — Control Flow Melding (Divergence Aware Region Melder, DARM), поддерживает только структурно простые ветви: вложенные if-then, if-then-else или natural loops.
Авторы предлагают два новых алгоритма для слияния ветвей и алгоритм HyBF, выбирающий лучшую из двух трансформаций для конкретного подграфа потока управления. Они работают с т.н. регионами графа потока управления – это подграфы с одной точкой входа.
Первый алгоритм, предложенный авторами — Control Flow Melding (CFM-CS), это улучшенная версия алгоритма DARM.
CFM-CS работает только с SESE-регионами (single-entry-single-exit, регионы с одной точкой выхода).
Первоначально, DARM предназначен для борьбы с control flow divergence. Это ситуация в моделях вычислений Single Instruction Multiple Threads, когда несколько потоков выполняют один и тот же код, но выбирают разные пути из-за условного ветвления [2]. Если ветви выполняются неодинаковое время, потоки, уже выполнившие более короткую ветвь, ожидают еще не завершившиеся потоки, занятые длинными ветвями, как при барьерной синхронизации.
DARM обычно ведёт к уменьшению размера кода, но не нацелен на это, и не способен работать со сложно структурированными подграфами потока управления.
Улучшенная версия DARM — CFM-CS — работает следующим образом:
1. Определить SESE-регион, где возможно слияние (блок с двумя исходящими ветвями, сходящимися в одном блоке).
2. Собрать подрегионы каждой ветви в дерево (авторы используют структуру данных region tree в LLVM).
3. Изо всех возможных пар подрегионов, принадлежащих двум ветвям, нужно выбрать пару изоморфных подрегионов, причем с наиболее "похожими" инструкциями внутри. Для этого регионы должны быть выровнены, как в проблеме "выравнивания последовательностей"[3]. Авторы используют специальную эвристику в качестве меры сходства, позволяющей выбрать пары подрегионов наиболее выгодные для слияния.
4. Чтобы объединить изоморфные подрегионы из двух ветвей необходимо выровнять уже инструкции внутри соответствующих блоков. Это разделит инструкции блоков на:
- не имеющие соответствия в блоке изоморфного подрегиона. Эти инструкции перемещаются в новые, условно выполняемые базовые блоки.
- совпадающие с инструкциями в блоке изоморфного подрегиона. Это одинаковые инструкции с разными операндами: они будут помещены в объединенный базовый блок, но их операнды будут вычисляться с использованием псевдоинструкций SELECT. Условием таких SELECT'ов будет, разумеется, условие из входного блока большого SESE-региона.
Исходный код алгоритма CFM-CS для LLVM IR.
Алгоритм CFM-CS эффективен, когда ветви имеют похожую структуру, но если одна из ветвей содержит всего один блок, такой блок можно обернуть в код, имитирующий структуру другой ветви, а затем запустить на полученном регионе CFM-CS. Эта техника называется Region Replication, и авторы также предлагают улучшение существующего алгоритма Region Replication используемого в DARM.
Второй предложенный алгоритм SEME-fusion обобщает алгоритм слияния функций HyFM, предложенный авторами в предыдущей статье [4], на любой SEME-регион (Single-Entry-Multiple-Exit). Он сравнивает блоки двух областей SEME на основе расстояний между их fingerprint'ами, вычисляя linear pairwise alignment [4]. После выравнивания и слияния блоков происходит технический процесс корректировки ϕ-функций в выходных блоках.
Исходный код алгоритма SEME-fusion для LLVM IR.
Авторы реализовали для LLVM IR два новых алгоритма слияния ветвей. 70% бенчмарков показали уменьшение размера кода до 4% поверх уже внедренных оптимизаций с пренебрежимо малым эффектом на производительность кода.
Распространенные алгоритмы слияния ветвей ограничены в применении:
- Первоначальная версия алгоритма слияния ветвей [1] работает только для похожих ветвей, содержащих по одному базовому блоку, т.е. для ромбов в графе потока управления.
- Другой алгоритм — Control Flow Melding (Divergence Aware Region Melder, DARM), поддерживает только структурно простые ветви: вложенные if-then, if-then-else или natural loops.
Авторы предлагают два новых алгоритма для слияния ветвей и алгоритм HyBF, выбирающий лучшую из двух трансформаций для конкретного подграфа потока управления. Они работают с т.н. регионами графа потока управления – это подграфы с одной точкой входа.
Первый алгоритм, предложенный авторами — Control Flow Melding (CFM-CS), это улучшенная версия алгоритма DARM.
CFM-CS работает только с SESE-регионами (single-entry-single-exit, регионы с одной точкой выхода).
Первоначально, DARM предназначен для борьбы с control flow divergence. Это ситуация в моделях вычислений Single Instruction Multiple Threads, когда несколько потоков выполняют один и тот же код, но выбирают разные пути из-за условного ветвления [2]. Если ветви выполняются неодинаковое время, потоки, уже выполнившие более короткую ветвь, ожидают еще не завершившиеся потоки, занятые длинными ветвями, как при барьерной синхронизации.
DARM обычно ведёт к уменьшению размера кода, но не нацелен на это, и не способен работать со сложно структурированными подграфами потока управления.
Улучшенная версия DARM — CFM-CS — работает следующим образом:
1. Определить SESE-регион, где возможно слияние (блок с двумя исходящими ветвями, сходящимися в одном блоке).
2. Собрать подрегионы каждой ветви в дерево (авторы используют структуру данных region tree в LLVM).
3. Изо всех возможных пар подрегионов, принадлежащих двум ветвям, нужно выбрать пару изоморфных подрегионов, причем с наиболее "похожими" инструкциями внутри. Для этого регионы должны быть выровнены, как в проблеме "выравнивания последовательностей"[3]. Авторы используют специальную эвристику в качестве меры сходства, позволяющей выбрать пары подрегионов наиболее выгодные для слияния.
4. Чтобы объединить изоморфные подрегионы из двух ветвей необходимо выровнять уже инструкции внутри соответствующих блоков. Это разделит инструкции блоков на:
- не имеющие соответствия в блоке изоморфного подрегиона. Эти инструкции перемещаются в новые, условно выполняемые базовые блоки.
- совпадающие с инструкциями в блоке изоморфного подрегиона. Это одинаковые инструкции с разными операндами: они будут помещены в объединенный базовый блок, но их операнды будут вычисляться с использованием псевдоинструкций SELECT. Условием таких SELECT'ов будет, разумеется, условие из входного блока большого SESE-региона.
Исходный код алгоритма CFM-CS для LLVM IR.
Алгоритм CFM-CS эффективен, когда ветви имеют похожую структуру, но если одна из ветвей содержит всего один блок, такой блок можно обернуть в код, имитирующий структуру другой ветви, а затем запустить на полученном регионе CFM-CS. Эта техника называется Region Replication, и авторы также предлагают улучшение существующего алгоритма Region Replication используемого в DARM.
Второй предложенный алгоритм SEME-fusion обобщает алгоритм слияния функций HyFM, предложенный авторами в предыдущей статье [4], на любой SEME-регион (Single-Entry-Multiple-Exit). Он сравнивает блоки двух областей SEME на основе расстояний между их fingerprint'ами, вычисляя linear pairwise alignment [4]. После выравнивания и слияния блоков происходит технический процесс корректировки ϕ-функций в выходных блоках.
Исходный код алгоритма SEME-fusion для LLVM IR.
ResearchGate
(PDF) HyBF: A Hybrid Branch Fusion Strategy for Code Size Reduction
PDF | On Feb 17, 2023, Rodrigo C. O. Rocha and others published HyBF: A Hybrid Branch Fusion Strategy for Code Size Reduction | Find, read and cite all the research you need on ResearchGate
👍12
Таким образом, CFM-CS лучше работает для ветвей с похожей структурой, а SEME-fusion предпочтителен в ситуациях SEME-регионов или для сильно различающихся по структуре ветвей.
Так как эти два подхода ортогональны, авторы реализовали специальный проход по модулям в LLVM, применяющий к регионам с ветвлением обе трансформации и выбирающий лучшую.
[1] B. Coutinho, D. Sampaio, F. M. Q. Pereira, and W. Meira Jr. 2011. Divergence Analysis and Optimizations. In 2011 International Conference on Parallel Architectures and Compilation Techniques. 320–329.
[2] Saumya, Charitha, Kirshanthan Sundararajah, and Milind Kulkarni. "DARM: Control-Flow Melding for SIMT Thread Divergence Reduction--Extended Version." arXiv preprint arXiv:2107.05681 (2021).
[3] https://en.wikipedia.org/wiki/Sequence_alignment
[4] Rocha, Rodrigo CO, et al. "HyFM: Function merging for free." Proceedings of the 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems. 2021.
#llvm #function_merging #optimization #branch_merging #code_size_reduction
Так как эти два подхода ортогональны, авторы реализовали специальный проход по модулям в LLVM, применяющий к регионам с ветвлением обе трансформации и выбирающий лучшую.
[1] B. Coutinho, D. Sampaio, F. M. Q. Pereira, and W. Meira Jr. 2011. Divergence Analysis and Optimizations. In 2011 International Conference on Parallel Architectures and Compilation Techniques. 320–329.
[2] Saumya, Charitha, Kirshanthan Sundararajah, and Milind Kulkarni. "DARM: Control-Flow Melding for SIMT Thread Divergence Reduction--Extended Version." arXiv preprint arXiv:2107.05681 (2021).
[3] https://en.wikipedia.org/wiki/Sequence_alignment
[4] Rocha, Rodrigo CO, et al. "HyFM: Function merging for free." Proceedings of the 22nd ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems. 2021.
#llvm #function_merging #optimization #branch_merging #code_size_reduction
ResearchGate
(PDF) HyBF: A Hybrid Branch Fusion Strategy for Code Size Reduction
PDF | On Feb 17, 2023, Rodrigo C. O. Rocha and others published HyBF: A Hybrid Branch Fusion Strategy for Code Size Reduction | Find, read and cite all the research you need on ResearchGate
👍11