Использование рекомендательных систем для автонастройки компилятора, с учетом собранной ранее информации. Результаты внушают оптимизм.
A Collaborative Filtering Approach for the Automatic Tuning of Compiler Optimisations
https://arxiv.org/pdf/2005.04092.pdf

#autotuning #machinelearning #compiler #optimization

Очередная работа Мюнш-Макканьони по превращению Окамла в своеобразный конкурент Раста, черновик предложения о добавлении возможности работы с off-heap указателями:

Towards better systems programming in OCaml with out-of-heap allocation (draft)
https://github.com/gadmm/RFCs/blob/interop/rfcs/interop.md

#ocaml

Сопоставление с образом (pattern matching) в наши дни упоминается прежде всего в контексте функциональных языков программирования семейства ML. Но техника эта имеет гораздо более широкое применение, в том числе и вне контекста разработки ЯП. Интереснейший из классических результатов - алгоритм Rete, позволяющий эффективно сопоставлять тысячи образов с тысячами же объектов.


Rete: A Fast Algorithm for the Many Pattern/Many Object Pattern Match Problem

Доклад Improving Compiler Construction Using Formal Methods (Jubi Taneja)
Обзор работ по теме использования супероптимизатора Souper в различных фазах компиляции (статический анализ, автоматизация создания правил локальной оптимизации).
https://www.youtube.com/watch?v=de8Ak0nY1hA

#smt #superoptimizer

Опубликовано "Руководство по эффективному программированию на платформе «Эльбрус»".

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

Эльбрус - процессор общего назначения, разрабатываемый фирмой МЦСТ, с архитектурой на основе широкого командного слова (VLIW).

http://www.mcst.ru/elbrus_prog

#vliw

Любопытная заметка от Intel на тему использования внешнего решателя задач целочисленного программирования в LLVM.
Речь идет об оптимальной расстановке команды LFENCE в управляющем графе. Это нужно для предотвращения LVI-атак.

An Optimized Mitigation Approach for Load Value Injection
https://software.intel.com/security-software-guidance/insights/optimized-mitigation-approach-load-value-injection

ILP-решатель для автоматической вставки fence применяли и ранее. См., например, работу Don’t sit on the fence. A static analysis approach to automatic fence insertion:
https://arxiv.org/pdf/1312.1411.pdf

#solver #analysis

Автоматическое извлечение КС-грамматики на основе динамического анализа управляющего графа программы на примерах входных данных. Любопытно, что авторы не стали даже упоминать грамматическое сжатие.

Mining Input Grammars from Dynamic Control Flow
https://publications.cispa.saarland/3101/1/fse2020-mimid.pdf

#analysis #parsing

Авторы оценивают верхнюю и нижнюю границы вычислительной сложности статического анализа указателей Андерсена (APA) и приводят свои варианты реализации APA.

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.

Авторы показывают, что их модель превосходит работы в данной области, основанные на подходе
использования правил. Из интересного, прямой цитатой из статьи:

• 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

Подход к выявлению "семантического клонов" в программе. Основан на насыщении равенствами и забытой концепции Programmer’s Apprentice. Утверждается, что работает лучше, чем популярное в этой области представление PDG.

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

Два небольших доклада об инструментах статического анализа, основанных на 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

Впечатляющая подборка материалов от серьезно настроенного исследователя.

По вопросам корректности компиляторов: 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

Formulog -- выразительный DSL для задач статического анализа.
Основан на 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

Обсуждения вокруг эффективности интерпретатора и компилятора 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

Очередное подтверждение тому факту, что работа над компиляторами -- это не только известные проекты-бегемоты в духе 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

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

Just write the #!%/* parser
https://tiarkrompf.github.io/notes/?/just-write-the-parser/

На первый взгляд эта новость не слишком подходит для PLComp, но обращает на себя внимание личность автора (Tiark Rompf — один из лучших специалистов в области DSL-компиляции) и идеологическая спорность его подхода.

Действительно ли это правильный путь — перейти в обучении сразу к нюансам низкоуровневого кодирования, оставив за бортом вопросы формальной спецификации языка, его синтаксиса? Известные примеры реальных проектов, безусловно, говорят, мол, да, так оно и происходит на практике. И даже если есть спецификация, то она остается «на бумаге» и со временем расходится с реализацией все больше и больше.

#parsing