8.2 今後の課題
8.2.1 A* 探索の性能改善
第 8 章
まとめと今後の課題
となっている．改善方法としては，まだインライン展開を行っていない関数をインライン 展開する，簡潔さのために多少冗長になっている部分があるため改善する，DSLの中間命 令列を構造体ではなくバイト列に圧縮しマクロとビット演算を用いてアクセスを行う，状 態の構造帯の評価値・コスト値・ヒューリスティック値のビット数を改善するなどが挙げ られる．
次に，プライオリティキューのロックの粒度の改善について説明する．A*探索に用いる キューは評価値をキーに状態のキューを値としたハッシュ表形式のプライオリティキュー となっている．現在の実装では複数スレッドからのアクセスの際にキュー全体にロックを かけているため，コア数を大きくしたときの並列化のオーバーヘッドが大きい．改善方法 として，ハッシュ表のキー別にロックをかける，または，各キーのキューを追加と削除で ロックを別にするなどの方法が挙げられる．
8.2.2 モデル検査へのヒューリスティクスの導入
今後の課題のひとつとして，モデル検査でのヒューリスティクスの導入がある．モデ ル検査器にヒューリスティクスを導入した代表例としてはHSF-SPIN[17]がある． HSF-SPINはモデル検査器SPINに各種ヒューリスティック探索アルゴリズムを用いて拡張し たものである．safetyの検証には，DFS，BFS，ダイクストラ法，A*探索，貪欲法BFS， IDA*，山登り法などがあり，liveness の検証にはNDFS，two-phase A*などの手法をサ ポートしている．ヒューリスティック関数の計算はSPINのpromelaのコードから算出さ れ，計算式の詳しい概要については論文[16]を参照．SPINにはプロセスという概念があ るため，プロセスが実行可能かブロックされているかなどの情報からアクティブであるか デッドロックかなどを式として定義し，ヒューリスティック関数の記述に利用してモデル 検査におけるヒューリスティック探索を実現している．そのため，LMNtalのモデル検査 にヒューリスティクスを導入するには，SPINにおけるプロセス，プログラムカウンタ，
プロセス間の通信などに対応する概念をLMNtalに導入することにより同様に実現できる と考えられる．
謝辞
本研究を進めるにあたり様々な方の指導・助言をいただきました．まず, ご指導を賜 わった上田 和紀教授に深く感謝致します．また，共に切磋琢磨した研究室の同期の皆様，
助言を頂いた言語班の先輩の皆様に深く感謝致します．最後に，入学から現在に至るま で，叱咤激励を私にかけてくれた家族に深く感謝致します．
2015年1月 小沼 賢
参考文献
[1] 上田和紀, 加藤紀夫: 言語モデル LMNtal,コンピュータソフトウェア, Vol.21, No.2, pp.126-142, 2004.
[2] 乾敦行, 工藤晋太郎, 原耕司, 水野謙, 加藤紀夫, 上田和紀：階層グラフ書換えモデ ルに基づく統合プログラミング言語 LMNtal, コンピュータソフトウェア, Vol. 25, No.1,2008, pp. 124-150.
[3] 川端 聡基: 並列モデル検査器SLIM の状態空間削減手法および最適化問題向けの 状態空間構築手法, 早稲田大学大学院基幹理工学研究科,情報理工学専攻,修士論文, 2012.
[4] 後町将,堀泰祐,上田和紀: LMNtal実行時処理系の並列モデル検査器への発展, コン
ピュータソフトウェア, Vol. 28, No. 4, pp. 137-157，2011.
[5] 広戸康平: LMNtalデータ構造のハッシュコード化と同型性判定,早稲田大学理工学
部,卒業論文, 2007.
[6] 吉田健人, 小沼賢, 上田和紀 : Hash Compaction を利用したグラフ書換え系モデル
検査の大規模化とその評価, 電子情報通信学会技術研究報告, Vol. 114, No. 156, pp.
9-16, 2013.
[7] Russell, J.S., Norvig, P.: エージェントアプローチ人工知能 第2 版, 共立出版, 2008, pp. 32-137.
[8] Zhang, Y.,Hansen, E. A.: Parallel Breadth-First Heuristic Search on a Shared-Memory Architecture, In Workshop on Heuristic Search, Memory-Based Heuristics and Their Applications (2006), 2006.
[9] Hart, P. E., Nilsson, N. J., Raphael, B.: A Formal Basis for the Heuristic Determination of Minimal Cost Paths, IEEE Transactions on Systems Science and Cybernetics, Vol. 4, pp. 100-107, 1968.
[10] R.E. Korf.: Depth-First Iterative-Deepening: An Optimal Admissible Tree Search,
Ar-tificial Intelligence, Vol.27, No.1, pp. 97-109, 1985.
[11] Korf, E. R., Reid, M., Edelkamp, S.: Time complexity of iterative deeping A*, Artificial Intelligence, Vol.129, pp. 199218, 2001.
[12] A.Kishimoto, A.Fukunaga,and A.Botea.: Scalable, parallel best-first search for optimal sequential planning., In Proc. ICAPS2009, pp. 201-208, 2009.
[13] Kobayashi, Y., Kishimoto, A., Watanabe, O.: Evaluations of Hash Distributed A* in Optimal Sequence Alignment, In Proc. IJCAI, pp. 584590, 2011.
[14] M.Evett, J.Hendler, A.Manhanti, and D.Nau.: PRA*: Massively parallel heuristic search. Journal of Parallel and Distributed Computing, Vol.25, No.2, pp. 133-143, 1995.
[15] Dutt,S., Mahapatra, R. N.: Parallel A* Algorithms and their Performance on Hypercube Multiprocessors, Proceedings of Seventh International Parallel Processing Symposium, pp. 797-803, 1993.
[16] Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Protocol verification with heuristic search, In AAAI Symposium on Model-based Validation of Intelligence, 2001.
[17] Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN, In 8th International SPIN Workshop on Model Checking of Software, LNCS 2057, pp. 57-79, 2001.
[18] Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed explicit-state model checking in the validation of communication protocols, Software Tools for Technology Transfer, Vol.5, pp. 247-267, 2004.
付録 A
使用したベンチマークプログラム
以下にベンチマークで使用したLMNtalソースコードとDSLの一部を記載する．
A.1 eight-puzzle.lmn
// map info
px(1,2,3,1,2,3,1,2,3).
py(1,1,1,2,2,2,3,3,3).
state(6,4,7,8,5,0,3,2,1).
// finish
state(1,2,3,4,5,6,7,8,0) :- finish.
// move // (1,1)
state(0,A,B,C,D,E,F,G,H) :- state(A,0,B,C,D,E,F,G,H).
state(0,A,B,C,D,E,F,G,H) :- state(C,A,B,0,D,E,F,G,H).
// (2,1)
state(A,0,B,C,D,E,F,G,H) :- state(0,A,B,C,D,E,F,G,H).
state(A,0,B,C,D,E,F,G,H) :- state(A,D,B,C,0,E,F,G,H).
state(A,0,B,C,D,E,F,G,H) :- state(A,B,0,C,D,E,F,G,H).
// (3,1)
state(A,B,0,C,D,E,F,G,H) :- state(A,0,B,C,D,E,F,G,H).
state(A,B,0,C,D,E,F,G,H) :- state(A,B,E,C,D,0,F,G,H).
// (1,2)
state(A,B,C,0,D,E,F,G,H) :- state(0,B,C,A,D,E,F,G,H).
state(A,B,C,0,D,E,F,G,H) :- state(A,B,C,D,0,E,F,G,H).
state(A,B,C,0,D,E,F,G,H) :- state(A,B,C,F,D,E,0,G,H).
// (2,2)
state(A,B,C,D,0,E,F,G,H) :- state(A,0,C,D,B,E,F,G,H).
state(A,B,C,D,0,E,F,G,H) :- state(A,B,C,0,D,E,F,G,H).
state(A,B,C,D,0,E,F,G,H) :- state(A,B,C,D,E,0,F,G,H).
state(A,B,C,D,0,E,F,G,H) :- state(A,B,C,D,G,E,F,0,H).
// (2,3)
state(A,B,C,D,E,0,F,G,H) :- state(A,B,0,D,E,C,F,G,H).
state(A,B,C,D,E,0,F,G,H) :- state(A,B,C,D,0,E,F,G,H).
state(A,B,C,D,E,0,F,G,H) :- state(A,B,C,D,E,H,F,G,0).
// (3,1)
state(A,B,C,D,E,F,0,G,H) :- state(A,B,C,0,E,F,D,G,H).
state(A,B,C,D,E,F,0,G,H) :- state(A,B,C,D,E,F,G,0,H).
// (3,2)
state(A,B,C,D,E,F,G,0,H) :- state(A,B,C,D,E,F,0,G,H).
state(A,B,C,D,E,F,G,0,H) :- state(A,B,C,D,0,F,G,E,H).
state(A,B,C,D,E,F,G,0,H) :- state(A,B,C,D,E,F,G,H,0).
// (3,3)
state(A,B,C,D,E,F,G,H,0) :- state(A,B,C,D,E,0,G,H,F).
state(A,B,C,D,E,F,G,H,0) :- state(A,B,C,D,E,F,G,0,H).
A.2 eight-puzzle.hlmn
manhattan1 = abs(get (px, 1) - get (px, get(state, 1))) + abs(get (py,1) - get (py, get(state, 1))) manhattan2 = abs(get (px, 2) - get (px, get(state, 2))) + abs(get (py,2) - get (py, get(state, 2))) manhattan3 = abs(get (px, 3) - get (px, get(state, 3))) + abs(get (py,3) - get (py, get(state, 3))) manhattan4 = abs(get (px, 4) - get (px, get(state, 4))) + abs(get (py,4) - get (py, get(state, 4))) manhattan5 = abs(get (px, 5) - get (px, get(state, 5))) + abs(get (py,5) - get (py, get(state, 5))) manhattan6 = abs(get (px, 6) - get (px, get(state, 6))) + abs(get (py,6) - get (py, get(state, 6))) manhattan7 = abs(get (px, 7) - get (px, get(state, 7))) + abs(get (py,7) - get (py, get(state, 7))) manhattan8 = abs(get (px, 8) - get (px, get(state, 8))) + abs(get (py,8) - get (py, get(state, 8))) manhattan9 = abs(get (px, 9) - get (px, get(state, 9))) + abs(get (py,9) - get (py, get(state, 9))) h = manhattan1 + manhattan2 + manhattan3 + manhattan4 + manhattan5
+ manhattan6 + manhattan7 + manhattan8 + manhattan9
A.3 eight-puzzle.hil
init [24] T0 store [0] T1 store [1] T2 store [1] T21 LOOP:
get [ state , T2 ] T5 eq [T5, 0] T6
BrT [L1, T6] T22 get [ px , T2 ] T7 get [ state , T2 ] T8 get [ px , T8 ] T9 sub [ T7, T9 ] T10 abs [ T10 ] T11 get [ py , T2 ] T12 get [ py , T8 ] T14 sub [ T12, T14 ] T15 abs [ T15 ] T16 add [ T11, T16 ] T17 store [T17] T18 Br [L2] T13 L1:
store [0] T18 L2:
store [T18] T19 add [T1, T19] T1 add [T2, T21] T2 eq [T2, 10] T3
not [T3] T20 BrT [LOOP, T20] T4 Lh:
store [T1] T24
A.4 shortestpath.lmn
/*
ルーマニアの都市間の最短経路問題。ゴールはブカレスト 各都市名
A - Arad B - Bucharest C - Craiova D - Dobreta E - Eforie F - Fagaras G - Giurgiu H - Hirsova I - Iasi L - Lugoj M - Mehadia N - Neamt O - Oradea P - Pitesti R - Rimnicu Vilcea S - Sibiu
T - Timisoara U - Urziceni V - Vaslui Z - Zerind
*/
// ブカレストまでの直線距離(straight line distance) sld(arad, 366), sld(bucharest, 0), sld(craiova, 160), sld(dobreta, 242), sld(eforie, 161), sld(fagaras, 176), sld(giurgiu, 77), sld(hirsova, 151), sld(iasi, 226), sld(lugoj, 244), sld(mehadia, 241), sld(neamt, 234),
sld(oradea, 380), sld(pitesti, 100), sld(rimnicu_vilcea, 193), sld(sibiu, 253), sld(timisoara, 329), sld(urziceni, 80), sld(vaslui, 199), sld(zerind, 374).
// エッジ
e(oradea, zerind, 71), e(zerind, oradea, 71), e(zerind, arad, 75), e(arad, zerind, 75), e(oradea, sibiu, 151), e(sibiu, oradea, 151), e(arad, sibiu, 140), e(sibiu, arad, 140), e(arad, timisoara, 118), e(timisoara, arad, 118), e(timisoara, lugoj, 111), e(lugoj, timisoara, 111), e(lugoj, mehadia, 70), e(mehadia, lugoj, 70), e(mehadia, dobreta, 75), e(dobreta, mehadia, 75), e(dobreta, craiova, 120), e(craiova, dobreta, 120), e(sibiu, fagaras, 99), e(fagaras, sibiu, 99), e(fagaras, bucharest, 211), e(bucharest, fagaras, 211), e(sibiu, rimnicu_vilcea, 80), e(rimnicu_vilcea, sibiu, 80), e(rimnicu_vilcea, craiova, 146), e(craiova, rimnicu_vilcea, 146), e(rimnicu_vilcea, pitesti, 97), e(pitesti, rimnicu_vilcea, 97), e(craiova, pitesti, 138), e(pitesti, craiova, 138), e(pitesti, bucharest, 101), e(bucharest, pitesti, 101), e(bucharest, giurgiu, 90), e(giurgiu, bucharest, 90), e(bucharest, urziceni, 85), e(urziceni, bucharest, 85), e(urziceni, hirsova, 98), e(hirsova, urziceni, 98),
e(hirsova, eforie, 86), e(eforie, hirsova, 86), e(urziceni, vaslui, 142), e(vaslui, urziceni, 142), e(vaslui, iasi, 92), e(iasi, vaslui, 92), e(iasi, neamt, 87), e(neamt, iasi, 87).
// 状態
state(arad, nothing).
//移動ルール
e(S, D, C) \ state(A, B) :- A==S, unary(B), unary(D) | state(D, S).
A.5 shortestpath.hlmn
// cost function
c = e[_.1 == state.2 & _.2 == state.1].3 // heuristic function
h = sld[_.1 == state.1].2
付録 B
ソースコード変更概略
以下に変更または追加したSLIMとDSLパーサのソースファイルの概略を示す．
• src/main.c
• src/task.c
• src/verifier/mc.c
• src/verifier/mc.h
• src/verifier/mc generator.c
• src/verifier/mc generator.h
• src/verifier/mc worker.c
• src/verifier/state.c
• src/verifier/state.h
• src/utility/priority queue.c
• src/utility/priority queue.h
• src/heuristics/heuristics.c
• src/heuristics/heuristics.h
• src/heuristics/hil lexer.l
• src/heuristics/hil parser.y
• src/heuristics/hsyntax.c
• src/heuristics/hsyntax.h
• HParser.scala
付録 C
実装した主要部分のソースコード
以下に本研究でSLIMに実装したA*探索のソースコードの主要部分を記載する．