Telegram Web
На Хабре несколько дней назад появилась статья, популярно поясняющая знаменитую технику реализации языка Scheme - Cheney on the M.T.A. Статья излагает историю названия и объясняет работу остроумного подхода к сборке мусора.

Исходный код Scheme здесь сначала должен быть преобразован в представление с продолжениями (см., например, книгу Compiling with Continuations). Функции этого представления один к одному компилируются в функции на языке C. Многочисленные временные значения, характерные для Scheme, сначала размещаются на стеке вызовов C. Во время работы программы стек вызовов функций C будет расти, так как при компиляции с продолжениями функции не возвращаются к точке исходного вызова.

При превышении допустимого размера стек сбрасывается вызовом longjmp. Размер проверяется, например, через численное значение адреса временной переменной. Перед сбросом живые значения из стека перемещаются в кучу для зачистки алгоритмом Чейни, мертвые же значения отбрасываются автоматически.

Техника сильно упрощает компиляцию Scheme в C (например, рекурсивные вызовы и их оптимизацию, легко выражаются продолжения), из-за чего ее используют минимум два популярных компилятора: Cyclone и Chicken.

Статья на Хабре: https://habr.com/ru/company/ruvds/blog/540502/

Подробности реализации техники от разработчика Chicken Scheme:
https://www.more-magic.net/posts/internals-gc.html

Реализация Cyclone: https://justinethier.github.io/cyclone/docs/Garbage-Collector

Оригинальная публикация по Cheney on the MTA: http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=3A988CF024FE807165D1CFA957445BC8?doi=10.1.1.54.7143&rep=rep1&type=pdf

Алгоритм сборки мусора Чейни: https://people.cs.umass.edu/~emery/classes/cmpsci691s-fall2004/papers/p677-cheney.pdf

Компиляторы, использующий другие подходы к компиляции в язык C:

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.50.8424&rep=rep1&type=pdf - Bigloo - компилятор Scheme и Standard ML

https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.48.8788&rep=rep1&type=pdf - Gambit - компилятор Scheme

#garbagecollection #scheme
https://grosskurth.ca/bib/1997/cardelli.pdf
"Program Fragments, Linking, and Modularization" Luca Cardelli.

Статья поднимает вопрос корректности раздельной компиляции и линковки, и потому — я считаю — обязательна к прочтению для всех авторов языков программирования! 😃

Уже во введении на простейшем примере создания воображаемой программы, состоящей всего из двух модулей, разрабатываемых независимо, автор иллюстрирует, наверное, все проблемы, при этом возникающие. Между делом Карделли упоминает публичные репозитории артефактов (типа Maven Central или Nuget. Напомню, что статья опубликована в 1996 году!). Многие из обозначенных проблем линковки раздельно скомпилированных модулей до сих пор не решены ни в мейнстримных, ни в исследовательских языках.

В качестве основного результата Карделли предлагает, вероятно, первую формальную модель раздельной компиляции и последующей линковки, позволяющую строго рассмотреть вопрос о корректности этих процессов. Корректность в этом смысле приведённой простейшей системы модулей для просто типизированного лямбда-исчисления (в качестве модельного языка) формально доказывается. Автор, конечно же, указывает на необходимость расширения модели как в сторону более развитых языков (параметрический полиморфизм, ООП), так и в сторону более сложных систем модулей (параметризованные модули, "функторы" в духе Standard ML, первоклассные модули). Существуют ли такие работы, непосредственно продолжающие это исследование, мне не известно.

Однако, в качестве related work и дальнейшего чтения могу указать на работы по формализации (и доказательству корректности) раздельной компиляции для языка C в рамках проекта CompCert.

#separatecompilation #linking #modules #stlc
Распределение регистров и планирование инструкций - важные аспекты реализации бэкенда компилятора. Обе задачи NP-полны и связаны между собой: распределение может внести в код новые инструкции, планирование же меняет инструкции местами. Несмотря на это в популярных компиляторах решаются они, как правило, раздельно и используют эвристические подходы.

