Авторы оценивают верхнюю и нижнюю границы вычислительной сложности статического анализа указателей Андерсена (APA) и приводят свои варианты реализации APA.
The Fine-Grained Complexity of Andersen’s Pointer Analysis
https://arxiv.org/pdf/2006.01491.pdf
#analysis
The Fine-Grained Complexity of Andersen’s Pointer Analysis
https://arxiv.org/pdf/2006.01491.pdf
#analysis
Unsupervised Translation of Programming Languages
Довольно любопытная статья на тему создания транскомпилятора от исследователей из Facebook AI Research.
Путем тренировки модели, на корпусе программ из Github, транслируют код языков C++, Java, Python.
Авторы показывают, что их модель превосходит работы в данной области, основанные на подходе
использования правил. Из интересного, прямой цитатой из статьи:
Paper:
https://arxiv.org/pdf/2006.03511
Video:
https://www.youtube.com/watch?v=xTzFJIknh7E&app=desktop
#ml #analysis #transpilation
Довольно любопытная статья на тему создания транскомпилятора от исследователей из Facebook AI Research.
Путем тренировки модели, на корпусе программ из Github, транслируют код языков C++, Java, Python.
Авторы показывают, что их модель превосходит работы в данной области, основанные на подходе
использования правил. Из интересного, прямой цитатой из статьи:
• We introduce a new approach to translate functions from a programming language to another,В видео можно послушать комментарии.
that is purely based on monolingual source code.
• We show that TransCoder successfully manages to grasp complex patterns specific to each
language, and to translate them to other languages.
• We show that a fully unsupervised method can outperform commercial systems that leverage
rule-based methods and advanced programming knowledge.
• We build and release a validation and a test set composed of 852 parallel functions in 3
languages, along with unit tests to evaluate the correctness of generated translations.
• We will make our code and pretrained models publicly available.
Paper:
https://arxiv.org/pdf/2006.03511
Video:
https://www.youtube.com/watch?v=xTzFJIknh7E&app=desktop
#ml #analysis #transpilation
YouTube
TransCoder: Unsupervised Translation of Programming Languages (Paper Explained)
Code migration between languages is an expensive and laborious task. To translate from one language to the other, one needs to be an expert at both. Current automatic tools often produce illegible and complicated code. This paper applies unsupervised neural…
Подход к выявлению "семантического клонов" в программе. Основан на насыщении равенствами и забытой концепции Programmer’s Apprentice. Утверждается, что работает лучше, чем популярное в этой области представление PDG.
Semantic Code Search via Equational Reasoning
https://dl.acm.org/doi/pdf/10.1145/3385412.3386001
#analysis
Semantic Code Search via Equational Reasoning
https://dl.acm.org/doi/pdf/10.1145/3385412.3386001
#analysis
В рамках PLDI Alex Aiken (известный многим по курсам компиляторостроения) рассказал о проекте TASO -- это автоматический синтез графовых оптимизирующих преобразований для нейросетевых фреймворков. Перечисляются все графы-шаблоны нейросетевых операций до фиксированного размера, между графами устанавливается соответствие с помощью Z3, преобразования графов программ происходят с помощью механизма отката и стоимостной модели. В целом, рассказ повторяет эту статью:
TASO: Optimizing Deep Learning Computation with Automatic Generation of Graph Substitutions
https://cs.stanford.edu/~padon/taso-sosp19.pdf
#synthesis #smt
TASO: Optimizing Deep Learning Computation with Automatic Generation of Graph Substitutions
https://cs.stanford.edu/~padon/taso-sosp19.pdf
#synthesis #smt
Два небольших доклада об инструментах статического анализа, основанных на Datalog.
DOOP
https://www.youtube.com/watch?v=FQRLB2xJC50
Soufflé
https://www.youtube.com/watch?v=Qp3zfM-JSx8
#analysis #datalog
DOOP
https://www.youtube.com/watch?v=FQRLB2xJC50
Soufflé
https://www.youtube.com/watch?v=Qp3zfM-JSx8
#analysis #datalog
Небольшая заметка на тему вопросов канонизации внутренних представлений в компиляторах. Тема затронута очень поверхностно, но даже в таком виде, думаю, заслуживает более пристального внимания со стороны компиляторщиков.
Canonicalization
https://sunfishcode.github.io/blog/2018/10/22/Canonicalization.html
Canonicalization
https://sunfishcode.github.io/blog/2018/10/22/Canonicalization.html
Впечатляющая подборка материалов от серьезно настроенного исследователя.
По вопросам корректности компиляторов: https://github.com/MattPD/cpplinks/blob/master/compilers.correctness.md
По статическому и динамическому анализу: https://gist.github.com/MattPD/00573ee14bf85ccac6bed3c0678ddbef
По компиляторам в целом: https://github.com/MattPD/cpplinks/blob/master/compilers.md
По вопросам корректности компиляторов: https://github.com/MattPD/cpplinks/blob/master/compilers.correctness.md
По статическому и динамическому анализу: https://gist.github.com/MattPD/00573ee14bf85ccac6bed3c0678ddbef
По компиляторам в целом: https://github.com/MattPD/cpplinks/blob/master/compilers.md
Детальный анализ трассирующего JIT-компилятора Lua
LuaJIT
https://github.com/MethodicalAcceleratorDesign/MADdocs/blob/master/luajit/luajit-doc.pdf
#JIT #lua
LuaJIT
https://github.com/MethodicalAcceleratorDesign/MADdocs/blob/master/luajit/luajit-doc.pdf
#JIT #lua
Formulog -- выразительный DSL для задач статического анализа.
Основан на Datalog и ML, реализация использует SMT-решатель.
Formulog: ML + Datalog + SMT
http://www.weaselhat.com/2020/08/07/formulog-ml-datalog-smt/
#analysis #datalog #smt
Основан на Datalog и ML, реализация использует SMT-решатель.
Formulog: ML + Datalog + SMT
http://www.weaselhat.com/2020/08/07/formulog-ml-datalog-smt/
#analysis #datalog #smt
Пособие по реализации проверки для refinement-типов. В духе разработки компиляторов на основе техники nanopass. Предикаты проверяются с помощью SMT-решателя Z3.
Refinement Types: A Tutorial
https://arxiv.org/abs/2010.07763
https://github.com/ranjitjhala/sprite-lang
#analysis #smt
Refinement Types: A Tutorial
https://arxiv.org/abs/2010.07763
https://github.com/ranjitjhala/sprite-lang
#analysis #smt
Обсуждения вокруг эффективности интерпретатора и компилятора LuaJIT не утихают в нишевых сообществах до сих пор, при этом сам автор развернутых пояснений так и не оставил. Отдельные его комментарии можно найти на Reddit и в рассылке lua:
http://lua-users.org/lists/lua-l/2008-07/msg00651.html
http://lua-users.org/lists/lua-l/2010-11/msg00437.html
http://lua-users.org/lists/lua-l/2011-02/msg00671.html
http://lua-users.org/lists/lua-l/2011-02/msg00742.html
https://www.reddit.com/r/programming/comments/hkzg8/author_of_luajit_explains_why_compilers_cant_beat/c1w8xyz/?context=3
https://www.reddit.com/r/programming/comments/badl2/luajit_2_beta_3_is_out_support_both_x32_x64/c0lrus0/
#JIT #Lua
http://lua-users.org/lists/lua-l/2008-07/msg00651.html
http://lua-users.org/lists/lua-l/2010-11/msg00437.html
http://lua-users.org/lists/lua-l/2011-02/msg00671.html
http://lua-users.org/lists/lua-l/2011-02/msg00742.html
https://www.reddit.com/r/programming/comments/hkzg8/author_of_luajit_explains_why_compilers_cant_beat/c1w8xyz/?context=3
https://www.reddit.com/r/programming/comments/badl2/luajit_2_beta_3_is_out_support_both_x32_x64/c0lrus0/
#JIT #Lua
Очередное подтверждение тому факту, что работа над компиляторами -- это не только известные проекты-бегемоты в духе LLVM/GCC для 2-3 популярных архитектур и виртуальных машин.
Вы слышали о BPF? Впрочем, что я говорю, если читаете внимательно PLComp, то, конечно, слышали. Но, в любом случае, есть замечательная заметка, которая вводит в предмет:
BPF, XDP, Packet Filters and UDP
https://fly.io/blog/bpf-xdp-packet-filters-and-udp/
Посмотрите, сколько всего интересного! Узкая предметная область, виртуальные машины, JIT-компиляция, статический анализ кода, верификация.
В заметке есть ссылка на хорошую статью 1999 года:
BPF+: Exploiting Global Data-flow Optimization in a Generalized Packet Filter Architecture
https://andrewbegel.com/papers/bpf.pdf
Ничего себе, да? Такие-то технологии для, вроде бы, заурядной задачи фильтрации пакетов!
И вот кульминация, статья уже совсем свежая:
Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel
https://unsat.cs.washington.edu/papers/nelson-jitterbug.pdf
Складывается ощущение, что BPF -- своеобразный полигон для обкатки перспективных технологий компиляции. Это объяснимо: на исходный язык и вычисления накладываются жесткие ограничения, сама виртуальная машина простая -- есть где развернуться и применить что-нибудь изощренное. И, разумеется, интересны перспективы использования BPF в специализированных аппаратных решениях.
P.S. Вообще, в области обработки сетевых пакетов компиляторные технологии в целом развиваются очень интересным образом, существуют работающие подходы из области синтеза программ и я к этой теме еще обязательно вернусь.
#jit #analysis #vm #verification #bpf
Вы слышали о BPF? Впрочем, что я говорю, если читаете внимательно PLComp, то, конечно, слышали. Но, в любом случае, есть замечательная заметка, которая вводит в предмет:
BPF, XDP, Packet Filters and UDP
https://fly.io/blog/bpf-xdp-packet-filters-and-udp/
Посмотрите, сколько всего интересного! Узкая предметная область, виртуальные машины, JIT-компиляция, статический анализ кода, верификация.
В заметке есть ссылка на хорошую статью 1999 года:
BPF+: Exploiting Global Data-flow Optimization in a Generalized Packet Filter Architecture
https://andrewbegel.com/papers/bpf.pdf
Ничего себе, да? Такие-то технологии для, вроде бы, заурядной задачи фильтрации пакетов!
И вот кульминация, статья уже совсем свежая:
Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel
https://unsat.cs.washington.edu/papers/nelson-jitterbug.pdf
Складывается ощущение, что BPF -- своеобразный полигон для обкатки перспективных технологий компиляции. Это объяснимо: на исходный язык и вычисления накладываются жесткие ограничения, сама виртуальная машина простая -- есть где развернуться и применить что-нибудь изощренное. И, разумеется, интересны перспективы использования BPF в специализированных аппаратных решениях.
P.S. Вообще, в области обработки сетевых пакетов компиляторные технологии в целом развиваются очень интересным образом, существуют работающие подходы из области синтеза программ и я к этой теме еще обязательно вернусь.
#jit #analysis #vm #verification #bpf
Очередной выпад в сторону классического подхода к преподаванию синтаксического разбора. Простое и изящное в части содержания пособие по написанию разбора арифметических выражений. Автор красиво и плавно приводит к идее использования рекурсивного спуска совместно с парсером Пратта.
Just write the #!%/* parser
https://tiarkrompf.github.io/notes/?/just-write-the-parser/
На первый взгляд эта новость не слишком подходит для PLComp, но обращает на себя внимание личность автора (Tiark Rompf — один из лучших специалистов в области DSL-компиляции) и идеологическая спорность его подхода.
Действительно ли это правильный путь — перейти в обучении сразу к нюансам низкоуровневого кодирования, оставив за бортом вопросы формальной спецификации языка, его синтаксиса? Известные примеры реальных проектов, безусловно, говорят, мол, да, так оно и происходит на практике. И даже если есть спецификация, то она остается «на бумаге» и со временем расходится с реализацией все больше и больше.
#parsing
Just write the #!%/* parser
https://tiarkrompf.github.io/notes/?/just-write-the-parser/
На первый взгляд эта новость не слишком подходит для PLComp, но обращает на себя внимание личность автора (Tiark Rompf — один из лучших специалистов в области DSL-компиляции) и идеологическая спорность его подхода.
Действительно ли это правильный путь — перейти в обучении сразу к нюансам низкоуровневого кодирования, оставив за бортом вопросы формальной спецификации языка, его синтаксиса? Известные примеры реальных проектов, безусловно, говорят, мол, да, так оно и происходит на практике. И даже если есть спецификация, то она остается «на бумаге» и со временем расходится с реализацией все больше и больше.
#parsing
Известно, что в компиляторе IR выбирается таким образом, чтобы облегчить порождение кода для выбранного класса целевых архитектур. Но бывает ли так, чтобы уже само абстрактное IR оказывало влияние на набор команд процессора? Оказывается, и такое существует, причем речь здесь не идет о предметно-ориентированном наборе команд или поддержке конструкций входного языка. Ниже два характерных примера.
BasicBlocker: Redesigning ISAs to Eliminate Speculative-Execution Attacks
https://arxiv.org/pdf/2007.15919.pdf
В этой работе предлагается добавить к ISA процессора специальную команду, отмечающую начало линейного участка (basic block) с указанием его длины. Это нужно для предотвращения Spectre-подобных атак. Здесь мы видим, как черты абстрактного управляющего графа (CFG) проступают в машинном коде.
Hardware Acceleration for Programs in SSA Form
https://pp.ipd.kit.edu/uploads/publikationen/mohr13cases.pdf
В современных компиляторах форму SSA стараются сохранять настолько долго, насколько возможно, включая и фазу распределения регистров. Тем не менее, в какой-то момент из формы SSA приходится выходить и выход это достаточно болезнен, поскольку требует формирования дополнительных машинных команд. Особенно это касается phi-инструкций, имитировать которые приходится с помощью команд, заменяющих параллельные копирования/перестановки регистровых значений. А если попробовать реализовать phi-инструкцию аппаратным образом? При этом вместо реального копирования часто можно обойтись перестановками, которые на аппаратном уровне заключаются в переименовании регистров. Здесь в ISA процессора появляются черты абстрактной phi-инструкции из формы SSA.
#ssa #isa
BasicBlocker: Redesigning ISAs to Eliminate Speculative-Execution Attacks
https://arxiv.org/pdf/2007.15919.pdf
В этой работе предлагается добавить к ISA процессора специальную команду, отмечающую начало линейного участка (basic block) с указанием его длины. Это нужно для предотвращения Spectre-подобных атак. Здесь мы видим, как черты абстрактного управляющего графа (CFG) проступают в машинном коде.
Hardware Acceleration for Programs in SSA Form
https://pp.ipd.kit.edu/uploads/publikationen/mohr13cases.pdf
В современных компиляторах форму SSA стараются сохранять настолько долго, насколько возможно, включая и фазу распределения регистров. Тем не менее, в какой-то момент из формы SSA приходится выходить и выход это достаточно болезнен, поскольку требует формирования дополнительных машинных команд. Особенно это касается phi-инструкций, имитировать которые приходится с помощью команд, заменяющих параллельные копирования/перестановки регистровых значений. А если попробовать реализовать phi-инструкцию аппаратным образом? При этом вместо реального копирования часто можно обойтись перестановками, которые на аппаратном уровне заключаются в переименовании регистров. Здесь в ISA процессора появляются черты абстрактной phi-инструкции из формы SSA.
#ssa #isa
Очередная работа от John Regehr со товарищи на тему супероптимизации.
Dataflow-based Pruning for Speeding up Superoptimization
https://www.cs.utah.edu/~regehr/dataflow-pruning.pdf
Заметно, как первая эйфория от полностью автоматического применения SMT-решателя и метода CEGIS уходит. Оказывается, для задач реалистичных размерностей все равно приходится придумывать если не полностью собственную процедуру поиска с учетом эвристик из предметной области, то хотя бы ее элементы -- иначе SMT-решателю справиться будет тяжело.
Ключевая идея авторов -- прежде чем передавать на вход SMT-решателю очередную программу-кандидат из пространства поиска, полезно эту недооформленную программу (описывающую целое семейство конкретных программ) проверить на соответствие спецификации с помощью абстрактной интерпретации (анализ потоков данных на предмет known bits, int. ranges и так далее). В том числе, на конкретных тестовых входах.
В завершающей части статьи есть краткий и полезный обзор современного положения дел в области синтеза программ.
#smt #analysis #synthesis
Dataflow-based Pruning for Speeding up Superoptimization
https://www.cs.utah.edu/~regehr/dataflow-pruning.pdf
Заметно, как первая эйфория от полностью автоматического применения SMT-решателя и метода CEGIS уходит. Оказывается, для задач реалистичных размерностей все равно приходится придумывать если не полностью собственную процедуру поиска с учетом эвристик из предметной области, то хотя бы ее элементы -- иначе SMT-решателю справиться будет тяжело.
Ключевая идея авторов -- прежде чем передавать на вход SMT-решателю очередную программу-кандидат из пространства поиска, полезно эту недооформленную программу (описывающую целое семейство конкретных программ) проверить на соответствие спецификации с помощью абстрактной интерпретации (анализ потоков данных на предмет known bits, int. ranges и так далее). В том числе, на конкретных тестовых входах.
В завершающей части статьи есть краткий и полезный обзор современного положения дел в области синтеза программ.
#smt #analysis #synthesis
(Это мой старый перечень, но интерес, как мне кажется, он все еще представляет) Ниже я хочу представить краткий список полновесных книг по специальным вопросам компиляции. Эти книги много дали лично мне. Надеюсь, они окажутся в соответствующий момент полезными и вам.
1. Automatic Algorithm Recognition and Replacement. A New Approach to Program Optimization (https://mitpress.mit.edu/books/automatic-algorithm-recognition-and-replacement?cr=reset).
Тема распознавания алгоритмов очень мало изучена. Но перспективы здесь самые впечатляющие. Оптимизации на уровне алгоритмов, автоматическое распараллеливание и проч. Весьма вдохновляющее чтение.
2. Reasoning About Program Transformations. Imperative Programming and Flow of Data. (https://www.springer.com/us/book/9780387953915).
Очень нетипичная книга по анализу и преобразованиям программ. Доходчиво написано, автор предмет понимает настолько глубоко, что не стесняется быть субъективным, оригинальным в изложении традиционной теории. Рассматривается в том числе полиэдральная модель программы.
3. Instruction Selection. Principles, Methods, and Applications. (https://www.springer.com/us/book/9783319340173).
Такого подробного, эницклопедического обзора подходов к выбору инструкций не хватало давно. Автор систематизировал различные приемы, использовал в изложении исторический контекст.
4. Partial Evaluation and Automatic Program Generation (https://www.itu.dk/~sestoft/pebook/).
В наше время все чаще на практике используются давние результаты Турчина, Футамуры, Ершова и других исследователей в области частичных вычислений/метапрограммирования. В какой-то момент, после прочтения очередной заметки в блоге с упоминанием проекций Футамуры (PyPy, Truffle и так далее), нелишне будет открыть и эту книгу, где подробно изложены все эти темы.
1. Automatic Algorithm Recognition and Replacement. A New Approach to Program Optimization (https://mitpress.mit.edu/books/automatic-algorithm-recognition-and-replacement?cr=reset).
Тема распознавания алгоритмов очень мало изучена. Но перспективы здесь самые впечатляющие. Оптимизации на уровне алгоритмов, автоматическое распараллеливание и проч. Весьма вдохновляющее чтение.
2. Reasoning About Program Transformations. Imperative Programming and Flow of Data. (https://www.springer.com/us/book/9780387953915).
Очень нетипичная книга по анализу и преобразованиям программ. Доходчиво написано, автор предмет понимает настолько глубоко, что не стесняется быть субъективным, оригинальным в изложении традиционной теории. Рассматривается в том числе полиэдральная модель программы.
3. Instruction Selection. Principles, Methods, and Applications. (https://www.springer.com/us/book/9783319340173).
Такого подробного, эницклопедического обзора подходов к выбору инструкций не хватало давно. Автор систематизировал различные приемы, использовал в изложении исторический контекст.
4. Partial Evaluation and Automatic Program Generation (https://www.itu.dk/~sestoft/pebook/).
В наше время все чаще на практике используются давние результаты Турчина, Футамуры, Ершова и других исследователей в области частичных вычислений/метапрограммирования. В какой-то момент, после прочтения очередной заметки в блоге с упоминанием проекций Футамуры (PyPy, Truffle и так далее), нелишне будет открыть и эту книгу, где подробно изложены все эти темы.
Классический редактор GNU Emacs в скором времени получит, наконец, нативный компилятор для своего языка расширений Emacs Lisp. Это уже третья попытка решить сопутствующие проблемы, но Andrea Corallo за последний год построил на базе libgccjit компилятор, показывающий достойный результат в пакете elisp-benchmarks. Уже сейчас компилятор готовится к вливанию в основную ветку репозитория GNU Emacs.
Презентация автора на Linux Plumbers Conference 2020:
http://akrl.sdf.org/Kludging_LPC_2020.pdf
Дневник разработки:
http://akrl.sdf.org/gccemacs.html
Обсуждение (в положительном ключе) состояния ветки репозитории:
https://debbugs.gnu.org/cgi/bugreport.cgi?bug=43725
Презентация автора на Linux Plumbers Conference 2020:
http://akrl.sdf.org/Kludging_LPC_2020.pdf
Дневник разработки:
http://akrl.sdf.org/gccemacs.html
Обсуждение (в положительном ключе) состояния ветки репозитории:
https://debbugs.gnu.org/cgi/bugreport.cgi?bug=43725
linear-scan-register-alloc-1999.pdf
225.4 KB
Распределение регистров - краеугольная задача любого порождающего машинный код компилятора. В работе Linear Scan Register Allocation (1999) был представлен один из двух популярнейших алгоритмов распределения регистров.
По сравнению с алгоритмами на основе раскраски графов алгоритм линейного сканирования отличается простотой в реализации, высокой скоростью работы самого алгоритма и эффективностью выходного кода. Авторы пишут, что даже простейший вариант алгоритма, представленный в публикации, порождает код, лишь немного уступающий в производительности алгоритмам на основе раскраски графов.
Благодаря своим свойствам алгоритм стал стандартным решением в динамических (just-in-time) и легковесных компиляторах.
Из известных компиляторов линейное сканирование используется, например, в luajit или Hotspot.
#history #registerallocation #linearscan
По сравнению с алгоритмами на основе раскраски графов алгоритм линейного сканирования отличается простотой в реализации, высокой скоростью работы самого алгоритма и эффективностью выходного кода. Авторы пишут, что даже простейший вариант алгоритма, представленный в публикации, порождает код, лишь немного уступающий в производительности алгоритмам на основе раскраски графов.
Благодаря своим свойствам алгоритм стал стандартным решением в динамических (just-in-time) и легковесных компиляторах.
Из известных компиляторов линейное сканирование используется, например, в luajit или Hotspot.
#history #registerallocation #linearscan
Популярный алгоритм распределения регистров линейным сканированием (Linear Scan Register Allocation, 1999) определен на живых интервалах (live intervals) и линейном списке инструкций. Построение и хранение списка интервалов в виде пар индексов инструкций занимает время и память, поэтому исследователи продолжали искать возможность не строить явно список интервалов.
Авторы Efficient Global Register Allocation (2020) предложили алгоритм из того же семейства, но определенный на графе потока исполнения (control flow graph). Ключевые идеи здесь две:
1. Список живых интервалов здесь отслеживаются неявно, на каждом из базовых блоков и инструкций внутри блоков.
2. Проход по отдельным инструкциям позволяет не только не строить в явном виде интервалы, но и высвобождать временно регистры внутри блоков, что решает проблему "пустот в живости" (liveness holes).
Алгоритм сравним по производительности порожденного кода с актуальными реализациями линейного сканирования, немного выигрывая в ресурсах на этапе компиляции. Из работы следует, что основное преимущество подхода заключается в возможностях специальных оптимизаций.
В настоящий момент этот вариант линейного сканирования используется при порождении регистрового байткода dex для виртуальной машины ART, используемый в Android.
https://arxiv.org/pdf/2011.05608.pdf
#registerallocation #linearscan #dex #art #android
Авторы Efficient Global Register Allocation (2020) предложили алгоритм из того же семейства, но определенный на графе потока исполнения (control flow graph). Ключевые идеи здесь две:
1. Список живых интервалов здесь отслеживаются неявно, на каждом из базовых блоков и инструкций внутри блоков.
2. Проход по отдельным инструкциям позволяет не только не строить в явном виде интервалы, но и высвобождать временно регистры внутри блоков, что решает проблему "пустот в живости" (liveness holes).
Алгоритм сравним по производительности порожденного кода с актуальными реализациями линейного сканирования, немного выигрывая в ресурсах на этапе компиляции. Из работы следует, что основное преимущество подхода заключается в возможностях специальных оптимизаций.
В настоящий момент этот вариант линейного сканирования используется при порождении регистрового байткода dex для виртуальной машины ART, используемый в Android.
https://arxiv.org/pdf/2011.05608.pdf
#registerallocation #linearscan #dex #art #android
https://www.jeffsmits.net/assets/articles/sle20-paper4.pdf
Gradually Typing Strategies
Статья рассказывает о применении популярной техники постепенной типизации (Gradual Typing) в необычной области -- к языку переписывания термов Stratego (который используется для "program normalization, type checkers, program analyses, code generators, and more"). Несмотря на отсутствие проверки типов в Stratego до сего момента, он тем не менее послужил для вдохновения авторов Haskell фреймворка SYB.
Использование Gradual Typing (постепенной типизации) мотивировано двумя факторами. Первый -- обратная совместимость, так как Stratego (в составе фреймворков Stratego/XT и Spoofax) используется в production-системах, разрабатываемых как в академии (researchr.org, conf.researchr.org, платформа онлайн-курсов TU Delft), так и в индустрии (где-то в недрах Oracle Labs). Второй -- высокая "динамичность" переписывания термов, которая в некоторых случаях используется (а кто-то скажет "эксплуатируется") для (временного) порождения нетипизируемых термов и превращения их обратно в типизируемые.
Дополнительно задача осложняется наличием в Stratego правил переписывания "высшего порядка" (называемых "стратегиями переписывания"), принимающих и применяющих другие правила переписывания (или стратегии). Отсюда возникает понятие Type-Preserving стратегий, реализующее ограниченную форму Higher-Kinded Types.
Кроме того, авторы применяют механизм "прозрачных" во время исполнения прокси-типов для того чтобы избежать накапливания лишних динамических преобразований типов при передаче правил переписывания из статически-типизированных стратегий в динамически-типизированные и обратно.
Проверка полученной системы типов на существующем проекте (учебный ассемблер для Java-байткода) продемонстрировала два достаточно ожидаемых результата: а) корректный динамический код написан так как если бы был статически типизирован, поэтому его легко аннотировать явными типами и почти не приходится при этом рефакторить; б) плохо протестированный динамический код содержит ошибки, которые легко обнаруживаются тайп-чекером (например, возврат списка вместо элемента — классика, сам на таком попадался).
#stratego #spoofax #gradual #types
Gradually Typing Strategies
Статья рассказывает о применении популярной техники постепенной типизации (Gradual Typing) в необычной области -- к языку переписывания термов Stratego (который используется для "program normalization, type checkers, program analyses, code generators, and more"). Несмотря на отсутствие проверки типов в Stratego до сего момента, он тем не менее послужил для вдохновения авторов Haskell фреймворка SYB.
Использование Gradual Typing (постепенной типизации) мотивировано двумя факторами. Первый -- обратная совместимость, так как Stratego (в составе фреймворков Stratego/XT и Spoofax) используется в production-системах, разрабатываемых как в академии (researchr.org, conf.researchr.org, платформа онлайн-курсов TU Delft), так и в индустрии (где-то в недрах Oracle Labs). Второй -- высокая "динамичность" переписывания термов, которая в некоторых случаях используется (а кто-то скажет "эксплуатируется") для (временного) порождения нетипизируемых термов и превращения их обратно в типизируемые.
Дополнительно задача осложняется наличием в Stratego правил переписывания "высшего порядка" (называемых "стратегиями переписывания"), принимающих и применяющих другие правила переписывания (или стратегии). Отсюда возникает понятие Type-Preserving стратегий, реализующее ограниченную форму Higher-Kinded Types.
Кроме того, авторы применяют механизм "прозрачных" во время исполнения прокси-типов для того чтобы избежать накапливания лишних динамических преобразований типов при передаче правил переписывания из статически-типизированных стратегий в динамически-типизированные и обратно.
Проверка полученной системы типов на существующем проекте (учебный ассемблер для Java-байткода) продемонстрировала два достаточно ожидаемых результата: а) корректный динамический код написан так как если бы был статически типизирован, поэтому его легко аннотировать явными типами и почти не приходится при этом рефакторить; б) плохо протестированный динамический код содержит ошибки, которые легко обнаруживаются тайп-чекером (например, возврат списка вместо элемента — классика, сам на таком попадался).
#stratego #spoofax #gradual #types