El artículo 'Semantics for 2D Rasterization', presentado en arXiv el 24 de marzo de 2026, introduce μSkia, una semántica formal para la biblioteca de gráficos 2D Skia. Este trabajo aborda la ineficiencia en las secuencias de operaciones de aplicaciones que utilizan librerías de rasterización como Skia, CoreGraphics o Direct2D, incluso en programas altamente optimizados como Google Chrome. La causa raíz de esta lentitud es la complejidad de las semánticas subyacentes y los modelos de ejecución opacos de estas librerías.
Para resolverlo, los autores formalizaron la semántica de Skia en el lenguaje de verificación Lean. El sistema μSkia cubre características clave como el estado del lienzo, la pila de capas, el mezclado de colores y los filtros de color, organizándose en tres estratos para facilitar la extensibilidad. El estudio identificó cuatro patrones de código de Skia subóptimos producidos por Google Chrome y desarrolló reemplazos para cada uno. Estos reemplazos fueron verificados mediante μSkia, lo que permitió detectar condiciones laterales complejas.
Basándose en esta semántica, los autores desarrollaron un optimizador de alto rendimiento para Skia. Al aplicar estos patrones a 99 programas de Skia recopilados de los 100 sitios web más visitados, el optimizador logró una aceleración del 18,7% sobre el backend GPU más moderno de Skia, con un tiempo de optimización máximo de 32 microsegundos. Estas mejoras persistieron en diversos sitios, backends y GPUs. Para garantizar una verificación de extremo a extremo, las trazas de optimización se cargaron en μSkia y se validaron en Lean, asegurando la corrección de las transformaciones.