日本ソフトウェア科学会第 34 回大会 (2017 年度) 講演論文集

頂点主体並列グラフ処理の制約解消器による効率化
森畑 明昌

江本 健斗

松崎 公紀

胡 振江

岩崎 英哉

本発表では、分散並列処理における無駄な通信や同期の除去などの効率化を制約解消器を用いて自動的に行う方法について、頂点主体並列グラフ処理を題材に報告する。頂点主体並列グラフ処理とは、各頂点が行う処理を指定することで大規模グラフを分散並列処理する枠組みである。我々が以前提案した関数型言語 Fregel では、各頂点が行う計算を宣言的に記述し通信や同期などは明示しないため、無駄な計算・通信・同期などが発生しており、また頂点主体
グラフ処理特有の効率化も行えていなかった。これに対し、効率化が可能な条件を論理的に記述し、それを制約解消器で確認することで効率化を行う手法を提案する。これにより、効率化がデッドロック等のバグをもたらさないことも自動的に保証される。本発表では、限定記号除去器を利用する方法と SMT ソルバを利用する方法を比較しながら提案手法を説明し、予備的な実験結果について報告する。

ができるが、その場合、逐次処理に比べかなりのオー

1 はじめに

バーヘッドが生じ、また負荷分散も難しくなりがちで

近年では、インターネットを初めとする情報技術のあり、良い実行速度が得られないことが多い。

発展により、一台の計算機ではとうてい処理できない

性能の良い分散並列処理を比較的簡単に達成する

ような大規模なデータも珍しくなくなってきている。

ための一つのアプローチは、プログラマは性能を気にこのようなデータを扱うには分散並列処理が必須となせず正しいプログラムを記述し、コンパイラが注意るが、一般に効率の良い分散並列プログラムを構築す

深い解析によって効率の良いコードを生成する、といるのは容易でない。分散並列処理には通信・同期・負うものである。このアプローチは宣言的並列処理言荷分散など逐次処理では現れない困難が多く現れる。

語などの文脈で長らく研究されてきた。本発表では、

これらを不適切に用いれば、デッドロックや正しくな

特に頂点主体並列処理 [13] を題材に、このアプロー

い結果が非決定的に現れるなど、除去の難しいバグ

チの可能性について調査した結果を報告する。

を埋め込んでしまうことになりかねない。細かく通頂点主体並列処理は、大規模グラフ処理を分散並信や同期を繰り返せばこのようなバグを避けること

列実行するためのフレームワークである。ソーシャル

Akimasa Morihata, 東京大学, The University of Tokyo.
Kento Emoto, 九 州 工 業 大 学, Kyushu Institute ofTechnology.
Kiminori Matsuzaki, 高知工科大学, Kochi Universityof Technology.
Zhenjiang Hu, 国立情報学研究所, National Institute ofInformatics.
Hideya Iwasaki, 電 気 通 信 大 学, The University ofElectro-Communications.
∗ Optimizing Vertex-centric Parallel Graph Processing using Constraint SolverThis is an unrefereed paper. Copyrights belong to
the Author(s).

ネットワークや顧客・商品関係ネットワーク、タンパ
ク質反応ネットワークなど、近年では大規模なグラフが多数手に入るようになり、その処理・解析を分散並列実行したいという要求が高い。しかし、グラフは配列や木構造の場合とは異なり、自明なデータの分割方法がなく、またグラフ処理はグラフ全体を繰り返し走査するようなアルゴリズムが多いため独立なタスクに分割しづらく、分散並列処理を実装することが難し
くなりやすい。頂点主体並列処理では、「各頂点が毎ステップどのような計算を行うか」という観点でグラsssp g = let init v = if v が始点 then 0 else ∞step v prev = min (prev v) (minimum [ prev u + e | (e, u) <- is v ])in fregel init step Fix g
図1

単一始点最短路問題に対する Fregel プログラム

フ処理を捉えることにより、この困難を軽減する。

• 計算ノードを跨ぐ情報は通信によって受け渡す。

例として、始点から各頂点までの最短路の長さを

これにより、プログラマは分散並列処理の実際の状求める計算（以下 SSSP と呼ぶ）を考える。図 1 が、況、例えば通信や同期など、を意識することなくプロ

頂点主体並列処理のための関数型言語 Fregel [5] で記

グラムを記述することができる。しかも、各頂点で述した SSSP のプログラムである。ただし、読みやすは概ね同じ処理を行うため、頂点を適切に計算ノーさのため、頂点に対応するデータ構造を省略するな

ドに分配すれば良い負荷分散が得られる可能性が高

ど、幾つか簡略化している。Fregel は Haskell のサブ

い。このように頂点主体並列処理はグラフの並列分散セットであり、その中核はグラフを処理する高階関数

処理の難しさを軽減することができるため、近年注

fregel である。その第 1 引数は初期化時に各頂点で目を集めいくつものフレームワークが提案されてい行う計算を表す。今回の場合、各頂点 v に対し、それる [5–7, 10–12, 20, 25, 28]。

が始点かどうかを加味して距離の初期値を求めていしかし、SSSP のようなかなり簡単な問題でも、実る。第 2 引数は処理の各ステップで各頂点に対し実際には効率の良い頂点主体並列処理プログラムを書行される。今回の場合、各ステップにおいて、各頂点くのはそれほど簡単ではない。図 1 のプログラムはv では、直前のステップでの各頂点の計算結果を格納

以下の点で非効率である。

するテーブル prev を用いてその頂点までの距離を更• プログラムの文面通りに読めば、全ての頂点が新する。新しい距離は、その頂点の前回の結果 prev

全てのステップで計算を行うことになる。しかv と、隣接頂点 u の前回の結果 prev u に接続辺の重し、実際にはそれは必要ない。隣接頂点の距離がみ e を加えたものの最小値となる。なお is は当該頂更新された頂点のみが計算をすれば十分である。

点に接続している辺の重みとその辺の他端頂点の対• 上と関連する話題だが、プログラムの文面上はのリストを返す。第 3 引数は停止条件であり、今回の（隣接頂点が別の計算ノードにあれば）全ての頂場合この計算はどの頂点の値も変化しなくなったら終点が毎ステップ通信を行う。しかし、上記の通了する。

り、自分の距離が更新された場合にのみ通信を行

頂点主体並列処理ではどのフレームワークでも、記法と細部は違えど似たようなプログラムを記述する。

えば十分である。

• そもそも、このプログラムは Bellman-Ford のア

すなわち、各頂点で毎ステップ、周辺の頂点の計算結

ルゴリズムと同等であり、グラフの大きさを n と果（ないしは周辺の頂点から送られてきたメッセー

して O(n2 ) 程度の計算を要する。しかし、もしダジ）を元にどのような計算を行うのか（またどのよ

イクストラ法を用いることができれば O(n log n)

うなメッセージを送るのか）、を記述する。フレーム程度の計算で済む。つまり、逐次実装に比べこのワークはこれらの記述をもとに分散並列グラフ処理

分散並列実装は漸近計算量でもかなり遅い。ダイを実行する。やはり細部に違いはあるが、おおむね以

クストラ法は分散並列実装に向かないとしても、下のような処理となる。

この差は無視しがたい。より適切なアルゴリズム• グラフの頂点集合は分割され各計算ノードに分配される。

• 各計算ノードは毎ステップ、自分に分配された頂点の処理を並列に行う。

の利用が望ましい。
既存の頂点主体並列処理フレームワークでも、これら問題を解決するための機能を提供している場合が多い。
例えば、Pregel [13] では、頂点を一時的に inactive

にする機能を提供し、また送るべきメッセージをプロバとして Z3 ソルバ †1 を用いた予備的実装を行った

グラマに明示的に特定させることで、1 番目と 2 番目

