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 и так далее). В том числе, на конкретных тестовых входах.
В завершающей части статьи есть краткий и полезный обзор современного положения дел в области синтеза программ.
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
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
26/05/2020, Peter Sovietov¶
Halide — яркий пример современного и популярного DSL для высокопроизводительных вычислений (обработка изображений, нейросети). В работе по ссылке ниже представлена его формальная семантика. Достаточная, по большому счету, для разработки собственного компилятора Halide. Любопытно, что в описании трансляции в императивное представление использован формализм из области синтеза программ. Formal Semantics for the Halide Language https://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-40.pdf
19/05/2020¶
Работа по синтезу программ с использованием Rosette (Racket). Cинтезируется JIT-компилятор DSL BPF (ядро Linux) в машинный код (в примере использован RISC-V) Synthesizing JIT Compilers for In-Kernel DSLs https://www.cs.utexas.edu/~isil/jitsynth.pdf
Подробности о BPF VM: BPF: A New Type of Software http://www.brendangregg.com/blog/2019-12-02/bpf-a-new-type-of-software.html