Affiliation: University of Utah, 201 Presidents’ Circle, Salt Lake City, UT, USA, 84112-0090email: bhargavk@utah.edu, Henry Whiting\nAffiliation: University of Utah, 201 Presidents’ Circle, Salt Lake City, UT, USA, 84112-0090email: u1598085@utah.edu and Pavel Panchekha\nAffiliation: University of Utah, 201 Presidents’ Circle, Salt Lake City, UT, USA, 84112-0090email: pavpan@cs.utah.edu© noneAbstract.
\nRasterization is the process of determining\nthe color of every pixel drawn by an application.\nPowerful rasterization libraries\nlike Skia, CoreGraphics, and Direct2D\nput exceptional effort into drawing, blending, and rendering efficiently.\nYet applications are still hindered\nby the inefficient sequences of instructions\nthat they ask these libraries to perform.\nEven Google Chrome, a highly optimized web browser\nco-developed with the Skia rasterization library,\nstill produces inefficient instruction sequences\neven on the top 100 most visited websites.\nThe underlying reason for this inefficiency\nis that rasterization libraries have complex semantics\nand opaque and non-obvious execution models.
\nTo address this issue, we introduce μ\\muSkia,\na formal semantics for the Skia 2D graphics library,\nand mechanize this semantics in Lean.\nμ\\muSkia covers language and graphics features\nlike canvas state, the layer stack, blending, and color filters,\nand the semantics itself is split into three strata\nto separate concerns and enable extensibility.\nWe then identify four patterns\nof sub-optimal Skia code produced by Google Chrome,\nand then write replacements for each pattern.\nμ\\muSkia allows us to verify that the replacements are correct,\nincluding identifying numerous tricky side conditions.\nWe then develop a high-performance Skia optimizer\nthat applies these patterns to speed up rasterization.\nOn 99 Skia programs\ngathered from the top 100 websites,\nthis optimizer yields a speedup of 18.7% over Skia’s most modern GPU backend,\nwhile taking just 32 µs for optimization.\nThe speedups persist across a variety of\nwebsites, Skia backends, and GPUs.\nTo provide true, end-to-end verification,\noptimization traces produced by the optimizer\nare loaded back into the μ\\muSkia semantics and translation validated in Lean.Keywords: Visual Languages, Rasterization, Computer Graphics, Compilers,\nSemantics, Automated Verification, Interactive Theorem Proving, Web Browsers
\nEvery pixel you see on a computer screen\nwas produced by a process called rasterization.\nPrograms like desktop, mobile, and web applications\nsend a series of instructions to a rasterization library;\nthese instructions draw shapes, render text,\nand blend overlapping visual elements.\nThen, the rasterization library—which might be Skia, CoreGraphics, Direct2D, Cairo, or something else—executes the instructions,\ndetermining the color of every pixel on the screen.\nRasterization must be done at interactive rates,\nideally 60 to 120 frames per second,\nto ensure a smooth experience for users.\nRasterization libraries are thus highly optimized.\nSkia, for example, targets\na wide variety of CPU- and GPU-based backends\nusing both legacy and modern graphics APIs\nlike OpenGL, Vulkan, and Metal.\nIn fact, between 2021 and 2025, the Skia team\nwrote an entirely new backend, Graphite,\nto improve rasterization times by about 15% (graphite-blog-post)\nby leveraging new GPU APIs.\nIt’s therefore no surprise\nthat Skia is the rasterization library of choice for\nthe Google Chrome, Firefox, and Ladybird browsers,\nthe Android operating system, the Flutter mobile application framework,\nas well as for native applications like Sublime Text.
\nDespite this extreme performance focus,\nrasterization is not a solved problem.\nWeb browsers, for example, struggle to render modern web pages,\nwith trendy effects like partial transparency, animations, and blurs,\nat a stable 60 frames per second,\nespecially on lower-end mobile devices.\nThe trend toward 120 Hz displays only raises the bar.\nThe reason this is so hard is that\nwhile rasterization libraries implement individual instructions efficiently,\nclients ask them to execute inefficient instruction sequences.\nFor example, the authors have manually examined\nthe instructions that Chrome executes to raster the top 100 websites (by traffic)\nand identified numerous straightforward performance problems.\nAnd Chrome is surely the most sophisticated Skia client:\nit is developed at the same company,\nwith engineers working in such close coordination\nthat Chrome and Skia make simultaneous releases.\nOther Skia clients are even worse off.\nImproving the quality of rasterization programs\nwould dramatically reduce rasterization time,\nbut doing that is unnecessarily difficult\nbecause rasterization libraries have strange, imperative semantics\nand an opaque, non-obvious execution model.
\nWe address this problem with μ\\muSkia,\na formal semantics for the Skia 2D rasterization library.\nμ\\muSkia captures key features of the Skia API\nlike canvas state, the layer stack, clipping, and blending.\nMore generally,\nsince these features appear in all rasterization libraries,\ndrawing from their common PostScript heritage,\nwe see our formalization as providing a foundation\nfor future language-driven rasterization research.\nOur 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.\nThe semantics is mechanized in Lean\nand enables automated reasoning and verification of μ\\muSkia programs.
\nTo demonstrate the utility of μ\\muSkia,\nwe identify four patterns of suboptimal Skia instructions\ngenerated by Google Chrome on the top 100 websites by traffic.\nFor each one, we provide a more efficient instruction sequence\nand prove the two sequences equivalent in Lean.\nμ\\muSkia enables us to identify non-trivial side conditions\nand ensure that the optimization is correct.\nWe then build an optimizer that\napplies these rewrite rules before rasterization,\nenabling significant speed-ups to rasterization.\nThis simple optimizer results in an average speedup\nof 18.7% over Skia’s most modern Graphite backend\non 99 Chrome-generated Skia programs\nfrom the top 100 websites.\nThe optimizer is also highly efficient,\nwith optimization taking at most 32 µs,\nand the optimizer improves rasterization time across Skia back-ends and GPUs.\nMoreover, the optimizer is able to generate optimization traces\nthat can be translation validated using μ\\muSkia,\nproviding an end-to-end proof of correctness for those programs.
\nIn short, the contributions in this paper are:
\nA new formalization of the Skia API and rasterization more generally ()
\nA collection of focused optimizations proven valid using this formalization ()
\nA efficient and correct Skia optimizer that applies these optimizations ().
","headings":[{"level":1,"text":"Semantics for 2D RasterizationCCS: Computing methodologies RasterizationCCS: Software and its engineering Visual languagesCCS: Software and its engineering SemanticsBhargav K Kulkarni","id":"semantics-for-2d-rasterizationccs-computing-methodologies-raster"},{"level":2,"text":"1. Introduction","id":"1-introduction"}]}}