Chromeでさえ非効率なSkia命令列、Lean検証済みオプティマイザで18.7%高速化
Compiler-style optimization for drawing via Skia
SkiaやCoreGraphicsなどのラスタライズライブラリは高速化に努めているが、アプリケーションが発行する命令列は依然として非効率だ。Skiaと共同開発されたGoogle Chromeでも、上位100サイトで無駄な命令列を生成している。本研究はSkiaの形式意味論μSkiaをLeanで機械化し、Chromeが生む4つの非効率パターンを特定。検証済みの置換を適用する高性能オプティマイザを開発し、最上位100サイトから集めた99のSkiaプログラムで最新GPUバックエンド比18.7%の高速化を達成した。最適化時間は最大32μsで、検証トレースはLeanに再ロードして翻訳を検証する。
Skiaラスタライズライブラリと共同開発された高度に最適化されたプログラムであるGoogle Chromeでさえ、最も訪問者の多い上位100のウェブサイト上でも非効率な命令列を依然として生成している。
HNでの議論
20- eigenblake
わあ！これはワクワクする。こういうことが可能だろうと推測していたんだ。データベースと動的なDBクエリ最適化について学んでいるうちに、もっと多くの計算の世界でも同じようなものがあってもおかしくないのにと驚いた。これが登場した今、同じ高レベルのテクニックを使って他に何を最適化できるのか気になってくる。
やりたいことを事前にどれだけ知っていれば、ステップの順序をより最適に並べ替えて、素朴な解法より良い解を得られる。これはすべてのソフトウェアをこうした抽象的な計算グラフとして捉えることにつながり、他に何を自動で最適化できるのかと考えさせられる。
もちろん、ここでは正式なモデルが絶対に必要で、DBエンジンが関係代数を裏付けモデルとして持つのと同じように、どんな編集が可能かを知ることができる。でもこの一連の話は、手作業のソフトウェア最適化がまもなくAIに取って代わられるような気にさせる。しかも、まずは昔ながらのAIであって、LLMは二の次だと思う。とはいえLLMもここでは役に立つだろう、特に形式化においては。
- mtklein
元Skiaコントリビューターとして、これを読むのはめちゃくちゃクールだ。まさに我々がSkRecordシステムを書いたときに念頭に置いていた最適化の仕事だし、nanobenchを活用してもらえたのは嬉しい。当時は適用できる小さな最適化がほんの少ししかなくて、主に不要なsaveLayer()呼び出しを排除しようとしていた。Leanを使って現代的なやり方で実現されているのを見るのはとてもクールだ。
- pavpanchekha
皆さんこんにちは！最後の著者です。質問には喜んで答えます。HNでこれを見るとはとても驚きました。取り組むのはすごく楽しかったです。付け加えると、GoogleのSkiaチームはとても協力的で、たくさんのことを説明するために何度もミーティングを開いてくれました。
このプロジェクトのアイデアは、Chris Harrelsonと『Web Browser Engineering』（https://browser.engineering/ 参照）を書いているときに何年も前に思いつきました。それから数年前にYuvaraj（https://droidkid.github.io/）とこのプロジェクトに最初の試みをしましたが、いろいろあってあまり進みませんでした。約1年前にBhargav（https://bhargavkk.com/）とプロジェクトを再開し、Skia自体のセマンティクスにはるかに真剣に焦点を当てたことで、進歩がずっと速くなりました。それでも、正直なところ、結果がこれほど良いとは驚きました。