Semantics for 2D Rasterization

12 hours ago

Rasterization libraries like Skia, CoreGraphics, and Direct2D are powerful but often used inefficiently by applications.
Google Chrome, despite optimization, still produces inefficient instruction sequences on top websites due to complex library semantics.
The paper introduces μSkia, a formal semantics for Skia mechanized in Lean, covering features like canvas state, layers, blending, and filters.
Four patterns of sub-optimal Skia code in Chrome are identified and replaced, with μSkia enabling verification of correctness and side conditions.
A high-performance Skia optimizer based on these patterns achieves an 18.7% speedup on 99 programs from top websites, with fast optimization times.
End-to-end verification is performed by loading optimizer traces into μSkia and translation validating them in Lean.

Hasty Briefsbeta