プログラミング

Skiaによる描画のためのコンパイラ風最適化

Compiler-style optimization for drawing via Skia (arxiv.org)

111 pointsby PaulDavisThe1st2026年9月18日21 コメント

要約

本論文では、2DラスタライゼーションライブラリであるSkiaの効率を向上させるための新しいアプローチを提案しています。研究者たちは、Skiaの複雑なセマンティクスと実行モデルに起因する非効率性を特定し、形式的な意味論「μSkia」を開発しました。これにより、Google Chromeが生成する非効率な描画コードパターンを検出し、最適化することで、GPUバックエンドと比較して18.7%の高速化を実現しました。

全文翻訳

コンピュータサイエンス > プログラミング言語

arXiv:2603.23696 (cs)

[2026年3月24日提出（v1）、2026年10月12日改訂（本版、v2）]

2Dラスタライゼーションの意味論

著者: Bhargav Kulkarni, Henry Whiting, Pavel Panchekha

Bhargav Kulkarniらによる「Semantics for 2D Rasterization」というタイトルの論文のPDFを表示

PDFを表示 HTML（実験的）

要約: ラスタライゼーションは、アプリケーションによって描画される各ピクセルの色を決定するプロセスです。Skia、CoreGraphics、Direct2Dのような強力なラスタライゼーションライブラリは、効率的な描画、ブレンド、レンダリングに多大な努力を払っています。しかし、アプリケーションは、これらのライブラリに実行させる非効率な命令シーケンスによって依然として妨げられています。Skiaラスタライゼーションライブラリと共同開発された高度に最適化されたWebブラウザであるGoogle Chromeでさえ、上位100の最も訪問されたWebサイトにおいても非効率な命令シーケンスを生成しています。この非効率性の根本的な理由は、ラスタライゼーションライブラリが複雑な意味論と、不透明で明白ではない実行モデルを持っていることです。
この問題に対処するため、Skia 2Dグラフィックスライブラリの形式意味論であるμSkiaを導入し、Leanでこの意味論を機械化しました。μSkiaは、キャンバス状態、レイヤスタック、ブレンド、カラーフィルターなどの言語およびグラフィックス機能をカバーしており、意味論自体は懸念事項を分離し拡張性を可能にするために3つの階層に分割されています。次に、Google Chromeによって生成される最適化されていないSkiaコードの4つのパターンを特定し、各パターンに対応する置換コードを作成しました。μSkiaにより、多数のトリッキーな副条件を特定することを含め、置換コードの正しさを検証できます。その後、これらのパターンを適用してラスタライゼーションを高速化する高性能Skiaオプティマイザを開発しました。上位100のWebサイトから収集された139のSkiaプログラムにおいて、このオプティマイザはSkiaの最新GPUバックエンドと比較して1.12倍の高速化を実現し、最適化にはわずか0.03ミリ秒しかかかりませんでした。この高速化は、さまざまなWebサイト、Skiaバックエンド、GPUで持続します。真のエンドツーエンド検証を提供するために、オプティマイザによって生成された最適化トレースはμSkia意味論にロードバックされ、Leanで翻訳検証されます。


コメント:	26ページ、17図。成果物: this https URL
件名:	プログラミング言語 (cs.PL)
ACMクラス:	I.3; D.3.1; D.3.2
引用:	arXiv:2603.23696 [cs.PL]
	（または本版の arXiv:2603.23696v2 [cs.PL]）
	https://doi.org/10.48550/arXiv.2603.23696 DataCite経由のarXiv発行DOI
ジャーナル参照:	Proceedings of the ACM on Programming Languages 10, OOPSLA2 (2026), 681-706
関連DOI:	https://doi.org/10.1145/3839471 関連リソースへのリンクDOI