Affiliation: University of Utah, 201 Presidents’ Circle, Salt Lake City, UT, USA, 84112-0090email: bhargavk@utah.edu, Henry Whiting
Affiliation: University of Utah, 201 Presidents’ Circle, Salt Lake City, UT, USA, 84112-0090email: u1598085@utah.edu and Pavel Panchekha
Affiliation: University of Utah, 201 Presidents’ Circle, Salt Lake City, UT, USA, 84112-0090email: pavpan@cs.utah.edu© noneAbstract.
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 instructions
that they ask these libraries to perform.
Even Google Chrome, a highly optimized web browser
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 μ\muSkia,
a formal semantics for the Skia 2D graphics library,
and mechanize this semantics in Lean.
μ\muSkia 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.
μ\muSkia allows us to verify that 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 just 32 µ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 μ\muSkia semantics and translation validated in Lean.Keywords: Visual Languages, Rasterization, Computer Graphics, Compilers,
Semantics, Automated Verification, Interactive Theorem Proving, Web Browsers
1. Introduction
Every pixel you see on a computer screen
was produced by a process called rasterization.
Programs like desktop, mobile, and web applications
send a series of instructions to a rasterization library;
these instructions draw shapes, render text,
and blend overlapping visual elements.
Then, the rasterization library—which might be Skia, CoreGraphics, Direct2D, Cairo, or something else—executes the instructions,
determining the color of every pixel on the screen.
Rasterization must be done at interactive rates,
ideally 60 to 120 frames per second,
to ensure a smooth experience for users.
Rasterization libraries are thus highly optimized.
Skia, for example, targets
a wide variety of CPU- and GPU-based backends
using both legacy and modern graphics APIs
like OpenGL, Vulkan, and Metal.
In fact, between 2021 and 2025, the Skia team
wrote an entirely new backend, Graphite,
to improve rasterization times by about 15% (graphite-blog-post)
by leveraging new GPU APIs.
It’s therefore no surprise
that Skia is the rasterization library of choice for
the Google Chrome, Firefox, and Ladybird browsers,
the Android operating system, the Flutter mobile application framework,
as well as for native applications like Sublime Text.
Despite this extreme performance focus,
rasterization is not a solved problem.
Web browsers, for example, struggle to render modern web pages,
with trendy effects like partial transparency, animations, and blurs,
at a stable 60 frames per second,
especially on lower-end mobile devices.
The trend toward 120 Hz displays only raises the bar.
The reason this is so hard is that
while rasterization libraries implement individual instructions efficiently,
clients ask them to execute inefficient instruction sequences.
For example, the authors have manually examined
the instructions that Chrome executes to raster the top 100 websites (by traffic)
and identified numerous straightforward performance problems.
And Chrome is surely the most sophisticated Skia client:
it is developed at the same company,
with engineers working in such close coordination
that Chrome and Skia make simultaneous releases.
Other Skia clients are even worse off.
Improving the quality of rasterization programs
would dramatically reduce rasterization time,
but doing that is unnecessarily difficult
because rasterization libraries have strange, imperative semantics
and an opaque, non-obvious execution model.
We address this problem with μ\muSkia,
a formal semantics for the Skia 2D rasterization library.
μ\muSkia captures key features of the Skia API
like canvas state, the layer stack, clipping, and blending.
More generally,
since these features appear in all rasterization libraries,
drawing from their common PostScript heritage,
we see our formalization as providing a foundation
for future language-driven rasterization research.
Our formalization is built in three strata—a command language, a functional core, and an abstract model—that seperate concerns, simplify reasoning, and allow for extensibility.
The semantics is mechanized in Lean
and enables automated reasoning and verification of μ\muSkia programs.
To demonstrate the utility of μ\muSkia,
we identify four patterns of suboptimal Skia instructions
generated by Google Chrome on the top 100 websites by traffic.
For each one, we provide a more efficient instruction sequence
and prove the two sequences equivalent in Lean.
μ\muSkia enables us to identify non-trivial side conditions
and ensure that the optimization is correct.
We then build an optimizer that
applies these rewrite rules before rasterization,
enabling significant speed-ups to rasterization.
This simple optimizer results in an average speedup
of 18.7% over Skia’s most modern Graphite backend
on 99 Chrome-generated Skia programs
from the top 100 websites.
The optimizer is also highly efficient,
with optimization taking at most 32 µs,
and the optimizer improves rasterization time across Skia back-ends and GPUs.
Moreover, the optimizer is able to generate optimization traces
that can be translation validated using μ\muSkia,
providing an end-to-end proof of correctness for those programs.
In short, the contributions in this paper are:
A new formalization of the Skia API and rasterization more generally ()
A collection of focused optimizations proven valid using this formalization ()
A efficient and correct Skia optimizer that applies these optimizations ().