結果についても報告する。

の問題への対処を可能としている。また、頂点主体並

本発表は Fregel で記述された特定の形式の並列プ

列処理の亜種である部分グラフ主体並列処理 [20, 25]

ログラムの効率化を扱っているに過ぎない。しかし、や、非同期の頂点主体並列処理で可能となる頂点処理

本発表で採り上げている問題は分散並列プログラム記

順序の優先度スケジューリング [3, 11, 18] を用いるこ

述の際には普遍的に現れるものである。例えば、並列とで、部分的にダイクストラ法を取り入れ並列性と逐グラフ処理に関しては、頂点主体並列処理以外の枠組

次性能を両立させることができる（詳細は 2. 3 節参

みでも、宣言的な記述から高度な効率化技法によって照）。しかしいずれにせよ、これら機能を用いるため効率的な分散並列プログラムを得る手法は近年いくには明示的なプログラミングが必要である。頂点のつも提案されている [3, 18, 19, 22]。また、SMT によinactive 化、通信の削減、部分グラフに対する特別なる実装の際に現れる幾つかのヒューリスティクスを除処理、また優先度の設定などは、いずれも不適切に用き、本発表のアプローチは Fregel や頂点主体並列処

いると計算結果が正しくなくなってしまうものであ理に特化したものではない。そのため、本発表の内容

り、その利用は容易でない。

は分散並列計算における無駄な通信や同期の削減等に以上の状況を背景に、本発表では、制約解消器を用ついての一般的な知見を与えるものと期待している。

いることでこれらの効率化を自動的に導入する手法を提案する。提案手法では、図 1 のように効率を気

2 頂点主体並列処理にせず記述した頂点主体並列処理プログラム（具体的2. 1 Pregelには Fregel で記述されたものを想定する）を入力とPregel [13] は Malewicz らによって提案された頂点

し、制約解消器を利用したプログラム解析によって、

主体並列処理フレームワークである。以降に現れた頂頂点の inactive 化や通信の削減等が可能かどうかを

点主体並列処理フレームワークのほとんどがこれを基判定する。

にしているため、本稿でもまず Pregel の紹介を行う。

制約解消器としては限定記号除去器 [2] と SMT ソ

Pregel は、手続き型言語と関数型言語という違い

ルバ [4] の 2 つを考える。限定記号除去は、限定記号

はあるが、Fregel と同様、各頂点が各ステップで実行（∀ ないし ∃）を含む論理式を、それらを含まない等する処理を指定する。各頂点はローカルな記憶領域を価な論理式に変換する手法である。これは限定記号もち、この記憶領域の更新が各ステップでの処理の主の任意の深さのネストを扱えるため強力である。さな内容である。この処理の記述に際しては以下の特別

らに、限定記号除去によって得られる式は効率的な実な機能を用いることができる。

装のために必要なプログラム断片も与える。しかし、• 受け取ったメッセージの読み出し

限定記号除去は、制約解消に時間がかかる、制約解消• 他の頂点へのメッセージの送信が可能な論理体系が少ないなど、実用上は扱いが難し• 次のステップからその頂点が inactive になるとい。これに対し、SMT はいずれか 1 つの限定記号のみを含む論理式を入力とし、その真偽を判定するもの
で、限定記号除去に比べ表現力は落ちるが、高速なソいう宣言• 全ての active な頂点からの値の集約（アグリゲータ）

ルバが近年開発されているため実用的な実装が可能

メッセージの送信は、送信先頂点の識別子が既知でである。以上の状況をふまえ、本発表では、まず効率あれば任意の頂点に対し可能である。しかし、各頂化を限定記号除去問題として定式化し、その現実的点では通常グラフの大域的なトポロジーの情報が利な実装として SMT ソルバを用いる手法を提案する。

用できないため、ほとんどの場合は隣接頂点へのメッ

さらに、提案手法の有用性の確認のため、SMT ソル†1 Z3 Solver: https://z3.codeplex.com/

セージの送信となる。

辺とその他端を返す）という特殊な関数（以下ジェネ各頂点は active ないしは inactive であり、上述のレータと呼ぶ）によって得られた v の隣接頂点が用い

通り、自らの宣言によって inactive になることができられている。これ以外にも、グラフ中の全ての頂点をる。他の頂点からのメッセージを受け取ると inactive

返すもの（アグリゲータの実現に利用）など、いくつな頂点は active になる。なお、メッセージを受け取かのジェネレータが提供されている。これらの機能にらなかった場合、inactive な頂点での処理はスキップ

より、「次に使われるであろう値を想像してメッセーされる。全ての頂点が inactive になりメッセージもジ送る」ことを避け、「今回の計算に必要な値を読み送出されなかった場合プログラムは終了する。

出す」形式でのプログラム記述が可能となっている。

大域的な情報（例えば総和、平均など）の取得のた読み出した値はリストとなり、それを適切な演算

めアグリゲータと呼ばれる機能が提供されている。こ（図 1 の場合 minimum）で集約する。読み出した値は

れは、全ての active な頂点から指定された値を集約

本質的には多重集合であるため、通常のリスト処理関し、各頂点に伝えるものである。

数で扱うのは不適切である。そのため、集約は結合的Pregel のプログラムは分散環境上で実行できる。グかつ交換的な演算子（加算、乗算、最大値、最小値な

ラフは頂点単位で各計算ノードへ分配される。なお、ど）によるものに限っている。また、メッセージが一辺は頂点に付随するデータとして扱われる。実行は

つも届かない場合があるため、集約の演算子は単位元

BSP (Bulk Synchronous Parallel) [26] の方式に則っをもつことを仮定している。

ている。各計算ステップは、各頂点の処理、メッセー

Fregel の処理系には 2 種類ある。一つは既存のジの送受信、そしてメッセージの待ち合わせを兼ねる

Haskell 処理系での実行を行うもので、主にテストの大域バリアから成る。そのため、メッセージは次の計ために用いることを想定している。この処理系は本算ステップになるまで到着せず、また次の計算ステッ

発表の趣旨と関係ないので以降無視する。もう一つ

プになれば必ず到着する。この挙動は、同一計算ス

は、既存の頂点主体並列処理フレームワークのプロテップ内では各頂点の処理が完全に独立であることを保証しており、並列計算を可能としている。このようグラムへと翻訳するもので、並列分散実行のために用いる。現時点では Giraph†2 および Pregel+ [29]†3

な計算ステップを全頂点が inactive になるまで繰りのコードを出力できる。Giraph は Java、Pregel+は返すのが Pregel プログラムである。

C++言語であるという違いはあるものの、いずれも機能としては Pregel に非常に近い。

2. 2 Fregel
Fregel [5] は Pregel を元にした関数型言語であり、

2. 3 頂点主体並列処理の亜種と最適化

明示的なメッセージ送受信や inactive 化によるプロ

Pregel で提案された頂点主体並列処理が単純である

グラム停止などを隠蔽することで記述性を向上させこともあり、早くからそのモデルの問題が指摘されて、ることを目的としている。Fregel は Haskell の部分集

様々な改善が提案されている。ここでは特に Pregel合となっており、基本的な記法の意味は Haskell のその性能上の問題に関連するものについて述べる。

れと同じである。

Pregel の BSP モデルの採用については議論が多例として図 1 のプログラムを再訪する。Fregel のい。BSP モデルは大域的な同期に従って計算が決定核となるのは高階関数 fregel である。これは引数と的に進むため計算の挙動は分かりやすいが、計算ノー

してプログラム停止の条件をとるため、各頂点の処

ドが多い場合には大域的同期のコストはかなり大き理の内部に停止のためのコードを記述する必要がな

い。一方、多くのグラフアルゴリズムは非同期的に実い。また、通信は「前回の値」を表すテーブル（図 1

