国立情報学研究所17階のクラウド、通称「17階クラウド」を使って、
DeVinEという分散モデル検証ツールを動かす。
冗談だと思っていたが本当に演習があった。
実際には17階クラウド(4コア＊9台)のキャパシティによると思われる不具合で、
分散モデル検証を各自で試すところまではいかなかったけれど、面白かった。
Eucalyptusを使ってクラウドを構築したり、
そのクラウド上に1+4台の仮想マシンを配備したりと
家庭用PCではできないことを体験できた。
DeVinEをmpiで分散していたけれど、本当に効率的にタスク分散してるのかな。
ちょっと怪しい動きだった。
最後にディスカッションの中で、サム・ロイドの15パズルの4×4の盤面が、
モデル検証ツールで検証できない(相当なメモリ容量のマシンでも
状態爆発に耐えられない)という話題で盛り上がった。
単純な全件探索を全部メモリに展開するのは結構辛いんだな。
私はLispで実装して、可能なバリエーションを片っ端から出力しちゃえばいいかと思っていた(メモリに展開してない)。
ClojureやScalaでモデル検査ツールを実装してみよう。
