LiquidHaskell コトハジメ
このエントリは Haskell Advent Calendar 2016 および Formal Method Advent Calendar 2016 の 23 日目の投稿です。のはずでしたがすでに日付が変わりました。謹んでお詫び申し上げます。
ちなみに 22 日目の担当者はそれぞれ
- Haskell Advent Calendar 2016 : heredocsの紹介 - Qiita
- Formal Method Advent Calendar 2016 : 農夫 山羊 キャベツ 狼 - Qiita
です。偶然ですが同じ方が執筆担当ですね。
さて、本エントリでは Haskell の型の表現力をより豊かにする仕組み、 LiquidHaskell について概要を紹介します。使用するサンプルコードは Samples of Verification by LiquidHaskell · GitHub にアップロードしてあります。
実行時エラーを防ぐには
簡単な例として、リストの先頭要素を取る関数 head の型を考えてみましょう。
*Main> :t head head :: [a] -> a
型としてはもちろんこれで正しいのですが、しかし空リストに対して haed を呼ぼうとすると実行時エラーが発生してしまいます。
*Main> head [] *** Exception: Prelude.head: empty list
では、このような実行時エラーをコンパイル時に、何らかの静的検査によって防ぐことはできないでしょうか？
head :: [a] -> a という型は、「何らかの型 a の要素を持つリストを引数に取って、同じ型 a を持つ値を返す」という head の制約を規定していますが、リストの長さについては何も主張していません。つまり上のエラーを防ぐためには、「引数となるリストが空でない」という事前条件を型にエンコードできればよいことになります。
これを実現する方法はいくつか考えられます。GADTs 言語拡張 を使って型レベル自然数を定義し、さらに型レベル自然数を長さとして持つ「長さ付きリスト型」を定義すれば空リストかどうかが型によって判定できそうです。また、依存型をフルに使える Haskell 以外の言語であればもっと素直な方法で表現できるでしょう。しかし、いずれも元の実装からは大きな改修が必要で、しかも関連箇所すべてを「長さ付きリスト型」で置き換えることになるため、なかなか骨が折れそうです。
LiquidHaskell では、専用のコメント {-@ ... @-} を使用して次のように記述します。
{-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-} safeHead :: [a] -> a safeHead [] = liquidError "empty list" safeHead (x : _) = x
「長さが 0 を超える (= 空リストでない)」という事前条件がコメント内に型として表現されていることがわかります。LiquidHaskell が使用する情報は通常の GHC から見るとあくまでも単なるコメントであって、通常と同じように (検証を行わない) コンパイルが可能です。実際、ここでは分かりやすさ優先で safeHead と名前をつけましたが、関数名を head にしておけば呼び出し側モジュールの import 文を書き換えるだけで実装の差し替えが可能です。
新しく登場した liquidError が何者なのかは若干気になりますが、とりあえず先に処理系を動かせる状態を作りましょう。
インストールと最初の一歩
LiquidHaskell はバックエンドとして SMT ソルバを使用するため、あらかじめ本体とは別にセットアップしておく必要があります。自分の場合は Z3 の最新版 v4.5.0を選択しました。
本体の方は cabal でインストールするか、もしくはソースコードを clone してきて stack build でコンパイルするかの選択肢が提供されています。残念ながら Stackage には登録されていないようで、だいぶ前から "We are working to put liquid on stackage" のままになっています。
セットアップができたら先ほどの例を動かしてみましょう。以下のコードを Sample.hs として適当なところに保存し、liquid Sample.hs を実行してみてください。
module Sample where import Language.Haskell.Liquid.Prelude ( liquidError ) {-@ safeHead :: { xs:[a] | len xs > 0 } -> a @-} safeHead [] = liquidError "empty list" safeHead (x : _) = x
実行時にいくつか進捗メッセージが表示されますが、最終的に
**** RESULT: SAFE **************************************************************
が表示されれば問題なくインストールできています。ようこそ、LiquidHaskell の世界へ！
LiquidHaskell の仕組み
型検査とサブタイピング
先ほどのコードスニペットをもう少しいじって動作を確かめてみましょう。まず、元のコードに次の関数を付け加えてみてください。
badUsage = safeHead []
safeHead を、事前条件に反して呼び出そうとしているわけです。liquid Sample.hs を実行すると、以下のようなエラーメッセージが返ってくるはずです。
**** RESULT: UNSAFE ************************************************************
/your/path/to/Sample.hs:9:12-22: Error: Liquid Type Mismatch
9 | badUsage = safeHead []
^^^^^^^^^^^
Inferred type
VV : {VV : [a] | len VV == 0
&& (null VV <=> true)
&& len VV >= 0
&& VV == ?a
&& len VV >= 0}
not a subtype of Required type
VV : {VV : [a] | len VV > 0}
In Context
?a : {?a : [a] | len ?a == 0
&& (null ?a <=> true)
&& len ?a >= 0}
「推論された型が要求された型のサブタイプではない」と言われていますね。
先ほど「a を要素とする空でないリスト」の型を { xs:[a] | len xs > 0 } と表現しましたが、LiquidHaskell では一般に「型 a のうち述語 P を満たすもの」は { x:a | P x } で表現されます。そして a 型の任意の値 x について P x => Q x が成り立つと SMT ソルバが判定した場合、LiquidHaskel は { x:a | P x} は { x:a | Q x } のサブタイプであると判断します。
この例でいえば、実引数 [] から推論された述語 len VV == 0 && ... から safeHead の事前条件 len VV > 0 は (当然) 従わないため、コンパイルエラーとして検出されているのです。
それでは逆に badUsage を削除、さらに safeHead の {-@ ... @-} コメントも無効化して実行してみましょう。今度は別のエラーになります。
**** RESULT: UNSAFE ************************************************************
/your/path/to/Sample.hs:6:32-43: Error: Liquid Type Mismatch
6 | safeHead [] = liquidError "empty list"
^^^^^^^^^^^^
Inferred type
VV : {VV : [Char] | VV ~~ ?b
&& len VV == strLen ?b
&& len VV >= 0
&& VV == ?a
&& len VV >= 0}
not a subtype of Required type
VV : {VV : [Char] | false}
In Context
?b : {?b : Addr# | ?b == "empty list"}
?a : {?a : [Char] | ?a ~~ ?b
&& len ?a == strLen ?b
&& len ?a >= 0}
これを見ると、liquidError の正体がわかります。
liquidError の引数として要求されている型は {VV : [Char] | false} です。false は決して真になることがない述語なので、いかなる引数であっても事前条件を満たすことができません。すなわち、liquidError は呼び出されうる場所に配置されると直ちにコンパイルを失敗させます。
もともとは safeHead の事前条件 { xs:[a] | len xs > 0 } が約束されていたためこのパターンマッチを通過しないことが LiquidHaskell によって推論されていたのですが、事前条件を外したことでエラーになったのでした。
もう少し単純な例を使って制約のかけ方を定式化してみましょう。
事前条件
上でも使用していたパターンですが、引数 (のうちのいくつか) に制約をつけることで関数の事前条件を表現することができます。例えば以下はゼロ除算エラーが発生しない割り算の定義です。
{-@ safeDiv :: Int -> { d:Int | d /= 0 } -> Int @-} safeDiv :: Int -> Int -> Int safeDiv n 0 = liquidError "zero divide" safeDiv n d = n `div` d
事前条件が指定されると、その関数のすべての呼び出しについて事前条件が守られているかどうかが検査されます。また、関数内のロジックや事後条件の検証は事前条件の仮定下で行われます。
事後条件
引数ではなく戻り値側に制約をつけて事後条件を表現することもできます。例えば以下は絶対値関数が常に 0 以上の値を返すことを表しています。
{-@ safeAbs :: Int -> { n:Int | n >= 0} @-} safeAbs :: Int -> Int safeAbs n | n >= 0 = n | otherwise = 0 - n
事後条件が指定されると、関数の事前条件および関数内のロジックから事後条件が従うかどうかが検査されます。また、他の関数内で呼び出された呼び出し側の検証は事後条件の仮定下で行われます。
事前条件に依存した事後条件
場合によっては、事前条件に依存した事後条件を記述する必要があります。
例えば整数に 1 を加算する関数について、事後条件に「戻り値は引数より真に大きい」という事後条件を与えてみましょう。条件を記述する際、次のように引数に名前をつけることができます。
{-@ safeIncr :: n:Int -> { v:Int | v > n } @-} safeIncr :: Int -> Int safeIncr n = n + 1
引数に事前条件を課し、さらに名前をつけて事後条件で引用することも可能です。
{-@ safeDouble :: n:{ v:Int | v > 2 } -> { w:Int | w > n + 2 } @-} safeDouble :: Int -> Int safeDouble n = 2 * n
例：ベクトルの次元付き計算
それでは例として、依存型を説明する際によく登場するベクトルの次元付き計算について、LiquidHaskell で表現してみましょう。
Haskell 上でベクトルを表現するもっともナイーブな方法は、単に Num インスタンスを要素とするリストを使用することです。例えばベクトル同士の足し算であればこんな感じでしょうか。
vecSum :: (Num a) => [a] -> [a] -> [a] vecSum xs ys = zipWith (+) xs ys
しかしお気付きの通り、次元が違うベクトル同士が加算できてしまうため、本来表現したい制約が表現できていません。
badSum = vecSum [1, 2, 3] [4, 5] *Main> badSum [5,7]
LiquidHaskell を使って、次元が異なるベクトルについて計算できないようにしてみましょう。そもそもの原因は、zipWith 関数が短い方のリストに合わせて残りを切り捨ててしまうことにあるため、まずこれを LiquidHaskell で書き直しておきます。
{-@ vecZipWith :: (a -> b -> c) -> xs:[a] -> { ys:[b] | len ys = len xs } -> { zs:[c] | len zs = len xs } @-} vecZipWith _ [] [] = [] vecZipWith f (x : xs) (y : ys) = f x y : vecZipWith f xs ys vecZipWith _ _ _ = liquidError "dimension mismatch"
事前条件として「第 2 引数の長さが第 1 引数に等しい」こと、さらに事後条件として「戻り値の長さが第 1 引数に等しいこと」が要求されています。この「次元付き zipWith」を使ってベクトルの足し算を以下のように定義すると
{-@ vecSum :: (Num a) => xs:[a] -> { ys:[a] | len ys = len xs } -> { zs:[a] | len zs = len xs } @-} vecSum xs ys = vecZipWith (+) xs ys
LiquidHaskell は狙い通り警告を出してコンパイルを失敗させます。
/your/path/to/Sample.hs:37:10-33: Error: Liquid Type Mismatch
37 | badSum = vecSum [1, 2, 3] [4, 5]
^^^^^^^^^^^^^^^^^^^^^^^^
同様にして引き算や
{-@ vecSubtr :: (Num a) => xs:[a] -> { ys:[a] | len ys = len xs } -> { zs:[a] | len zs = len xs } @-} vecSubtr xs ys = vecZipWith (-) xs ys
ベクトル同士の内積
{-@ dot :: (Num a) => xs:[a] -> { ys:[a] | len ys = len xs } -> a @-} dot xs ys = sum $ vecZipWith (*) xs ys
あるいはベクトルのスカラー倍
{-@ vecMap :: (a -> b) -> xs:[a] -> { ys:[b] | len ys = len xs } @-} vecMap f [] = [] vecMap f (x : xs) = f x : vecMap f xs {-@ scalar :: (Num a) => a -> xs:[a] -> { ys:[a] | len ys = len xs } @-} scalar c xs = vecMap (c *) xs
も次元に対して安全に定義可能です。長さが正しくないリストをこれらの関数に与えて、実際にエラーになることを確認してみましょう。
まとめ
本エントリでは、LiquidHaskell を利用してリスト操作関数に対して事前条件と事後条件を定義する方法を扱いました。通常の Haskell ではリストの長さに関するエラーは型検査の対象外であり実行してみるまでわかりませんが、LiquidHaskell を用いることでコンパイル時に検出することができます。
今回紹介したのは、LiquidHaskell が持つ機能の一部分にすぎません。もし面白そうだと感じた人は、対話型チュートリアル もしくは 公式ブログ を眺めてみると良いと思います。というかこれを書いている自分自身もまだ全容を把握できていません。一緒に勉強しましょう。
さて、Advent Calendar の 24 日目の担当者はそれぞれ
- Haskell Advent Calendar 2016 : タイトル未定 (@maoe さん)
- Formal Method Advent Calendar 2016 : 空席
となっておりますが、それはまた別の話。
NGK2016B で Kubernetes + Alloy について話してきました
先日、毎年恒例のなごや LT 大会 NGK2016B / 名古屋合同懇親会 2016 忘年会 で発表してきました。
www.slideshare.net
当日の動画は NGK 2016B LT #2 - YouTube から見ることができます。
ちなみに NGK での発表は 4 年連続 4 回目です。今回も含めてすべてモデル検査が題材になっています。
- NGK2013B : Alloy ではじめる簡単モデル検査
- NGK2014B : 猫でもわかる！ モデル検査器 SPIN 入門 (ブログ記事)
- NGK2015B : AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計 (ブログ記事)
Kubernetes に関わる役者たち
さすがに 5 分に詰め込むにはハイコンテクストすぎました。いろいろな登場人物が出てくる上に図でしか説明していない部分もあるため、後からスライドだけ見て最低限の意味が取れるように補足しておきます。
Master/Node
Master がいわゆるコントロール用のサーバ (群) であり、その下に実際にコンテナが載る Node がぶら下がる形になっています。
なぜか Kubernetes のバージョンによってしばしば呼び名が変わっていて、過去には Master/Minion とか、Master Node/Worker Node とか呼ばれていたりしました。
Pod
Kubernetes がコンテナを管理する単位で、1 個以上のコンテナからなります。スライド中では破線で囲まれた「A」と「B」のペアが Pod です。
同じ Pod に属するコンテナ同士は常にひとまとまりになって同じノードにデプロイされます。例えば、アプリケーションのコンテナとそれを監視するエージェントのコンテナを Pod として組にしておく、といった使い方が典型的です。
Replica Set
常時起動させておきたい Pod に対して、使用する Docker イメージや環境変数などの設定と合わせて必要な Pod 数を定める定義書のようなものです。スライド中では「× 2 組」という表現で Replica Set を表しています。
何らかの原因で Pod が異常終了してしまった際は、Replica Set で指定された個数に合わせるように自動で新しい Pod が作成されます。これは後述する Controller Manager のはたらきによるものです。
ちなみに、今回はモデリングの都合上 Replica Set が生で登場していますが、実際には直接扱うことはあまりなく、rolling update など高レベルな操作が可能な Deployment と呼ばれる仕組みと組み合わせて使用するのが普通です。以前のバージョンの Kubernetes では Replication Controller という仕組みがこのポジションにいたのですが、Deployment と組み合わせるため、より柔軟にラベリングが可能な Replica Set に移行しました。
etcd
Kubernetes の状態を保持している分散 KVS です。分散なのでもちろん etcd 自体もクラスタリングできるのですが、今回は話がややこしくなるので単独のサーバが存在する体で説明しています。
API Server
ユーザ、あるいは他のコンポーネントに対して JSON ベースの REST API を提供します。Controller Manager や Scheduler は etcd 上の情報を監視して必要に応じて書き換えますが、その際、直接 etcd にアクセスすることはなく、常に API Server が窓口役になります。
Controller Manager
API Server 経由で etcd に登録されている Replica Set の定義を確認し、それに見合った Pod が存在するかどうかをチェックします。前述のようにもし Pod が足りなくなっている場合は新規登録し、逆に多すぎる場合は登録を抹消します。
Scheduler
コンテナのスケジューリング (= どこのサーバに配置するか) を担当します。より具体的には、API Server 経由で etcd に登録されている Pod の中から割り当て Node が未定になっているものを監視し、見つけた場合にはあらかじめ与えたアルゴリズムにしたがって適切な Node に割り当てます。
Kubelet
各 Node に常駐しているエージェントです。API Server 経由で etcd に登録されている Pod の情報をチェックして、自分がいる Node に割り当てられた Pod を発見すると Docker に命じてコンテナを立ち上げさせます。また、今回のモデルには含まれていませんが、Node やコンテナに関して必要な情報を取得する監視エージェントとしての役割も持っています。
サンプルコードを動かしてみよう！
さて、Kubernetes の動作についてスライド + 上の説明で大体のところを理解したら、ぜひ実際に Alloy のモデルを確認してみましょう。
インストールと実行
公式のダウンロードページ Alloy - download から alloy4.2.jar をダウンロードしましょう。dmg 版は古い JRE でしか動かない ので使わないように。
java -jar alloy4.2.jar
でウィンドウが起動するはずです。
今回使用するサンプルコードは Alloy による Kubernetes のコンテナスケジューリングのモデリング · GitHub にアップロードしてあります。kubernetes.als をダウンロードして開いてください。
Alloy が正しく動作していれば、Execute をクリック (もしくは command + E ) すると以下のような図が表示されるはずです。何も出ない場合は Show をクリックしてみてください。
……なんかやばいのが出ました。矢印が多すぎて訳がわからない！
可視化結果を整える
図がごちゃごちゃになっている原因のひとつは、etcd の持つデータが時刻に依存しており、それを 1 枚の図にすべて表示していることです。まずこれをどうにかして、各時刻における状態をそれぞれ独立して図示できるようにしましょう。
先ほどの状態から、可視化ウィンドウのツールバーにある「Projection: none」を開いて「Time」にチェックを入れてください。図が次のように変化するはずです。
ちょっとましになりました。またよく見ると、ウィンドウの下側に「Time0」と表示されるようになったはずです。Time は今回のモデルで時刻を表すパラメータになっていて、etcd の状態の時間断面を表示することができます。射影 (projection) と呼ばれる操作です。射影する時刻を動かして図が変化することを確認しましょう。
それでもまだ矢印が多すぎてわかりづらいので、必要な情報だけを残して非表示にしてしまいたいと思います。手動で設定することも可能ですが、Alloy は可視化時の設定を XML ファイル (拡張子は .thm) として書き出す/読み込む機能があるのでこれを使います。
先ほどの Alloy による Kubernetes のコンテナスケジューリングのモデリング · GitHub から、alloy_kubernetes.thm をダウンロードしておきます。メインウィンドウのツールバーから「Theme」を選び「Load Theme...」してください。
この状態で 「Time0」で射影すると、上のような状態になるはずです。これは etcd の初期状態で、
- API Server は etcd に接続している
- etcd は Node の一覧を持っているが、Replica Set や Pod はまだ登録されていない
という状態を表しています。時刻を変化させて、上の説明で登場した各コンポーネントが仕事する様子を心ゆくまで確認してみましょう。
まとめ
さて、本エントリでは NGK2016B での LT を補足するものとして
- Kubernetes のコンポーネントの概要
- サンプルコードを使ってスライドと同じ可視化結果を得る方法
を説明しました。
サンプルコード alloy_kubernetes.als が何を表しているのか、あるいはどのようにしてこのモデルを実装したかという話題も色々と面白いところではあるのですが、ちょっと長くなるので、それはまた別の話。
Frege のチュートリアル集「Frege Goodness」を翻訳しました
Frege のチュートリアル集を日本語に翻訳しました。原著は Dierk Koenig 氏による Frege Goodness · GitBook です。
対象読者
まえがきでも述べられている通り、Frege の (すなわち Haskell の) 基本的な文法については既知のものとして扱われます。より具体的には「すごい Haskell」の前半部分を読んだ、ぐらいでしょうか。例えば型クラス自体は知っている必要がありますが、モナドに対する理解は要求しません。
ちなみに、目を通していただけるとすぐにわかりますが、実は Frege に特有な内容はさほど登場しません。どちらかというと Java プログラマに対して Haskell 的な考え方を導入するために Frege を題材にしている、という印象が近いでしょう。
ただし 「ドット記法の威力」の記事は例外 です。Frege では Haskell と異なり、 Lens に似たドットアクセッサを使用する機能がデフォルトで定義されています。ちょっとした目新しさのある部分なので、すでに Haskell をよく知っている方はここをエントリポイントにするのがオススメです。
公開プラットフォーム
今回の翻訳版は、原著に合わせる意味もあって、GitBook で公開しています。GitBook は特定の形式を持つ Git レポジトリと紐付けておくと自動で電子書籍としてレンダリングしてくれるサービスです。原稿は Markdown あるいは AsciiDoc が使用可能で、各種形式でのダウンロードにも対応しています。
なお、原稿本体は GitHub にホスティングしてあります。誤植や表記ゆれ、誤訳などお気付きの際には issue や PR を上げていただけると大変にありがたいです。
ところで現状、GitBook から日本語書籍を PDF 出力するとフォントが正しく埋め込まれず、中国語フォントになってしまうようです。CSS できちんと指定する必要があるのですが、それはまた別の話。
Frege からメールが送信できるようになりました
ちょっとした Web アプリを作成しようと思うと、メール送信機能がないと困ります。例えば、ログイン機能を持っていれば必然的にパスワードリセットとかも必要になりますからね。
Haskell 風の JVM 言語 Frege でもフレームワーク Chinook を使用して Web アプリが作れますが、メールを送信するライブラリが見当たらなかったので自作しました。
なお、すでに Bintray に公開済みなので、各種ビルドツール経由で呼び出すことができます。現状、Frege のビルドは Gradle がデファクトスタンダードなので、以下でも Gradle で説明しましょう。
使い方
Gradle ビルド時に Bintray に問い合わせに行くように、build.gradle にリポジトリを追加する必要があります。普段 Maven Central とか jCenter だけ使っていると忘れがちなので気を付けましょう。
あとは Frege コンパイラ自体と、Frege 用のタスクを Gradle に認識させるプラグインを追加すると、ビルド可能な最小の build.gradle は以下のようになります。
plugins {
id 'org.frege-lang' version '0.5'
}
apply plugin: 'org.frege-lang'
repositories {
jcenter()
maven {
url 'http://dl.bintray.com/y-taka-23/maven'
}
}
dependencies {
compile 'org.frege-lang:frege:3.23.288-gaa3af0c'
compile 'io.cheshirecat:frege-email:0.1.0'
}
さて、実際にメールを送信するコードを書いてみましょう。
送信サーバとしてはとりあえず Gmail を使用します。残念なことに現状 安全性の低いアプリからのアクセスを許可 しておく必要がありますが、いずれは対応したい。
コードはこんな感じになります。yourusername と yourpassword は手持ちの Google アカウントに差し替えてください。
module Main where import io.cheshirecat.frege.Email server = sslSMTPServer.{ hostName = "smtp.gmail.com" } auth = authentication.{ userName = "yourusername" , password = "yourpassword" } addr = address.{ email = "foo@gmail.com" } testMail = email.{ subject = "Test Mail" , from = addr , to = [addr] , message = "This is a test mail." } main _ = do flip catch handler $ do sendEmail server (Just auth) testMail where handler = \(e::EmailException) -> e.printStackTrace
このコードを src/main/frege/Main.fr に置いておきます。
生成されるクラスファイルを直接 java コマンドで叩いても実行できますが、Gradle から実行するのであればさらに build.gradle に
apply plugin: 'application' mainClassName = 'Main'
を追加した上で gradle run で実行すると Gmail にテストメールが届くはず。
Frege のおいしいところ
今回のライブラリは Apache Commons Email を呼び出していて、自前で実装しているロジックはほとんどありません。JVM 言語の利点としてよく「既存の Java 資産を使用できる」という点が挙げられますが、Frege もその例外ではなく、面倒な処理は全部 Java 呼び出しで済ませました。
ちなみに呼び出し部分のコードは こんな感じ になります。Frege による Java 連携に興味がある人は、次のスライドが役に立つはずです。
www.slideshare.net
また、前述の Gradle ビルドからわかる通り、作成したライブラリの配布についても、既存の Java のエコシステムに乗っかることができます。ライブラリを作る側の作業については若干気をつける点があるため、備忘録を兼ねてこのブログで書くつもりではありますが、それはまた別の話。
JAWS FESTA 東海道 2016 で形式手法によるネットワーク設計について話してきました
先日行われた JAWS FESTA 東海道 2016 で登壇してきました。
www.slideshare.net
テーマは以前 AWS Summit で発表したものと同じですが、前回が 5 分の LT だったのに比べて今回は 25 分の枠を頂きました。そこで、形式手法を用いる動機を中心に据えた前回と比較して、以下のような実践的なトピックを充実させてあります。
- Alloy を使うためにの最低限必要な言語機能を知る
- シンプルな Web サーバ周りのネットワークについて、仕様から設計を導出する
ちなみに前回の AWS Summit 2016 での発表に関してはこちらから。
寄せられた質問
発表後に頂いたいくつかコメントや質問について、ここで説明しておきます。
「全探索」と言っているが、無限の範囲を探索するのは不可能なのでは？
はい、その通りです。Alloy におけるシグネチャは有限集合でしかありえないので、探索はその範囲に限られます。例えば、
run fooPred for 5
とすると各シグネチャの要素数が 5 個以下の場合を探索します。デフォルトは 3 です。
とはいえ、資料中に登場する 3 個の要素を持つ 2 種類のシグネチャ間の関係だけを考えるケースでさえ、考えうる関係の数は 2 の 3 * 3 乗で 512 通りもあります。実用的なモデルを書こうと思えば場合の数は急激に増えていくため、人力でテストケースを組むことを考えれば Alloy も捨てたものではありません。
ちなみにこのような Alloy の設計思想は「もし仕様バグが存在するなら、それは比較的小さなモデルの時点ですでに問題になるはずだ」というアイデアで正当化されています。この考え方は 小スコープ仮説 (small scope hypothesis) と呼ばれています。
AWS リソースを自前でモデル化するのは辛そう。ライブラリ化の予定は？
できたら面白いとは思っていますが、現実的には厳しそうです。
これは、ライブラリを作成しようと思うと、必然的に個別事例では必要のない部分（例えばセキュリティグループのみ考えてネットワーク ACL は使わない、など）までモデルに含まれてしまうためです。Alloy のモデルは関係が必ず集合に結びつく形で定義されているため合成可能性に乏しく、必要な要素のみライブラリから取り出して使用することが困難なのです。
現時点では、個別にそのとき必要な部分を取捨選択してモデル化するのが妥協案だと思います。
Alloy を勉強しようと思ったら何から始めるのがいい？
毎回名前を挙げていますが、以下の書籍がおすすめです。初見だと多少記述がとっつきづらく感じるかもしれませんが、実際に Alloy を動かしつつ読むと理解が深まるでしょう。なおこの本の内容を把握したら後は慣れの問題です。
おわりに
今回の発表、実は当初はここまで Alloy に特化せず、参照した論文中で述べられている AWS 内での取り組みをもう少し前面に出そうかと思っていました。スライドの途中で TLA+ の名前が出てくるのは名残です。
ただ TLA+ は完全にオートマトン型の典型的なモデル検査器であり、AWS を 使う側 とは相性があまり良くなかったため、具体的な内容は結局すべて外してしまいました。その分 Alloy についてはこの発表を聞いた人がとりあえず触ってみる程度のことは説明できたので、まあ結果オーライかなとは思います。
ところで、今年もまた名古屋のコミュニティ合同忘年会 NGK2016B がありますね？ 自分はここ数年連続して色々なモデル検査ツールの発表をしているのですが、それはまた別の話。
AWS Summit Tokyo 2016 で形式手法について話してきました
先日行われた AWS Summit Tokyo 2016 で、形式手法のインフラ設計への応用について発表してきました。
www.slideshare.net
モデル検査器 Alloy を利用して AWS の設定を検査する、という内容の LT で、昨年 12 月の NGK2015B でも同じテーマについて話しています。よければ以下の記事も合わせてお読みください。
NGK2015B の発表ではサンプルコードの紹介に比較的時間を割いているのに対して、今回の発表では「動機」の部分によりウェイトを置いた構成になっています。
なぜ形式手法なのか？
今回のテーマを一言でまとめると以下のようになります。
インフラ構成が「秘伝のタレ」と化すのをどう防ぐべきか？
ある程度の規模のインフラを長期間運用していると、どうしても初期の想定が変質してくることは避け得ません。アプリ側の要件が変わったりして、インフラ側がアドホックな対応を迫られるケースも（本来望ましくないですが）一定の割合で生じるものです。また、担当者が代替わりして暗黙知がうまく引き継がれない状況もあるでしょう。
必然的にカオスの縁にいる我々は、どうやってこの状況に対抗すべきでしょう？ アプリ開発であればきっと「単体テスト書こうぜ！」みたいな流れになるわけですが、さてインフラを検証したい場合にどんな手段が取れるのか？
awspec
「AWS + テスト」というキーワードで真っ先に思い出すのはおそらく awspec ではないかと思います。
awspec は servespec に着想を得たツールで、RSpec を利用して AWS リソースをテストできるようになっています。また、人間が直接 spec を記述するだけでなく、現に存在するリソースから awspec generate コマンドを使ってテストケースを自動生成することも可能です。
しかし、すでに存在するリソースをテストするという性質上、設計を考える段階での試行錯誤にはあまり向いていません。また、何かを変更しようとした際にそれをあらかじめ検証するという用途も難しいでしょう。好き好んで Amazon にお布施をしたい人は別として、テストそれ自体に掛かるコスト面も大きな問題です。
IAM Policy Simulator
さて、翻って他の方法を考えてみると、IAM のアクセス権限については、公式がシミュレータを提供してくれています。
実際の操作を行わなくとも dry run で検証できる、というのが大きなメリットで、例えば「削除」の権限をテストするのに実際の削除は発生しません。これがあれば、少なくとも IAM のアクセスポリシーを設定する際には、心ゆくまで試行錯誤ができそうです。
しかし（当たり前ですが）この機能は IAM 限定。となると、以下のような疑問が自然に生じます。
「現物」がなくても検証できる、汎用的な手法はないか？
この疑問への答えとして、現物ではなく形式化したモデルを検証することで有益な結果が得られるのではないか、というのが今回の発表の主題です。
形式手法とその限界
形式手法とは、システムの静的解析の中でも特に
- システムの仕様を数学的に厳密に記述する
- その正しさをやはり数学的に保証する
という特徴を持つ一連の手法を指して使われる用語です。現物と離れたところで堅く検証を行う、という意味では今回の目的にはピッタリです。
しかし如何せん、形式手法はコストがかかります。そもそも形式手法が扱える人間が少ないことに加え、大抵のツールでは従来のテストよりもずっと多くの工数が必要になります。そのため実際の形式手法の導入は、そのコストを支払ってもお釣りがくるほど高信頼性が求められる案件に限られているのが現状です。
今回の場合、どの程度ならコストとメリットが釣り合うのかはよく考える必要があります。形式手法を採用するのは手段であって目的ではないわけで、そこに必要以上に時間をかけるのはどう考えても本末転倒です。
このジレンマをなんとかするために登場するツールが Alloy Analyzer です。
アンチテーゼとしての Alloy
Alloy では関係論理を利用してシステムのモデルを定義し、さらにそこに検査したい制約を加えたものを充足可能性問題に変換することで、SAT ソルバを利用して条件を満たす例・満たさない例を全探索します。モデルの定義や制約の記述にはやや慣れが必要ですが、他のツールと異なり検証作業自体は自動化されており、上で述べたコストの問題はある程度クリアできます。
手軽に使用できる反面、当然ある種の欠点もあります。テストと比較して形式手法を語る際、メリットとしてよく「テストは有限個のケースしか検証できない。形式手法では無限個の入力に対して正しさを保証できる」という言い回しがなされることがありますが、Alloy についてこれは成り立ちません。
全探索を行うことからもわかる通り、Alloy による検証では、モデル中の要素の個数を制限する必要があります。この制限は例えば今回であれば「セキュリティーグループが 3 個以下の場合」のような但し書きとして現れます。
実は Alloy の背景には「仕様バグは小さなモデルで十分再現できる」という哲学があります。つまり、セキュリティグループが 10 個以上の場合に初めて現れる問題はそうそうないだろう、というわけです。この哲学は 小スコープ仮説 (small scope hypothesis) と呼ばれており、ある種の割り切りによって支えられています。
おわりに
今回の発表では、インフラの検証に形式手法が使えること、およびそのためのツールとして Alloy Analyzer を紹介しました。Alloy に興味を持った人は、以前の記事でも紹介していますが、以下の参考書が鉄板です。
ちなみに余談ですが、実は（AWS を利用する側ではなく）AWS そのものの設計にも形式手法が利用されています。しかも、形式手法を導入するにあたって Alloy が検討されていたにもかかわらず、結果的には要件に合わずに TLA+ という別のツールが採用されるという経緯を辿っています。
この辺り、ツールの特性の比較などと絡めて考えると面白い話題でもあるのですが、それはまた別の話。
NL 名古屋で Frege の評価戦略について話してきました
先日の 歌舞伎座.tech に引き続き、NL名古屋 - connpass で Haskell 風 JVM 言語 Frege について発表してきました。
今回の発表では、Frege の持つ Haskell 的特徴である非正格評価に焦点を当て、正格評価を行うはずの Java 上でなぜ評価を遅延させられるのか、その内幕を解説しています。
www.slideshare.net
なお当日の様子は NL名古屋 -NLとはなんだったのか- #nlnagoya - Togetterまとめ にまとめられています。長丁場でしたが、各々さまざまなテーマの発表があり、楽しめるイベントだったと思います。
Java のコード生成を試してみよう！
発表中に述べている通り、Frege のコンパイラはバイトコードではなく Java のソースコードを出力します。ただしスライド中で言及されているコードは Frege が生成した Java コードそのものではなく、今回の内容との関連が薄い部分をわかりやすく改変したものです。ここでは実際にどのようなコンパイル結果が得られるのかを見てみましょう。
コンパイラとコードの準備
Frege の Java 生成ロジックは、最新バージョン v3.24 から大きく変更になりました。今回の発表で述べられているのはこの新しい方のロジックです。
最新のコンパイラはまだ α 版で、各種ビルドツールではまだ使用できないようなので、直接バイナリをダウンロードします。
$ wget -O fregec.jar https://github.com/Frege/frege/releases/download/3.24alpha/frege3.24.61.jar $ chmod +x fregec.jar
次に、スライド中で登場した竹内のたらい回し関数をサンプルとして使用します。以下の Frege コードを Tarai.fr として保存してください。
module Tarai where tarai :: Int -> Int -> Int -> Int tarai x y z = if x <= y then y else tarai (tarai (x - 1) y z) (tarai (y - 1) z x) (tarai (z - 1) x y)
ビルド結果が散らからないように、出力先として build ディレクトリを作成しておきましょう。
$ mkdir build
コンパイル結果の確認
以下のコマンドでコンパイルを実行します。
$ java -Xss1m -jar fregec.jar -d build Tarai.fr
しばらく待つと build 以下に Tarai.java と Tarai.class が生成されます。
今回の目的である build/Tarai.java を確認してみましょう。ファイルの前半はボイラープレートなので無視して、以下の部分が tarai 関数の変換結果です。
final public static int tarai(int arg$1, int arg$2, Lazy<Integer> arg$3) { tailrecursion: while (true) { final int arg$1f = arg$1; final int arg$2f = arg$2; final Lazy<Integer> arg$3f = arg$3; if (arg$1f <= arg$2f) { return arg$2f; } else { arg$1 = Tarai.tarai(arg$1f - 1, arg$2f, arg$3f); arg$2 = Tarai.tarai(arg$2f - 1, (int)arg$3f.call(), Thunk.<Integer>lazy(arg$1f)); arg$3 = Thunk.<Integer>shared( (Lazy<Integer>)(() -> Tarai.tarai((int)arg$3f.call() - 1, arg$1f, Thunk.<Integer>lazy(arg$2f))) ); continue tailrecursion; } } }
まず気づくこととして、Frege 側の tarai 関数は再帰の形で定義されていましたが、末尾再帰最適化の結果ループ tailrecursion に変換されています。このままだと本題が見えづらいので、Tarai.fr を以下のように書き換えてあえて最適化しないようにしてみましょう。
module Tarai where tarai :: Int -> Int -> Int -> Int tarai x y z = if x <= y then y else 0 + tarai (tarai (x - 1) y z) (tarai (y - 1) z x) (tarai (z - 1) x y)
生成される build/Tarai.java は以下のように変化します。
final public static int tarai(final int arg$1, final int arg$2, final Lazy<Integer> arg$3) { if (arg$1 <= arg$2) { return arg$2; } else { return 0 + Tarai.tarai( Tarai.tarai(arg$1 - 1, arg$2, arg$3), Tarai.tarai(arg$2 - 1, (int)arg$3.call(), Thunk.<Integer>lazy(arg$1)), Thunk.<Integer>shared( (Lazy<Integer>)(() -> Tarai.tarai((int)arg$3.call() - 1, arg$1, Thunk.<Integer>lazy(arg$2))) ) ); } }
ここから、識別子をわかりやすく x y z に変更して不要な修飾子も削ったものがスライド中に登場したコードです。
static int tarai(int x, int y, Lazy<Integer> z) { if (x <= y) { return y; } else { return tarai( tarai(x - 1, y, z), tarai(y - 1, (int)z.call(), Thunk.<Integer>lazy(x)), Thunk.<Integer>shared( (Lazy<Integer>)(() -> tarai((int)z.call() - 1, x, Thunk.<Integer>lazy(y)))) ); } }
まとめ
本記事では、発表中に端折り気味だった Java のコード生成部分について、実際のたらい回し関数のコンパイル結果を挙げて補足しました。スライドも合わせて確認してもらえると幸いです。
ちなみに、今回のたらい回し関数は単純に int をとって int を返すだけの関数でした。しかし実際の Frege コードにはもっと複雑な言語機能がいくらでも登場し、
などを Java 上で再現するために語るべきことは尽きません。いずれこのブログのネタにでもしますが、それはまた別の話。