Последние два десятилетия много исследований было посвящено точным комбинаторным методам решения тех же самых задач: предложены методы на основе целочисленного программирования, PBQP, программирования в ограничениях и др. Слабость таких подходов - большое время поиска оптимальных решений, что заставляет исследователей упрощать задачу, делая методы неприменимыми в универсальных компиляторах.

Роберто Лозано (Roberto Castaneda Lozano) задался целью разработать одновременно точный и легкий в реализации подход, причем решающий задачи планирования инструкций и распределения регистров совместно. За основу он взял программирование в ограничениях (constraint programming), позволяющее удобно выразить условия обеих задач и для которого существуют мощные решатели.

Проект Unison заменяет три фазы LLVM: предварительное планирование инструкций, распределение регистров и финальное планирование. Распределение проводится глобальное, планирование же локальное - последнее упрощение дает ощутимый эффект при умеренной сложности.

В отличие от предшественников Unison не упрощает задачу распределения. Все практические аспекты проблемы учитываются в решениях: спиллинг, алиасинг (aliasing), рематериализация (rematerialisation), разбиение областей жизни переменных (live range splitting), слияние (coalescing) и др. Программирование в ограничениях позволяет выразить любые проблемы распределения регистров лаконично и просто.

Оптимальность имеет свою цену: поиск решений занимает много времени. Размер компилируемых функций - до 1000 инструкций. Наибольший эффект от Unison был показан на спецпроцессоре Hexagon с длинным машинным словом (VLIW), где важно оптимальное расписание: на некоторых тестах реальное время исполнения снижается на 40%.

Лозано предлагает использовать Unison как инструмент для порождения кода к спецпроцессорам, оценки эффективности эвристических решений, поиска оптимальных решений в отдельных функциях.

Презентация на конференции LLVM (2017): https://www.youtube.com/watch?v=kx64V74Mba0

Обобщающая исследования Лозано диссертация (2018 год): http://kth.diva-portal.org/smash/get/diva2:1232941/FULLTEXT01.pdf

Оценка производительности Unison (2017): https://www.diva-portal.org/smash/get/diva2:1119107/FULLTEXT01.pdf

Сайт проекта: https://unison-code.github.io/

Программирование в ограничениях: https://ru.wikipedia.org/wiki/Программирование_в_ограничениях

Программная статья от именитых исследователей (Nuno P. Lopes и John Regehr) о роли точных методов в будущих компиляторах: https://arxiv.org/pdf/1809.02161.pdf

#registeralloc #instructionscheduling #constraintprogramming #unison #llvm
https://hal.inria.fr/hal-01499946/document
"A modular module system", Xavier Leroy

Утверждение, что (ML-style) система модулей не зависит от "базового" языка программирования, и может быть реализована почти для любого, а не только ML, широко известно и озвучивалось в литературе. Данная статья приводит конструктивное доказательство этого тезиса, реализуя такую (слегка упрощённую) систему модулей, в виде, явно параметризованном относительно синтаксиса и системы типов базового языка.

Несмотря на ряд упрощений по сравнению с системой модулей того же Standard ML, представленная модельная система содержит (и корректно реализует) все базовые возможности, включая структурную типизацию модулей, абстрактные типы, функторы, зависимость (типа) результата функтора от (типа) аргумента а также равенства между (абстрактными) типами.

> All in all, module type matching resembles subtyping in a functional language with records, with some extra complications due to the dependencies in functor types and signatures.

