📚 Статья 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
Implementation Strategies for Mutable Value Semantics
Dimitri Racordon, Denys Shabalin, Daniel Zheng, Dave Abrahams, Brennan Saeta
https://kyouko-taiga.github.io/assets/papers/jot2022-mvs.pdf
Одно из неоспоримых достоинств языка Rust — он наглядно показал, что безопасная работа с указателями и ссылками сложна, и требует следовать довольно замысловатым правилам, уберегающим от неочевидных потенциальных проблем. Даже опыт более простых языков, повсеместно использующих ссылки и GC — например, Java — показывает, что непреднамеренный алиасинг (aliasing) может создавать дыры в системе безопасности, помимо других проблем.
Эти два фактора — сложность системы типов и владения в Rust, и сложность безопасного использования ссылок без контроля алиасинга — привели к появлению ряда языков, например, https://www.hylo-lang.org/ или https://vale.dev/, отказавшихся от первоклассных ссылок вообще. Отказ от первоклассных ссылок означает, что в языке просто нет механизмов, позволяющих явным образом взять ссылку на объект в памяти, передать её в функцию или того хуже — записать в поле другого объекта.
Отказавшись от ссылок и ссылочной семантики, мы приходим к семантике значений. Концептуально, каждое присваивание копирует значение целиком из одного места в другое, а каждый объект владеет своими частями (whole-part relation). Благодаря этому все данные в программе образуют лес, корни деревьев которого располагаются в переменных. И поскольку в такой структуре не может быть алиасинга, можно безбоязненно сделать значения изменяемыми, откуда и возникает Mutable Value Semantics — семантика изменяемых значений. Возможность изменения "по месту" (in-place) частей объектов и отличает MVS от семантики неизменных (immutable) значений в функциональном программировании, которая тривиально реализуется поверх ссылок на общие части в персистентных структурах данных.
Естественно, что наивная реализация такой семантики крайне неэффективна из-за постоянного копирования развесистых структур данных. Самое очевидное узкое место — работа с массивами: при передаче массивов в функции их пришлось бы копировать, а единственный способ вернуть массив из функции — снова создать копию. Для обхода этой проблемы и реализации работы с массивами и другими структурами "по месту" (in-place) предлагается использовать ключевое слово
Тем не менее, поскольку по ссылке могут передаваться только аргументы функций, а всё остальное должно копироваться — это всё ещё непозволительно много копирований. Особенно "лишних" копирований значений, которые никогда и не меняются, что значит для них алиасинг не наблюдаем и не создаёт проблем (аналогично ФП, упоминавшемуся выше). Чтобы избавиться от этих копий предлагается использовать механизмы Copy-on-Write и подсчёт ссылок при реализации языка. Для уменьшения инкрементов и декрементов счётчика предлагается обратиться к таким работам как Perceus для Koka и Lean 4.
Однако возникает вопрос: коль скоро мы вводим неявные ссылки в наш язык и его реализацию, не сломают ли они семантику изменяемых значений? Чтобы на него ответить, авторы формализуют core language, его систему типов и операционную семантику, после чего доказывают корректность оптимизаций и сохранение семантики изменяемых значений теми правилами, которым подчиняется работа
Но авторы не ограничились теоретическим рассмотрением вопроса, а пошли дальше, и реализовали прототип предлагаемой семантики с оптимизациями в виде упрощённого языка программирования на основе Swift, используя LLVM в качестве бэкенда. Это позволило оценить производительность прототипа в сравнении с другими языками, использующими LLVM (C++, Swift, Scala Native) на ряде синтетических бенчмарков и общеизвестных примеров (Mandelbrot, NBody, NQueens, etc.).
Dimitri Racordon, Denys Shabalin, Daniel Zheng, Dave Abrahams, Brennan Saeta
https://kyouko-taiga.github.io/assets/papers/jot2022-mvs.pdf
Одно из неоспоримых достоинств языка Rust — он наглядно показал, что безопасная работа с указателями и ссылками сложна, и требует следовать довольно замысловатым правилам, уберегающим от неочевидных потенциальных проблем. Даже опыт более простых языков, повсеместно использующих ссылки и GC — например, Java — показывает, что непреднамеренный алиасинг (aliasing) может создавать дыры в системе безопасности, помимо других проблем.
Эти два фактора — сложность системы типов и владения в Rust, и сложность безопасного использования ссылок без контроля алиасинга — привели к появлению ряда языков, например, https://www.hylo-lang.org/ или https://vale.dev/, отказавшихся от первоклассных ссылок вообще. Отказ от первоклассных ссылок означает, что в языке просто нет механизмов, позволяющих явным образом взять ссылку на объект в памяти, передать её в функцию или того хуже — записать в поле другого объекта.
Отказавшись от ссылок и ссылочной семантики, мы приходим к семантике значений. Концептуально, каждое присваивание копирует значение целиком из одного места в другое, а каждый объект владеет своими частями (whole-part relation). Благодаря этому все данные в программе образуют лес, корни деревьев которого располагаются в переменных. И поскольку в такой структуре не может быть алиасинга, можно безбоязненно сделать значения изменяемыми, откуда и возникает Mutable Value Semantics — семантика изменяемых значений. Возможность изменения "по месту" (in-place) частей объектов и отличает MVS от семантики неизменных (immutable) значений в функциональном программировании, которая тривиально реализуется поверх ссылок на общие части в персистентных структурах данных.
Естественно, что наивная реализация такой семантики крайне неэффективна из-за постоянного копирования развесистых структур данных. Самое очевидное узкое место — работа с массивами: при передаче массивов в функции их пришлось бы копировать, а единственный способ вернуть массив из функции — снова создать копию. Для обхода этой проблемы и реализации работы с массивами и другими структурами "по месту" (in-place) предлагается использовать ключевое слово
inout для параметров функций, передаваемых "по ссылке". Это и есть "ссылки второго класса", которые возникают и используются неявно, без возможности сохранения в переменных или полях объектов.Тем не менее, поскольку по ссылке могут передаваться только аргументы функций, а всё остальное должно копироваться — это всё ещё непозволительно много копирований. Особенно "лишних" копирований значений, которые никогда и не меняются, что значит для них алиасинг не наблюдаем и не создаёт проблем (аналогично ФП, упоминавшемуся выше). Чтобы избавиться от этих копий предлагается использовать механизмы Copy-on-Write и подсчёт ссылок при реализации языка. Для уменьшения инкрементов и декрементов счётчика предлагается обратиться к таким работам как Perceus для Koka и Lean 4.
Однако возникает вопрос: коль скоро мы вводим неявные ссылки в наш язык и его реализацию, не сломают ли они семантику изменяемых значений? Чтобы на него ответить, авторы формализуют core language, его систему типов и операционную семантику, после чего доказывают корректность оптимизаций и сохранение семантики изменяемых значений теми правилами, которым подчиняется работа
inout аргументов.Но авторы не ограничились теоретическим рассмотрением вопроса, а пошли дальше, и реализовали прототип предлагаемой семантики с оптимизациями в виде упрощённого языка программирования на основе Swift, используя LLVM в качестве бэкенда. Это позволило оценить производительность прототипа в сравнении с другими языками, использующими LLVM (C++, Swift, Scala Native) на ряде синтетических бенчмарков и общеизвестных примеров (Mandelbrot, NBody, NQueens, etc.).
👍20
Бенчмарки показали жизнеспособность подхода MVS — производительность оказалась на уровне между Scala Native и Swift. Отставание от Swift авторы объясняют тем, что в прототипе не использовались более продвинутые оптимизации, в частности, уменьшающие количество обращений к счётчику ссылок. Таким образом подход имеет перспективы значительного дальнейшего улучшения за счёт комбинирования с другими известными оптимизациями (например, упоминавшийся Perceus).
C++ в бенчмарках использовался в качестве реализации наивного подхода "копируем всё и всегда, но с агрессивными компиляторными оптимизациями", поэтому ожидаемо показал худшую производительность, кроме тестов с преобладающим количеством изменений "по месту" с передачей аргументов через
По итогу, MVS предлагает перспективную, формально проработанную семантику для производительных и (более) безопасных прикладных императивных языков программирования. Применимость для системных языков остаётся под вопросом как из-за недостаточной проработанности вопроса оптимизаций на текущий момент, так и по причине ограничений модели программирования, не позволяющей выражать алгоритмы, полагающиеся на использование указателей (в противовес индексам и хэндлам).
#mutable_value_semantics #swift #CoW
C++ в бенчмарках использовался в качестве реализации наивного подхода "копируем всё и всегда, но с агрессивными компиляторными оптимизациями", поэтому ожидаемо показал худшую производительность, кроме тестов с преобладающим количеством изменений "по месту" с передачей аргументов через
inout параметры.По итогу, MVS предлагает перспективную, формально проработанную семантику для производительных и (более) безопасных прикладных императивных языков программирования. Применимость для системных языков остаётся под вопросом как из-за недостаточной проработанности вопроса оптимизаций на текущий момент, так и по причине ограничений модели программирования, не позволяющей выражать алгоритмы, полагающиеся на использование указателей (в противовес индексам и хэндлам).
#mutable_value_semantics #swift #CoW
👍24
Возможно вы знакомы с алгоритмами сборки мусора, которые используются в языках программирования. Американский программист Кен Фокс (Ken Fox) написал программу с использованием разных алгоритмов сборки мусора и вариант программы без освобождения памяти, собрал данные для каждого варианта запуска программы и сгенерировал анимированные изображения для них. В репозитории представлены визуализации четырех основных алгоритмов сборки мусора:
- Mark-sweep
- Mark-compact
- Copying
- Reference counting
Каждому из этих алгоритмов посвящена отдельная глава в основополагающем учебнике The Garbage Collection Handbook. Рекомендуем обратиться к этому учебнику для полного погружения в тему.
Каждое анимированное изображение - это пространство памяти, выделенное процессу. Чёрным цветом изображена неиспользуемая память, по мере использования память начинает подсвечиваться жёлтым (операции записи) и зелёным (операции чтения) цветами. Цвет фрагментов памяти, которые используются дольше, начинает тускнеть, чтобы визуализировать развитие процесса во времени. По ходу выполнения программа перестаёт использовать отдельные участки памяти. Они и считаются "мусором".
Первая анимация демонстирует отсутствие всякой сборки мусора -
Вторая анимация демонстрирует работу сборщика мусора с использованием техники подсчёта ссылок. Суть алгоритма заключается в подсчёте количества ссылок на объекты в памяти, если количество ссылок становится равным нулю, то объект удаляется. Подсчёт ссылок - единственный алгоритм, хорошо совместимый с разными менеджерами ресурсов. По сравнению с первой анимацией появились красные пиксели, они соответствуют операциям подсчёта ссылок. Можно оценить и эффективность сборщика, если сразу после красной вспышки область памяти освобождается.
Третья анимация демонстрирует работу алгоритма "mark-and-sweep". Все объекты делятся на достижимые и недостижимые. Определённое множество объектов считается достижимым изначально - так называемые корневые объекты. Объект, на который есть ссылка из достижимого объекта, тоже считается достижимым. При запуске сборщик мусора выполняет следующие шаги:
- Фаза Mark: отмечает все достижимые объекты
- Фаза Sweep: проходит рекурсивно по объектам в куче, удаляет недостижимые объекты и возвращает их в пул свободной памяти.
Визуализации остальных алгоритмов приведены в репозитории. Помимо описанных визуализаций алгоритмов сборки мусора есть и другие, например интерактивная визуализация алгоритма tricolor mark-sweep, используемого в реализации языка Go.
- Mark-sweep
- Mark-compact
- Copying
- Reference counting
Каждому из этих алгоритмов посвящена отдельная глава в основополагающем учебнике The Garbage Collection Handbook. Рекомендуем обратиться к этому учебнику для полного погружения в тему.
Каждое анимированное изображение - это пространство памяти, выделенное процессу. Чёрным цветом изображена неиспользуемая память, по мере использования память начинает подсвечиваться жёлтым (операции записи) и зелёным (операции чтения) цветами. Цвет фрагментов памяти, которые используются дольше, начинает тускнеть, чтобы визуализировать развитие процесса во времени. По ходу выполнения программа перестаёт использовать отдельные участки памяти. Они и считаются "мусором".
Первая анимация демонстирует отсутствие всякой сборки мусора -
NO_GC, в этом случае память освобождается только при завершении процесса. Механизм NO_GC прост в реализации, он удобен, когда есть способ разбить задачу на отдельные подпроцессы. Так, например, работает веб-сервер Apache.Вторая анимация демонстрирует работу сборщика мусора с использованием техники подсчёта ссылок. Суть алгоритма заключается в подсчёте количества ссылок на объекты в памяти, если количество ссылок становится равным нулю, то объект удаляется. Подсчёт ссылок - единственный алгоритм, хорошо совместимый с разными менеджерами ресурсов. По сравнению с первой анимацией появились красные пиксели, они соответствуют операциям подсчёта ссылок. Можно оценить и эффективность сборщика, если сразу после красной вспышки область памяти освобождается.
Третья анимация демонстрирует работу алгоритма "mark-and-sweep". Все объекты делятся на достижимые и недостижимые. Определённое множество объектов считается достижимым изначально - так называемые корневые объекты. Объект, на который есть ссылка из достижимого объекта, тоже считается достижимым. При запуске сборщик мусора выполняет следующие шаги:
- Фаза Mark: отмечает все достижимые объекты
- Фаза Sweep: проходит рекурсивно по объектам в куче, удаляет недостижимые объекты и возвращает их в пул свободной памяти.
Визуализации остальных алгоритмов приведены в репозитории. Помимо описанных визуализаций алгоритмов сборки мусора есть и другие, например интерактивная визуализация алгоритма tricolor mark-sweep, используемого в реализации языка Go.
GitHub
GitHub - kenfox/gc-viz: Animated visualizations of several garbage collection algorithms
Animated visualizations of several garbage collection algorithms - kenfox/gc-viz
👍29
This media is not supported in your browser
VIEW IN TELEGRAM
Программа без освобождения памяти (NO_GC).
👍5
This media is not supported in your browser
VIEW IN TELEGRAM
Программа с использованием сборщика мусора с алгоритмом Mark and Sweep.
👍13
Forwarded from Covalue
Bertot, [2008] "Structural abstract interpretation, A formal study using Coq"
+ порт на Агду
В статье обсуждается кодирование внутри теории типов подхода к статическому анализу программ, известного как абстрактная интерпретация (АИ). Для анализа взят простой императивный язык с целочисленными значениями (можно ограничить до натуральных) со сложением и булевым сравнением, мутабельными переменными, последовательной композицией и while-циклами. Корректность полученного абстрактного интерпретатора доказана относительно аксиоматической (Хоаровой) семантики языка, а гарантия завершимости получается по построению.
Идея абстрактной интерпретации заключается в вычислении приближенных значений для некоторых аспектов поведения программы - обычно анализ делается по графу потока управления программы, но в статье анализируется напрямую синтаксическое дерево. Такую аппроксимацию, как правило, можно получить значительно быстрее, нежели исполнять саму программу, при этом на её основании можно проводить компиляторные оптимизации и делать выводы о корректности. Стандартным примером приближенного анализа является огрубление точных значений числовых переменных до бита четности или интервала значений. Классически при этом выводится аппроксимация "сверху" (overapproximation), т.е. мы хотим гарантировать отсутствие ложноотрицательных результатов за счет возможных ложноположительных (стандартный компромисс статического анализа). Формально отношения между точными (конкретными) и приближенными (абстрактными) множествами значений описываются в теории АИ через соответствия Галуа (пара функции абстракции α и функции конкретизации γ, необходимы для транспорта отношений порядка), в статье используется ad-hoc форма этой конструкции. Также требуется, чтобы домен абстрактных значений имел структуры полугруппы (т.к. моделируются числовые значения) и ограниченной (полу)решетки.
Для задания семантики анализируемого языка используется исчисление предусловий, состоящее из (1) бескванторных логических формул (предусловий/assertions) и аннотированных ими программ, (2) функции вычисления наислабейшего предусловия (формулы, которой должны удовлетворять переменные в начале исполнения) по аннотированной программе и (3) функции для генерации условий проверки (набор импликаций, которые, будучи валидными, гарантируют что любое исполнение программы, стартующее из удовлетворяющего предусловию состояния, будет удовлетворять всем последующим формулам). Для while-циклов также добавляются явные инварианты. Нужно заметить, что в самой статье полноценная аксиоматическая семантика c пред- и постусловиями не вводится, но это проделано в предыдущей статье автора, откуда я взял соответствующий кусок с доказательствами корректности аксиоматической семантики относительно операционной и корректности генератора условий. Ключевым же свойством генератора условий для корректности абстрактного интерпретатора является монотонность, т.е. валидность условий, построенных из некой формулы влечет валидность условий, построенных из её ослабления. Задача абстрактного интерпретатора - по исходной программе и абстрактному начальному состоянию одновременно вывести аннотированную программу и абстрактное конечное состояние.
В статье демонстрируется построение двух вариантов абстрактного интерпретатора, причем во втором, более продвинутом, сделана попытка обнаруживать незавершимость и мёртвые ветки кода. В качестве базовой инфраструктуры для обоих вариантов вводится таблица поиска (lookup table) для абстрактных состояний переменных (пары из имени переменной и абстрактного значения; отсутствующие переменные имеют по умолчанию значение верхнего элемента полурешетки) и набор функций для отображения этих состояний в логические формулы, каковые функции должны иметь ряд свойств (включающие, например, требования параметричности отображения и перевода верхнего элемента в тривиальную истину). Для верификации интерпретатора также нужна функция построения предиката внутри метатеории (теории типов) по его сигнатуре.
+ порт на Агду
В статье обсуждается кодирование внутри теории типов подхода к статическому анализу программ, известного как абстрактная интерпретация (АИ). Для анализа взят простой императивный язык с целочисленными значениями (можно ограничить до натуральных) со сложением и булевым сравнением, мутабельными переменными, последовательной композицией и while-циклами. Корректность полученного абстрактного интерпретатора доказана относительно аксиоматической (Хоаровой) семантики языка, а гарантия завершимости получается по построению.
Идея абстрактной интерпретации заключается в вычислении приближенных значений для некоторых аспектов поведения программы - обычно анализ делается по графу потока управления программы, но в статье анализируется напрямую синтаксическое дерево. Такую аппроксимацию, как правило, можно получить значительно быстрее, нежели исполнять саму программу, при этом на её основании можно проводить компиляторные оптимизации и делать выводы о корректности. Стандартным примером приближенного анализа является огрубление точных значений числовых переменных до бита четности или интервала значений. Классически при этом выводится аппроксимация "сверху" (overapproximation), т.е. мы хотим гарантировать отсутствие ложноотрицательных результатов за счет возможных ложноположительных (стандартный компромисс статического анализа). Формально отношения между точными (конкретными) и приближенными (абстрактными) множествами значений описываются в теории АИ через соответствия Галуа (пара функции абстракции α и функции конкретизации γ, необходимы для транспорта отношений порядка), в статье используется ad-hoc форма этой конструкции. Также требуется, чтобы домен абстрактных значений имел структуры полугруппы (т.к. моделируются числовые значения) и ограниченной (полу)решетки.
Для задания семантики анализируемого языка используется исчисление предусловий, состоящее из (1) бескванторных логических формул (предусловий/assertions) и аннотированных ими программ, (2) функции вычисления наислабейшего предусловия (формулы, которой должны удовлетворять переменные в начале исполнения) по аннотированной программе и (3) функции для генерации условий проверки (набор импликаций, которые, будучи валидными, гарантируют что любое исполнение программы, стартующее из удовлетворяющего предусловию состояния, будет удовлетворять всем последующим формулам). Для while-циклов также добавляются явные инварианты. Нужно заметить, что в самой статье полноценная аксиоматическая семантика c пред- и постусловиями не вводится, но это проделано в предыдущей статье автора, откуда я взял соответствующий кусок с доказательствами корректности аксиоматической семантики относительно операционной и корректности генератора условий. Ключевым же свойством генератора условий для корректности абстрактного интерпретатора является монотонность, т.е. валидность условий, построенных из некой формулы влечет валидность условий, построенных из её ослабления. Задача абстрактного интерпретатора - по исходной программе и абстрактному начальному состоянию одновременно вывести аннотированную программу и абстрактное конечное состояние.
В статье демонстрируется построение двух вариантов абстрактного интерпретатора, причем во втором, более продвинутом, сделана попытка обнаруживать незавершимость и мёртвые ветки кода. В качестве базовой инфраструктуры для обоих вариантов вводится таблица поиска (lookup table) для абстрактных состояний переменных (пары из имени переменной и абстрактного значения; отсутствующие переменные имеют по умолчанию значение верхнего элемента полурешетки) и набор функций для отображения этих состояний в логические формулы, каковые функции должны иметь ряд свойств (включающие, например, требования параметричности отображения и перевода верхнего элемента в тривиальную истину). Для верификации интерпретатора также нужна функция построения предиката внутри метатеории (теории типов) по его сигнатуре.
👍12
Forwarded from Covalue
Первый интерпретатор просто использует эти функции напрямую для рекурсивного аннотирования программы, не пытаясь вывести инварианты циклов (подставляя вместо них тривиально истинные формулы). Его корректность сводится к трем свойствам: (1) наислабейшее предусловие, полученное из вычисленного конечного состояния, действительно слабее предусловия, полученного из начального состояния, (2) все условия проверки, полученные из вычисленной аннотированной программы и конечного состояния, являются валидными и (3) вычисленная аннотированная программа идентична исходной программе после стирания аннотаций. Пример работы этого интерпретатора проиллюстрирован на домене битов четности со свободно добавленным верхним элементом (кодирующим отсутствие информации).
Второй интерпретатор более серьезно подходит к работе с циклами, используя информацию о том, что тест цикла всегда истинен внутри его тела и ложен на выходе. Незавершимость кодируется обертыванием конечного состояния в опциональный тип в выдаче интерпретатора. К параметрам добавляются две новые функции, которые вычисляют уточнения абстрактного состояния в зависимости от успешно и неуспешно пройденного теста цикла соответственно; именно эти функции берут на себя основную сложность задачи, в частности, они пытаются выводить информацию о незавершимости, и эта же информация позволяет пометить мертвый код тривиально ложными аннотациями. Схема процесса вывода инварианта цикла (в общем случае эта задача неразрешима!) выглядит так: (1) несколько абстрактных прогонов тела цикла (их количество контролируется эвристикой) с нарастающим расширением множества значений переменных - если процесс стабилизировался, инвариант найден; (2) если инвариант не найден, запускаем процесс 1 еще раз с переаппроксимацией для значений некоторых переменных - это позволяет ускорить процесс схождения (количество этих повторов также контролируется отдельной эвристикой); (3) если инвариант всё еще не найден, выбрать гарантированный инвариант (первый интерпретатор сразу же делает это, используя тривиальную истину); (4) сужение переаппроксимированных инвариантов повторным запуском интерпретатора (наличие этого шага приводит к определению интерпретатора через вложенную рекурсию).
Реализация этих шагов требует введения ряда вспомогательных функций-параметров, например, для сравнения количества информации в двух абстрактных значениях. Для доказательства корректности второго интерпретатора (состоящего из тех же трёх частей, что и в первом случае) также требуются 14 новых условий, описывающих все эти новые функции и их взаимодействие. Обе реализации интерпретаторов и их доказательства упакованы в модули, параметризующие их по абстрактному домену. Первый интерпретатор уже был ранее инстанцирован доменом чётности, а для второго описано кодирование домена числовых интервалов с потенциально бесконечными границами, где роль верхнего элемента играет интервал (-∞,+∞), а переаппроксимация заключается в замене одной из границ на -/+∞.
В заключение автор отмечает, что статью не следует рассматривать как полноценное введение в теорию АИ, а реализованные интерпретаторы являются моделями, т.к. оставляют желать лучшего в плане производительности - например, при вычислении аннотаций повторяется работа, уже проделанная ранее при поиске инварианта цикла. Кроме того, статический анализ может быть эффективнее, если рассматривать не отдельные переменные, а отношения между несколькими переменными.
#automatedreasoning
Второй интерпретатор более серьезно подходит к работе с циклами, используя информацию о том, что тест цикла всегда истинен внутри его тела и ложен на выходе. Незавершимость кодируется обертыванием конечного состояния в опциональный тип в выдаче интерпретатора. К параметрам добавляются две новые функции, которые вычисляют уточнения абстрактного состояния в зависимости от успешно и неуспешно пройденного теста цикла соответственно; именно эти функции берут на себя основную сложность задачи, в частности, они пытаются выводить информацию о незавершимости, и эта же информация позволяет пометить мертвый код тривиально ложными аннотациями. Схема процесса вывода инварианта цикла (в общем случае эта задача неразрешима!) выглядит так: (1) несколько абстрактных прогонов тела цикла (их количество контролируется эвристикой) с нарастающим расширением множества значений переменных - если процесс стабилизировался, инвариант найден; (2) если инвариант не найден, запускаем процесс 1 еще раз с переаппроксимацией для значений некоторых переменных - это позволяет ускорить процесс схождения (количество этих повторов также контролируется отдельной эвристикой); (3) если инвариант всё еще не найден, выбрать гарантированный инвариант (первый интерпретатор сразу же делает это, используя тривиальную истину); (4) сужение переаппроксимированных инвариантов повторным запуском интерпретатора (наличие этого шага приводит к определению интерпретатора через вложенную рекурсию).
Реализация этих шагов требует введения ряда вспомогательных функций-параметров, например, для сравнения количества информации в двух абстрактных значениях. Для доказательства корректности второго интерпретатора (состоящего из тех же трёх частей, что и в первом случае) также требуются 14 новых условий, описывающих все эти новые функции и их взаимодействие. Обе реализации интерпретаторов и их доказательства упакованы в модули, параметризующие их по абстрактному домену. Первый интерпретатор уже был ранее инстанцирован доменом чётности, а для второго описано кодирование домена числовых интервалов с потенциально бесконечными границами, где роль верхнего элемента играет интервал (-∞,+∞), а переаппроксимация заключается в замене одной из границ на -/+∞.
В заключение автор отмечает, что статью не следует рассматривать как полноценное введение в теорию АИ, а реализованные интерпретаторы являются моделями, т.к. оставляют желать лучшего в плане производительности - например, при вычислении аннотаций повторяется работа, уже проделанная ранее при поиске инварианта цикла. Кроме того, статический анализ может быть эффективнее, если рассматривать не отдельные переменные, а отношения между несколькими переменными.
#automatedreasoning
👍12
Я и мой студент, Кирилл Павлов, опубликовали статью "Библиотека llvm2py для анализа промежуточного представления LLVM и её применение в оценке степени распараллеливания линейных участков кода".
Чем может быть интересна работа студента второго курса бакалавриата? Анализ распараллеливания делается для варианта LLVM IR, где линейные участки заданы ярусно-параллельной формой (ЯПФ). Автоматическое построение ЯПФ позволяет узнать минимальное число шагов, за которое неограниченно параллельный LLVM-процессор может выполнить код линейного участка.
В реальных процессорах число параллельно работающих вычислительных элементов конечно. Поэтому важно экономить ресурсы: получить минимальную ширину ЯПФ, при которой достигается минимальное число шагов параллельной LLVM-машины. Так можно предварительно оценить выбор того или иного аппаратного ускорителя или же узнать, какой "шириной" должен обладать проектируемый нами ускоритель. В статье эта задача сводится к задаче программирования в ограничениях и эффективно решается с помощью инструментария Google OR-Tools.
P.S. Сама библиотека llvm2py, предназначенная для создания такого рода статических анализаторов кода LLVM IR, была полностью реализована Кириллом.
#llvm #analysis #solver
Чем может быть интересна работа студента второго курса бакалавриата? Анализ распараллеливания делается для варианта LLVM IR, где линейные участки заданы ярусно-параллельной формой (ЯПФ). Автоматическое построение ЯПФ позволяет узнать минимальное число шагов, за которое неограниченно параллельный LLVM-процессор может выполнить код линейного участка.
В реальных процессорах число параллельно работающих вычислительных элементов конечно. Поэтому важно экономить ресурсы: получить минимальную ширину ЯПФ, при которой достигается минимальное число шагов параллельной LLVM-машины. Так можно предварительно оценить выбор того или иного аппаратного ускорителя или же узнать, какой "шириной" должен обладать проектируемый нами ускоритель. В статье эта задача сводится к задаче программирования в ограничениях и эффективно решается с помощью инструментария Google OR-Tools.
P.S. Сама библиотека llvm2py, предназначенная для создания такого рода статических анализаторов кода LLVM IR, была полностью реализована Кириллом.
#llvm #analysis #solver
👍56
В ближайшее время в Москве пройдет три конференции, связанные с системным программированием, а, значит, и с компиляторами.
1. 11-12 декабря. Открытая конференция ИСП РАН. Часть программы уже опубликована. Для преподавателей отдельный интерес представляет круглый стол по проблемам образования в области системного программирования. Для компиляторщиков -- секция «Технологии анализа, моделирования и трансформации программ».
2. 20–21 марта. Хорошо известная C++ Russia 2025. Заявки до 28 декабря. На конференции регулярно бывают компиляторные доклады.
3. 22 марта. Sysconf 2025. Заявки до 15 декабря (возможно продление). Совершенно новая конференция по системному программированию. Компиляторы, низкоуровневое программирование, ... Здорово, что появилась отдельная конференция по такой тематике!
1. 11-12 декабря. Открытая конференция ИСП РАН. Часть программы уже опубликована. Для преподавателей отдельный интерес представляет круглый стол по проблемам образования в области системного программирования. Для компиляторщиков -- секция «Технологии анализа, моделирования и трансформации программ».
2. 20–21 марта. Хорошо известная C++ Russia 2025. Заявки до 28 декабря. На конференции регулярно бывают компиляторные доклады.
3. 22 марта. Sysconf 2025. Заявки до 15 декабря (возможно продление). Совершенно новая конференция по системному программированию. Компиляторы, низкоуровневое программирование, ... Здорово, что появилась отдельная конференция по такой тематике!
👍29
Дмитрий_Мельник_и_Иван_Кулагин_из_ИСП_РАН.pdf
886 KB
Недавно удалось лично пообщаться с несколькими известными преподавателями разработки компиляторов.
Евгений Зуев. Я был экспертом на его докладе. За семестр студентам необходимо разработать реализацию одного из возможных проектных языков. Преподаватель объясняет основы, используя мастер-язык. Идея мастер-языка мне показалась перспективной.
Иван Кулагин и Дмитрий Мельник. В рамках круглого стола они подготовили детальную презентацию с обзором своего и других известных компиляторных курсов. Слайды прилагаю. На уровне слухов: эти уважаемые коллеги из ИСП РАН собираются обновить материал своего курса, в том числе, с учетом презентации.
Дмитрий Булычев. Его курс по разработке компиляторов построен с точки зрения функционального программирования. Ранняя версия курса описана в статье. Особенность курса в использовании символических интерпретаторов для реализации различных компиляторных задач. Это очень красивая идея. На уровне слухов: возможно, стоит ожидать и учебник по разработке компиляторов от Дмитрия.
Евгений Зуев. Я был экспертом на его докладе. За семестр студентам необходимо разработать реализацию одного из возможных проектных языков. Преподаватель объясняет основы, используя мастер-язык. Идея мастер-языка мне показалась перспективной.
Иван Кулагин и Дмитрий Мельник. В рамках круглого стола они подготовили детальную презентацию с обзором своего и других известных компиляторных курсов. Слайды прилагаю. На уровне слухов: эти уважаемые коллеги из ИСП РАН собираются обновить материал своего курса, в том числе, с учетом презентации.
Дмитрий Булычев. Его курс по разработке компиляторов построен с точки зрения функционального программирования. Ранняя версия курса описана в статье. Особенность курса в использовании символических интерпретаторов для реализации различных компиляторных задач. Это очень красивая идея. На уровне слухов: возможно, стоит ожидать и учебник по разработке компиляторов от Дмитрия.
👍32
Forwarded from sysconf — канал конференции
#видеозаписи
Начинаем публиковать видео докладов sysconf 2025. Первым — выступление Петра Советова «Генератор случайных процессорных архитектур для обучения системному программированию»
YouTube | VK Видео
Скачать презентацию с сайта sysconf
Начинаем публиковать видео докладов sysconf 2025. Первым — выступление Петра Советова «Генератор случайных процессорных архитектур для обучения системному программированию»
YouTube | VK Видео
Скачать презентацию с сайта sysconf
YouTube
Петр Советов — Генератор случайных процессорных архитектур для обучения системному программированию
Подробнее о конференции sysconf: https://jrg.su/Czu8Za
— —
Скачать презентацию с сайта sysconf — https://jrg.su/ezRsdM
Что нужно для масштабируемой проверки знаний и навыков будущих системных программистов? Нужно дать каждому студенту индивидуальные, нетривиальные…
— —
Скачать презентацию с сайта sysconf — https://jrg.su/ezRsdM
Что нужно для масштабируемой проверки знаний и навыков будущих системных программистов? Нужно дать каждому студенту индивидуальные, нетривиальные…
👍33
В наше время может сложиться впечатление, что компиляторы вне LLVM уже не создаются. Это, конечно, не так и я хочу привести в пример два небольших компилятора, над которыми я работал в последнее время.
1. Компилятор HOREC из статьи HOREC: компилятор специализированных регулярных выражений для проектирования программируемой и ресурсоэффективной аппаратной архитектуры.
2. DSL-компилятор для проекта учебной игровой приставки Брус-16.
Использование LLVM в этих проектах оказалось бы, по меньшей мере, избыточным.
1. Компилятор HOREC из статьи HOREC: компилятор специализированных регулярных выражений для проектирования программируемой и ресурсоэффективной аппаратной архитектуры.
2. DSL-компилятор для проекта учебной игровой приставки Брус-16.
Использование LLVM в этих проектах оказалось бы, по меньшей мере, избыточным.
👍31