社内勉強会でPLDI論文読み会を開催しました

2022年6月14日 18:55

κeenです。しばらく前になってしまいましたが、Idein社内でPLDI '21論文読み会が開催されたので報告します。

Programming Language Design and Implementation（PLDI）はその名の通りプログラミング言語の設計と実装に関連するトピックを集めた最高峰の研究カンファレンスです^1。個人的感覚ですが、実装も含めたトピックを扱うということから大企業での実例も含んだ論文が多いのが特徴かなと思ってます。

社内でインターネットの闇さんがこのPLDI '21の論文読み会を開催したいので読んでくる人を募集すると呼び掛けたところ想定以上の反響があり、合計8人が集ったのでそのまま開催される運びになりました。それぞれ読んでくる論文を決め、1ヶ月程度の準備期間を置いて30分程度で発表する形式となりました。

以下、二日に分けて開催された読み会の発表順にめいめいが読んできた論文を紹介します

Perceus: Garbage Free Reference Counting with Reuse

著者: Alex Reinking, Ningning Xie, Leonardo de Moura, Daan Leijen
読み担当: κeen
参考リンク: 概要、発表資料
本論文はPLDI '21のDistinguished Papersに選ばれています。

初日の1本目はκeenから、コンパイル言語での参照カウントの扱いを改善してメモリ効率を向上したり、新しいプログラミング様式を提案したりしたPerceusの論文です。PerceusはKoka言語のメモリ管理に使われています。

本手法では参照カウントの値のdup/dropを明示的に扱う体系を導入しています。その体系の上でdup/dropを挿入するアルゴリズムや不要なdup/dropを減らす最適化を提案し、それらが健全性(必要なメモリを不用意に開放しないこと)と正確性(ゴミを発生させずに直ちに回収すること。最終的にゴミが回収される完全性より強い)を満たすことを証明しています。内容が盛り沢山で焦点を絞りづらいのですが、ここではメモリの再利用とそれを利用した新しいプログラミング様式、Functional But In Place (FBIP)についてもう少し詳細に紹介します。

例としてリストの map 関数を見てみましょう。

fun map( xs : list ⟨a⟩, f : a -> e b ) : e list ⟨b⟩ {
  match(xs) {
    Cons(x,xx) -> Cons(f(x), map(xx,f))
    Nil        -> Nil
  }
}

これに愚直に dup/dropを差し込むとこうなります。

fun map( xs, f ) {
  match(xs) {
    Cons(x,xx) {
      dup(x); dup(xx); drop(xs)
      Cons(dup(f)(x), map(xx, f))
    }
    Nil { drop(xs); drop(f); Nil }
  }
}

dupやdropが多いですね。Cons 節の dup(x); dup(xx); drop(xs) 付近でもう少し上手くやれそうです。

xs の参照カウントが1の場合( xs がユニークの場合)、 drop で x と xx の参照カウントが減るので直前の dup と相殺できる
同じく xs がユニークの場合、メモリを開放するが直後に同じサイズの Cons を確保しているので相殺できる

これらを組み合わせると効率的なメモリ管理ができます。2をするためヘルパとして再利用できるメモリがあれば新たに確保せずに利用する Cons@ru を定義しておきます。

fun Cons@ru(x, xx) {
  if (ru!=NULL)
  then { ru->head := x; ru->tail := xx; ru } // in-place
  else Cons(x,xx)                            // malloc’d
}

すると map は以下のように無駄な操作がない形に変形できます。

fun map( xs, f ) {
  match(xs) {
    Cons(x,xx) {
      val ru = if (is-unique(xs))
               then &xs
               else dup(x); (dup xx);
                    decref(xs); NULL
      Cons@ru(dup(f)(x), map(xx, f))
    }
    Nil { drop(xs); drop(f); Nil }
  }
}

これを利用して、関数型だがメモリを使わないプログラミング様式FBIPが可能になります。FBIPは末尾呼出(再帰)の最適化と比べられます。関数呼出で必ずスタックを使うと、実用上関数だけでプログラミングはできませんが、末尾呼出の最適化があると関数で実用的なループが書けるようになります。
同様にメモリの再利用を保証できればFBIPというプログラムの書き方ができるようになります。

実例として論文中では二分木の操作が挙げられています。二分木の定義とそのmap操作(tmap)は愚直には以下のように定義できます。

type tree {
  Tip
  Bin(left: tree, value : int, right: tree )
}
fun tmap(t : tree, f : int -> int ) : tree {
  match(t) {
    Bin(l,x,r) -> Bin(tmap(l,f), f(x), tmap(r,f) )
    Tip -> Tip
  }
}