Статья составлена в духе Literate Programming, перемежая пояснительный текст и реальный рабочий код на языке OCaml. Реализация системы модулей ML с помощью системы модулей ML отсылает к традиции метациркулярных интерпретаторов Лисп. Леруа выражает надежду, что такой способ представления материала не только не запутает читателя, но и дополнительно прояснит связь конкретного и абстрактного синтаксиса как и практическую полезность (и даже необходимость) всех возможностей представленной системы. (По-видимому, метациркулярность системы не оставила Лисперов равнодушными, что привело к появлению реализации MiniML с полноценной системой модулей на Scheme: http://wiki.call-cc.org/eggref/4/miniML 😊)

Для иллюстрации приводятся два примера "надстраивания" реализованной системы модулей над "упрощённым C" в качестве императивного (процедурного) базового языка и Mini-ML в качестве функционального, приближенного к используемым на практике, в частности, реализующего типы высших порядков (Higher-Kinded Types).

Кратко обсуждаются вопросы (модульной) компиляции таких модулей. Упоминаются три основных варианта: компиляция самих модулей в виде структур данных, а функторов — в виде (полиморфных) функций, специализация функторов для всех применений в духе C++ templates и полное стирание модулей во время компиляции (аналогично девиртуализации вызовов методов в ООП). Но за деталями интересующиеся читатели отсылаются к соответствующим публикациям.

В заключительной части Леруа обсуждает ряд расширений модельной системы модулей — как реализованных на практике, так и не до конца проработанных даже в теории — но уже без фактической реализации.

Таким образом, статья представляет собой практическое введение в ML-style системы модулей и связанные вопросы, полезное как для пользователей таких систем, так и для авторов языков программирования, желающих реализовать собственную систему модулей. 😊

#modules #sml #ocaml #leroy #classic
В традиционных алгоритмах распределения регистров на основе задач упаковки в контейнеры или раскраски графов трудно учесть дополнительные ограничения на доступ к регистрам.

Речь идет об архитектурах с нерегулярным доступом к регистрам (register aliasing, ограничения на использование конкретных регистров в командах). И это относится к x86, но в еще большей мере — к DSP-процессорам и другим специализированным архитектурам.

За последние 3 десятилетия исследователи предложили несколько подходов к проблеме, в том числе метод на базе задачи о квадратичном присваивании (quadratic assignment problem, или QAP), верней частном ее случае: partitioned boolean quadratic optimization problem, или PBQP.

Бернард Шольц (Bernhard Scholz) в работе 2002 года сформулировал распределение регистров как задачу PBQP и показал, что метод позволяет моделировать особенности сложных архитектур. PBQP - NP-полная задача, поэтому впоследствии для метода были разработаны эффективные эвристики, делающие время поиска решений приемлемым.

Интересным метод является не только из-за применимости к отдельным архитектурам:

- возможно регулировать время работы решателя, то есть алгоритм становится прогрессивным;
- решатель может, применяя или не применяя эвристику, находить субоптимальные или оптимальные решения;
- алгоритм пытается избегать применения эвристики и в большинстве случаев находит оптимальные решения.

Наилучшие относительно других подходов результаты PBQP показывает именно в нерегулярных архитектурах, ради которых решатель PBQP был реализован сначала в libfirm, после - и в LLVM.

Впоследствии исследования применимости PBQP в распределении регистров и порождении кода вдохновили эксперименты в применении метода, например, к тестированию памяти или методам машинного обучения.

Понятия регулярности и ортогональности архитектур процессоров в классической работе (1981): https://www.cs.auckland.ac.nz/compsci703s1c/resources/Wulf.pdf

Оригинальная публикация, представляющая PBQP (2002): http://www.complang.tuwien.ac.at/scholz/publications/lctes02.ps.gz

Развитие идей, обновленный алгоритм и новая эвристика (2006): https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.131.4551&rep=rep1&type=pdf

Разработчики libfirm о применении к SSA (2011): https://link.springer.com/content/pdf/10.1007/978-3-642-19861-8_4.pdf

Неформальный пост от разработчиков libfirm (2011): https://beza1e1.tuxen.de/articles/pbqp.html

Сама задача: https://en.wikipedia.org/wiki/Quadratic_assignment_problem

Тестирование памяти (2020): https://dl.acm.org/doi/fullHtml/10.1145/3427378

Машинное обучение (2018): https://arxiv.org/pdf/1710.01079.pdf

#pbqp #registeralloc #libfirm #llvm
Уильям Вульф (William Wulf) - исследователь в области компиляторов, сотрудничавший со знаменитой компанией DEC. Вульф - создатель раннего оптимизирующего компилятора языка BLISS и один из авторов классической книги The Design of an Optimizing Compiler (1975).

После работы над BLISS команда Вульфа переключилась на амбициозный проект PQCC (Production-Quality Compiler-Compiler Project), в рамках которого шла работа над универсальным компилятором компиляторов, целью которого было порождение всех этапов компилятора для новых архитектур из декларативных описаний - актуальной проблемы для DEC, продававшей разнородные платформы (семейства PDP и VAX, позже - Alpha).

Статья Compilers and Computer Architecture (1981) - выводы из этой работы. В ней Вульф указывает, что экономику разработки новых архитектур нельзя рассматривать без стоимости разработки сопутствующего компилятора. То есть дизайн набор инструкций нельзя создавать без учета будущих компиляторов.

Исходя из этих наблюдений Вульф предлагает принципы разработки компьютерных архитектур общего назначения:

1. Регулярность (regularity) - должен быть один способ делать что-либо, и он должен быть применим везде (например, ADD работает для всех регистров и типов данных).

2. Ортогональность (orthogonality) - аспекты архитектуры должны обсуждаться независимо, без взаимного влияния (режим адресации, к примеру, не должен влиять на выбор примитивов).

3. Композиционность (composability) - в регулярной и ортогональной архитектуре можно соединить различные аспекты произвольным образом (каждая из инструкций поддерживает работы с любым регистром и режимом адресации).

От базовых принципов статья переходит к принципам-следствиям: вопросам адресации, выбора примитивов, отклонения от принципов. Интересный вывод касается поддержки примитивов, специфичных для конкретных языков высокого уровня: "In many cases these turn out to be more trouble than they are worth".

Это очень интересная и по-прежнему актуальная статья от одного из известнейших специалистов по компиляторам своей эпохи. Пересказывать ее полностью нет смысла, остается только рекомендовать интересующимся темой компьютерных архитектур и неотделимой от нее темой разработки компиляторов.

Compilers and Computer Architecture (1981) - статья

https://en.wikipedia.org/wiki/William_Wulf - автор

https://en.wikipedia.org/wiki/BLISS - известнейшая работа автора

https://en.wikipedia.org/wiki/The_Design_of_an_Optimizing_Compiler - классическая книга автора

#bliss #pqcc #architecture #isa #history
Представленный в 1969 году компилятор Fortran-H применял множество прежде трудных оптимизаций. Ключом к ним стала новаторская техника статического анализа: использование доминаторов узлов графа потока исполнения програмы.

Доминатором заданного узла называют такой узел, через который проходят все пути от входного узла к заданному. Непосредственные (то есть ближайшие к каждому из узлов) доминаторы образуют дерево доминаторов с корнем во входном узле графа.

Fortran-H показал, что в сочетании с анализом потоков данных отношение доминирования позволяет расширить до глобальной область применения локальных оптимизаций. К примеру, при помощи доминаторов проводилось удаление общих подвыражений: если среди доминаторов текущего узла уже вычислялось какое-либо выражение и ни один из операндов на пути к узлу не менялся, то результат выражения можно не вычислять повторно.

Одной из проблем использованного в Fortran-H метода поиска доминаторов стала высокая алгоритмическая сложность. Алгоритм Пурдома-Мура (Purdom-Moore, по именам разработчиков компилятора) элементарно объясняется и реализуется, но имеет квадратичную сложность.

Более эффективная версия алгоритма сложностью в O(m*log n) будет представлена только через 10 лет в статье 1979 года A Fast Algorithm for Finding Dominators in a Flowgraph за авторством Томаса Ленгауэра (Thomas Lengauer) и Роберта Тарьяна (Robert Tarjan).

Несмотря на наличие эффективного алгоритма доминаторы широко не использовались, пока в знаменитой публикации 1989 года (Efficiently Computing Static Single Assignment Form and the Control Dependence Graph) доминаторы не были использованы для размещения phi-узлов при построении SSA.

На волне обновленного интереса были предложены новые применения доминаторов: глобальная нумерация значений, глобальное планирование инструкций и прочие. Исследователи стали предлагать альтернативные алгоритмы поиска доминаторов, которые, впрочем, широкого распространения не получили, а алгоритм Ленгауэра-Тарьяна (или просто ЛТ) до сих пор широко используется, в том числе в GCC и LLVM.

https://en.wikipedia.org/wiki/Dominator_(graph_theory)

https://www.cs.princeton.edu/courses/archive/fall03/cs528/handouts/a%20fast%20algorithm%20for%20finding.pdf - алгоритм Ленгауэра-Тарьяна (1979)

https://www.researchgate.net/profile/Edward-Lowry/publication/220421196_Object_code_optimization/links/564ca77708aedda4c13432b4/Object-code-optimization.pdf - описание реализации Fortran-H (1969), где впервые формулируется алгоритм Пурдома-Мура.

http://pages.cs.wisc.edu/~fischer/cs701.f08/ssa.pdf - получение SSA (1989)

https://www.doc.ic.ac.uk/~livshits/classes/CO444H/reading/dom14.pdf - предложение Купера по получению доминаторов путем анализа потоков данных (2001)

https://github.com/gcc-mirror/gcc/blob/master/gcc/dominance.c - реализация алгоритма ЛТ в GCC

#dominator #lengauertarjan #fortranh #llvm #gcc
https://dl.acm.org/doi/pdf/10.1145/3428297
Macros for Domain-Specific Languages

"Yo dawg I heard you like macros so I put macros in your macros so you can expand while you expand!"

Как ни забавно, эта фраза верно передаёт содержание статьи, а именно, два главных нововведения авторов: 1) введение пользовательской макросистемы для разрабатываемого пользователем же DSL (на макросах хост-языка, Racket в данном случае), и 2) переиспользование macro expander из хост-языка для реализации пользовательской системы макросов (за счёт предоставления API к определённым функциям macro expander).

