More than 5 years have passed since last update.

@wwwcojp(k y)in

日鉄ソリューションズ株式会社

SQL等価性検証ツールCosetteを使ってみた

Last updated at 2018-12-04Posted at 2018-12-03

はじめに

皆さん、SQLチューニングしてますか？（唐突）

私は仕事柄RDBMSのSQLチューニングをすることが多いのですが、たまにチューニングの一環で SQL文の書き換え をすることがあります。
その際に問題になるのが、書き換えたSQL文が等価であるかどうかの確認が大変なことです。
SQL文を書き換えた場合には、想定通りの結果を取得できるか確認するために、テストをやり直す必要があります。
これが開発早期のフェーズならまだましなのですが、結合テスト以降だと手戻りも多くかなりコストがかかりますし、既に本番運用が始まったシステムともなると、テスト自体が困難なこともあります。
また、複雑なSQL文だと網羅的なテストケースを作成すること自体が困難であるため、完全に正しいと確信することはできません。
なので、SQL文の書き換えの正しさを証明する良い手段はないかと考えていました。

SQLチューニングとは？

そもそも、何故SQLチューニングなどというタスクが必要なのかについて簡単に説明しておきます。

SQL文は、 どんなデータを取得するか（What） を定義する言語です
（通常のプログラミング言語が、 どのように処理するか（How） を定義するのと対照的ですね）。
DBMSは、SQL文や参照するオブジェクトの定義、オブジェクトの統計情報等を入力として、Howにあたる 実行計画 を生成してくれます。
こうしてDBMSがHowを自動的に考えてくれるので、ユーザはWhatだけを考えることに集中でき、生産性が上がるわけですね。

しかし、残念ながら現代のDBMSであっても完全には程遠いため、最適な実行計画を生成してくれないことが多々あります。
よって、私達エンジニアが最適な実行計画が生成されるように誘導してあげる必要があります。

よく行われるSQLチューニングには、以下のようなものがあります。

索引の作成
統計情報の最新化
正規化 / 非正規化
実行計画の固定化
- OracleDBであればヒント句の付与等
SQL文の書き換え
- 等価な書き換え（今回のターゲット）
- 非等価な書き換え

SQL文の等価な書き換えは、DBMSが実行計画を生成する際、SQL文が特定の書き方であると特定の実行計画が生成されるという性質を利用しています。
よくあるのがINとEXISTSの使い分けですが、DBMSによって実行計画生成アルゴリズムは異なりますし、最適化機能により内部的に書き換えが行われることもあります。よって、DBMSの振る舞いをよく把握した上で実施する必要があります。

Cosetteとは？

Cosetteとは、SQL文の等価性を自動的に検証してくれるツールです。
詳しいことは公式ガイドを見ていただくとして、ざっと検証の流れを説明すると、

「Cosette Language」というDSLにより、表の定義や検証したいSQL文を記述
検証により、等価/非等価/決定不能を判定。非等価の場合、反例も出力
等価でない場合、クエリを修正して2に戻るか、検証を終了する

となります。

今のところ、検証可能なSQL文には以下のような制約があります。

SELECT文のみ対応
制約は表現不可能（ユニーク制約はDISTINCT句で表現）
Group By句に式は書けない
集合演算子は「UNION ALL」のみ
関係演算子は「<, >, =」のみ
論理演算子は「AND, OR, NOT」のみ
分析関数は「SUM,COUNT」のみ
EXISTS句は書けるが、NOT EXISTS句やIN句/NOT IN句は非対応

DMLの検証や制約の考慮ができないのは残念ですね。とはいえ、現時点でどこまで実用性があるか、とりあえず検証してみようと思います。

さっそく使ってみる

オンライン・デモが用意されているので、すぐにでも試せます。

私が以前書いた記事「SQL等価性検証ツールCosetteを、Dockerで立ててみた」ではローカルに立てる手順を紹介してますが、どうもオンライン版と振る舞いが異なる場合があるので、ここではオンライン版での検証結果を載せています。

まずは、公式サンプルでいくつか動作確認してみましょう。

JOINの除去（Join Elimination）

余計に結合している表を除去したSQL文の等価性を検証しています。
ビューを無闇やたらに利用してしまっているシステムで、稀にこのようなパターンがありますね。

等価であることを正しく示せていますね。

副問い合わせ⇒結合への書き換え誤り（Count Bug）

