用编译器思维优化 Skia 绘图
Compiler-style optimization for drawing via Skia
即使是 Google Chrome 这样高度优化的浏览器，在调用 Skia 绘图库时仍会产生低效指令序列。问题根源在于 Skia 复杂的语义和不透明的执行模型。研究团队为此构建了 μSkia，一套基于 Lean 的形式化语义系统，用于精确描述 Skia 的画布状态、图层栈及混合模式。通过识别并替换四种典型低效模式，他们开发出一款高性能优化器。在涵盖前 100 大网站的 99 个 Skia 程序测试中，该优化器在 GPU 后端上实现了 18.7% 的加速，且优化耗时不超过 32 微秒。整个过程通过 Lean 进行端到端的验证，确保优化后的代码逻辑正确无误。
即使是 Google Chrome 这样高度优化的程序，在与 Skia 绘图库共同开发时，依然会在访问量最高的前 100 个网站上产生低效的指令序列。
HN 评论区
20- eigenblake
Wow! 这太令人兴奋了。我一直猜测这是可行的。自从开始学习数据库和动态查询优化以来，我就觉得奇怪，为什么我们的计算宇宙中没有更多类似的东西。既然现在有了，我不禁想知道还能用同样的高级技术优化什么。
你对要做什么了解得越早，就越能最优地重排步骤顺序，从而得到比朴素方案更好的解。这让我开始用抽象计算图的视角看待所有软件，并好奇还能自动优化什么。
当然，我们绝对需要一个形式化模型，就像数据库引擎以关系代数作为支撑模型一样，这样我们才知道哪些修改是可行的。但整个事情让我觉得，手动软件优化很快就要被 AI 取代了。而且我指的是先有传统 AI，而不是大语言模型（LLM）。不过，我相信 LLM 在这里也会很有用，尤其是在形式化方面。
- mtklein
作为前 Skia 贡献者，读这篇简直酷到没边。这正是我们当初编写 SkRecord 系统时设想的优化工作，很高兴看到你能用上 nanobench。那时候我们只能应用少数几个小优化，主要是试图消除不必要的 saveLayer() 调用。看到用 Lean 以现代方式实现这一点，真的非常酷。
- pavpanchekha
大家好！我是最后一位作者，很乐意回答问题，看到这篇帖子出现在 HN 上非常惊讶。我们做这个项目玩得超级开心。补充一点，Google 的 Skia 团队非常支持我们，多次与我们会面，解释了大量内容。
我在和 Chris Harrelson 合著《Web Browser Engineering》（见 https://browser.engineering/）时就有了这个项目的想法。几年前，我和 Yuvaraj 第一次尝试了这个项目（https://droidkid.github.io/），但由于各种原因，我们没能走多远。大约一年前，我和 Bhargav（https://bhargavkk.com/）重启了该项目，并更认真地关注 Skia 本身的语义，这让进展快了很多。尽管如此，老实说，结果之好还是让我震惊了。