Звучит круто, но зачем это нужно? Почему нельзя обойтись макросами хост-языка? На это снова можно выделить две причины.

Первое — это новые name binding constructs, работающие не так, как в хост-языке. Например, в статье рассматривается реализация PEG DSL, в котором конструкции захвата подвыражения и связывания его с именем могут находиться внутри звезды Клини. Но в таком случае эти имена связываются не с одним подвыражением, а со всем подсписком внутри списка выражений, порождённого звездой Клини. Например, в выражении
(define-peg arith-expr
(=> (seq (: e1 term) (* (seq (: op* (alt "+" "-")) (: e* term))))
(left-associate-binops e1 op* e*)))
идентификаторы op* и e* связываются со списками операторов и термов соответственно (так как находятся "под звёздочкой"), в то время как e1 связывается с одним термом.

По сравнению со стандартным связыванием имён в функциях или let-выражениях такие связывания работают "шиворот навыворот", а потому требуют реализации "руками". В данном примере такая реализация написана авторами PEG DSL на макросах хост-языка, но если мы хотим чтобы пользователи DSL могли запрограммировать binding constructs по собственному вкусу, нам придётся предоставить им развитую макро-систему поверх нашего DSL.

Вторая причина связана с тем, что авторы называют "hosted DSL". Мне кажется, иначе это можно было бы назвать "deeply embedded DSL". Суть в том, что DSL, который мы реализуем на макросах, является не просто синтаксическим сахаром, а требует полноценного конвейера компиляции, начиная (потенциально) с парсера вводимого нами синтаксиса, продолжая специфическим разрешением имён, нетривиальными binding context и scoping rules, возможно, проверкой типов или другим статическим анализом корректности программ, и заканчивая полноценным IR и оптимизациями. Для того чтобы дать пользователям писать макросы для такого DSL с помощью макро-системы хост-языка, нам придётся открыть доступ к внутренностям нашего компилятора чтобы пользователи могли порождать AST или даже IR нашего DSL, и "скармливать" его далее компилятору. В противном случае макросы смогут порождать только разрозненные куски (скомпилированного) DSL, связанные между собой вызовами анонимных (или не очень) функций хост-языка, которые компилятор нашего DSL проанализировать и оптимизировать уже не сможет.