行してもよい。ここで「非同期実行」とは、大域的なの prev）の値の参照として暗黙に記述される。テー
ブル読み出しのキーとしては is v（頂点 v に向かう

†2 Apache Giraph: http://giraph.apache.org/†3 Pregel+: http://www.cse.cuhk.edu.hk/pregelplus/??
?? 

89:;
?>=<
/.-,
()*+
v ?
 ???


=⇒

図2

;;
;;
'&%$
!"#




する必要がある。一方、非同期実行を前提としていれ

?>=<
89:;
/.-,
()*+
v



'&%$
!"#;
;;
;

高次数頂点の分割

ば、特定頂点の実行が他の頂点より遅れることは想定の範囲内であるため、特別な取り扱いは不要になる。
優先度実行 グラフ処理では往々にして全ての頂点の処理が同等に有意義であるとは限らない。例えばSSSP では開始点から遠い点の処理はいくら行っても同期毎に各頂点を 1 回ずつ走査するのではなく、各頂最終結果にほとんど貢献しない。このことをふまえ、点を適当なスケジューリングに従って走査し、走査の非同期実行が可能であれば、開始点から近い点の処理瞬間に利用可能なメッセージを用いて計算を進めるものである †4 。非同期実行を採用している既存フレーを優先的に行うスケジューリングによってより高速に

ムワークも少なくない [6, 10, 12]。また、非同期実行

供しているシステム [3, 11, 18] も複数ある。

と BSP モデルでの実行を併用することでさらに効率を高める方法も提案されている [11, 28]。

最終結果を得ることができる。優先度実行の機構を提また、「頂点主体」というモデルそのものにも疑問が投げかけられている。頂点という単位はグラフ処理

非同期実行は同期を取り除くことができるだけでとしてはあまりに粒度が細かい。実際には各計算ノー

なく、さらなる最適化をもたらしうるという点でも重ドは部分グラフを保持しており、より広い範囲の情報要である。以下 2 つ例を挙げる。

を用いて高速な処理ができる可能性がある。例えば、高次数頂点の分割

現実に現れるグラフの多くで

SSSP であれば、各部分グラフ内ではダイクストラ法

は、非常に次数の高い頂点が少数存在する。各頂点がを使うというのも合理的である。このような観点か受け取るメッセージの量は概ね次数に比例すること、ら、部分グラフ主体（または近傍主体）の計算モデル

往々にして各頂点の仕事のほとんどはメッセージの集も提案されている [20, 25]。このモデルでは、ユーザ約であることもあり、次数の高い頂点がボトルネック

は頂点ではなく部分グラフを処理するアルゴリズムになることは多い。このボトルネックを避けるため、を記述する。

図 2 のように次数の高い頂点を複数の頂点に分割する手法がよく用いられる [27, 29]†5 。分割で得られた分がある。非同期実行の観点からは、部分グラフ主体

各頂点はそれぞれに届くメッセージの集約のみを担当

並列処理は同一計算ノード内にある部分グラフを計し、最終的にその結果が当該頂点に届いたらその頂点

算ノードを跨ぐメッセージ送受信に優先して行うスケの処理を行う。メッセージの送信も同様である。しかジューリングと見なすことができる。部分グラフ主体

し、頂点分割は BSP モデルでは単純には適用できな並列処理はこれに加え部分グラフに特化したアルゴリ

い。高次数頂点に届く・高次数頂点から送られるメッズムを用いることができる点で異なるが、これもスケ

セージは、本来届くべきであった計算ステップより遅ジューリングの一部と考えられる場合もある。例えばれることになるため、他の頂点との計算の同期が崩れ

SSSP であれば、優先度実行を行えば部分グラフ内のてしまう。よって、BSP モデルでは分割された頂点

処理はダイクストラ法に変更できる。ダイクストラ法

に対しては追加の特別な処理を行うよう実装を拡張と Bellman-Ford 法を組み合わせることで同一ノード

部分グラフ主体並列処理は非同期的実行と似た部

内での計算の逐次性能と全体としての並列性を両立†4 実際には、フレームワークによって非同期実行の実態は異なる。例えば gather-apply-scatter モデル [6,12]では頂点の走査順序は任意だが、その頂点が必要なメッセージは全て手に入っている必要があるというモデルである（実装上はそのために古いメッセージをキャッシュする）。
†5 このアプローチは、頂点を計算ノードに分配するのではなく辺を分配していると考えることもできる。

させるのは、SSSP の高速な並列アルゴリズムである∆-stepping 法 [14, 18, 22] などにも繋がりうるものである。

step v prev = let c1 =
..
.
cn =

⊕

⊕

1 [f1 (e, prevu) | (e,u) <- is v, p1 (prev u)]n [fn (e, prevu) | (e,u) <- is v, pn (prev u)]in g(v, c1 , . . . , cm )図3

提案手法で扱うプログラムの一般形

合せによってできており、近年の SAT ソルバーの高3 限定記号除去と SMT

速化を背景に、十分に実用的な速度で動作する実装が3. 1 限定記号除去

開発されてきている。

限定記号除去とは、限定記号（∀ または ∃）を含む
論理式をそれと等価で限定記号を含まないものへと

4 提案手法

変換する手法である。例えば、∀x. x2 + ax + b > 0

それでは、Fregel プログラムの効率化を限定記号

を 4b − a2 > 0 に変換するのが限定記号除去の一例で除去や SMT ソルバを利用しつつ実現する手法を与ある。特に論理式中の変数が全て限定記号によって束える。対象とするのは各 fregel 関数である。以下で縛されている場合、限定記号除去後の式の真偽は自明

は説明の単純さのためジェネレータは is に限る。まであるため、論理式の真偽判定の一手法として用いらた、停止条件は「値が変化しなくなると終了」（Fix）

れる。

のみを考える。これ以外にも細かい制限がある。これ命題論理では、真偽値全てを単に列挙すれば良いのらについては 4. 5 節で議論を行う。

で、限定記号除去は常に可能である。述語論理の場合

以下、fregel 関数が各計算ステップで実行する関には限定記号除去の方法が知られている体系は限ら数の名前を step とする。step 関数は図 3 の形式でれており、Presburger 算術や実閉体などが挙げられ定義されているとする。各 fi (1 ≤ i ≤ n) は隣接頂る。命題論理の場合の議論からも分かるとおり、限定記号除去が例え可能であったとしても、その計算量は点から読み出す情報を表す式、pi (1 ≤ i ≤ n) はその⊕情報が必要になる条件を表す式、 i (1 ≤ i ≤ n) は理論上も実用上も非常に大きい場合が多い。詳細は専その情報を集約する結合的かつ交換的な演算子、g は

門書 [2] などを参照されたい。

隣接頂点の情報をふまえて当該頂点の新しい値を計算する式である。

3. 2 SMT
SMT（Satisfiability Modulo Theories）[4] は命題

4. 1 通信の削減

論理における SAT を述語論理へと拡張したものであまずは通信を削減する方法について考える。Fregelる。限定記号除去とのアナロジーで言えば、SMT はでは隣接頂点の情報を読み出す形式でプログラムを記

1 種類の限定記号のみを含む論理式を入力とし、その述するが、実際には「次のステップで読み出される値

真偽を判定するものと言える。ただし、SMT は限定を送信する」プログラムへと翻訳される。そのため、記号を取り除くのではなく、様々な代入（∃ なら論理

ここでは「送信する必要のない値」すなわち「読み出式を満たす代入、∀ なら満たさない代入）を探索するしたとしても計算結果に影響しない値」を特定するこことで結果を得る。

とを目標とする。以下では n 個ある情報読み出しのSMT の計算量は扱う述語によりけりだが、少なく

うち k 番目のものについて考える。

