Очень доходчивый и практико-ориентированный разбор одной из ключевых статей в области супероптимизации на основе метода CEGIS. Автор даже не поленился расшифровать формулы из статьи для тех, кто сторонится математической нотации.
Synthesizing Loop-Free Programs with Rust and Z3
https://fitzgeraldnick.com/2020/01/13/synthesizing-loop-free-programs.html

#synthesis #smt

Синтаксический анализ программ считается давно изученной и почти даже скучной областью. Но при применении теории к практике текстовых редакторов часто выясняется, что привычные формализмы работают плохо и разработчикам приходится предлагать неординарные решения. В своей статье "SMIE: Simple Minded Indentation Engine" Стефан Монье излагает суть проблемы автоматического расставления отступов и описывает решение на базе грамматик с операторным предшествованием (operator-precedence grammars), используемое в Емаксе.

http://www-labs.iro.umontreal.ca/~monnier/smie.pdf

#parsing #editor #indentation #emacs #smie

SSA в историческом контексте. Очень хорошая систематизация знаний по теме.
Program Analisys and Transformation Survey and Links
https://github.com/pfalcon/awesome-program-analysis

#analysis #ssa

Использование рекомендательных систем для автонастройки компилятора, с учетом собранной ранее информации. Результаты внушают оптимизм.
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