Compiler-style optimization for drawing via Skia
a day ago
- Rasterization determines pixel colors but inefficient in applications like Chrome due to complex library semantics.
- Paper introduces μSkia, a formal semantics for Skia 2D graphics library, mechanized in Lean with three strata.
- Identifies four patterns of sub-optimal Skia code from Chrome and provides verified replacements.
- Develops a high-performance optimizer that achieves 18.7% speedup on 99 Skia programs from top 100 websites.
- Optimization traces are validated back in μSkia semantics for end-to-end verification.