これは、発案当初は正しいと信じられていた書き換えだったらしいです。
たとえば、以下のようなデータの時に異なる結果が出力されます(理由は各自考えてみてください)。

parts表

pnum	qoh
0	1
1	0

supply表

pnum	shipdate
0	9

さて、検証してみると・・・

結果を見ると、等価で無いことは示せていますが、反例がおかしいですね
（論文に載ってる画像だと、ちゃんとした反例が出てるんですが・・・）。

反例はあまり参考にしないほうが良いかもしれません。

さて、ここからは公式サンプルに無い、私が検証したいものを試していきます。

論理演算の分配法則

索引をうまく使ってくれない等の理由で、OR条件を分割したくなることがたまにあります。そういった際に、AND条件をきちんと分配法則にしたがって分配できているか不安になるので、検証してみました。

検証コード

schema s_employee(eid:int, age:int, gender:int , ??);     

table t_employee(s_employee);
predicate p1(s_employee);
predicate p2(s_employee);
predicate p3(s_employee);

query q1                
`select distinct *
 from t_employee e
 where p1(e) and (p2(e) or p3(e))`;

query q2                
`select distinct *
 from 
 (select  *
  from t_employee e
  where p1(e) and p2(e)
  union all
  select  *
  from t_employee e
  where p1(e) and p3(e)) e`;

verify q1 q2;

等価性を確認できましたね。

ただ、SELECT句で列名を指定すると、決定不能になってしまいました。

生成されるRosetteやCoqのコードを眺めるだけでは、なぜこうなるのかはよくわかりませんでした。Cosetteの中身を理解する必要がありそうです（やるとは言っていない）。

EXISTS ⇒ JOIN への書き換え

EXISTSとJOINの書き換えも良くある書き換えパターンですが、どうでしょうか？
ちなみに、distinctしているのは結合キーに重複値がある場合を考慮しているためです（なぜ重複値があるとダメなのかは考えてみてください）。

検証コード

schema s_employee(eid:int, depid:int , ??);
schema s_department(depid:int, ??);

table t_employee(s_employee);
table t_department(s_department);

predicate p1(s_employee,s_department);
predicate p2(s_department);
predicate p3(s_employee);

query q1
`select *
 from t_employee e
 where exists (select * from t_department d where e.depid = d.depid)`;

query q2
`select e.*
 from t_employee e, (select distinct d.depid as depid from t_department d) d2
 where e.depid = d2.depid`;

verify q1 q2;

検証してみると・・・

エラー・・・だと・・・？しかも、このエラーメッセージからは何が悪かったのかまったく汲み取れない。手詰まりです。

一応、あえて間違った書き換えも検証してみます。

こちらはちゃんと等価ではないことが示せました（反例がやたら冗長なのが気になりますが・・・）。

式の書き換え

DBMSによっては、式に含まれる列に対して索引が使えないことがあります。そういった場合、索引を使わない側に式を移すことがよくあります。

検証コード

schema s_prod(pid:int, price:int , ??);    

table t_prod(s_prod);

query q1
`select p.pid as pid
 from t_prod p
 where p.price - 5 < 10`;

query q2
`select p.pid as pid
 from t_prod p
 where p.price < 15`;

verify q1 q2;

さて、どうなるでしょうか？

決定不能だと・・・？算術演算は難しいのか？

ちなみに、書き換えを間違えると、↑のようにちゃんと反例を出してくれます。間違いの検出自体には使える・・・？

だめだったよ。

まとめ

パターン	判定結果	備考
論理演算の分配法則	正しく判定	ただし、列名を指定すると判定不能に
EXISTS ⇒ JOIN への書き換え	エラー	間違った書き換えについては間違っていると正しく判定
式の書き換え	判定不能	足し算・引き算の間違いは判定できたが、掛け算・割り算は正しく判定できず

以上のように、現時点では検証できないパターンが多く、実用性は乏しいという結果になりました。

とはいえ、このツールのリポジトリを見る限りメンテはされているようですし、Issueにも改善要望はあがっているので、今後実用性が増していく可能性はあります。

また、Cosette作者の最新の論文には、Cosetteよりも多くのパターンについて等価性検証が可能な手法を開発したとありました。今後、より実用的なツールが世に出てくる可能性は十分にありそうです。

ということで、私はこの分野の発展を気長に待ちたいと思います。

You get articles that match your needs
You can efficiently read back useful information
You can use dark theme

What you can do with signing up