とも SAT よりは悪いため、理論的にはそれほど高速

頂点 u（値 u̇）から値を読み出したとしても計算結な解法は望めそうにない。しかし、多くの SMT ソル果に影響しない、という状況を素直に定式化すると以バーは SAT ソルバーと述語を扱う論理ソルバーの組

下となる。
∀v, e, w1 , . . . , wn .

g(v, w1 , . . . , wn ) =g(v, w1 , . . . , wk−1 , wk ⊕k f (e, u̇), wk+1 , . . . , wn )(1)
ここで、v は値を読み出す頂点の値、e はその頂点と様であり、限定記号除去を用いて等価な式 ψ(u̇, ü) を得た後、条件 p を更新すれば良い †6 。
k

再び SSSP について考える。式 (2) を具体化すると以下となる。
∀v, e, w, w′ . min{v ′ , w′ } = min{v ′ , min{w′ , e + u̇}}u を繋ぐ辺の値、各 wi (1 ≤ i ≤ n) は他の頂点から

where v ′ = min{v, min{w, e + ü}}
限定記号除去を行うと u̇ ≥ ü が得られる。これは直の情報を集約した値に対応する。つまりこの式は、他

感とはやや反するが正しい。今回の距離の見積もりがの頂点からの情報や値を読み出す頂点の状況によら前回より悪ければ、隣接頂点の距離を更新できないた

ず、頂点 u の値が不要である状況を表している。

め送る必要がない。SSSP の場合、実際には頂点の距

頂点 u から隣接頂点へ値を送る必要があるのは式(1) が偽となる場合のみである。よって、この真偽を実離の見積もりが真に悪化することはないので、この条件は「値が変化しない」と等価である。

行時に確認できれば、それをもとに通信を削減するこ

以上が限定記号除去を用いる方法である。理論上はとができる。しかしこれは一見現実的でない。一つの明瞭だが、式 (2) を用いるとなるとかなりの数の変数

方法は、限定記号除去により u̇ 以外の変数を除去したが必要となる可能性があり、現実的であるかどうかは式 ψ(u̇) を得ることである。これは u̇ と基本的な計算疑わしい。以降は代わりに SMT を用いる方法を説明のみを含むため実行時にも問題なく真偽を計算できる。

する。

具体的には、コンパイラが k 番目の通信の必要性を

式 (1) や式 (2) は限定記号を ∀ しか含んでおらず、表す条件 pk (prev u) を pk (prev u) ∧ ¬ψ(prev u)

一見 SMT ソルバで扱えるように見える。しかし、と変更すればよい。

我々の目的はこの式の真偽を判定することではなく、この素直な定式化は実際にはそれほど有用ではな

通信が不要となる条件の効率的な実装 ψ を導出する

い。例として SSSP を考えると、式 (1) は以下となる。

ことである。SMT ソルバはこの条件を導出する機能∀v, e, w. min{v, w} = min{v, min{w, e + u̇}}を持たないため、事前にある程度 ψ のテンプレート

この条件を満たすためには u̇ = ∞ である必要があを用意する必要がある。自然な発想は、前回の値と同る。確かに正しいが、SSSP に関する効率化を完全にじであれば通信を行わない、というものである。これは捉えていない。

を定式化すると以下となる。
∀u̇, v, e, w1 , . . . , wn , w1′ , . . . , wn′ .

SSSP では頂点の値が更新されていなければメッ
セージを送る必要はない。これは送信先頂点の値が前g(v ′ , w1′ , . . . , wn′ ) =回送ったメッセージを十分に考慮しており、二度目はg(v ′ , w1′ , . . . , wk′ ⊕k f (e, u̇), . . . , wn′ )必要ない状況だと理解できる。この状況を先ほどと同where v ′ = g(v, w1 , . . . , wk ⊕k f (e, u̇), . . . , wn )(3)様に定式化してみる。いま、頂点 u の前回の値を u̇、前々回の値を ü とする。
∀v, e, w1 , . . . , wn , w1′ , . . . , wn′ .

式 (2) とは細かい違いがある。まず、u̇ と ü の違いがなくなっている。これは、前回と値が同じ状況を表現

g(v ′ , w1′ , . . . , wn′ ) =しているためである。さらに、u̇ が ∀ で限定されていg(v ′ , w1′ , . . . , wk′ ⊕k f (e, u̇), . . . , wn′ )る。これは、「どんな u̇ であっても、前回と値が同じ

where v ′ = g(v, w1 , . . . , wk ⊕k f (e, ü), . . . , wn )(2)

であれば通信は不要か？」ということを問うているた

この定式化では、式 (1) の場合に比べ、値を読み出す

ルバで判定が行えるようになる。これが真であれば、めである。これにより自由変数がなくなり、SMT ソ′

頂点の値 v は前々回の値 ü をもとに計算を行っている、ということが考慮されている。これにより、より正確に通信の必要性を判断できる。具体的な処理は同†6 ü に対応する値は Fregel の表層言語では得られないが、内部的には「前回と値が変更されていないか」を確認するためにこの値を保持している。

前回と値が同じ頂点はメッセージを送る必要がないこ

これは限定記号除去や SMT ソルバを用いるまでもなとがわかる。なお、SSSP であれば、u̇ = ü は u̇ ≥ ü

く適切な条件が得られている。コンパイラは、この条の一部であるため、当然真となる。

件が成り立つならば inactive になる、というコード

適当なテンプレートがありさえすれば、SMT ソルを挿入すればよい。

バは「前回と値が同じ」以外のケースでも扱うことがアグリゲータがある場合には注意が必要である。アできる。例えば、各頂点が複数の値を保持している場

グリゲータの結果はその頂点にメッセージが届かなく合、一部の値が等しければ通信をする必要がない可ても変化しうるので、頂点の inactive 化に際しては能性は十分ある。このようなケースも、同様に条件をその結果を単位元ではなく任意の値としなければな

生成し調べれば良い。アプリケーション領域に関するらない。例えば k 番目のデータ読み出しが実はアグ知識があれば、さらに異なる条件（例えば値が大きい

リゲータであった場合、

なら・小さいなら通信しないなど）を考える可能性もp∗ (u̇) ∧ (∀wk . g(u̇, ι1 , . . . , wk , . . . , ιn ) = u̇)

あるだろう。SMT ソルバは限定記号除去に比べて高という式から wk を削除し u̇ に関する条件を得る必要速であるため、これら可能性やその組合せを探索すがある。これに対応し、SMT ソルバの場合にはテンることも現実的である可能性が高い。とはいえ、ア

プレートが必要となる。この場合の素直なテンプレー

プリケーションを限らない状況では、「前回の値と同

トは「通信が不要な場合には inactive になってよい」

じ」という条件は十分に一般的であると考えている。

だろう。これを定式化すると以下となる。

また、この条件は inactive である時に満たされるた∀u̇, wk . p∗ (u̇) ⇒ (g(u̇, ι1 , . . . , wk , . . . , ιn ) = u̇)め、次に述べる頂点の inactive 化と相性が良いとい

SSSP の場合、p∗ (u̇) ⇒ (min{u̇, ∞} = u̇) となり、明う利点もある。

らかに成り立つ。

4. 2 頂点の inactive 化

4. 3 非同期実行

次に、頂点を inactive 化する効率化について述べ

Fregel の fregel 関数は、Pregel と同様、BSP にる。頂点が inactive になると、メッセージが届かな

基づいた同期的ば実行が想定されており、それ故 prev

い限り、その頂点の値は更新されずその頂点からメッ

テーブルの利用が正当化されている。一方で、SSSP

セージは送出されない。つまり、頂点の inactive 化であれば、実際には非同期的に実行しても最終的な結はその頂点がメッセージを送る必要がない場合にのみ果は変わらない。このことを自動的に示すため、まず可能である。よってこの効率化は通信削減の効率化のは以下の補題を準備する。なお証明は難しくないので後に行う。いま、通信削減の効率化を行った後のプロ省略する。