Так вот, чтобы получить преимущества и того, и другого, нам придётся предоставить отдельную макро-систему поверх нашего hosted DSL. А поскольку реализовать хорошую макросистему (гигиеничную, с разделением фаз и интегрирующуюся с системой модулей хост-языка) очень непросто, было бы полезно переиспользовать возможности macro-expander хост-языка. Статья предлагает API, позволяющий это сделать.

#scheme #racket #macros #dsl
Некоторые идеи опережают свою эпоху на десятилетия. Автор данной заметки к оным безусловно относит систему META II, представленную еще в 1964 году. Среди прочих эта работа впечатлила Дональда Кнута, послужив одним из источников вдохновения для атрибутных грамматик.

Автор всего на 6 страницах легкого текста статьи[1] описывает виртуальную машину для разбора входной строки и предметно-ориентированный язык, схожий с расширенной версией БНФ (форме Бэкуса-Науэра). В качестве иллюстрации возможностей META II показано, как этот предметно-ориентированный язык позволяет транслировать выражения из упрощенного варианта Алгола (VALGOL) в инструкции абстрактной стековой машины; естественно, что и языки алгебраических выражений[3] тоже легко разбираются META II.

Но самый интересный аспект META II это возможность метакомпиляции: опорный предметно-ориентированный язык можно выразить в терминах самого себя, что позволяет пошагово расширять исходные виртуальную машину и язык (см. инструкцию в [3]). Предполагалось, что пользователи реализуют виртуальную машину (всего 19 инструкций), после чего, запустив на ней код для языка META II, будут раскручивать компилятор до нужного состояния. Более того, первая версия META II тоже была написана на метаязыке-предшественнике (META), после чего повторно реализована уже на самой META II. Кульминацией публичных исследований автора стал язык TREE-META[2], применявший те же идеи к преобразованию дерева абстрактного синтаксиса.

