Compiler-style optimization for drawing via Skia
Recorded: Sept. 19, 2026, 10 p.m.
| Original | Summarized |
[2603.23696] Semantics for 2D Rasterization
Skip to main content Search Log in Search arXiv Press Enter to search · Advanced search Computer Science > Programming Languages arXiv:2603.23696 (cs) [Submitted on 24 Mar 2026] Abstract:Rasterization is the process of determining the color of every pixel drawn by an application. Powerful rasterization libraries like Skia, CoreGraphics, and Direct2D put exceptional effort into drawing, blending, and rendering efficiently. Yet applications are still hindered by the inefficient sequences of operations that they ask these libraries to perform. 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. The underlying reason for this inefficiency is that rasterization libraries have complex semantics and opaque and non-obvious execution models. Subjects: Programming Languages (cs.PL) Cite as: Focus to learn more arXiv-issued DOI via DataCite Submission history From: Bhargav Kulkarni [view email] [v1]
Full-text links: View a PDF of the paper titled Semantics for 2D Rasterization, by Bhargav Kulkarni and 2 other authorsView PDFHTML (experimental)TeX Source view license < prev | new Change to browse by: References & Citations NASA ADSGoogle Scholar export BibTeX citation BibTeX formatted citation loading... Data provided by: Bookmark
Bibliographic Tools Bibliographic and Citation Tools Bibliographic Explorer Toggle Bibliographic Explorer (What is the Explorer?) Connected Papers Toggle Connected Papers (What is Connected Papers?) Litmaps Toggle Litmaps (What is Litmaps?) scite.ai Toggle scite Smart Citations (What are Smart Citations?) Code, Data, Media Code, Data and Media Associated with this Article alphaXiv Toggle alphaXiv (What is alphaXiv?) Links to Code Toggle CatalyzeX Code Finder for Papers (What is CatalyzeX?) DagsHub Toggle DagsHub (What is DagsHub?) GotitPub Toggle Gotit.pub (What is GotitPub?) Huggingface Toggle Hugging Face (What is Huggingface?) ScienceCast Toggle ScienceCast (What is ScienceCast?) Demos Demos Replicate Toggle Replicate (What is Replicate?) Spaces Toggle Hugging Face Spaces (What is Spaces?) Spaces Toggle TXYZ.AI (What is TXYZ.AI?) Related Papers Recommenders and Search Tools Link to Influence Flower Influence Flower (What are Influence Flowers?) Core recommender toggle CORE Recommender (What is CORE?) Author About arXivLabs arXivLabs: experimental projects with community collaborators Which authors of this paper are endorsers? | We gratefully acknowledge support from About Major funding support from |
The research introduces $\mu$Skia, a formal semantics for the Skia 2D graphics library, aimed at addressing the inefficiency arising from the complex and opaque execution models within rasterization systems. While powerful rasterization libraries such as Skia, CoreGraphics, and Direct2D are designed for efficient drawing, applications often execute sequences of operations that are inherently suboptimal. This inefficiency stems from the intricate semantics and execution models embedded within these rasterization libraries. To formalize this complexity and enable verifiable optimizations, the authors developed $\mu$Skia, which covers critical language and graphics features including canvas state management, the layer stack, blending operations, and color filters. The semantics of $\mu$Skia are structured into three distinct strata to effectively separate concerns, which enhances extensibility of the framework. A key methodological step involved identifying four specific patterns of sub-optimal code generated by Google Chrome and subsequently developing replacements for these patterns. The $\mu$Skia framework was instrumental in verifying that these replacements were correct, including the identification of numerous complex side conditions associated with the operations. Building upon this formal foundation, the research developed a high-performance Skia optimizer. This optimizer uses the identified sub-optimal patterns to speed up the rasterization process significantly. Empirical testing on 99 Skia programs drawn from the top one hundred visited websites demonstrated that this optimizer achieves an 18.7 percent speedup compared to Skia’s most modern GPU backend, with the optimization process itself requiring at most thirty-two microseconds. These observed speedups were consistent across various websites, Skia backends, and different graphics processing units. Furthermore, true end-to-end verification was achieved by loading the optimization traces produced by the optimizer back into the $\mu$Skia semantics to validate the results. This closed-loop verification process ensures the correctness of the optimizations by validating them against the formal semantics established in Lean. |