グラムが図 3 であるとする。さらに∧p∗ (prev u) =¬pi (prev u)

補題 1. 関数 h と h′ および 2 項関係 ⪯ に対し、以下

1≤i≤nとする。p∗ (u̇) は、値 u̇ である頂点は何一つメッセー
ジを送る必要がないことを意味する。
頂点を inactive 化しても問題ないのは、「メッセー
ジが届かない限り、頂点の値を更新する必要も、メッ
セージを送る必要もない」という条件を満たす場合である。これを頂点の値 u̇ に対する条件として定式化
すると以下となる。ιi (1 ≤ i ≤ n) は ⊕i の単位元であり、メッセージが届かない状況に対応する。

p∗ (u̇) ∧ (g(u̇, ι1 , . . . , ιn ) = u̇)の条件が成り立つとする。

h と h′ の大小: 任意の x に対し、x ⪯ h′ (x) かつ
h′ (x) ⪯ h(x)。
⪯ の反対称性: 任意の x と y に対し、x ⪯ y かつ
y ⪯ x ならば x = y 。
h の単調性: 任意の x ⪯ y に対し、h(x) ⪯ h(y)。
このとき、ある x に対し hn (x) = hn+1 (x)（ただし h0 (x) = x かつ hk+1 (x) = h(hk (x))）ならば、hn (x) = hn (h′ (x))。
いま、補題 1 を以下のように解釈する。まず、h をグラフ全体に対する 1 ステップの完全な処理、h′ を部分的な処理と捉える。つまり、非同期実行は 1 ス
テップを完全には行わず、処理された頂点と処理されなかった頂点が混在するものとみなしている。このとき、h を繰り返し適用して最終的に得られる結果が′h を適用しても得られるか、を調べたい。なお ⪯ は処理の進捗度合いを表しており、最終的に十分大きく

3 の一般形を元に書き下すと、以下の 3 条件となる。
h と h′ の大小:x ⪯ h′ (x) は定義より自明なので∀x, m, m′ . ∃w. g(g(x, m), w) = g(x, m ⊕ m′ )⪯ の反対称性:∀x, m. (∃w. g(g(x, m), w) = x) ⇒ (g(x, m) = x)
h の単調性:

なったところで処理が終了することになる。以上の∀x, m, m′ . ∃w. g(g(x, m′ ), w) = g(g(x, m), m′ )対応をふまえ、fregel 関数で記述された処理に補題「h と h′ の大小」では h′ (x) と h(x) をそれぞれ g(x, m)

1 が適用できれば、非決定的実行が可能であることが確認できる †7 。

と g(x, m ⊕ m′ ) で表している。h′ はメッセージが十′分に届く前の実行を意味することに注意せよ。また、以上の議論は h や h 、⪯ などがグラフを対象とし「⪯ の反対称性」と「⪯ の単調性」では、x ⪯ y なるたものである。しかし、プログラムは各頂点を処理す

y を g(x, m) で表している。これら 3 条件は本質的にるものとして記述されているため、頂点に関する条

は限定記号除去で確認が可能である。

件に読み替える必要がある。幸い、グラフに対する比例として SSSP を考える。まず関係 ⪯ の定義は較を「全ての頂点がその関係を満たす」として定義

x ⪯ y ⇐⇒ ∃w. min{x, w} = y

すれば、頂点に対する処理に対して補題 1 が適用でであり、限定記号を除去すると x ⪯ y ⇐⇒ x ≥ y

きれば、グラフ処理に対しても適用できる。よって、であることが分かる。このことをふまえれば、上記 3′以降は h や h 、⪯ などは頂点を対象としたものとする。このとき、h は「本来あるべきメッセージを全て′条件は簡単に確認できる。
次に SMT ソルバで条件を確認することを考える。

受け取っての処理」、「h は本来あるべきメッセージ

反対称性は以下と等価であるため SMT ソルバでも確の一部を受け取っての処理」となる。

認できる。

補題 1 の前提条件を限定記号除去で確認すること∀x, m, w. (g(g(x, m), w) = x) ⇒ (g(x, m) = x)を考える。この場合、反対称性の確認のためには ⪯残り 2 つの条件は限定記号のネストがあるため直接の定義が必要となる。反対称性以外の条件を満たす関は扱えない。この問題を解消するため、十分条件とし係を ⪯ の定義としても良いのだが、仕様を満たす要て w = m′ の場合を考える。このとき、⊕ の交換性に素のみを関係づけるとすると比較可能な要素が少な

注意すると、両条件は以下の 1 条件にまとめられる。

すぎて反対称性を満たさない可能性もあり、有益であ∀x, m, m′ . g(g(x, m), m′ ) = g(x, m ⊕ m′ )るかは疑わしい。ここでは、⪯ は本質的に計算の進

この条件は「遅れてやってきたメッセージ m′ を反映

行を表すものだという洞察をもとに、⪯ の定義を以すると最初から全てのメッセージが揃っていた場合

下の通り天下り的に与える。

と同じ結果が得られる」ということを主張しており、

x⪯y∃w1 , . . . , wn . g(x, w1 , . . . , wn ) = y

メッセージの未達にかかわらず処理を行う非同期実行

この定義は x ⪯ y を「x から何らかのメッセージを受の状況をまさしく捉えている。そのため、この条件にけ取って処理を進めると y となる」と読み替えるもよってほとんどの場合は非同期実行可能性が適切に判ので、自然な定義の一つである。以降、式の簡便のた断できると思われる。

⇐⇒

め、g はメッセージを 1 つだけ受け取るものとする。
多数受け取る場合も全く同様である。
上記 ⪯ の定義をもとに補題 1 の条件を確認する。図
†7 ただし、終了判定は最終的に h（すなわち同期的な 1
ステップ）を実行して結果が変わらないことをもって判断する必要がある。

4. 4 優先度スケジューリング
2. 3 節において、非同期実行が他の様々な最適化を導くことを述べた。この中で、部分グラフ主体処理と高次数頂点分割はこれ以上の解析なしに適用できる。
しかし、優先度スケジューリングを行うためには、優先度を判断する方法が必要となる。

考え、アグリゲータはその頂点との通信と捉えれば優先度スケジューリングの基本はより最終結果に良い。ただし、この頂点は独自の値を持たないため、貢献するであろう値を優先的に伝播させることであ前回送信した値を考慮した通信の削減は意味を持たる。幸い、非同期実行の定式化に用いてきた関係 ⪯ない。

が、値が最終的な結果に近いかどうかの判定に利用で停止条件は「値が変化しなくなると終了」（Fix）のきる。この関係で「大きい」ほど最終結果に近いはずみを考えてきた。これ以外の停止条件を用いたプロで、それ故優先的に伝播すべきである。例えば SSSP

グラムは Fix を用いたものに翻訳できる。大まかにであれば「小さい」値ほど優先的に伝播すべき、とは、停止条件の真偽を各頂点が追加の値として保持なる。しかし、この自然なアプローチは実用上常にし、それが真となったら次の計算ステップでは値を変有用であるわけではない。特に、⪯ が全順序ではな

化させなければよい。実際、この変換は Fregel 処理

く、推移則を満たさなかったり比較不能な値があった系のコンパイル過程の一つである。

りする場合が問題である。この場合、プライオリティ提案手法では fregel 関数のみを対象としてきた。

キューを用いるような標準的で効率的な実装が利用で他のグラフ処理関数、例えば gmap や gzip は通信をきない。

行わず処理の繰り返しも行わないため提案手法の対以上の状況をふまえれば、望まれるのは ⪯ を拡張