Perceusのおかげでメモリは再利用されるものの、 tmap は非末尾再帰なのでコールスタックを使ってしまいます。そこで補助データ構造として visitor を導入することでメモリを再利用しつつ末尾再帰関数で tmap を実装できます。

type visitor {
  Done
  BinR(right:tree, value : int, visit : visitor )
  BinL(left:tree, value : int, visit : visitor )
}

type direction { Up; Down }

fun tmap(f : int -> int, t : tree, visit : visitor, d : direction ) : tree {
  match(d) {
    Down -> match(t) {       // going down a left spine
      Bin(l,x,r) -> tmap(f,l,BinR(r,x,visit),Down) // A
      Tip -> tmap(f,Tip,visit,Up)                  // B
    }
    Up -> match(visit) { // go up through the visitor
      Done -> t                                    // C
      BinR(r,x,v) -> tmap(f,r,BinL(t,f(x),v),Down) // D
      BinL(l,x,v) -> tmap(f,Bin(l,x,t),v,Up)       // E
    }
  }
}

visitor は zipperと呼ばれるもので、 tree の構造から自然に導出できます。
また、これはモリスの行きがけ順巡回に相当するコードになっています。

ある程度意識して書くことで関数型な書き方でも効率的なコードになるのは面白いですね。

自分の担当なので少し力が入ってしまいましたが次からはもう少しサクサクいきます。因みに現実の発表でもκeenの発表が一番時間を使ってしまいました。

Provable Repair of Deep Neural Networks

著者: Matthew Sotoudeh, Aditya V. Thakur
読み担当: notogawa
参考リンク: 概要、発表資料↓

2本目はnotogawaからDNNの学習済みデータにおいて特定の入力に対する振る舞いに変更をかける手法を提案する論文の紹介です。

DNNを運用していて特定のケースでの推論に問題が見付かった際にその振る舞いを修正したくなることがあります。修正する1つの方法はその特定のケースでのデータを追加して再学習というのがありますが、学習時間が長くて現実的でなかったり学習に用いたデータが今では使えないようなケースがありえます。再学習より効率的な他の修正方法にファインチューニングもありますが、今度は無関係な入力に対する精度の劣化がありえます。そこで以下の条件を満たす修正手法が欲しくなります。

有効性: 修正対象の入力に対して正しく修正した出力を返す
汎化性: 修正対象の入力に似た入力に対しても修正した出力に似た出力を返す
局所性: 修正対象の入力に似ていない入力に対しては元のままの出力を返す
効率性: 効率的に修正できる

そこでこれらの条件を満たす Provable Point-wise Repair という手法を提案しています。この手法では修正対象の入力と望ましい出力の組をいくつか与えてDNNへのパッチを当てます。また、 Provable Polytope Repair という手法も提案しています。こちらはPoint-wiseとは異なり、修正対象の入力を(凸)超多面体で指定するので無限の入力に対する修正が与えれられます。

さらに、これらの手法を適用するのにDNNの層に最小限の修正を加えるのは非線型な活性化関数を考えるとNP困難であるためDecoupled DNNというアーキテクチャを導入し、その上での解法を考えています。こうすることで線型計画法で問題を解けるようにしています。ReLUのように適切なドメインに分割してあげるとそのドメイン毎に等価なアフィン変換があるような関数を考えると良い感じの変形を線形計画法で解けるというのが基本的なアイディアのようです。

これらの手法の有効性を確認するため何種類かのファインチューニングと比較したベンチマークを取っています。提案手法は有効性、局所性、効率性のバランスが取れた結果となっていました。

DNNFusion: Accelerating Deep Neural Networks Execution with Advanced Operator Fusion

著者: Wei Niu, Jiexiong Guan, Yanzhi Wang, Gagan Agrawal, Bin Ren
読み担当: bonotake
参考リンク: 概要、発表資料↓

1日目の最後はbonotakeから、DNNにおけるオペレータのフュージョンのパターンを一般化して汎用性と最適化性能を上げた論文の紹介です。

DNNをコンパイルして最適化するときにオペレータのフュージョンはよく使われる手法の1つですが、既存の多面体解析やTVMなどのフレームワークでは汎用性に問題がありました。そこでフュージョンの判断を汎用的にしたのが提案手法です。以下のような流れでフュージョンを行います。

