μSkia optimiert Skia-Code und beschleunigt das Rendering um 18,7 %
Compiler-style optimization for drawing via Skia
Selbst Google Chrome erzeugt auf den 100 meistbesuchten Websites ineffiziente Skia-Instruktionssequenzen, weil die Semantik der Rasterisierungsbibliothek komplex und undurchsichtig ist. μSkia, eine in Lean mechanisierte formale Semantik für Skia, deckt Canvas-Zustand, Layer-Stack, Blending und Farbfilter ab und identifiziert vier Muster suboptimalen Codes. Ein darauf aufbauender Optimierer ersetzt diese Muster, validiert die Übersetzung in Lean und erreicht auf 99 Skia-Programmen 18,7 % mehr Geschwindigkeit gegenüber Skia's modernstem GPU-Backend – bei maximal 32 μs Optimierungszeit.
Selbst Google Chrome, ein hochoptimiertes Programm, das gemeinsam mit der Skia-Rasterisierungsbibliothek entwickelt wurde, erzeugt noch ineffiziente Instruktionssequenzen, sogar auf den 100 meistbesuchten Websites.