Оптимизатор на базе формальной семантики Skia ускоряет растеризацию на 18,7%
Compiler-style optimization for drawing via Skia
Даже Chrome, разработанный вместе со Skia, порождает неэффективные последовательности операций растеризации. Исследователи представили μSkia — формальную семантику библиотеки Skia, механизированную в Lean. Они выявили четыре паттерна неоптимального кода и построили оптимизатор, который на 99 программах с топ-100 сайтов даёт ускорение 18,7% относительно самого современного GPU-бэкенда Skia, затрачивая не более 32 мкс. Корректность замен подтверждается в Lean.
Даже Google Chrome, высокооптимизированная программа, совместно разработанная с библиотекой растеризации Skia, всё ещё порождает неэффективные последовательности инструкций даже на 100 самых посещаемых сайтах.