GenericなパターンでFusionするかを判断
- 各オペレータにmapping typeという型を導入
- 組み合わせの “収益性” (profitability) を導入
- 型の組み合わせ＋収益性のあるなしでfusionするかを判断
Extended Computational Graph (ECG) の導入
- 普通のCG ＋ mapping type
代数的な性質に基づいたグラフ書き換え
Mapping type に基づいた fusion plan generation

これらの手法を用いて実験したところ、以下の結果が得られました。

モバイル端末（Galaxy S20）上でTVMの1.5～3.5倍、TFLiteの1.4～3.3倍高速化
従来のコンパイラでは非対応だったネットワーク（Faster R-CNNなど）もモバイル端末で動かせるように

発表のあと議論があり、フュージョンができることは分かるが、実装を生成する方法には触れられていないので1つ1つ手で実装しないといけないのではないかという話になりました。汎用的な手法なだけあって実装対象はかなりの数(〜100)になるはずですが、実際にベンチマークを取っていることから裏でとてつもない努力をしていることが偲ばれます。

一日目はκeenが喋りすぎたのと準備が間に合わなかった人がいたのでここまででした。次週の同じ時間に二日目が開催され、5人が発表しています。

AKG: Automatic Kernel Generation for Neural Processing Units using Polyhedral Transformations

著者: Jie Zhao, Bojie Li, Wang Nie, Zhen Geng, Renwei Zhang, Xiong Gao, Bin Cheng, Chen Wu, Yun Cheng, Zheng Li, Peng Di, Kun Zhang, Xuefeng Jin
読み担当: インターネットの闇
参考リンク: 概要、発表資料↓

二日目のトップバッターはインターネットの闇さんからで、Huawei Ascend 910というNPU向けのグラフコンパイラ、AKGの実装について報告した論文の紹介です。実装の難しい点としてメモリ階層がやや入り組んでいたり特殊なデータフローを持っていたり、NPU向けのハード固有最適化が従来の手法ではサポートされていなかったりなどの問題が挙げられます。

AKGは大枠ではTVMを改造して多面体最適化しつつNPU固有の最適化もしています。例えばHuawei Ascend 910にはim2colをしてくれるMemory Transfer Engineがあるのでそこを考慮する必要があります。他にもタイル化する際のタイルサイズの決定を自動化したりなどの気合が必要な実装もやっているようです。

実装したコンパイラは単一のオペレータ、サブグラフ、End-to-Endネットワークのベンチマーク、コードサイズなどで比較評価し、手動最適化や素のTVMと比べて遜色ない、あるいは上回るパフォーマンスを出していました。

コンパイラで使う個々の要素技術ではなく全体を通しての設計や頑張りどころが示されておりTonsor Compilerを作る上で参考になりそうでした。

Specification Synthesis with Constrained Horn Clauses

著者: Sumanth Prabhu, Grigory Fedyukovich, Kumar Madhukar, Deepak D'Souza
読み担当: wasabiz
参考リンク: 概要、発表資料↓
本論文はPLDI '21のDistinguished Papersに選ばれています。

サイズの問題で埋め込み形式だと左右が切れてしまうようなので全画面での閲覧をお願いします

続いてwasabizから、極大かつ非空な仕様合成をする新しいアルゴリズムを提案した論文の紹介です。

プログラム検証などの文脈で、仕様合成(Specification Synthesis)呼ばれる問題があります。この問題で応用上求められる性質として極大(Maximal)であることと非空(Non-vacous)であることが求められます。本論文では既存の手法を使ってこれらの性質を満たす仕様をみつける新しいアルゴリズムを提案しています。

仕様合成の例を挙げておきます。以下のようなコードを考えます。

in x = 19;
while(*) {
  int z = f();
  x = x + z;
}
int y = g();
assert(y >= x);

このコードは未知の関数 f 、 g を含んんでいたり、 while の条件が * のように非決定的選択になっています(ループの終了条件は一般には解析できない)。この設定で末尾の assert(y >= x); 充足するには f と g がどのような仕様を満たさないといけないか探索せよ、というのが仕様合成の例です。仕様は $${F(z): \iff z = -1, G(y): \iff y = 19}$$ のような限定的なものでも条件を満たせますが、可能な限り広い極大な仕様だと $${F(z): \iff z \le 0, G(y): \iff y \ge 19}$$ になります。

仕様合成する方法にConstrained Horn Clauses (CHC)を使ったものがあります。上記の例でいえばループ不変条件を $${Inv(x)}$$ とすると以下のCHCが書けます。

$$
x = 19 \implies Inv(x) \\ Inv(x) \land f(z) \land x' = x + z \implies Inv(x') \\ Inv(x) \land g(y) \land \lnot (y \ge x) \implies \bot
$$

