Chrome's own drawing code is inefficient, and a verified optimizer fixes it
Compiler-style optimization for drawing via Skia
Rasterization libraries like Skia are fast, but apps still feed them inefficient operation sequences — even Chrome, co-developed with Skia, does so on the top 100 websites. The paper introduces μSkia, a formal Lean semantics for Skia covering canvas state, layers, blending, and color filters. It identifies four sub-optimal Chrome patterns, verifies replacements, and builds an optimizer that speeds up 99 Skia programs from top websites by 18.7% over Skia's modern GPU backend, with optimization taking at most 32 μs.
Even Google Chrome, a highly optimized program co-developed with the Skia rasterization library, still produces inefficient instruction sequences even on the top 100 most visited websites.
- eigenblake
Wow! This is exciting. I have speculated that this would be possible. Since I've been learning about databases and dynamic db query optimization, it struck me as surprising that we didn't have similar things for more of our computational universe. Now that this is here, it makes me wonder what else we can optimize in using the same high level techniques.
The more you know about what you want to do ahead of time, the more optimally you can reorder your sequence of steps to give a better-than-naive solution. It makes me think about all software in terms of these abstract computation graphs and makes me wonder what else we can optimize automatically.
Of course, we do absolutely do need a formal model here, so we know what edits are possible, the same way db engines have relational algebra as their backing model. But this whole thing makes me feel like manual software optimization is soon to fall to AI. And I'm thinking that includes good-old-fashion AI first, not second, to LLM's. But I'm sure LLMs would be useful here too, especially for the formalization.
- mtklein
As a former Skia contrib, this is cool as heck to read. It's exactly the sort of optimization work we had in mind when we wrote that SkRecord system, and I'm pleased that you were able to make use of nanobench. Back in those days we had just a few small optimizations that we could apply, mostly trying to eliminate unnecessary saveLayer() calls. Very cool to see it done in a modern way with Lean.
- pavpanchekha
Hi folks! Last author here, happy to answer questions, very surprised to see this on HN. We had a blast working on this. Let me add that the Skia team at Google was super supportive, met with us many times to explain a lot of stuff.
I had the idea for this project years ago while writing Web Browser Engineering with Chris Harrelson (see https://browser.engineering/). Then a few years ago I made a first attempt at this project with Yuvaraj (https://droidkid.github.io/), but for various reasons we never got very far. I restarted the project with Bhargav (https://bhargavkk.com/) about a year ago, and focused much more seriously on the semantics of Skia itself, which made progress much more rapid. Still, I was, frankly, shocked by how good the results are.