Scala UDF を SQL に変換する技術
論文メモ。今日はプログラム合成を用いてプログラムを変換する手法について。
論文
UDF to SQL Translation through Compositional Lazy Inductive Synthesis
OOPSLA2021
https://www.cs.utexas.edu/~isil/clis.pdf (preprint)
論文の概要
データベースシステムが提供する一般的な機能として、ユーザが独自に定義した UDF（user-defined function）を SQL から呼び出す機能がある。UDF は一般的なプログラミング言語で書けるため利便性が高い一方で、実行時に性能に問題が出ることがしばしばある。この問題に対して本論文では UDF をピュアな SQL に自動変換する技術を提案する。本手法の特徴は、あらかじめ定義された変換ルールを適用するルールベースの手法ではない点である。具体的には、lazy inductive synthesis というプログラム合成を用いた新たなアプローチを提案している。
手法の入出力
手法の入力
手法の出力
- SQL クエリ
- ただし
と
は任意の入力に対して同じ出力を返す。
- ただし
データフローグラフ
まずは本手法の前提としてデータフローグラフを簡単に説明する。データフローグラフはプログラム中の変数の定義と使用の関係を示したグラフである。論文中では以下が例として挙げられている。
左がプログラムで、右がデータフローグラフである。データフローグラフの各ノードが命令列であり、各エッジが変数の流れを示している。
ノードの作り方には自由度があり、なるべく多くの命令をまとめて1つのノードとしてもよいし、少ない命令をまとめて1つのノードとしてもよい。ちなみに、一般的なデータフローグラフはループ構造がある場合はループを持つグラフになるが、論文では Direct Acyclic Graph（DAG）であると書かれている。これは cyclic になるようなノードの作り方は許さないという暗黙の前提を意味しているのだと思われる。
本研究では、ノードの分割方法に応じてグラフ同士の順序関係を定義している。より細かくノードを分割しているほど "小さい" ような順序関係になっている。たとえば、以下の2つのグラフ ,
を考える。
このとき は
よりノードを細かく分割しているので
となる。
本手法では、グラフのノードごとに合成を行うアプローチを取る。1つのノードに含まれる命令数が多いほど合成の難易度が高くなるという前提を取っているため、グラフの分割の仕方としては より
のほうが合成の難易度が低いものと考えている。
Counter-Example Guided Inductive Synthesis
Counter-Example Guided Inductive Synthesis（CEGIS）は、段階的に複雑なプログラムを合成してゆく手法である。プログラム合成の研究をしている人にとってはお馴染みのアプローチであり、本手法でも変換前と同値なプログラムを合成するために用いられる。
CEGIS では、有限個の入出力例からプログラムを合成し、そのプログラムが合成の仕様を満たしているか検証する。仕様を満たしている場合は合成に成功した状況なのでおしまい。一方で仕様を満たしていない場合は、検証結果として反例が与えられるので、それを有限個の入出力例に追加することで満たすべき入出力例を精緻化する。このように合成と検証（と反例の生成）を繰り返すことで仕様を満たすプログラムを合成するアプローチである。
本手法では、変換前と同値なプログラムを合成することが目的である。そのため合成問題の仕様は「変換前のプログラムと同値であること」となる。したがって CEGIS においてプログラムの同値性を検証する必要があるが、そのために既存のモデル検査器（Clarke et al., 2004）を用いている。この検査器は C 言語で書かれたプログラムの同値性を検証するものであるため、変換前後のそれぞれのプログラムを C 言語のプログラムに変換しておく必要がある。この Ｃ 言語への変換処理は著者らが実装したとのこと。
入出力例からの SQL の合成には Trinty（Martins et al., 2019） というプログラム合成のフレームワークを用いており、73個の SQL の命令をもつ DSL を独自に定義することで合成を行っている。使用する定数の探索空間は、整数なら 1, 0, -1 などよく使われそうなもののみを用いるようにしている。
手法のアプローチ
本手法の合成アルゴリズムについて説明する。まずは、変換元となるプログラムからデータフローグラフを構築する。このときノードの分割方法はいろいろあるが、分割方法が細かいものから順に合成の対象とする。そしてデータフローグラフのノードごとに合成を行う。具体的には、各ノードに入ってくる辺を入力変数、ノードから出ていく辺を出力変数と見なしたうえで CEGIS として合成を行う。つまり元の Scala の命令列に対応する処理を SQL の命令列として合成することになる。CEGIS では、合成結果として得られたプログラムと、元の命令列が同値であるかを検証する。すべてのノードに対して合成に成功すればおしまい。一方で合成に失敗した場合は、より粗いノードの分割をもつデータフローグラフを対象に合成を試みる。以降、この流れをすべてのノードにおいて合成が成功するまで繰り返す。
細かいノードの分割からスタートして徐々に粗い分割を対象としていく流れが独自性が高い部分であり、本手法の貢献となっている。必要に応じて合成を行うという点から著者らはこのアプローチを lazy inductive synthesis と呼んでいる。
評価実験
Github からランダムに抽出した Scala の UDF に対して実験を行った。人手での調査によると100件のうち63件が UDF を除去できることが分かった。本手法を用いることで、63件のうち58件において UDF を除去できた。
所感
- inductive program synthesis を用いた変換手法という点が新しくて面白い。スクラップ＆ビルドという感じ。
- 本手法では Scala のシーケンシャルな命令列を SQL の命令に置き換えることが狙いといえる。先行研究はカーソルループを用いた集約計算を SQL 化することに重きを置いたものが多いが、本手法では集約計算はサポートされていない。この点おいて、ルールベースではないことの強みを生かしきれてない印象を受けた。（変換ルールを定義することが本質的に難しいのは集約計算のような処理だと思うので。）
- 評価実験の結果はかなり素晴らしいように見える。UDF をピュアな SQL に変換できるのは、そもそもユーザが「Scala では使うべき関数が分かるけど SQL ではどの命令を使えばよいか分からない」みたいな状況のときにUDF を使うからなのかな。つまり SQL を書くにあたって構文的な難しさがあるというより、単に SQL の命令を知らないことが主な原因な気がした。もしそうならルールベースで命令の対応関係を大量に作ってあげるだけで、実はかなりの精度が出るのかもしれない。