CHCのソルバは既存のものがいくつかあるのであとはこれをソルバに投げれば解いてくれるはずです。ですが、いくつか問題を孕んでいます。

帰納的なCHCがあると求解に時間が掛かる
$${F(z): \iff \mathbf{false}, G(y): \iff \mathbf{false}, Inv(x): \iff \mathbf{true}}$$ のような面白くない(空な)解が出てくる
解が極大とは限らない

そこで、これらの問題を解消するアルゴリズムを作ったというのが本論文の趣旨です。既存のCHCソルバなどいくつかのシステムを組み合わせてNon-Vacuousな解をみつけつつ、それが極大であるか検査して極大であればそれを出力し、極大でなければもっと弱い条件の解を探しているようです。

ベンチマークをとって既存のソルバ(z3, CVC4)と比較した結果、30秒以内に解けた問題数などで提案手法が上回っていたようです。

Cyclic Program Synthesis

著者: Shachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe, Ilya Sergey
読み担当: 江口
参考リンク: 概要、発表資料↓
本論文はPLDI '21のDistinguished Papersに選ばれています。

続いて江口から再帰的な補助関数を含むheap-manipulating programの自動生成に関する論文の紹介です。先ほどのものがプログラムから仕様を生成するのに対してこちらは仕様からプログラムを生成します。

ここでプログラムの仕様を記述するのには分離論理を使います。分離論理を使うとメモリ上の2つのデータを入れ替える swap や木構造を表現したりとヒープを扱う仕様が記述できます。分離論理を使ったプログラム合成はSynthetic Separation Logic(SSL)というプログラム生成用の推論体系を使ったSusLicというものが存在していました。

しかし、既存の手法では補助関数付きのプログラムが生成できませんでした。例えば木を単方向連結リストに変換する flatten は補助関数としてlistのappendも必要になるため、生成できません。これは一般に補助関数の仕様を自動で見付けるのが難しいという問題でもあります。

そこで本論文では循環証明を用いてSSLを拡張した体系を考案し、その上でプログラム合成を行うことで補助関数付きプログラムも生成できるようにしました。ここで出てきた循環証明は証明木に循環を許す証明体系です。

提案手法を用いてリストの重複除去などいくつかの複雑なプログラムの生成に成功しています。ただし、いくつかは仕様を上手く調整してあげる必要があったり、生成したプログラムが普通のプログラムとは程遠いものになったりはしたようです。

生成するプログラムには新たなデータ構造を使うものはできない、パフォーマンスは保証されないなどの制約はあるものの、再帰的な補助関数を含むheap-manipulating programの自動生成に成功しました。

High Performance Correctly Rounded Math Libraries for 32-bit Floating Point Representations

著者: Jay P. Lim, Santosh Nagarakatte
読み担当: koiking213
参考リンク: 概要、発表資料↓
本論文はPLDI '21のDistinguished Papersに選ばれています。

続いてkoiking213から高速で正しく丸められた32bit浮動小数点数ライブラリを実装した論文の紹介です。

浮動小数点数の計算はよく使われているライブラリでは近似値が使われることもあり、正しく丸められた値を返しているとは限りません。ここでいう正しく丸められたというのは正しい実数から32bitに丸めた値のことです。既存の実装として正確なライブラリもありますが、性能が低いという問題がありました。そこで以前16bit版のライブラリを作った著者らが32bit版のライブラリを実装しました。実装したのは32-bit floatとpositのフォーマットです。私はpositについて詳しくなかったのですが、Wikipediaの記事によると0付近の精度が高い浮動小数点数の規格だそうです。

先行研究では、全ての入力と出力の正しいペアを用意しておき、それを近似する多項式を生成して正しい結果に対する最大の誤差を最小化するような方法がとられていましたが、それだといくつか誤差が発生する箇所が存在しました。筆者らによる16bit版での実装はその誤差発生ポイントを抑えて誤差がでないようにしており、線形計画法で多項式を出力していました。

本研究では筆者らの16bit版の拡張になりますが、線形計画法の制約条件が16bitでは数千だったのに対して32bitでは数十億になって現実的には求解できないなど、一筋縄ではいかない点が多々あります。そこで、いくつかの工夫を入れています。まず入力を全て制約条件にするのではなく、サンプリングして使います。その結果の多項式で失敗する入力があれば、それを制約条件に加えて新たに解き直すようにしています。次に入力をサブドメインに分割し、それぞれのサブドメインに対する多項式を生成しています。さらに、range reductionをそれぞれの関数の特性を使うように改良しています。

