Skia, Formalized in Lean, and 18.7% Faster Rasterization
A Lean formalization of Skia lets three researchers verify four rewrite patterns correct, and the optimizer built on them makes Skia programs run 18.7% faster than the library's most modern GPU backend.
Google Chrome, co-developed with the Skia rasterization library, still emits inefficient instruction sequences on the top 100 most visited websites. The paper blames the interface: “rasterization libraries have complex semantics and opaque and non-obvious execution models.”
Bhargav Kulkarni, Henry Whiting, and Pavel Panchekha answer with μSkia, a formal semantics for Skia mechanized in Lean. It covers canvas state, the layer stack, blending, and color filters, split into three strata to separate concerns. They find four patterns of sub-optimal Skia code Chrome produces, write replacements, and prove them correct, tricky side conditions included.
The optimizer built on those patterns runs on 99 Skia programs from the top 100 websites. Those programs come out 18.7% faster than Skia’s most modern GPU backend, at most 32 μs per optimization, holding across websites, backends, and GPUs. Optimization traces are loaded back into μSkia and validated in Lean, so the 18.7% arrives with a proof attached.
Our Take: the semantics did the work. The 18.7% is what happens when proofs and a benchmark agree. Skip it if you want a patch for your own renderer this week — this is a model of Skia, not a change to Chrome. Picture a 32 μs pass handing back 18.7%; read the four rewrite patterns first.