象ではない。これらグラフ処理関数による計算を外部した全順序 ⊑、すなわち a ⪯ b ⇒ a ⊑ b を満たすよのコントロール構造によって繰り返している可能性はうなものである。これは、限定記号除去を用いるとしあるが、このようなケースの取り扱いについては今後ても、SMT ソルバを用いるとしても、全順序 ⊑ のテの課題である。

ンプレートなしには与えることができず、またテンプ

ここまでの説明では、fregel 関数は前回の計算ス

レートがあれば自動的に検証できる。テンプレートとテップの値を保持する prev という表のみを用いていしては、アプリケーションに関する知識が無いとすれたが、実際には今回の計算ステップの値を保持する

ば、値の型から分かるよく知られた全順序（数値に対curr という表も利用できる。curr を用いたプログラ

して大小比較など）やその組合せ（組の各要素を辞書

ムも curr を用いないプログラムへと変換でき、実際式に比較するなど）を網羅的に試すのが適当である。

Fregel コンパイラはこれを行っている。よって、理論上は curr の利用に問題はない。しかし、この変換の4. 5 拡張と制限

結果、各計算ステップでの関数は内部状態次第で計算

ここまででは、他の頂点のデータの読み出し（すな

内容を完全に切り替えるような複雑なものとなるた

わち通信）はジェネレータとして is を用いたものの

め、変換後のプログラムに対して効率化が可能だと判みを考えていた。ジェネレータとして何を用いるか定できるかどうかは定かでない。変換を経ずに直接最は、どのような頂点間で通信するかを規定する。しか適化を行う方法は今後の課題である。

し、ここまで議論は、注目している通信以外の通信は誰が何を送っているのか全く分からないという定式

5 実装と実験化で行っており、複数のジェネレータが混在するとし提案手法の可能性を探るため、前述の効率化を行うても問題はない。逆に言えば、例えば同じ値を何度もよう既存の Fregel コンパイラを改造し、効率化の効送るようなプログラムだった場合、同じジェネレータ

果を確認した。

を使っているかどうかを調べることで、通信が不要な条件をより詳しく調べることができるかも知れない。

5. 1 実装の方針

ジェネレータとして全頂点を返すものを用いる場合、実装の簡便のため以下の方針で臨んだ。

すなわちアグリゲータを使う場合についても同様で

まず、既存実装の利用が難しいと思われる限定記号ある。論理的には、全ての頂点と接続している頂点を除去は諦め、SMT ソルバを用いる手法のみを実装し表1

実験用グラフデータ

表2

SSSP プログラムに対する最適化の効果（単位：秒）

名前

頂点数

辺数

データ名

最適化前 通信削減 inactive 化 手書き

WebBerkStan

685, 230

7,600,595

WebBerkStan

401.3

RoadNet-PA

1,088,092

1,541,898

RoadNet-PA

Rand1M/10M 1,048,576 10,485,760

Rand1M/10M

54.2

47.3

24.2

228.8

69.6

53.5

29.0

29.5

10.7

9.9

4.3

た。SMT ソルバによる手法は限定記号除去による手

はじめとする初期化・終了処理の時間を含まない。

法に比べ効率化の能力が低いため、SMT ソルバでも実験環境は 16 台の PC がギガビットイーサで繋十分な効率化が可能であれば、提案手法の有用性は十がった PC クラスタである。各計算機は CPU が Intel分であると言える、との判断である。

Core i5（9 台は Core i5-2500、残り 7 台は i5-760）、

次に、現時点での Fregel コンパイラのバックエン

メモリ 8 GB 、そして 128 GB の SSD を積んでいる。

ドである Giraph と Pregel+が非同期実行をサポート

OS は Ubuntu 14.04.3 LTS である。Fregel のバックしていないため、非同期実行に関する効率化の実装はエンドとしては Giraph を用いており、Giraph 1.2、

諦めた。非同期実行の効果に関しては既に詳しく調べ

Hadoop 1.2.1、Java 1.8.0 121 からなる。全ての実られており [10, 11, 28]、改めて調査する価値は低い。

験で 16 ワーカーで実行をしている。

また、効率化手法としては通信量削減等の延長線上にあり、本質的な困難があるとは考えがたい。

実験用のグラフデータは表 1 に示す 3 つを用いさらに、Fregel コンパイラの中間表現ではなく抽た。WebBerkStan と RoadNet-PA はスタンフォード大学が提供しているグラフデータ †8 であり、前象構文木に対する変換として効率化を実装した。こ者は web グラフ、後者は道路ネットワークである。

れは、抽象構文木に対してあれば前節の議論が全く

Rand1M/10M は頂点間をランダムに繋いだグラフでそのまま使え簡便であり、また中間表現に変換する過ある。

程でもたらされるコードの複雑性が効率化可能性の判定に悪影響を与える可能性を危惧したためである。

5. 3 実験結果

この結果、Fix 以外の停止条件や curr などは扱えな

以下、実験結果について述べる。まず、SMT ソル

くなってしまっている。

バによる効率化可能性の判定は一瞬で終了し、通信

SMT ソルバとしては、Z3 ソルバ（version 4.3.2）の削減、及び inactive 化が可能であることが判断さを用いた。実装に際して必要な機能はほとんどが既れた。次に、各プログラムの実行時間を表 2 に示す。

に提供されていた。ただし、min や max の単位元でデータにもよるが、最適化前は手書きのコードに比べある ∞ と −∞ が必要となるため、数値（特に整数）て数倍から十数倍程度実行性能が悪かった。これに対に関してはこれらを含む直和型として拡張し、各演算し、通信削減、inactive 化両方を行うことで、2 倍程を適切に再定義する Z3 プログラムを記述した。

度の遅さにまで改善しており、最適化の効果は非常に大きい。特に通信削減の効果は大きく、Fregel の自然

5. 2 実験の概要な記述がもたらす無駄な通信が大きなコストになって

図 1 に示した SSSP の Fregel プログラムに対していたことが示唆される。また、inactive 化の効果も、最適化を適用し、その効果を確認した。最適化の効果

通信削減ほどではないものの、10 ∼ 20% 程度の改善を詳しく見るため、(1) 最適化前 (2) 通信の削減のみであり小さくはない。残る差は Fregel コンパイラのを適用したもの (3) 通信の削減と inactive 化を適用生成するコードに含まれる細かいオーバーヘッドだとしたもの (4) 手書きのプログラム、の 4 種類を用意

思われるが、精査はしていない。

し、それぞれの 5 回の実行の平均時間算出した。な
お、実行時間はグラフデータの読み出し・書き込みを†8 https://snap.stanford.edu/data/

本研究では Fregel でプログラムを記述するという

6 関連研究方針をとった。Fregel の特徴の一つは宣言的である

頂点主体並列処理に関する関連研究については 2. 3

ことである。このことは宣言的な記述を要求するソ節で既に述べた。本研究は、これら研究で提案されてルバーの利用を容易にしている。しかし、宣言的できた頂点主体並列処理の効率化方法を背景に、効率化あることは本研究の顕著な特徴ではない。まず、非宣を適用したプログラムを自動的に、しかも可能な限り

言的なプログラムであったとしても、多少の現実的アプリケーションに関する知識を用いずに得る手法をな仮定の下で、ソルバーの利用は多少困難にはなる提案した。

ものの可能ではある。また、Fregel 以外にも宣言的

限定記号除去に代表される高度な制約解消器を並列に並列分散グラフ処理を記述する枠組みはいくつもプログラムの生成に用いること自体は以前から行われあり [3, 7, 18, 19, 22]、特に頂点主体並列処理に限ってている。典型的な利用方法は、例えばステンシルコー

も GraphX [7] という完成度の高いシステムがある。

ドのように、ネストしたループ構造をもつ配列操作プ