これらの工夫を加えて数百分計算を回すと正しく丸められた関数を計算する式が出力できるようです。筆者らが実装したライブラリをglibcやIntelのlibmと比較すると平均してglibcの1.1倍、intelの1.5倍速かったそうです。

Quantum Abstract Interpretation

著者: Nengkun Yu, Jens Palsberg
読み担当: 中村
参考リンク: 概要、発表資料↓
本論文はPLDI '21のDistinguished Papersに選ばれています。

長丁場の2日目の最後は中村から量子プログラムを抽象解釈する手法を提案した論文の紹介です。

抽象解釈とはプログラムの静的解析のフレームワークの1つで、プログラムを何らかの抽象領域の上で実行します。プログラムの意味を全て静的に解析することはできないので近似して解析しているようなものです。例えば具体的な数値を計算することなく除算の母数に使われてる数が0にならないかなどを検査できます。抽象解釈で使う抽象領域は束として表現されます。

もう1つ、量子プログラムは量子ビットとそれを操作する量子ゲートを使って記述されます。 $${n}$$ 個の量子ビットは $${2^n}$$ 個の複素数で、量子ゲートはユニタリ行列で表現されます。

量子プログラムを実行する前にある程度性質が分かると嬉しいのですが、愚直に静的解析をやるには無理があります。現時点で世の中に72量子ビットの量子コンピュータがありますが、これをシミュレートするには $${4.7 \times 10^{21}}$$ 個の複素数が必要となり、現実的ではありません。そこで本論文では量子ビットに対して多項式時間で実行可能な抽象解釈手法を提案しています。

本論文では抽象解釈に使う抽象領域を部分線型空間/射影行列のなす束を元に構成しています。射影行列とは $${P = P^\dagger = P^2}$$ を満たす正方行列のことで、 $${P}$$ はベクトルをある部分線型空間 $${S_P}$$ に移します。 $${P}$$ と $${S_P}$$ は一対一の対応関係があるので、射影行列の包含関係を部分線型空間の包含関係で定義できます。そこで、本論文では抽象領域を射影行列の組(タプル)、抽象領域上の2要素間の順序をタプルのすべて要素毎に順序がつくときに定義しています(論文中では束になることは確認していませんでした。分岐などの制御構造がないので束でなくてもよいのかな？)。小さな射影行列をあつめることで計算を抑えています。具体的にどの射影行列を何個とは指定していないので1つの抽象領域を定義したというよりは抽象領域の定義のやり方を示している形ですね。

ここで定義した抽象領域の間には、いくつか重要な性質があります。

2つの抽象領域の関係として細かさ(fine)を定義できる
抽象領域の中の特別な場合に具象領域、すなわちプログラムの意味を正確に反映した領域がある
細かさを定義できる2つの抽象領域の間にガロア接続が定義できる
1. 具象領域と抽象領域の間にガロア接続が定義できる

これで量子ビットの抽象解釈が準備できました。

量子ゲートについても同様に抽象操作を定義します。詳しくは説明しませんが、ガロア接続を使って一度ユニタリ行列を表現するのに十分な領域に移って演算して、また元の領域に戻ってきているようです。同じく、最終目標は静的解析だったので抽象領域上での表明も定義されています。そして主定理として抽象領域上で表明が成立していた場合は具象領域上でも同等の表明が成り立っていることを示しています。

3つの重要な問題に対してベンチマークを取っていて、一応現実的な時間で静的解析が終わっているようです。例えば300量子ビットでGroverのアルゴリズムを解く例では166633秒(約2日)で解析が完了し、表明が成り立つことを確認できました。

結論として、量子計算のための抽象解釈の手法を提案しました。この手法はScalableであり(300量子ビットの解析ができた)、Usefulであり(3つの重要な問題に対して表明を検査できた)、Flexibleであり(射影を使えばいいのでAbstract Domainの設計自由度が高い)ました。

開催前は雑談でこういう論文読み会できたらいいよねと話してそのままの勢いで開催しましたが、ちゃんと人が集まるかなど不安もありました。しかし蓋を開けてみれば当初の想像以上に充実した会になりました。参加者が意識的だったかは分かりませんが、8件中5件の発表がDistinguished Papersと濃い内容になっています(因みにDistinguished Papersは8本選出されています)。参加者も非情報系出身のエンジニアや社会人博士、社長など様々なバックグラウンドの人が揃いました。もう次のPLDIの開催が目の前に迫ってきました。次も良い会が開催できるといいですね。