[2603.23696] Semantics for 2D Rasterization

-->

Computer Science > Programming Languages

arXiv:2603.23696 (cs)

[Submitted on 24 Mar 2026]

Title:Semantics for 2D Rasterization

Authors:Bhargav Kulkarni, Henry Whiting, Pavel Panchekha<br>View a PDF of the paper titled Semantics for 2D Rasterization, by Bhargav Kulkarni and 2 other authors

View PDF<br>HTML (experimental)

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.

To address this issue, we introduce $\mu$Skia, a formal semantics for the Skia 2D graphics library, and mechanize this semantics in Lean. $\mu$Skia covers language and graphics features like canvas state, the layer stack, blending, and color filters, and the semantics itself is split into three strata to separate concerns and enable extensibility. We then identify four patterns of sub-optimal Skia code produced by Google Chrome, and then write replacements for each pattern. $\mu$Skia allows us to verify the replacements are correct, including identifying numerous tricky side conditions. We then develop a high-performance Skia optimizer that applies these patterns to speed up rasterization. On 99 Skia programs gathered from the top 100 websites, this optimizer yields a speedup of 18.7% over Skia's most modern GPU backend, while taking at most 32 $\mu$s for optimization. The speedups persist across a variety of websites, Skia backends, and GPUs. To provide true, end-to-end verification, optimization traces produced by the optimizer are loaded back into the $\mu$Skia semantics and translation validated in Lean.

Comments:<br>23 pages, 15 figures

Subjects:

Programming Languages (cs.PL)

ACM classes:<br>I.3; D.3.1; D.3.2

Cite as:<br>arXiv:2603.23696 [cs.PL]

(or<br>arXiv:2603.23696v1 [cs.PL] for this version)

https://doi.org/10.48550/arXiv.2603.23696

Focus to learn more

arXiv-issued DOI via DataCite

Submission history<br>From: Bhargav Kulkarni [view email]<br>[v1]<br>Tue, 24 Mar 2026 20:14:34 UTC (1,399 KB)

Full-text links:<br>Access Paper:

View a PDF of the paper titled Semantics for 2D Rasterization, by Bhargav Kulkarni and 2 other authors<br>View PDF<br>HTML (experimental)<br>TeX Source

view license

Current browse context:

cs.PL

next >

new<br>recent<br>| 2026-03

Change to browse by:

cs

References & Citations

NASA ADS<br>Google Scholar

Semantic Scholar

export BibTeX citation<br>Loading...

BibTeX formatted citation

&times;

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

Venue

Institution

Topic

About arXivLabs

arXivLabs: experimental projects with community collaborators

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs .

Which authors of this paper are endorsers? |<br>Disable MathJax (What is MathJax?)