GraphX は Scala 上の並列グラフ処理フレームワー

ログラムに対し、適切なループ変換の方法を模索した

クで、MapReduce のようにデータの流れを高階関数り、その際の無駄な計算・通信などを取り除いたりすを用いて記述することを特徴としており、その一環とるものである [1, 8, 17]。特にプログラムを線形不等式

して Pregel API も提供している。

系によって特徴付ける多面体モデルを用いるアプロー

本研究に特に関連する Fregel の特徴は、処理がチでは、線形不等式系に対する限定記号除去操作が知BSP モデルに基づいている点、そしてメッセージやられているため、これら制約解消器が解析の基礎とし頂点処理の必要性、頂点の走査順序などを全く指定て用いられている。また、これ以外にも、分割統治並しないという点である。まず前者の点により、Fregel

列プログラムのためのプログラム断片を得る手段とプログラムの挙動は決定的であり、並列実行の計算結して用いた例もある [15, 16, 21, 23]。SMT ソルバー

果は逐次実行の結果と必ず一致する。これは他の宣等がこのようなプログラム生成の手段として有用で言的な枠組みの多くが、出力の満たすべき条件を論あることは、近年では広く認識されつつある [9, 24]。

理的に特定することを主眼に置いており、その条件を本研究ではこれら手法を大規模グラフ処理という満たす出力が複数ある場合について非決定性を許し極めてイレギュラーな並列処理の効率化に用いた。イているのとは異なる。非決定性を許す方針の方がよレギュラーは並列処理では、その計算の構造を多面体

り宣言的であり、また本発表でも論じたように効率化モデルなどで捉えることが難しいため、一般にプログも行いやすいが、現実的にはこれはプログラムの構

ラムの解析は困難となる。例えば、頂点主体並列処理

築、特にデバッグを難しくしてしまう。また、宣言的を計算ステップを繰り返す while ループと全ての頂な枠組みであっても、効率をプログラマが改善するた点を操作する for ループからなる 2 重ループだと思めの何らかの記述を前提としていることが多い。例

えば、非同期実行可能性の検査はループ入れ子の実行

えば、GraphX の Pregel API は本家 Pregel と同様、順序の変換であり、まさに制約解消器などがよく用い送信すべきメッセージや inactive にすべき頂点などられる題材である。しかし、グラフの構造に依存したを明示的に指定するものとなっている。Coordinated

データ依存性や計算結果に依存した停止条件などのた

Linear Meld [22] はグラフ処理のための論理型言語だ

め、このループ変換は難しい。これに対し、本研究でが、データの分割やデータ処理の優先順位を追加で指は、頂点主体並列処理プログラムの構造に着目するこ定することで効率を高めるようになっている。

とで補題 1 を導入し、これにより現実的な検査方法を本研究と最も関連の深い研究は、Elixir [18, 19] と提案している。以上の議論からも見て取れるように、Distributed SociaLite [22] である。Elixir は出力グ

本研究の主要な新しさは、既存技術をもとに頂点主体

ラフが満たすべき性質の論理的な記述からグラフを分並列処理に対する解析・変換手法を与えた点である。

散並列処理するプログラムを自動導出するシステムである。特に、次の計算ステップでグラフ全体を走査すが有効であるか否かを調べるのは今後の課題である。

ることを避けるため、走査する必要のある頂点集合を

また、同様の手法は本論文で述べた以外の高度な効率特定するプログラムを SMT ソルバの助けを借りつつ化にも有用である可能性がある。そのような可能性も合成している点が、本研究における inactive 化とよ

今後模索してゆくことを考えている。

く似ている。なお、頂点がメッセージを送る条件や頂謝辞

提案手法と関連する研究についての情報を点を走査する優先順位などはユーザが明示的に指定提供してくださった高知工科大学の佐藤重幸氏に感謝している。Distributed SociaLite は datalog をもとする。本研究の一部は、JSPS 科研費 JP26280020、にした宣言的なグラフ処理言語である。SSSP のよう

JP15K15974 の助成を受けている。

