通过Skia进行绘制的编译器风格优化

# 二维光栅化的形式化语义
来源：https://arxiv.org/html/2603.23696  
CCS:计算方法学 光栅化  
CCS:软件及其工程 可视语言  
CCS:软件及其工程 形式化语义  
Bhargav K Kulkarni  
隶属机构：犹他大学，201 总统圈，盐湖城，犹他州，美国，84112-0090  
邮箱：[[email protected]](mailto:[email protected])  
Henry Whiting  
隶属机构：犹他大学，201 总统圈，盐湖城，犹他州，美国，84112-0090  
邮箱：[[email protected]](mailto:[email protected])  
以及  
Pavel Panchekha  
隶属机构：犹他大学，201 总统圈，盐湖城，犹他州，美国，84112-0090  
邮箱：[[email protected]](mailto:[email protected])

© 无

###### 摘要

光栅化是确定应用程序绘制的每个像素颜色的过程。像 Skia、CoreGraphics 和 Direct2D 这样强大的光栅化库在绘图、混合和高效渲染方面投入了巨大努力。然而，应用程序仍然受到它们要求这些库执行的低效指令序列的制约。即使是与 Skia 光栅化库共同开发的高度优化的网络浏览器 Google Chrome，在访问量最大的前100个网站上仍然会产生低效的指令序列。这种低效的根本原因在于光栅化库具有复杂的语义和不透明、非显式的执行模型。

为了解决这个问题，我们引入了 μSkia，一个针对 Skia 二维图形库的形式化语义，并在 Lean 中将此语义机械化。μSkia 涵盖了诸如画布状态、图层栈、混合以及颜色过滤器等语言和图形特性，语义本身被分为三个层次以分离关注点并支持可扩展性。随后，我们识别了 Google Chrome 生成的四种次优 Skia 代码模式，并为每种模式编写了替换代码。μSkia 使我们能够验证这些替换的正确性，包括识别出许多棘手的次要条件。接着，我们开发了一个高性能的 Skia 优化器，应用这些模式来加速光栅化。在来自前100个网站的 99 个 Skia 程序上，该优化器相比 Skia 最现代的 GPU 后端实现了 18.7% 的加速，而优化时间仅需 32 微秒。这种加速效果在各种网站、Skia 后端和 GPU 上都得以保持。为提供真正端到端的验证，优化器生成的优化轨迹被加载回 μSkia 语义中，并在 Lean 中进行翻译验证。

###### 关键词：
可视语言，光栅化，计算机图形学，编译器，形式化语义，自动化验证，交互式定理证明，网络浏览器

## 1. 引言

你在计算机屏幕上看到的每一个像素，都是由一个称为*光栅化*的过程产生的。桌面、移动和网络应用程序等程序会向一个*光栅化库*发送一系列指令；这些指令绘制形状、渲染文本并混合重叠的视觉元素。然后，光栅化库——可能是 Skia、CoreGraphics、Direct2D、Cairo 或其他库——执行这些指令，确定屏幕上每个像素的颜色。光栅化必须以交互速率完成，理想情况下是每秒 60 到 120 帧，以确保用户获得流畅的体验。因此，光栅化库被高度优化。例如，Skia 针对多种基于 CPU 和 GPU 的后端，并使用 OpenGL、Vulkan 和 Metal 等传统和现代图形 API。事实上，在 2021 年至 2025 年间，Skia 团队编写了一个全新的后端 Graphite，通过利用新的 GPU API 将光栅化时间缩短了约 15%（graphite-blog-post）。因此，Skia 成为 Google Chrome、Firefox 和 Ladybird 浏览器、Android 操作系统、Flutter 移动应用框架以及 Sublime Text 等原生应用程序的首选光栅化库也就不足为奇了。

尽管极其注重性能，光栅化*并未*成为一个已解决的问题。例如，网络浏览器在低端移动设备上难以以稳定的 60 帧每秒渲染具有部分透明度、动画和模糊等流行效果的现代网页。120 Hz 显示屏的趋势更是提高了要求。其困难之处在于，尽管光栅化库能够高效地执行单个指令，但*客户端却要求它们执行低效的指令序列*。例如，作者手动检查了 Chrome 为光栅化访问量前 100 的网站（按流量计）所执行的指令，并发现了许多直接的性能问题。而 Chrome 无疑是最复杂的 Skia 客户端：它与 Skia 在同一家公司开发，工程师之间紧密协作，使得 Chrome 和 Skia 能够同步发布。其他 Skia 客户端的情况则更糟。提高光栅化程序的质量将大大减少光栅化时间，但做到这一点之所以异常困难，是因为光栅化库具有奇怪的命令式语义和不透明、非显式的执行模型。

我们通过 μSkia 来解决这个问题，μSkia 是针对 Skia 二维光栅化库的形式化语义。μSkia 捕获了 Skia API 的关键特性，如画布状态、图层栈、裁剪和混合。更广泛地说，由于这些特性出现在所有光栅化库中（源于它们共同的 PostScript 传统），我们认为我们的形式化为未来语言驱动的光栅化研究奠定了基础。我们的形式化建立在三个层次上——命令语言、函数式内核和抽象模型——这分离了关注点，简化了推理，并允许可扩展性。该语义在 Lean 中被机械化，使得 μSkia 程序的自动化推理和验证成为可能。

为了展示 μSkia 的实用性，我们识别了 Google Chrome 在访问量前 100 网站上生成的四种次优 Skia 指令模式。对于每一种模式，我们提供了一个更高效的指令序列，并在 Lean 中证明了这两个序列的等价性。μSkia 使我们能够识别非平凡的次要条件，并确保优化的正确性。接着，我们构建了一个优化器，在光栅化之前应用这些重写规则，从而显著加速光栅化。这个简单的优化器在来自前 100 网站的 99 个 Chrome 生成的 Skia 程序上，相比 Skia 最现代的 Graphite 后端平均实现了 18.7% 的加速。该优化器效率也很高，优化时间最多仅需 32 微秒，并且它在不同的 Skia 后端和 GPU 上都缩短了光栅化时间。此外，该优化器能够生成优化轨迹，这些轨迹可以使用 μSkia 进行翻译验证，从而为这些程序提供了端到端的正确性证明。

简而言之，本文的贡献如下：

1. (1) 对 Skia API 及更一般的光栅化过程的形式化新表述 ()
2. (2) 利用该形式化验证有效的一系列针对性优化 ()
3. (3) 一个高效且正确的 Skia 优化器，应用这些优化 ()