Помимо теоретических работ Кнута META II стала предтечей более современного формализма - PEG, который набирает все большую популярность в прикладных разработках[4]. Схожие идеи легли в основу систем OMeta[5] и Ohm[6]. О META II тепло отзывались Алан Кэй, Джо Армстронг и другие известные ислледователи языков программирования. В Интернете можно найти множество реализаций виртуальной машины META II, среди которых и версия для Python 3[7] от автора заметки.

Литература:
1. http://www.chilton-computing.org.uk/acl/literature/reports/p025.htm - исходная публикация
2. https://en.wikipedia.org/wiki/TREE-META - кульминация развития исходной системы авторами
3. http://www.bayfronttechnologies.com/mc_tutorial.html - подробная интерактивная демонстрация возможностей метакомпилирующих систем, отталкивающееся от META II
4. https://www.python.org/dev/peps/pep-0617/ - реализация разбора в Python 3
5. https://en.wikipedia.org/wiki/OMeta - современное развитие идей META II
6. https://ohmlang.github.io/ - еще более современная система
7. https://github.com/vkazanov/pymetaii - реализация META II на Python 3 от автора данной заметки
8. https://github.com/stevenbagley/metaii - реализация на Common Lisp
9. https://github.com/EyeBool/Meta-II-Compiler - реализация на C++
10. https://github.com/siraben/meta-II - реализация на Scheme

#classic #parsing #metaii #peg
https://arxiv.org/pdf/2002.06187v1.pdf
Reusing Static Analysis across Different Domain-Specific Languages using Reference Attribute Grammars