な計算を加速するため、計算がある種の単調性を満たすことをユーザが保証することで、∆-stepping [14]参 考 文 献の一般化を適用している。以上のように、本研究は[ 1 ] Bondhugula, U., Baskaran, M. M., Krishnamoorthy, S., Ramanujam, J., Rountev, A., andSadayappan, P.: Automatic Transformations forCommunication-Minimized Parallelization and Locality Optimization in the Polyhedral Model, Compiler Construction, 17th International Conference,
CC 2008, Held as Part of the Joint European
Conferences on Theory and Practice of Software,
ETAPS 2008, Budapest, Hungary, March 29 - April
6, 2008. Proceedings, Hendren, L. J.(ed.), Lecture
Notes in Computer Science, Vol. 4959, Springer,
2008, pp. 132–146.
[ 2 ] Caviness, B. F. and Johnson, J. R.(eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition, Springer Vienna, Vienna, 1998.
[ 3 ] Cruz, F., Rocha, R., and Goldstein, S. C.:
Declarative coordination of graph-based parallel
programs, Proceedings of the 21st ACM SIGPLAN
Symposium on Principles and Practice of Parallel Programming, PPoPP 2016, Barcelona, Spain,
March 12-16, 2016, Asenjo, R. and Harris, T.(eds.),
ACM, 2016, pp. 4:1–4:12.
[ 4 ] de Moura, L. M. and Bjørner, N.: Satisfiability modulo theories: introduction and applications,
Commun. ACM, Vol. 54, No. 9(2011), pp. 69–77.
[ 5 ] Emoto, K., Matsuzaki, K., Hu, Z., Morihata,A., and Iwasaki, H.: Think like a vertex, behave
like a function! a functional DSL for vertex-centric
big graph processing, Proceedings of the 21st ACM
SIGPLAN International Conference on Functional
Programming, ICFP 2016, Nara, Japan, September
18-22, 2016, Garrigue, J., Keller, G., and Sumii,E.(eds.), ACM, 2016, pp. 200–213.
[ 6 ] Gonzalez, J. E., Low, Y., Gu, H., Bickson,D., and Guestrin, C.: PowerGraph: Distributed
Graph-Parallel Computation on Natural Graphs,
10th USENIX Symposium on Operating Systems
Design and Implementation, OSDI 2012, Hollywood, CA, USA, October 8-10, 2012, Thekkath, C.
and Vahdat, A.(eds.), USENIX Association, 2012,
pp. 17–30.
[ 7 ] Gonzalez, J. E., Xin, R. S., Dave, A.,
Crankshaw, D., Franklin, M. J., and Stoica,
I.: GraphX: Graph Processing in a Distributed

Elixir や Distributed SociaLite に比べ、より少ない情報から、より多くの最適化を自動的に適用することを目指しており、頂点走査の優先順位や単調性など、

Elixir や Distributed SociaLite ではユーザが指定していた部分も自動導出している。同時に、∆-steppingのような既存アルゴリズムを適用するのではなく、そのようなアルゴリズムが自動的に導出されるような効率化手法を目指し、非同期実行や優先度スケジューリングの導入方法を提案している。また、Elixir もDistributed SociaLite もその仕様記述の性質上非決
定的実行を想定しているが、Fregel があえてより最適化の難しい BSP モデルから出発している点も小さくない差異である。しかし、Elixir も Distributed

SociaLite も頂点主体に限らないグラフ処理をサポートしており、より表現力は高い。本研究のアプローチ
がより広いグラフ処理へと適用できるかの議論は今後の課題である。

7 まとめと今後の課題
本発表では、頂点主体並列処理を効率化する手法を提案した。限定記号除去・SMT ソルバーを用いることで、通信量の削減や頂点の inactive 化はもちろん、非同期的実行や優先度スケジューリングも自動的に導入できることを示した。SMT ソルバーを用いた予備的実装は現実的な時間で最適化を行えており、最適化の効果も大きいことが観察できている。
現状の実装は予備的なものであり、大きく複雑なプ
ログラムの取り扱いを前提にしたものではない。本
格的な実装を行い、複雑なプログラムにも提案手法

Dataflow Framework, 11th USENIX Symposium
on Operating Systems Design and Implementation,
OSDI ’14, Broomfield, CO, USA, October 6-8,
2014., Flinn, J. and Levy, H.(eds.), USENIX Association, 2014, pp. 599–613.
[ 8 ] Größlinger, A., Griebl, M., and Lengauer, C.:
Quantifier elimination in automatic loop parallelization, J. Symb. Comput., Vol. 41, No. 11(2006),
pp. 1206–1221.
[ 9 ] Gulwani, S., Jha, S., Tiwari, A., and Venkatesan, R.: Synthesis of loop-free programs, Proceedings of the 32nd ACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI 2011, San Jose, CA, USA, June 4-8,
2011, Hall, M. W. and Padua, D. A.(eds.), ACM,
2011, pp. 62–73.
[10] Han, M. and Daudjee, K.: Giraph Unchained:
Barrierless Asynchronous Parallel Execution inPregel-like Graph Processing Systems, PVLDB,
Vol. 8, No. 9(2015), pp. 950–961.
[11] Liu, Y., Zhou, C., Gao, J., and Fan, Z.: GiraphAsync: Supporting Online and Oﬄine Graph
Processing via Adaptive Asynchronous Message
Processing, Proceedings of the 25th ACM International Conference on Information and Knowledge
Management, CIKM 2016, Indianapolis, IN, USA,
October 24-28, 2016, Mukhopadhyay, S., Zhai, C.,
Bertino, E., Crestani, F., Mostafa, J., Tang, J.,
Si, L., Zhou, X., Chang, Y., Li, Y., and Sondhi,P.(eds.), ACM, 2016, pp. 479–488.
[12] Low, Y., Gonzalez, J., Kyrola, A., Bickson, D.,
Guestrin, C., and Hellerstein, J. M.: Distributed
GraphLab: A Framework for Machine Learning in
the Cloud, PVLDB, Vol. 5, No. 8(2012), pp. 716–
727.
[13] Malewicz, G., Austern, M. H., Bik, A. J. C.,
Dehnert, J. C., Horn, I., Leiser, N., and Czajkowski,
G.: Pregel: a system for large-scale graph processing, Proceedings of the ACM SIGMOD International Conference on Management of Data, SIGMOD 2010, Indianapolis, Indiana, USA, June 610, 2010, Elmagarmid, A. K. and Agrawal, D.(eds.),
ACM, 2010, pp. 135–146.
[14] Meyer, U. and Sanders, P.: [Delta]-stepping:a parallelizable shortest path algorithm, J. Algorithms, Vol. 49, No. 1(2003), pp. 114–152.
[15] Morihata, A. and Matsuzaki, K.: Automatic
Parallelization of Recursive Functions Using Quantifier Elimination, Functional and Logic Programming, 10th International Symposium, FLOPS
2010, Sendai, Japan, April 19-21, 2010. Proceedings, Blume, M., Kobayashi, N., and Vidal, G.(eds.), Lecture Notes in Computer Science,Vol. 6009, Springer, 2010, pp. 321–336.
[16] Morita, K., Morihata, A., Matsuzaki, K., Hu, Z.,
and Takeichi, M.: Automatic inversion generates
divide-and-conquer parallel programs, Proceedingsof the ACM SIGPLAN 2007 Conference on Pro-

gramming Language Design and Implementation,
San Diego, California, USA, June 10-13, 2007, Ferrante, J. and McKinley, K. S.(eds.), ACM, 2007,
pp. 146–155.
[17] Pouchet, L., Bondhugula, U., Bastoul, C., Cohen, A., Ramanujam, J., Sadayappan, P., and Vasilache, N.: Loop transformations: convexity, pruning and optimization, Proceedings of the 38th ACM
SIGPLAN-SIGACT Symposium on Principles ofProgramming Languages, POPL 2011, Austin, TX,
USA, January 26-28, 2011, Ball, T. and Sagiv,
M.(eds.), ACM, 2011, pp. 549–562.
[18] Prountzos, D., Manevich, R., and Pingali, K.:
Elixir: a system for synthesizing concurrent graphprograms, Proceedings of the 27th Annual ACM
SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications,OOPSLA 2012, part of SPLASH 2012, Tucson,
AZ, USA, October 21-25, 2012, Leavens, G. T. and
Dwyer, M. B.(eds.), ACM, 2012, pp. 375–394.
[19] Prountzos, D., Manevich, R., and Pingali, K.:
Synthesizing parallel graph programs via automatedplanning, Proceedings of the 36th ACM SIGPLAN
Conference on Programming Language Design and
Implementation, Portland, OR, USA, June 15-17,
2015, Grove, D. and Blackburn, S.(eds.), ACM,
2015, pp. 533–544.
[20] Quamar, A., Deshpande, A., and Lin, J. J.:
NScale: neighborhood-centric large-scale graph analytics in the cloud, VLDB J., Vol. 25, No. 2(2016),
pp. 125–150.
[21] Sato, S. and Iwasaki, H.: Automatic parallelization via matrix multiplication, Proceedings of the
32nd ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI 2011,
San Jose, CA, USA, June 4-8, 2011, Hall, M. W.
and Padua, D. A.(eds.), ACM, 2011, pp. 470–479.
[22] Seo, J., Park, J., Shin, J., and Lam, M. S.:
Distributed SociaLite: A Datalog-Based Language
for Large-Scale Graph Analysis, PVLDB, Vol. 6,
No. 14(2013), pp. 1906–1917.
[23] Smith, C. and Albarghouthi, A.: MapReduce
program synthesis, Proceedings of the 37th ACM
SIGPLAN Conference on Programming Language
Design and Implementation, PLDI 2016, Santa
Barbara, CA, USA, June 13-17, 2016, Krintz, C.
and Berger, E.(eds.), ACM, 2016, pp. 326–340.
[24] Srivastava, S., Gulwani, S., and Foster, J. S.:
Template-based program verification and program
synthesis, STTT, Vol. 15, No. 5-6(2013), pp. 497–
518.
[25] Tian, Y., Balmin, A., Corsten, S. A., Tatikonda,
S., and McPherson, J.: From ”Think Like a Vertex” to ”Think Like a Graph”, PVLDB, Vol. 7,
No. 3(2013), pp. 193–204.
[26] Valiant, L. G.: A Bridging Model for Parallel Computation, Commun. ACM, Vol. 33,
No. 8(1990), pp. 103–111.

[27] Verma, S., Leslie, L. M., Shin, Y., and Gupta,
I.: An Experimental Comparison of Partitioning Strategies in Distributed Graph Processing,
PVLDB, Vol. 10, No. 5(2017), pp. 493–504.
[28] Xie, C., Chen, R., Guan, H., Zang, B., andChen, H.: SYNC or ASYNC: time to fuse for distributed graph-parallel computation, Proceedings ofthe 20th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP
2015, San Francisco, CA, USA, February 7-11,

2015, Cohen, A. and Grove, D.(eds.), ACM, 2015,
pp. 194–204.
[29] Yan, D., Cheng, J., Lu, Y., and Ng, W.: Effective Techniques for Message Reduction and Load
Balancing in Distributed Graph Computation, Proceedings of the 24th International Conference on
World Wide Web, WWW 2015, Florence, Italy,
May 18-22, 2015, Gangemi, A., Leonardi, S., andPanconesi, A.(eds.), ACM, 2015, pp. 1307–1317.