计算机科学 > 编程语言
提交于 2026 年 3 月 24 日
标题：二维光栅化的形式语义
作者：Bhargav Kulkarni、Henry Whiting、Pavel Panchekha
查看论文《Semantics for 2D Rasterization》（作者 Bhargav Kulkarni 等 2 人）的 PDF
摘要：光栅化是确定应用程序所绘制的每一个像素颜色的过程。Skia、CoreGraphics、Direct2D 等强大的光栅化库在高效绘图、混合与渲染方面投入了极大的精力。然而，应用程序要求这些库执行的低效操作序列仍在拖累其表现。即便是 Google Chrome——一个与 Skia 光栅化库协同开发、经过高度优化的程序——在最常访问的前 100 个网站上仍会生成低效的指令序列。这种低效的根本原因在于：光栅化库具有复杂的语义，以及不透明、不直观的执行模型。 为解决这一问题，我们提出 μSkia——Skia 2D 图形库的形式语义，并在 Lean 中对该语义进行机械化。μSkia 涵盖画布状态、图层栈、混合与颜色滤镜等语言及图形特性，且该语义本身分为三个层次，以实现关注点分离并支持扩展。随后，我们识别出 Google Chrome 生成的四类次优 Skia 代码模式，并为每种模式编写了替换实现。μSkia 使我们能够验证这些替换实现的正确性，包括识别出大量棘手的附带条件。接着，我们开发了一个高性能的 Skia 优化器，通过应用这些模式来加速光栅化。在从访问量前 100 的网站收集的 99 个 Skia 程序上，该优化器相比 Skia 最新的 GPU 后端实现了 18.7% 的加速，而优化本身耗时最多不超过 32 微秒。这些加速在多种网站、Skia 后端和 GPU 上均能保持。为提供真正的端到端验证，优化器生成的优化轨迹会被重新载入 μSkia 语义，并在 Lean 中完成翻译验证。
备注：（无）
学科：编程语言
ACM 分类：I.3；D.3.1；D.3.2
引用方式：arXiv:2603.23696 [cs.PL]
（或 arXiv:2603.23696v1 为本版本）
https://doi.org/10.48550/arXiv.2603.23696
arXiv 通过 DataCite 发放的 DOI
提交历史
来自：Bhargav Kulkarni [查看电子邮件]
[v1] 2026 年 3 月 24 日（周二）20:14:34 UTC（1,399 KB）
全文链接：
获取论文：
查看许可协议（CC BY 4.0）
当前浏览上下文：
cs.PL
新的 | 最新 | 2026 年 3 月
参考文献与引用
BibTeX 格式引用
数据由相关服务提供。
书签
文献与引用工具
- Bibliographic Explorer（文献浏览器）
- Connected Papers
- Litmaps
- scite.ai（智能引用）
本文相关的代码、数据与媒体
- alphaXiv
- CatalyzeX Code Finder
- DagsHub
- GotitPub
演示
- Replicate
- Hugging Face Spaces
- TXYZ.AI
相关论文
- Influence Flower
- CORE Recommender（支持按作者、会议、机构、主题推荐）
arXivLabs：与社区合作者共同开展的实验性项目
arXivLabs 是一个允许合作者在我们网站上开发并分享新 arXiv 功能的框架。
个人与组织均认可我们所秉持的开放、社区、卓越与用户数据隐私的价值观。arXiv 致力于这些价值观，并只与遵循这些价值观的伙伴合作。
对为 arXiv 社区增添价值的项目有想法？进一步了解 arXivLabs。
哪些作者是本文的认可者？ | [禁用 MathJax]