02/11/2020, Peter Sovietov¶
Очередная работа от 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 и так далее). В том числе, на конкретных тестовых входах.
В завершающей части статьи есть краткий и полезный обзор современного положения дел в области синтеза программ.
16/10/2020, Peter Sovietov¶
Пособие по реализации проверки для refinement-типов. В духе разработки компиляторов на основе техники nanopass. Предикаты проверяются с помощью SMT-решателя Z3.
Refinement Types: A Tutorial https://arxiv.org/abs/2010.07763 https://github.com/ranjitjhala/sprite-lang
08/08/2020, Peter Sovietov¶
Formulog – выразительный DSL для задач статического анализа. Основан на Datalog и ML, реализация использует SMT-решатель.
Formulog: ML + Datalog + SMT http://www.weaselhat.com/2020/08/07/formulog-ml-datalog-smt/
17/06/2020, Peter Sovietov¶
В рамках PLDI Alex Aiken (известный многим по курсам компиляторостроения) рассказал о проекте TASO – это автоматический синтез графовых оптимизирующих преобразований для нейросетевых фреймворков. Перечисляются все графы-шаблоны нейросетевых операций до фиксированного размера, между графами устанавливается соответствие с помощью Z3, преобразования графов программ происходят с помощью механизма отката и стоимостной модели. В целом, рассказ повторяет эту статью:
TASO: Optimizing Deep Learning Computation with Automatic Generation of Graph Substitutions https://cs.stanford.edu/~padon/taso-sosp19.pdf
05/06/2020, Peter Sovietov¶
Доклад Improving Compiler Construction Using Formal Methods (Jubi Taneja) Обзор работ по теме использования супероптимизатора Souper в различных фазах компиляции (статический анализ, автоматизация создания правил локальной оптимизации). https://www.youtube.com/watch?v=de8Ak0nY1hA
27/05/2020, Peter Sovietov¶
Очень доходчивый и практико-ориентированный разбор одной из ключевых статей в области супероптимизации на основе метода CEGIS. Автор даже не поленился расшифровать формулы из статьи для тех, кто сторонится математической нотации. Synthesizing Loop-Free Programs with Rust and Z3 https://fitzgeraldnick.com/2020/01/13/synthesizing-loop-free-programs.html