Авторы немного поскромничали с названием статьи — в работе используются не просто ссылочные атрибутные грамматики (Reference Attribute Grammars, RAGs), а их расширение — реляционные ссылочные атрибутные грамматики (Relational Reference Attribute Grammars) и конкретно фреймворк JastAdd.

Если говорить совсем по-простому, то авторы предлагают решение аналога Expression Problem в области языков и алгоритмов статического анализа (N языков x M алгоритмов) при помощи языка промежуточного представления (Intermediate Representation, IR). Идея не нова, но есть нюанс. 😊

При традиционном подходе к (универсальному) IR, как, например, в проекте LLVM, один и тот же IR используется для всех типов статического анализа и трансформаций. С одной стороны, это действительно позволяет переиспользовать алгоритмы анализа для всех языков, которые транслируются в данный IR. Но с другой стороны, такой IR с необходимостью должен содержать информацию, требующуюся каждому реализованному алгоритму и преобразованию. Это приводит к "раздуванию" IR, как видно по тому же LLVM, но также это приводит и к "радуванию" транслятора язык->IR, поскольку разработчику приходится строить корректный IR со всей требуемой информацией даже если он использует только один алгоритм анализа, который опирается на одну десятую доступных данных. Это едва ли можно считать проблемой General-Purpose фреймворка, но для работы с Domain-Specific языками может заметно повысить сложность и трудоёмкость реализации.

Другой пример нежелательного дублирования может возникнуть при применении одного и того же алгоритма к разным элементам IR. Так, авторы рассматривают применение алгоритма нахождения циклических зависимостей в программах на Java как на уровне классов, так и на уровне пакетов. Поскольку в IR эти концепции будут представлены разными узлами, применение в точности одного и того же алгоритма к ним может оказаться невозможно, и потребует дублирования кода. Разумеется, на этот фактор влияют как встроенные возможности обобщённого программирования языка реализации, так и архитектура системы анализа и трансформации вокруг IR.

Но авторы предлагают подход, по построению лишённый указанных проблем: для каждого вида и алгоритма статического анализа использовать собственный IR, содержащий только ту информацию, которая необходима, и ничего лишнего! 😊

Несомненно, такой подход был бы крайне неудобным и неэффективным, если бы не фреймворк реляционных ссылочных атрибутных грамматик. Он зиждится на нескольких столпах:

1. нетерминальные атрибуты (Nonterminal Attributes, NTA aka Higher-Order Attributes) позволяют лаконично и декларативно задавать преобразования AST->AST, что сильно облегчает построение специализированных IR для каждого отдельного вида статического анализа;

2. ссылочные атрибуты позволяют добавлять рёбра, связывающие произвольные узлы, превращая дерево в направленный граф общего вида, что сильно расширяет спектр применимых алгоритмов анализа;

3. наконец, отношения (Relations) между узлами задают рёбра "внешним" по отношению к графу способом, что позволяет "автоматически" получить ссылки из узлов IR к соответствующим узлам в исходном дереве DSL.

В качестве иллюстрирующих примеров авторы приводят уже упомянутый анализ циклов как для DSL, описывающего конечные автоматы, так и для языка Java на уровне классов и пакетов по отдельности, и алгоритм выявления случаев "затенения" переменных, снова для Java и для языка Modelica.

Для полноты картины, авторы приводят результаты анализа производительности реализованных алгоритмов на наборе открытых Java-проектов по сравнению с традиционной реализацией на основе паттерна "посетитель" (Visitor Pattern). Благодаря механизмам мемоизации внутри фреймворка Relational RAGs (использовался JastAdd), производительность не уступает, а в некоторых случаях и превосходит традиционную реализацию, которую невозможно переиспользовать.
Тем не менее несколько моментов вызывают вопросы, если не к подходу в целом, то к его реализации в JastAdd.

Во-первых, как упоминалось ранее, отношения (Relations) задаются "внешним" по отношению к дереву образом, и авторы для этого используют обычный императивный код на Java, да ещё и опирающийся на неявные, генерируемые фреймворком методы. Мне такой способ не кажется декларативным и особо высокоуровневым.

Во-вторых, несмотря на то, что дерево разбора превращается в направленный граф общего вида, возможность реализации Control Flow Analysis и Data Flow Analysis остаётся под вопросом. Возможно, этому мешают ограничения на неизменяемость графа, связанные с мемоизацией (в свою очередь, необходимой для эффективной работы алгоритмов). В частности, это накладывает ограничения на построение отношений между "обычными" и узлами в NTA.

В любом случае, для прояснения деталей предлагаемого подхода читателю предлагается ознакомиться со статьёй, благо, она достаточно проста для понимания. Механизм Relational RAGs весьма мощный и универсальный – его полезно иметь в виду при реализации самых разных аспектов работы с языками программирования, не только статического анализа. 😊

#dsl #rag #static #analysis
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
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
За этим следует оптимизационный шаг constraint elimination. Предыдущий проход, декомпозиция, создает большое количество избыточных guard-команд, что упрощает верификацию алгоритма, но снижает быстродействие получаемого кода, поэтому данный этап нацелен на их стирание. Тут используется еще одно IR - PolyLoopSimpl, куда добавлен примитив simplify, минимизирующий политоп по заданному ограничению.

Последний шаг - трансляция программы в AST Loop, состоящее из классических команд типа if и for, которое и является результатом работы кодогенератора. Основная задача на этом этапе - трансляция loop-команд.

Полученный кодогенератор (фактически, аналог CLooG) может быть экстрагирован в Окамл и позволяет получать модели императивных программ из полиэдрального представления, впрочем, работающего фронтенда у него нет, так что представления нужно расписывать вручную.

Формализация на Coq (около 8 тысяч строк) потребовала реализовать небольшую библиотеку для линейной алгебры, операции для работы над политопами, а также описать семантику промежуточных представлений и доказать соответствующие теоремы о корректности трансляции в Loop. Как правило, верификация компиляторных проходов делается либо через доказательства сохранения семантики, либо методом валидации трансляции. В статье использована их комбинация - валидация для полиэдральных операций и доказательства для семантик всех проходов кодогенератора. Здесь заметно, что статья является продолжением линии французских работ по (в том числе верифицированным) полиэдральным методам - дается ряд ссылок на предшественников.

В заключении дан обзор методов полиэдральной кодогенерации, упомянуты применения для верификации нейросетей. Также сообщается о найденной потенциальной ошибке, связанной с упорядочиванием трёх и более политопов в алгоритме генерации циклов Quillere [2000]. Авторы выражают желание в будущем заняться верификацией непосредственно оптимизаций и реализовать генерацию С кода из Loop AST, как шаг к добавлению полиэдрального оптимизатора в CompCert. Основная потенциальная проблема - переход от арифметики произвольной точности к операциям с переполнениям.

#codegen #coq #polyhedral #verification
На днях, и даже в одно и то же время, прошли два ежегодных российских мероприятия, в том числе и на темы языков и компиляторов. Это -- Национальный Суперкомпьютерный Форум (НСКФ) и Открытая конференция ИСП РАН.

По НСКФ доступны тезисы докладов: https://2021.nscf.ru/nauchno-prakticheskaya-konferenciya/tezisy-dokladov/
В телеграм-канале Открытой конференции есть ссылки на видеозаписи докладов: https://www.tgoop.com/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://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
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, и оптимизации. И потому представляют собой интереснейшее расширение "поля деятельности компиляторщиков" в сравнительно новую, но стремительно набирающую популярность, область.
Первая часть цикла докладов об автоматизации программирования в СССР доступна на 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/
Эта небольшая заметка посвящена нескольким новостям по нашей тематике.

Во-первых, хочу напомнить, что в июне прошла конференция 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
2024/11/23 03:50:54
Back to Top
HTML Embed Code: