elm/time の使い方
はじめに
先日、Elm v0.19 がリリースされました。公式ライブラリのリポジトリが elm-lang
から elm
に変更され、その中身も大きく再構成されています。
本記事では、これらの変更のうち特に時刻や日付の扱いに関する部分について、新しい API の使い方を含めて簡単に解説します。
v0.18 における時刻の扱い
v0.18 では、時刻を扱う機能は標準パッケージ elm-lang/core
の中で提供されていました。時刻を扱う Time
モジュールと日付を扱う Date
モジュールで、それぞれデータ型や関数が定義されているのが特徴です。
なお、旧バージョンのライブラリは現在 Elm Packages の検索にはヒットしない ので、中身を確認するためには直接 URL にアクセスする必要があります。
旧 Time モジュール
時刻を扱う Time
型を提供します。Time
型の実体は Float
型のエイリアスで、Unix Epoch からの経過ミリ秒数を表します。
メインの関数は現在時刻を取得する now
と指定した時間間隔で Msg を送出する every
です。その他、every
と組み合わせて使用する単位として second : Time
や minute : Time
が定義されており、例えば毎秒何かを行う Subscription は次のように書けます。
type Msg = DoSomethingAt Time.Time subscriptions : Model -> Sub Msg subscriptions _ = Time.every Time.second DoSomethingAt
旧 Date モジュール
日付を扱う Date
型を提供します。また Time
型との変換用の関数もこちらで定義されています。
その他、紛らわしいですが Date
モジュールでも now
関数がエクスポートされており、こちらは現在の日付を取得します。
特徴的なのは、Time
型と Date
型の変換においてタイムゾーンを指定する機能がないことです。したがって API 定義上は
toTime : Date -> Time fromTime : Time -> Date
の変換は純粋な関数に見えますが、実際にはシステムのタイムゾーンに依存する副作用を持っていることになります。
v0.19 における時刻の扱い
さて、今回新しくなったバージョンでは、旧 Time
と Date
に相当する機能が再編成されてひとつのモジュール Time
になり、さらに別ライブラリ elm/time
として切り出されました。
新 Time モジュール
大きな変更点は、Unix 時間を表す Posix
型に加えて、タイムゾーンを表す Zone
型が陽に導入されたことです。
現在時刻を取得するには今まで通り now
で、現在のタイムゾーンを取得するには here
を使用します。例えば初期化の際、両者を同時に取得する Cmd
は以下のように書けます。
type Msg = SetSystemTime (Time.Zone, Time,Posix) setSystemTime : Cmd Msg setSystemTime = Task.perform SetSystemTime <| Task.map2 Tuple.pair Time.here Time.now
旧 Date
モジュールにあった日付への変換も Time
の中にまとめられました。Unix 時間が同じでも実際の日付はタイムゾーンに依存するため、変換には Zone
型が必要になっているのが分かります。新しい変換関数名には toXXX
で統一されており、Day
型は Weekday
型に、dayOfWeek
は toWeekday
に変更されました。
toYear : Zone -> Posix -> Int toMonth : Zone -> Posix -> Month toWeekday : Zone -> Posix -> Weekday toHour : Zone -> Posix -> Int toMinute : Zone -> Posix -> Int toSecond : Zone -> Posix -> Int toMillis : Zone -> Posix -> Int
また、旧 Time
モジュールにあった時間の単位 minute
や second
は外されました。ミリ秒単位で直接指定する必要があります。
サンプル:デジタル時計
以上をまとめると、Elm v0.19 対応の簡単なデジタル時計は次のように実装することができます。
- 初期化時に
setSystemTime
で現在のタイムゾーンと時刻を取得 - それ以後 1000 ミリ秒ごとに
setCurrentTime
で現在時刻を更新 - 表示の際は
toHour
とtoMinute
でタイムゾーン依存の時刻に変換
という流れになっています。
module Main exposing (main) import Browser import Html exposing (..) import Task import Time main : Program () Model Msg main = Browser.element { init = init , update = update , view = view , subscriptions = subscriptions } type alias Model = { zone : Time.Zone , posix : Time.Posix } type Msg = SetSystemTime ( Time.Zone, Time.Posix ) | SetCurrentTime Time.Posix init : () -> ( Model, Cmd Msg ) init _ = ( { zone = Time.utc, posix = Time.millisToPosix 0 }, setSystemTime ) update : Msg -> Model -> ( Model, Cmd Msg ) update msg model = case msg of SetSystemTime ( zone, time ) -> ( { zone = zone, posix = time }, Cmd.none ) SetCurrentTime time -> ( { model | posix = time }, Cmd.none ) view : Model -> Html Msg view model = let h = Time.toHour model.zone model.posix m = Time.toMinute model.zone model.posix in div [] [ text <| String.fromInt h ++ ":" ++ String.fromInt m ] setSystemTime : Cmd Msg setSystemTime = Task.perform SetSystemTime <| Task.map2 Tuple.pair Time.here Time.now subscriptions : Model -> Sub Msg subscriptions _ = Time.every 1000 SetCurrentTime
Time.Extra モジュール
ところで、実際に時刻を扱うアプリを書いてみると、elm/time
はかなり非力であることがわかります。特に以下のようなケースは問題になりそうです。
- 時刻 + タイムゾーンから Unix 時間に変換できない(例:特定の日付と現在時刻を比較したい)
- 時刻の和や差が取れない(例:ちょうど 1 か月後の日付が欲しい)
- 時刻を丸めることができない(例:次に 00 秒になるタイミングで Msg を発生させたい)
このような問題を解決するために、justinmimbs/time-extra
が使用できます。
Time.Extra
モジュールでは旧 Date
型に代わるものとして Parts
型を定義しており、Zone
型を組み合わせることで各タイムゾーンにおけるその時刻の Unix 時間を得ることができます。
partsToPosix : Zone -> Parts -> Posix -- UTC における 2018/09/26 11:23.45.00 time1 : Posix time1 = partsToPosix utc <| Parts 2018 Sep 26 11 23 45 0
また、旧 Time
モジュールの minute
や second
や代わる時間単位として Interval
型を定義しており、これを使って「1 か月後の日付」や「次に 00 秒ちょうどになる時刻」が取得できるようになっています。
add : Interval -> Int -> Zone -> Posix -> Posix ceiling : Interval -> Zone -> Posix -> Posix -- UTC における 2018/09/26 11:23.45.00 の 1 か月後 time2 : Posix time2 = add Month 1 utc <| partsToPosix utc <| Parts 2018 Sep 26 11 23 45 0 -- UTC における 2018/09/26 11:23.45.00 以降、最初に 00 秒になる瞬間 time3 : Posix time3 = ceiling Minute utc <| partsToPosix utc <| Parts 2018 Sep 26 11 23 45 0
まとめ
本記事では Elm v0.19 で刷新された elm/time
について、旧バージョンとの違いや使い方について簡単に解説しました。
- 時刻パッケージは
elm-lang/core
からelm/time
に移動 - 原則
Posix
を操作し、通常の時刻表示に変換した時はZone
と合わせる - 時刻を操作するには
justinmimbs/time-extra
ライブラリが使える
ところで、今回紹介した新しい API を使ってちょっと面白いサンプルアプリを作ってみたので、GIF アニメにしたものを貼っておきます。
元ネタは Humans since 1982 の作品 ClockClock 24 です。ソースコードは以下にあるので elm/time
の使い方の参考に。
ちなみにこのサンプル、実際には elm/time
ではなくそれ以外の部分の実装のほうが大変だったのですが、それはまた別の話。
詳解! Elm における Fuzzing
先日行われた We Are JavaScripters! @23rd で、Elm のテストフレームワーク elm-test に搭載されている Fuzzing 機能について発表してきました。
Fuzzing を利用するとテストデータを自動で生成することができるため、例えば「encode と decode を行うと元に戻る」といった、入力に依存しない 関数の性質に関するテスト をより簡単かつ効率的に実装することができます。
さらに、後で詳しく解説する通り、elm-test の Fuzzer にはバグが起こりやすいエッジケースを集中的に生成してくれるというメリットもあります。
elm-test の使い方は、すでに偉大なる先達によって大部分が解説済みです。普通にテストする上では、これらの内容を押さえておけば困ることはないでしょう。
- [Elm] Fuzzer でテストデータを量産しよう (by jinjor さん)
- [Elm]キミだけのッ最強Fuzzerを手に入れろ! (by arowM さん)
そこでこの記事では、もう少し内部の実装にも踏み込んで説明します。なお、ソースコードを載せる際には執筆時点の master
ブランチ (19f0bb3
) を参照しています。
Fuzzer コンビネータの一覧
elm-test では、Fuzzing 関連の機能は Fuzz
モジュールで定義されています。このモジュールが expose しているすべての関数を以下にリストアップしました。
便宜上「コンビネータ」と呼んではいますが種類さほど多くなく、Persec のような色々入ったライブラリを想像するとちょっと肩透かしかもしれません。特定の条件に従うような値を生成したい場合は、自分で Fuzzer を定義する必要があります。
組み込み型に対応するタイプ
基本パーツとなる Fuzzer です。読んで字のごとく、生成する値の型名に対応した Fuzzer が用意されています。
bool : Fuzzer Bool int : Fuzzer Int float : Fuzzer Float char : Fuzzer Char string : Fuzzer String order : Fuzzer Order unit : Fuzzer ()
最後の unit
は常にユニット値 ()
のみを生成する Fuzzer です。テストに直接関係しない引数をプレースホルダーとして埋めるために用意されていて、例えば elm-test の内部では Result
型のエラー側に unit
が使用されています。
パラメータが付いたタイプ
Int
および Float
用には、範囲を指定するとその間の値を生成する Fuzzer が用意されています。
intRange : Int -> Int -> Fuzzer Int floatRange : Float -> Float -> Fuzzer Float percentage : Fuzzer Float
percentage
は 0 から 1 の値を生成するための Fuzzer です。パーセンテージなら 0 から 100 であるべき気がしますがどうしてこうなった。
用途によっては最小値(もしくは最大値)のみ指定したいこともあるでしょう。その場合は intRange 0 Random.intMax
のようにすれば表現することができます。
候補から選択するタイプ
あらかじめいくつかの Fuzzer を与えると、その中から乱択するタイプです。
constant : a -> Fuzzer a oneOf : List (Fuzzer a) - Fuzzer a frequency : List ( Float, Fuzzer a ) -> Fuzzer a
constant x
は常に同じ値 x
を返す Fuzzer です。これと oneOf
を組み合わせると、与えられた選択肢からランダムにどれかを選ぶ Fuzzer になります。
logLevel = Fuzzer String logLevel = Fuzz.oneOf [ Fuzz.constant "ERROR" , Fuzz.constant "WARN" , Fuzz.constant "INFO" ]
また oneOf
の代わりに frequency
を使用すると、選択される割合に重みを掛けることができます。例えば次のように書けば、"ERROR"
を 10%、"WARN"
を 30%。"INFO"
を 60% の内訳で生成する Fuzzer が得られます。
logLevel = Fuzzer String logLevel = Fuzz.frequency [ (1, Fuzz.constant "ERROR") , (3, Fuzz.constant "WARN") , (6, Fuzz.constant "INFO") ]
コンテナタイプ
中身の型に対する Fuzzer が与えられているとき、外側のコンテナ部分を含めた値を生成させるために使用します。
maybe : Fuzzer a -> Fuzzer (Maybe a) result : Fuzzer error -> Fuzzer value -> Fuzzer (Result error value) list : Fuzzer a -> Fuzzer (List a) array : Fuzzer a -> Fuzzer (Array a) tuple : (Fuzzer a, Fuzzer b) -> Fuzzer (a, b) tuple3 : (Fuzzer a, Fuzzer b, Fuzzer c) -> Fuzzer (a, b. d) tuple4 : (Fuzzer a, Fuzzer b, Fuzzer c, Fuzzer d) -> Fuzzer (a, b. c. d) tuple5 : (Fuzzer a, Fuzzer b, Fuzzer c, Fuzzer d, Fuzzer e) -> Fuzzer (a, b, c, d, e)
合成を定義するタイプ
必要な Fuzzer が以上の関数の組み合わせで表現できない場合は、Fuzzer どうしの合成を自分で定義しましょう。
Fuzz.map
map : (a -> b) -> Fuzzer a -> Fuzzer b map2 : (a -> b -> c) -> Fuzzer a -> Fuzzer b ->Fuzzer c map3 : (a -> b -> c -> d) -> Fuzzer a -> Fuzzer b ->Fuzzer c -> Fuzzer d map4 : (a -> b -> c -> d -> e) -> Fuzzer a -> Fuzzer b -> Fuzzer c -> Fuzzer d -> Fuzzer e map5 : (a -> b -> c -> d -> e -> f) -> Fuzzer a -> Fuzzer b -> Fuzzer c -> Fuzzer d -> Fuzzer e -> Fuzzer f
典型的な用途として、自作のデータ型に対して、各フィールド用の Fuzzer にコンストラクタを map
すればそのデータ型用の Fuzzer を定義することができます。例えば以下は、String
、Int
、Bool
をそれぞれ生成する Fuzzer を組み立てて User
型の Fuzzer を得る例です。
type alias User = { name : String , age : Int , active : Bool } user : Fuzzer User user = Fuzz.map3 User Fuzz.string (Fuzz.intRange 20 60) Fuzz.bool
map
は 5 引数までしか用意されていません。6 個以上のフィールドを持つようなレコードに対して Fuzzer を定義したい場合には、次の andMap
を使用しましょう。
Fuzz.andMap
andMap : Fuzzer a -> Fuzzer (a -> b) -> Fuzzer b
Haskell でいうところの Applicative
型クラスの <*>
に相当します。部分適用を繰り返すことで、任意個の引数を持つ関数を Fuzzer に持ち上げることができます。
上で map3
を用いて定義した User
の例は、次のように書き換えることが可能です。
user : Fuzzer User user = Fuzz.map User Fuzz.string |> Fuzz.andMap (Fuzz.intRange 20 60) |> Fuzz.andMap Fuzz.bool
Fuzz.andThen
andThen : (a -> Fuzzer b) -> Fuzzer a -> Fuzzer b
Haskell でいうところの Monad
型クラスの =<<
に相当します。複数の Fuzzer に対して依存関係にある値を生成させることができます。
あまり効果的な用途が思いつかなかったのですが、例えば以下の Fuzzer は一度生成した文字列を逆順にしてくっつけることで、偶数文字からなる回文をランダムに生成します。
mkPalindrome : String -> Fuzzer String mkPalindrome x = Fuzz.constant <| x ++ String.reverse x palindrome : Fuzzer String palindrome = Fuzz.string |> Fuzz.andThen mkPalindrome
その他
それ以外にも、特殊な用途を持つ Fuzzer がいくつか定義されています。
Fuzz.invalid
invalid :: String -> Fuzzer a
常に失敗する Fuzzer で、第一引数はエラーメッセージを表します。
他の Fuzzer コンビネータに対して無効値が与えられたときに使用します。例として、elm-test 内では oneOf
に空リストが与えられた場合の値として使用されています。
Fuzz.conditional
conditional : { retries : Int, fallback : a -> a, condition : a -> Bool } -> Fuzzer a -> Fuzzer a
いったん値を生成した後、それが条件 condition
に合わないときに生成し直します。retries
は再生成の最大回数で、それでも条件に合う値が得られなかった場合は fallback
から得られる値を(condition
は無視して)使用します。
ちなみに ドキュメント によれば retries
の推奨値は 10 です。
custom
custom : Generator a -> Shrinker a -> Fuzzer a
ここまでに挙げたすべての Fuzzer の大元になっている最も抽象的な定義です。
定義を見ると、a
型に対する Fuzzer を定義するためには、a
型に対する Generator
と Shrinker
を与えればよいことが分かります。次節でそれぞれの役割を確認しましょう。
Fuzzer の構成要素と役割
Generator と Shrinker について説明する前に、Fuzz
モジュール冒頭の ドキュメンテーションコメント を少し眺めてみましょう。
A `Fuzzer a` knows how to create values of type `a` in two different ways. It
can create them randomly, so that your test's expectations are run against many
values. Fuzzers will often generate edge cases likely to find bugs. If the
fuzzer can make your test fail, it also knows how to "shrink" that failing input
into more minimal examples, some of which might also cause the tests to fail. In
this way, fuzzers can usually find the smallest or simplest input that
reproduces a bug.
ここでは Fuzzing に関する重要なふたつの性質が述べられています。
- エッジケース(コーナーケース)をより頻繁に生成する
- テストに失敗した場合、入力を「縮小する」ことで失敗を再現する最小例を求める
前者の戦略を定義するのが Generator、後者の戦略を定義するのが Shrinker です。
Generator
エッジケースの判定
まずドキュメント通り、本当にエッジケースが多めに選ばれていることを確認するために、-4 以上 5 以下の整数を生成させてみましょう。intRange -4 5
により 10,000 ケース生成したところ、内訳は次のようになりました。
value | count |
---|---|
-4 | 1833 |
-3 | 745 |
-2 | 823 |
-1 | 802 |
0 | 825 |
1 | 825 |
2 | 787 |
3 | 758 |
4 | 788 |
5 | 1814 |
一見して、-4 と 5 が他の数値より特異的に多く生成されていることがわかります。区間の両端の値ですね。確かにバグの原因になる可能性は高そうです。
では、範囲を指定しない int
ではどうでしょう? 同じく 10,000 ケース生成して 0 の個数を数えてみると、10,000 個中 424 個が 0 でした。int
は Int
値全体を生成する可能性があるため、424/10000 というのは特異的に多く 0 が生成されていることを予想させます。
もし仮に、intRange
が単純に int
により整数を生成してから -5 以下と 6 以上の数を捨てているとしたら、intRange
の場合でも 0 にピークがあるはずです。このことから、生成される値の「エッジケースらしさ」は Fuzzer によって異なるロジックで判定されていることがわかります。
Generator の実装
この「エッジケースらしさ」を Fuzzer ごとに定義しているのが Generator です。
intRange
の定義を見てみましょう。hi < lo
の部分はエラー処理ですが本筋に関係ないので省略してあります。
intRange : Int -> Int -> Fuzzer Int intRange lo hi = if hi < lo then ... else custom (Random.frequency [ ( 8, Random.int lo hi ) , ( 1, Random.constant lo ) , ( 1, Random.constant hi ) ] ) (Shrink.keepIf (\i -> i >= lo && i <= hi) Shrink.int)
custom
の第一引数に注目してください。Fuzzer 一覧の中に登場した Fuzz.frequency
と紛らわしいですが、ここでは Random.frequency
によって Generator が定義されていることがわかります。
区間の下端 lo
と上端 hi
の間の整数に対して 80%、さらに上下端の値については固定値に 10% の重みが掛けられています。これが、先ほど intRange -4 5
で -4 と 5 が多めになっていた原因です。
同様に int
の実装を確認すると次のようになっています。
int : Fuzzer Int int = let generator = Random.frequency [ ( 3, Random.int -50 50 ) , ( 0.2, Random.constant 0 ) , ( 1, Random.int 0 (Random.maxInt - Random.minInt) ) , ( 1, Random.int (Random.minInt - Random.maxInt) 0 ) ] in custom generator Shrink.int
こちらも同じく、ケースごとの生起確率が定義されています。int
の場合は区間ごとに確率が変えられていて、特に注意すべきケースは 0、また極端な値よりも -50 から 50 までの範囲を重視する、という定義になっています。
Shrinker
反例の発見
それでは二点目の論点に移りましょう。Shrinker について説明するために、まずわざと失敗するテストを書いてみます。
suite : Test suite = describe "String.reverse" [ fuzz Fuzz.string "is identity" <| \randomString -> randomString |> String.reverse |> Expect.equal randomString ]
このテストが判定しているのは「任意の文字列は、反転すると元の文字列に等しい」ですね。当然、回文でない文字列に対してこのテストは失敗します。
elm-test 0.18.12 ---------------- Running 1 test. To reproduce these results, run: elm-test --fuzz 100 --seed 1428851996 ↓ Example ↓ String.reverse ✗ is identity Given "\t\n" "\n\t" ╷ │ Expect.equal ╵ "\t\n" ...
テストの反例として "\t\n"
が見つかりました。これ以外に複数挙げられる反例も 2 文字になっているはずです。
しかし、Generator がランダムに生成した値に対して単純に条件を判定しているとするとこれはやや奇妙です。当然もっと長い(回文でない)文字列も検出されてしかるべきに思えます。
逆に言えば、ドキュメントにうたわれている通り、Fuzzer は何らかの戦略によってテストを失敗させる「最小の例」を見つけていることになります。この戦略を定義しているのが Shrinker です。
Shrinker の役割
Shrinker は別パッケージ eeue56/elm-shrink で定義されています。
type alias Shrinker a = a -> LazyList a
標語的に述べるならば、入力された値を何らかの意味で「縮小」する関数が Shrinker です。複数の縮小結果を候補として考えるため、戻り値は(遅延)リストになっています。
Fuzzer は、次のような考え方で Shrinker 利用してテストが失敗する最小の入力を探します。
- テストが失敗した入力に対して、Shrinker で一段階「縮小」した値の候補の一覧を得る
- 「縮小」した値を新しい入力とし、テストが失敗する限り同じ手順を繰り返す
- 失敗しなくなったひとつ手前の入力が最小の反例
つまり先ほどの回文の例で言えば、最初に生成した(ほぼ確実にテストが失敗する)例から始めて文字列を「縮小」していくと、1 文字まで縮小された時点でテストが成功するようになります。結果として 2 文字の例が「最小の反例」として出力されるわけです。
Shrinker の実装
上では「文字列を縮小する」と簡単に書きましたが、実際の Shrinker は単に文字列の長さを縮めているだけではありません。実際にどのような実装になっているかも確認しておきましょう。以下に挙げたのが Shrink.string
の実装です。
string : Shrinker String string = convert String.fromList String.toList (list character)
convert
は文字列と文字のリストを相互変換するために使用されますが、「縮小」の動作にとって本質的ではありません。構成要素である Shrink.character
と Shrink.list
についてそれぞれ追いかけます。
Shrink.character
まず Char
型に対して定義された Shrinker です。
character : Shrinker Char character = atLeastChar (Char.fromCode 32) atLeastChar : Char -> Shrinker Char atLeastChar char = convert Char.fromCode Char.toCode (atLeastInt (Char.toCode char)) atLeastInt : Int -> Shrinker Int atLeastInt min n = if n < 0 && n >= min then -n ::: Lazy.List.map ((*) -1) (seriesInt 0 -n) else seriesInt (max 0 min) n
定義を追いかけていくと、文字コード n
を持つ文字の「縮小」は、最終的に Int
区間の「縮小」である seriesInt 32 n
に帰着されています。seriesInt
の実装は以下です。
seriesInt : Int -> Int -> LazyList Int seriesInt low high = if low >= high then empty else if low == high - 1 then low ::: empty else let low_ = low + ((high - low) // 2) in low ::: seriesInt low_ high
このロジックに従うと、例えば文字コード 42 の '*'
を「縮小」すると得られる候補は以下のリストであることがわかります。
Char.fromCode 32 ::: Char.fromCode 37 ::: Char.fromCode 39 ::: Char.fromCode 40 ::: Char.fromCode 41 ::: empty
すなわち、テストを失敗させる Char
型の値が発見された場合 Fuzzer は、元の値より文字コードが小さい側の印字可能文字を(元の値に近いほど密に)いくつかピックアップし、それでもテストが失敗するかどうか試す、ということになります。
Shrink.list
次に List a
型に対する Shrinker の実装です。
実際には遅延リストである Lazy.List a
型を経由して定義されていますが、ここではアルゴリズムに対する分かりやすさを優先して通常の List a
で書き直してあります。擬似コードみたいなものだと思ってください。
list : Shrinker a -> Shrinker (List a) list shrink l = let n : Int n = List.length l in List.Extra.andThen (\k -> removes k n l) (List.Extra.takeWhile (\x -> x > 0) (List.Extra.iterate (\n -> n // 2) n)) +++ shrinkOne l shrinkOne : Shrinker a -> List a -> List (List a) shrinkOne shrink l = case l of [] -> [] x :: xs -> List.map (flip (::) xs) (shrink x) ++ List.map ((::) x) (shrinkOne xs) removes : Int -> Int -> Shrinker (List a) removes k n l = if k > n then [] else if List.isEmpty l then [ [] ] else let first = List.take k l rest = List.drop k l in rest :: List.map ((++) first) (removes k (n - k) rest)
ロジックを追っていくと、リストを「縮小」した結果は
shrinkOne
によって得られる、リストの各要素に Shrinker を適用したものremoves
によって得られる、元のリストから一部の要素を除外したもの
のいずれかに由来することがわかります。
具体例で考えましょう。a
型の値 x
、y
、z
があって、あらかじめ与えられた shrink : Shrinker a
によってそれぞれ
shrink x == x1 ::: x2 ::: empty shrink y == y1 ::: y2 ::: y3 empty shrink z == z1 ::: empty
のように「縮小」されるとします。このとき、List a
型の値 [x, y, z]
は新しく組み立てられた list shrinker : Shrinker (List a)
によって
list shrinker [x, y, z] == [] ::: [y, z] ::: [x, z] ::: [x, y] ::: [x1, y, z] ::: [x2, y, z] ::: [x, y1, z] ::: [x, y2, z] ::: [x, y3, z] ::: [x, y, z1] ::: empty
と「縮小」されます。リストの長さもしくは各構成要素のいずれかの意味で、元の値 [x, y, z]
より小さくなっていることがわかります。
まとめ
今回の記事では、elm-test の Fuzz モジュールの実装について簡単にソースコードを挙げながら解説しました。特に
- 小さく単純な Fuzzer を組み立てることでより大きなデータ型や複雑な条件を表現する Fuzzer を構築できる
- Fuzzer は Generator と Shrinker によって構成される
という二点がポイントです。
ところで、つい先日 Elm の v0.19 がリリース されましたね。かなりいろいろな変更が入ったらしく、現在の elm-test はコンパイルできなくなる気がしますが、それはまた別の話。
July Tech Festa 2018 で分散システムの検証について話してきました / #JTF2018
先日行われた July Tech Festa 2018 で、モデル検査を使った分散アルゴリズムの検証について発表してきました。
前半はオートマトンによるシステムの記述と検査の基礎について、後半は三種類のツール SPIN、TLA+、P による記述方法の紹介、といった内容です。
後半のソースコード紹介が散文的な感じになってしまって、いまいちメリットが伝わらない感じだったので、次回があればもっとエモいスライドにしようと思います。
分散アルゴリズムの形式化
定理証明による検証
今回の話の流れとして「分散システムにはモデル検査が有効」と述べていますが、必ずしも定理証明が分散システムの検証に向かないという趣旨ではありません。
例えば、定理証明器 Coq によって分散システムを証明するためのフレームワークとして Verdi が開発されています。
さらに、Coq は実行可能なコードも出力できるので、Coq で Raft 合意アルゴリズムを証明したものから OCaml を出力して作られた「証明済み分散 KVS」も公開されています。
トランザクションコミットの形式化
今回の発表では、分散アルゴリズムの例として、古典的な二相コミット(を単純化したもの)を使用しました。元ネタになっているのは以下の論文で、発表中取りあげた TLA+ による形式化もこれに基づきます。
アブストラクトを読むとわかる通り、実はこの論文は二相コミットに関するものではありません。「トランザクションコミットに Paxos を使用した」というのが趣旨で、二相コミットは単なる引き立て役です。とはいえ今回の発表と無関係というわけでもなく、Paxos を用いたコミットについても TLA+ コードが載っているので、興味がある人は読んでみると面白いでしょう。
各ツールの簡単な紹介
SPIN
今回紹介した中では、おそらくもっともメジャーなツールです。日本語の書籍も出ています。
形式化の特徴
記述には Promela と呼ばれる DSL を使用します。C 言語にチャンネルと非決定性を足したような言語ですが、配列以外のデータ構造のサポートがほとんどないため複雑な処理を書こうとすると辛いことがあります。
チャンネルの送受信はそれぞれ !
と ?
です。pi 計算にルーツを持つ記号ですが、*1今風に言うなら Go 言語をイメージするとわかりやすいでしょう。
非決定性は if .. fi
または do .. od
内のブランチとして記述し、ブランチの先頭の文が実行可能なものの中から非決定的に次の状態が定義されます。例えば
if :: chan_a ! msg -> ... :: chan_b ? msg -> ... fi
と書くと、この if
節全体として chan_a
への送信または chan_b
からの受信のうちその状態において可能なもの(両方なら非決定的)が選択されます。
ちなみに発表中でも述べましたが、SPIN のチャンネルは完全な FIFO です。もちろんこれはこれで便利なのですが、表現しづらい状況もあって、例えば今回の例で使用した「Transaction Manager から Resource Manager 全体に Commit 命令をブロードキャスト」はとても書きにくい例です。
「ブロードキャスト用のキュー」を用意すると最初の RM が受信した時点でメッセージがキューから消えてしまい他の RM が読めなくなります。「受信できるかどうか確認だけする文」もありますが、これを使うと逆にチャンネル内に残ったメッセージを処理する方法に困ります。さらに、システムが停止したタイミングで中身が残ったチャンネルがあると、SPIN は一種のデッドロックであると考えエラーを報告します。
困った末、今回は各 RM 宛に一つづつチャンネルを用意するという形になりました。
検査の特徴
特定のプロセスの特定の箇所における条件を記述するために assert
文が使えます。通常のプログラム言語と同じように使ってももちろん機能しますが、SPIN の場合はその並列性を生かして「条件を監視するだけのプロセス」を用意しておくという tips が使えます。
byte counter = 0; proctype Incrementer { do :: counter = counter + 1; od } proctype Monitor { do :: assert(counter < 2) od }
上のシステムの実行パスの中には、例えば次のような実行パスがエラーとして含まれます。
Incrementer
が遷移してcounter
を 0 から 1 へ- もう一度
Incrementer
が遷移してcounter
を 1 から 2 へ Monitor
が遷移してassert
文を踏む
Incrementer
と Monitor
は実際には積オートマトンとして検査されるため、任意のタイミングの組み合わせについて、つまり Incrementer
が n 回続けて遷移した後に Monitor
が遷移するパターンはすべて検査されます。要するに「他のプロセスがどんな動き方をしても常に counter < 2
」という大域的な条件が検査できるわけです。
また LTL による検査も可能です。この場合は定義の中に直接書き込むのではなく、外部ファイルとして準備して実行時にオプションで与えます。その他、詳しくは以前に開催した勉強会の資料を参照してください。
TLA+
AWS 内で S3 や DynamoDB の検証に採用されたことで有名なツールです。
GUI サポート (TLA Toolbox) が充実している他、マニュアルやチュートリアルの類も公開されているので始めるための敷居は割と低いです。とりあえず雰囲気を掴みたいなら ビデオチュートリアル を眺めてみるのもよいでしょう。"These videos are not light entertainment." という脅し文句が太字で書かれていますが、言うほど難しくはありませんし、スクリプトも付いています。
形式化の特徴
生のままの TLA+ では、システムの初期状態と遷移を直接記述します。スライド中のサンプルよりもっと簡単な例で見たほうが分かりやすいでしょう。
VARIABLE b Init == /\ b = TRUE Next == b' = ~b
1 ステップごとに真偽値を反転させるだけのシステムです。b'
は b
の遷移先での値を表します。検査についてはこの後で述べますが、この Init
を初期状態、Next
を遷移関係として指定して検査させることになります。
プロセスについては陽には現れません。複数のプロセスが存在する場合、ナイーブにはそれらすべてを状態については /\
で、遷移については \/
でそれぞれ繋いで人間が積オートマトンを書くことになります。例えばこの真偽値反転システムが二つ非同期で動いているとしたら以下のようになります。
VARIABLES b1, b2 Init == /\ b1 = TRUE /\ b2 = TRUE Next == \/ b1' = ~b1 \/ b2' = ~b2
今回の発表で触れたのはここまでですが、実際にシステムを表現しようとすると、人間が明示的に各ステップを状態遷移に書き換える必要があるため非常に大変です。
この問題を解決するユーティリティとして、TLA+ では +CAL あるいは PlusCal と呼ばれるプログラミング言語チックな DSL も用意していて、ブロックコメント内に +CAL を記述すると、自動的に TLA+ の記法に変換されるようになっています。まずは単純な例から。
--algorithm SingleOscillator { variable b = TRUE; { while (TRUE) { b := ~b; } } }
ここから生成される TLA+ の仕様は以下のようになります。
VARIABLE b vars == << b >> Init == (* Global variables *) /\ b = TRUE Next == b' = ~b Spec == Init /\ [][Next]_vars
手書きの場合とおおむね同じような出力になりました。最後の Spec
は検査に使用する LTL 式ですが、後ほど説明します。
さらに、複数プロセスがある場合の +CAL 記述は次のようになります。
--algorithm MultiOscillator { process (oscillator \in {0, 1, 2}) variable b = TRUE; { start:while (TRUE) { b := ~b; } } }
新しい要素として、ラベル start
が導入されました。ラベルはブレイクポイントのように働き、不可分実行される単位を決めます。
生成される TLA+ 仕様は以下です。ハイライトがないとちょっと見づらいですね。
VARIABLE b vars == << b >> ProcSet == ({0, 1, 2}) Init == (* Process oscillator *) /\ b = [self \in {0, 1, 2} |-> TRUE] oscillator(self) == b' = [b EXCEPT ![self] = ~b[self]] Next == (\E self \in {0, 1, 2}: oscillator(self)) Spec == Init /\ [][Next]_vars
先ほどと違うのは、変数 b
が単なる TRUE
から [self \in {0, 1, 2} |-> TRUE]
、すなわちプロセスの識別子を取って TRUE
を返す関数に変わっていることです。これに伴って遷移条件 Next
もパラメータを導入した形に変わっています。\E
は存在量化子なので、遷移の条件は「プロセス 0, 1, 2 のいずれか一つについて遷移 occillator
が発生」と読むことができます。
検査の特徴
TLA+ でも、検査すべき性質として常に成立する条件 (Invariant) もしくは LTL による指定 (property) が可能です。
また、システムの遷移として Init
と Next
をナイーブに与える代わりに、LTL 式を指定することもできます。上で登場している
Spec == Init /\ [][Next]_vars
という記述がそれです。_vars
の部分は状態として含める変数の集合を指定しますが、特に意図がない限り VARIABLES
に定義したものをすべて入れておけば大丈夫です。
さらに、WF_vars(A)
と SF_vars(A)
という記法があらかじめ用意されています。前者は論理式 A
についての弱い公平性、後者は強い公平性をそれぞれ表現していて、公平性自体を検査対象にしたり、あるいは公平性を仮定して別の性質を検証できます。
P
Microsoft Research によるツールです。ちなみに同じチームから .NET 用のフレームワーク P# もリリースされています。
実行可能コードが出力できることを売り文句にしていて、MS Research の公式ブログでも SPIN や TLA+ に対して名指しで優位性を主張しています。SPIN はともかく TLA+ の開発者はかの Lamport 先生で、MS Research 所属なんですけども。
形式化の特徴
P による記述は、他の二つのツールより明らかに複雑です。各プロセス(P では machine と呼ばれます)の定義は、state とその state で反応すべき event、反応の内容を列挙する記述が基本になります。
machine Server { start state WaitPing { on PING goto SendPong; } state SendPong { entry (payload: machine) { send payload, PONG; raise SUCCESS; } on SUCCESS goto WaitPing; } }
上記のコードで定義された machine は以下のようなリアクティブな挙動をします。
- 初期状態は
WaitPing
PING
イベントを受信すると状態SendPong
に遷移payload
に格納されたクライアントの PID 宛にPONG
イベントを送り返し、かつ自分自身にSUCCESS
を発行- 状態
WaitPing
に遷移して次のイベントを待機
プロセスと独立にチャンネルが存在する SPIN とは異なり、メッセージの受信は 各 machine が所持している自分用の入力キューを介して行われます。送信側にキューはなく、送信したメッセージは即座に相手の入力キューに積まれます。
コード中に state
という予約語が出てきますが、紛らわしいことに、この state は実はオートマトンとしての状態とは必ずしも対応しません。というのも、P では「state を push/pop する」という操作があり、実際にオートマトンとしての状態に相当するのは state がスタックされたものになっているからです。新しい state が push されると、スタックの下側にある state に由来するハンドラは上書きされます。次に挙げたのはやや人工的な例です。
machine Server { start stat Init { entry { ... raise UNIT; } on TIMEOUT do {...} on UNIT push WaitPing; } start state WaitPing { on PING goto SendPong; } }
このとき、state Init
の上に state WaitPing
が積まれた状態になり、WaitPing
にいる間も Init
で定義された TIMEOUT
に対するハンドラが継承されます。
なお、イベントに対して処理を定義する以外にも、特定のイベントが発生した際にメッセージをデキューだけして捨てる ignore
、およびデキュー自体をブロックする deferred
が存在します。
検査の特徴
P では、検査したい条件も他の machine と同様、イベントハンドリングを用いて定義する必要があります。大域的な条件を検査するための記述は、例えば次のようなものです。
spec Safety observes PONG {
on PONG do (payload: machine) {
assert (...);
}
}
上のように spec
と observes
を定義すると、指定したイベント(ここでは PONG
)がシステム全体のどこかで発生したときは常にキャプチャされるようになり、内部に記述した assert
文の成立をチェックすることができます。ちょうど SPIN で「監視専用のプロセス」を定義したのと同じような仕組みです。
残念なことに、P は LTL による検査を直接にはサポートしません。その代わり、state に cold
および hot
のラベルを付けることが可能になっています。検査の際には、そのシステムの任意の実行パスが
cold
状態を無限回通過するかどうかhot
状態を無限回通過しないかどうか
が検査され、この二つを組み合わせることで LTL に相当する検査を行うことができます。
実は、SPIN ではこれに相当するプロセス (never claim) を処理系が生成してくれているのですが、このあたりをきちんと述べるには、スライドにも名前だけ出てきた Büchi オートマトンに関する説明が必要です。長くなりそうなのでまた記事を改めて解説したいと思います。
まとめ
この記事では、July Tech Festa 2018 での発表スライドを補足する形で、SPIN、TLA+、P のそれぞれについて簡単に紹介しました。ただ、ツールの特徴というか、書き心地みたいなものは実際に触ってみないとわからない部分も大きいので、もし今回の発表でモデル検査に興味を持った方はインストールして動かしてみて頂ければ幸いです。
ところで、ここまで説明しておいてなんですが、個人的には本当の初心者にまず薦めたいモデル検査ツールは Alloy なんですよね。近々 Alloy の初心者向けハンズオンを開催しようという腹案も温めていますが、それはまた別の話。
*1:2018/08/01 勘違いだったので撤回
We Are JavaScripters! @19th で Haskell 製フレームワーク Miso について話してきました
先日行われた We Are JavaScripters! @19th で Haskell によるフロントエンド開発について発表してきました。
Elm の代わりにフレームワーク Miso を使うことで、クライアントサイドとサーバサイドの両方を Haskell で実装することができる、という内容です。
なお今回のプレゼンでは、参加者のほとんどは Haskell に馴染みがないだろう*1ということもあって、実装上の詳細にはほとんど触れませんでした。
Elm と Miso の詳しい比較、さらに Servant と組み合わせた Isomorphic なアプリの作り方については、記事を改めて解説する予定です。特に現在、よく知られた Elm のチュートリアルを Miso で書き直している のですが、それはまた別の話。
*1:実際、Elm ですら聞いたことない人は結構いました。
JAWS DAYS 2018 で形式手法による IAM の検証について話してきました
だいぶ日が空いてしまって今更ですが、先日行われた JAWS DAYS 2018 で登壇してきました*1。モデル検査器 Alloy を使って AWS の IAM を検証してみるという内容です。
形式手法 × AWS というテーマではこれまでにもいくつかのイベントで発表していますが、題材はネットワーク関連の検証がメインでした。
さすがに同じことばかり話していても芸がないので、今回は新ネタとして IAM を投入してみました。CFP も Security Slot で採択されています。
現状と既存手法の限界
IAM 設定の難しさ
いや、説明するまでもなく実際ややこしいですよね。一つ一つはさほど複雑ではないんですが、多数の設定項目が互いに影響し合うため最終的な影響を把握するのに神経を使います。
一例を挙げると、IAM には NotAction という記述方法があって、指定した「以外」のアクションについて制御をかけることができます。しかし「Action を指定して Allow」と「NotAction を指定して Deny」は字面は似ていても最終的に表れる効果が違っていたりして、しかもそんな設定が複数重複して作用するとなるとどう考えても混乱のもとです。会場で聞いた感じでも、完璧に活用されている現場はさほど多くないようでした。
それでも、日々の固定されたフローを回すだけなら何とかなります。問題はインフラの構成や運用をドラスティックに追加・変更する必要があるときです。既存のインフラに影響を与えないようにして新しい要素を導入しようとすると、ちょっと考えたくない程度に複雑になるというのは、経験者の皆様には同意して頂けるでしょう。
特にセキュリティ系は設定ミスが直接リアルなダメージにつながるため、他の部分より余計に気を使わざるを得ません。
Policy Simulator
さて、この複雑性を何とかするためのツールとして、既に公式から IAM Policy Simulator が提供されています。
リンク先を見てもらえばわかる通り、このツールは割とよくできていて、IAM のポリシが最終的にどういう影響を与えるか、実際に運用中の設定に影響を与えないよう確認することができるようになっています。
しかしこの Policy Simulator も完璧ではありません。特にここで指摘したいのは以下の 3 点です。
論理的な不整合が検出できない
Simulator が返してくるのは「指定したリソースに対して最終的にアクションが許可されるか否か」です。したがって、設定が論理的に矛盾していて無駄があるとき、より具体的には例えば
- あるポリシに複数のステートメントが設定されていて、同じリソースに対してそれぞれが Allow と Deny を指定している
- あるロールに複数のポリシが指定されていて、個々のポリシは問題なくてもポリシ間で矛盾している
といった状況では、Simulator は単に Deny を返すだけで矛盾を指摘することはできません。
一方、このような設定は少なくとも設計者が意図したものではないでしょう。ポリシやロールの数が少ないうちは明らかにおかしいことに気付くことができますが、運用が長期化するに従って複雑化、やがて既存の設定に手が付けられなくなりカオス化の原因になります。
仕様から設定を得ることができない
Simulator では「こう変えたら結果がどうなる」は確認できますが、逆ができません。つまり、アクセス制御の要件があるときにそれをどうやったら実現できるかは試行錯誤が必要で、結局のところ個人の経験とカンに基づいた作業になります。
これも問題になるのは既にある程度の規模で運用されている設定が多数あるときで、新しい要素を導入しようとすると、あっちを変えるとこっちが壊れる、みたいなループに陥って非常に疲れます。もうちょっとシステマティックに解決する方法が欲しいところです。
IAM 以外の要素を考慮できない
Simulator はあくまでも「IAM ポリシの評価器」なので、当然ですが IAM 以外の要素まで含めて確認することができません。
しかし実際のインフラ設計は IAM だけで完結するわけではなく、
- このインスタンスは他の VPC にいるので直接通信できない
- S3 へのアクセス経路がインタネット経由とエンドポイント経由の 2 種類ある
- 他システムとの連携の都合で CIDR によって通信の許可・不許可を切り替える必要がある
みたいな条件について(システムの本質か、あるいは政治的な妥協かはおいといて)考えざるを得なくなる場合は少なからず発生します。
今回の提案手法
このような、人間が直接整合性を把握するには困難な対象を扱う場合、形式手法、特にモデル検査が有効な手段になり得ます。
Alloy 以外のモデル検査器だと、SPIN/Promela や TLA+ が有名です。しかしこの両者はオートマトンをベースにしていて、(特に分散)アルゴリズムを検証する目的には便利ですが、今回のような設定の整合性の検証には向きません。
これに対して Alloy では関係論理を用いてモデルを記述するため、IAM の評価ルールをずっと自然な形でモデル化することが可能です。
Alloy による検証のメリット
Policy Simulator の不足点として上に挙げた 3 つのそれぞれに対して、Alloy を用いた検証は以下のようなアドバンテージを持ちます。
矛盾した設定の検出
モデル検査器の用途そのものです。Alloy では aseert
で守られるべき条件記述して check
で検査すると、自動的に全探索が行われて条件に違反する例を列挙・図示してくれます。
プレゼン中では「同じリソースに対して Allow と Deny が同時に指定されない」という条件を検査するサンプルを挙げました。
仕様からの設定の導出
Alloy に特徴的な機能ですが、pred
で欲しい条件を記述して run
で検査すると、assert
とは逆にその条件を満たす具体例を出力してきます。Alloy が「モデル発見器 (model finder)」とも呼ばれる所以です。
実は内部的な仕組みは assert
と共通していて、pred
で指定された条件の否定を検査することで、もし具体例が存在すれば反例として検出されるようになっています。
プレゼン中では、同じ仕様に対して設定を自動的に探索させ、「Action を指定して Allow する」「NotAction を指定して Deny する」という二つのパターンを人の手に依らず発見するサンプルを挙げました。
IAM 以外の条件の記述
Alloy は簡単なモジュールシステムを持っていて、モデルを分割して記述・再利用することができます。
プレゼン中ではこれを利用して、
- IAM ポリシの評価ロジック
- S3 関連のリソース
- EC2 関連のリソース
を別々に記述する方法をサンプルとして挙げました。
関連研究
というほど仰々しい話ではないのですが、IAM ポリシを形式手法を用いて検証する、という論文が見つかったので参考までに読んでみました。
- Zahoor E., Asma Z., Perrin O. (2017) A Formal Approach for the Verification of AWS IAM Access Control Policies. In: De Paoli F., Schulte S., Broch Johnsen E. (eds) Service-Oriented and Cloud Computing. ESOCC 2017. Lecture Notes in Computer Science, vol 10465. Springer, Cham
論文の内容は、IAM の設定をイベント計算にエンコードして Discrete Event Calculus Reasoner というツールで検証する、というものです。Alloy との直接的な関係は薄いですが、モデル検査のバックエンドとして SAT ソルバを使用するという点は Alloy と共通しています。こう言ってはなんですが、単なる「やってみた」系の論文で新規性には乏しそうです。
もっと一般の Role Based Access Control (RBAC) あるいは Attribute-Based Access Control (ABAC) について形式化する研究は他にも多数見つかりますが、IAM に特化した論文は(当然、研究としての意義が薄いという意味でも)あまりないようです。
まとめ
以上、AWS の IAM 設定について、既存の Policy Simulator がカバーできない部分を Alloy で検証する、という内容をお話ししました。スライド中にはサンプルコードも挙げてあるので、このブログと合わせて読んでもらえればおおむね当日話した情報量と同程度になるかと思います。
ちなみに上に挙げた論点の内、モジュール化の部分は割と非自明です。いくつか方法は考えられるのですが、普通に書こうとするとロジックの重複が排除できずモジュール化の恩恵が得られないことがわかります。
このモジュール化の工夫についてはいずれ記事を改めて解説したいと思っていますが、それはまた別の話。
*1:所属がいつもの「ProofCafe」ではなく「非公開」になっているのは、単に連絡に行き違いがあったためです。
Kubernetes Meetup Tokyo #10 で Pod の Preemption について話してきました
だいぶ日が空いてしまって今更ですが、先日行われた Kubernetes Meetup Tokyo #10 で、v1.8*1 から導入された新機能 Preemption について発表してきました。
Preemption は、Kubernetes クラスタのリソースが不足した際に、優先度が低い Pod を追い出して優先度が高い Pod の稼働を保証する仕組みです。
当日は時間が不足気味だったので、説明不十分だったかなと思われる点についていくつか補足しておきます。
Priority の指定について
スライド中では詳しく説明しませんでしたが、ユーザは直接 Pod(や Deployment 中の Pod Template)に対して Priority を指定するのではなく、
- Priority の値を保持する PriorityClass を作成する
- Pod Template には priorityClassName を指定する
という手続きを踏むことになります。Persistent Volume を使用する際あらかじめ StorageClass を作成しておくのに似ていますね。
なお、Pod の Priority が確定するのはその Pod が作成されるタイミング(のみ)である、という点には若干注意が必要です。 Pod 作成時に Admission Control が Pod に指定された priorityClassName を確認して、 PriorityClass から Priority の値を取得し、その値を Pod の status に書き込みます。実際の Preemption に際して Scheduler が参照するのは priorityClassName ではなく、status に書き込まれた値の方です。
このことから、以下の挙動が従います。
- API Server に対して明示的に Admission Control を有効化する必要があり、したがって MiniKube ではそもそも実験ができなかったりする
- Priority 指定なしで起動した Pod は、後からデフォルトの PriorityClass を作成しても反映されず Priority が 0 の扱いになる
- 逆に、PriorityClass を削除した後も Pod に設定された Priority は有効のまま残り続ける
仕組みを理解していれば納得できる話ではありますが、やや混乱しがちなのでもし実践投入する場合は気を付けましょう。
配置待ち Pod のキューについて
スライド中では適当な図でごまかしていますが、今回の Priority/Preemption 導入に伴って、配置待ち(Pending 状態)の Pod が登録されるキューの実装が変更されています。
- Priority 導入のために、文字通りキューが優先度付きキューになった
- 「まだ配置可能かどうかの判定がされていない Pod」と「一度 Preemption の可能性を含めて判定したが配置不能だった Pod」が区別されるようになった
機能としての Preemption を使う立場からすると中身を知らなくても取り立てて困ることはないですが、スライド中の図がミスリーディングだった気がするのでここで補足しておきます。
Affinity との兼ね合いについて
スライドでも説明している通り、Preemption のアルゴリズムは
- 判定対象 Node 上にある Pod の内、配置したい Pod より Priority が低いものをすべて追い出したと仮定して配置可能かどうか確認
- 配置できる場合は、一度追い出したと仮定した Pod を戻せるところまで戻してみて、最終的に追い出しの影響が一番少なく済む Node を選択
という 2 ステップで行われます。
このアルゴリズムの特性として、Pod 間の Affinity もしくは Anti-Affinity が指定されている場合、Preemption のアルゴリズムが上手く機能しない可能性があります。大きく分けて次の二つのパターンです。
Affinity による影響
配置したい Pod X と、今 Node 上にいる Pod Y の間に Affinity が指定されているパターンです。
このとき、もし Y の Priority が X より低いと、最初のステップで Y が追い出された状態で判定が行われるため、実際には X と Y が同居できるだけのリソースがあっても配置できないと判定されてしまいます。
プロポーザルを読むと、この可能性は考慮されていて、しかしなお
- すべての Pod 間の関係について考慮すると組み合わせ爆発でパフォーマンスが落ちる
- 組み合わせ爆発を防ぐために調べる組み合わせを制限すると、ユーザから見て挙動が理解しづらくなる
- Affinity が指定されているならば、その相手はより必要性の高い(= Priority が高い)Pod のはずで、このパターンは現実には発生しにくい
という理由から特に対策は取らない、という選択がなされたようです。
Anti-Affinity による影響
Node を N 上に Pod X が配置できるかどうか判定するとしましょう。N と同じ障害ドメイン内に Node N' があって、その N' 上で Pod Y がいるとします。
このとき、もし Pod X と Pod Y の間に Anti Affinity が指定されていると、Preemption の「仮想追い出し判定」は Node ごとに行われるため、N 上の Pod をすべて追い出したと仮定しても N' 上の Y が邪魔で X が配置できません。
こちらの問題もプロポーザルで指摘されているのですが、残念ながら「いい方法が見つからないので特に対策せず」という消極的な結論になっています。
まとめ
Kubernetes v1.9 から導入された Pod の Priority 指定および Preemption の仕組みについて補足しました。簡単ですがこれ以上遅くなってもまた放置するだけになりそうなのでこの記事はこれで一度公開します。
本当は、ソースコードを追いながら Preemption のアルゴリズムを説明する記事を書こうと思った(そして実際途中まで書いてある)のですが、それはまた別の話。
参考文献
猫でもわかる rkt + Kubernetes
このエントリは Kubernetes Advent Calendar 2017 の 23 日目の記事です。ちなみに昨日は takezaki さんの「GCBを利用したContinuous Delivery環境」でした。
LT で使用したスライド
先日、市ヶ谷Geek★Night #16 の 10 分 LT 枠で、CoreOS 社によるコンテナ実装 rkt とその Kubernetes 連携について発表してきました。今回のエントリはこの LT の内容を補足しつつ、実際に手を動かして rkt を試せるような構成にしてあります。
Hello, rkt!
rkt は、Docker の対抗馬として CoreOS によって開発されたコンテナ管理ツールです。プロジェクトの初期は普通に Rocket という名前でコマンド名が rkt
という扱いでしたが、途中からツールの名前自体が rkt に変更されました。
現在は Cloud Native Computing Foundation (CNCF) にプロジェクトごと寄贈されていますが、メンテナ を確認すると 11 人中 8 人が CoreOS 所属で、実際には依然として CoreOS が中心となっているようです。ちなみに残りの 3 人は Kinvolk 社 所属で、後で登場する rktlet の開発元でもあります。
rkt のインストール
Go で作られたツールの常として、rkt もインストールは簡単です。
Linux の場合、各ディストリビューション向けのパッケージ配布もされていますが、触ってみるだけであれば直接バイナリをダウンロードすればすぐ試せます。
この記事の後半で rkt app
コマンドを使用するためには現時点の最新版である v1.29.0
が必要なのでそこだけ注意してください。
$ wget https://github.com/rkt/rkt/releases/download/v1.29.0/rkt-v1.29.0.tar.gz $ tar xzvf rkt-v1.29.0.tar.gz $ sudo mv rkt-v1.29.0/rkt /usr/local/bin/rkt $ rkt version rkt Version: 1.29.0 appc Version: 0.8.11 Go Version: go1.8.3 Go OS/Arch: linux/amd64 Features: -TPM +SDJOURNAL
残念ながら rkt は Linux 専用です。rkt のレポジトリが Vagrantfile を提供しているので、Mac や Windows の人はこれで VM を立ち上げれば大丈夫です。
git clone https://github.com/rkt/rkt cd rkt vagrant up
特徴その1:デーモンが存在しない
Docker の場合、docker
コマンドを使い始める前に Docker Engine をサービスとして登録・起動する作業(実際にはパッケージマネージャがやってくれると思いますが)が必要です。
rkt の場合 Docker Engine に相当するコンポーネントがないため、ダウンロードしたバイナリだけでツールとして完結しています。 実際にちょっと触ってみましょう。
Docker と少しだけ異なる点として、rkt ではイメージに署名が付けられています。信頼した公開鍵は /etc/rkt/trustedkeys
以下に記録されています。
$ sudo rkt trust --prefix coreos.com/etcd ... $ tree /etc/rkt/trustedkeys/ /etc/rkt/trustedkeys/ └── prefix.d └── coreos.com └── etcd ├── 18ad5014c99ef7e3ba5f6ce950bdd3e0fc8a365e └── 8b86de38890ddb7291867b025210bd8888182190
あとの操作は Docker とほぼ同じです。イメージをダウンロードしてからコンテナを立ち上げて消すまでの一連の流れを試してみましょう。
$ sudo rkt fetch coreos.com/etcd:v3.1.7 ... image: signature verified: CoreOS Application Signing Key <security@coreos.com> ... $ sudo rkt image list ID NAME SIZE IMPORT TIME LAST USED sha512-e7a54697d04d coreos.com/etcd:v3.1.7 58MiB 43 seconds ago 43 seconds ago $ sudo rkt run coreos.com/etcd:v3.1.7 (別ターミナルで) $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS a79a0bd6 etcd coreos.com/etcd:v3.1.7 running 1 minute ago 1 minute ago default:ip4=172.16.28.2 $ sudo rkt stop a79a0bd6 "a79a0bd6-4260-479d-993d-08f032781007" $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS a79a0bd6 etcd coreos.com/etcd:v3.1.7 exited 12 minutes ago 12 minutes ago $ sudo rkt rm a79a0bd6 "a79a0bd6-4260-479d-993d-08f032781007" $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS
Docker Hub にホストされているイメージを立ち上げることも可能で、イメージの指定は docker://IMAGE:TAG
という形式になります。この場合は署名の検証ができないので --insecure-options=image
を付けます。
$ sudo rkt run --insecure-options=image docker://redis:4.0.6 $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS 2df6d5ee redis registry-1.docker.io/library/redis:4.0.6 running 11 seconds ago 11 seconds ago default:ip4=172.16.28.2 (以下同様)
特徴その2:Pod が最初からサポートされている
もう一つ、Docker に対する rkt の特徴として挙げられるのは Pod のサポートです。上の例ではコンテナが一つしかないのではっきりとわかりませんが、実は UUID
はコンテナではなく Pod に対して振られています。
あまり意味のある組み合わせではありませんが、先ほど fetch
した etcd
と redis
を同じ Pod 内で起動させてみましょう。
$ sudo rkt run coreos.com/etcd:v3.1.7 docker://redis:4.0.6 (別ターミナルで) $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS 1f752f5c etcd coreos.com/etcd:v3.1.7 running 8 seconds ago 8 seconds ago default:ip4=172.16.28.2 redis registry-1.docker.io/library/redis:4.0.6
Pod 1f752f5c
の内部で etcd
と redis
が立ち上がっている様子がわかります。
この二つのコンテナは、systemd の機能によって他から隔離されています。例えば以下のように ip netns list
コマンドを実行してみましょう。Pod に対応する network namespace が作成されているのがわかるはずです。また、Pod を rm
すると namespace も消えます。
$ ip netns list cni-e0f06652-1a94-2cfd-3ccc-c684c473992f (id: 1) $ sudo rkt stop 1f752f5c "1f752f5c-6046-4458-8105-832227a07cfa" $ sudo rkt rm 1f752f5c "1f752f5c-6046-4458-8105-832227a07cfa" $ ip netns list (出力なし)
さて、ここでもう一度イメージの一覧を表示してみましょう。
$ sudo rkt image list ID NAME SIZE IMPORT TIME LAST USED sha512-e7a54697d04d coreos.com/etcd:v3.1.7 58MiB 1 hour ago 1 hour ago sha512-e50b77423452 coreos.com/rkt/stage1-coreos:1.29.0 211MiB 1 hour ago 1 hour ago sha512-eb03c7ec1861 registry-1.docker.io/library/redis:4.0.6 204MiB 1 hour ago 1 hour ago
立ち上げた覚えのないイメージ coreos.com/rkt/stage1-coreos:1.29.0
がいつの間にか fetch
されていますね。このイメージこそ、rkt がネイティブで Pod をサポートできる仕掛けです。
rkt のアーキテクチャでは、コンポーネントは三つの役割に階層化されています。先ほど rkt
コマンドを操作した際は目立ちませんでしたが、ユーザの操作とアプリケーションコンテナの起動の間に Stage1 が入っているのがポイントです。Stage1 は Pod の実装を提供し、Pod 内のコンテナを他のプロセスから隔離します。
- Stage0:ユーザと直接やりとりする
- Stage1:Pod の実装を提供する。Stage0 から呼び出される
- Stage2:コンテナ化されたアプリケーション本体。Stage1 から呼び出される
ここで面白いのは、Stage1 を切り替えることで、Pod ごとに隔離レベルを変えられる点です。rkt は以下の三つの実装を公式に提供しています 。
- stage1-coreos:デフォルトの設定。systemd の namespace および cgroup を使用して隔離する
- stage1-fly:より隔離レベルが低い設定。chroot でファイルシステムのみを切り替え、namespace は隔離しない
- stage1-kvm:より隔離レベルが高い設定。KVM を使用して Pod ごとに仮想マシンを作成し隔離する
使用する Stage1 の実装は、--stage1-name
オプションで指定することができます。試しに fly による Pod 作成を試してみましょう。
fly による Pod を作成する場合、イメージ側で定義された volume
に対して自動的にマウントポイントをつくる仕組みがうまく動作しないようです。ここでは --volume
オプションで明示的に指定して起動させました。
$ sudo mkdir /mnt/etcd-data $ sudo rkt run --stage1-name=coreos.com/rkt/stage1-fly:1.29.0 --volume data-dir,kind=host,source=/mnt/etcd-data coreos.com/etcd:v3.1.7 (別ターミナルで) $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS 307f689f etcd coreos.com/etcd:v3.1.7 running 16 seconds ago 16 seconds ago
先ほどの場合と異なり、NETWORK
欄が空のままになっていることに注目しましょう。これは network namespace が隔離されていないことによるもので、実際、Pod が running の状態にもかかわらず ip netns list
コマンドを実行しても何も返ってきません。
Container Runtime Interface
rktnetes
さて、ここまで見てきたように、rkt には次のような特徴がありました。
- Docker と違ってデーモンがなく、Linux 付属の systemd を使用
- 複数のコンテナを Pod としてまとめて隔離する仕組みを持っている
これらの性質を見ると、いかにも Kubernetes(あるいはそれ以外のオーケストレータも)との相性が良さそうに見えます。
実際、rkt 側はもちろん Kubernetes 自身もそう考えていたようで、Kubernetes v1.3、Docker 以外の初のコンテナランタイムとして rkt 連携がサポートされました。時系列としては 2016 年 7 月のことです。
この rkt 連携機能は rktnetes と通称されていました。当時の Kubernetes 公式ブログ の表現を引用しましょう。
rktnetes is about more than just rkt. It’s also about refining and exercising Kubernetes interfaces, and paving the way for other modular runtimes in the future.
すなわち、rktnetes は Kubernetes とコンテナランタイムとの間のインターフェースを設計する上での先行事例として位置づけられていたことがわかります。
しかしその目的に反して、実装の中身はかなり乱暴です。Kubernetes のレポジトリ内、kubernetes/pkg/kubelet/rkt
にある ソースコード を見ると、インタフェースを作ったというよりは、rkt のデータ構造や動作を Kubelet 側でも実装した、と表現したほうが近いように見えます。
CRI の登場
Kubernetes v1.5 でまた別の動きが現れます。Container Runtime Interface (CRI) の策定です。
CRI が定義する API は .proto
ファイル の形で提供されており、大きく分けて二つの gRPC サービスからできています。
前者のイメージの操作については、それぞれ CRI に対応するコマンドが rkt 側にももともと存在するので大きな障害にはなりません。
問題は後者のコンテナ操作です。CRI には
- Pod を作成する
- Pod 内にコンテナを作成する
- コンテナを起動する
といった逐次実行命令型のインタフェースが規定されています。しかし rkt の Pod は 基本的に起動後に状態を変更することができない、いわゆる immutable なつくりになっていて、そのままでは Pod の作成とコンテナの追加を独立して行うことができません。
CRI の策定に当たって Pod レベルの宣言的なインタフェースを避けた理由は、初期段階のプロポーザル で触れられています。
- すべてのランタイムが Pod をネイティブサポートしているとは限らず、対応負荷が大きくなるため
- インタフェースが抽象的すぎると、再起動や LifecycteHook のロジックを各ランタイム側で実装することになり重複が生じるため
- 開発速度の速さから、Pod の設定項目はすぐ変化する可能性があるため
後者二つはともかく、最初の要件は rkt 側からすれば完全に梯子を外された形です。
ちなみに、もちろん Docker はいち早く CRI に反応しました。それまで Kubernetes が Docker を呼び出すコードは kubernetes/pkg/kubelet/dockerutils
にありましたが、新たに CRI 対応版である kubernetes/pkg/kubelet/dockershim
が開発され、半年後である v1.7 の段階 では移行が完全に完了してdockerutils
は姿を消しています。
一方 rkt はと言えば、実は Docker 同じように v1.5 の段階ですでに rktshim
が 作成されて います。しかし中身を覗いてみると実装はなく単に panic
が呼ばれるだけのスタブになっており、さらに残念なことに最新版 v1.9 になってもやはり 実装はされない まま放置されています。
rkt app サブコマンドと rktlet
さて、rkt もここで Kubernetes 連携を諦めたわけではありません。放置されている rktshim
に代わって、新しいプロジェクト rktlet の開発が進められています。rktlet は Kubernetes Incubator プロジェクト の中の一つであり、中心となっているメンバは rkt のメンテナの件で言及した Kinvolk 社です。
rktlet では、以下の二つの変更によって CRI 対応を実現しようとしています。
まず、rkt そのものに手を入れることで、CRI に対応するために新たにPod に対して mutable な操作を行う rkt app
サブコマンドが追加されました。
さらに、デーモンを持たないという哲学は妥協して、rktlet がデーモンとして起動し gRPC を待ち受ける仕組みになりました。ただしコンテナ操作のロジックをデーモンに持たせることはせず、あくまでも rkt を外部コマンドとして呼びます。
実際に触って試してみましょう。とはいえ Kubelet から呼ばれている最中の様子を確認するのは原理的に難しいので、まず手で rkt app
コマンドを実行してみて、それから実際の Kubernetes との連携に進みます。
rkt app サブコマンド
rkt app
サブコマンドを使用することで、もともと rkt ではできなかった Pod の mutable な操作が可能になります。
最新版の v1.29.0 でもまだ開発中のステータスなので、コマンド実行時には環境変数 RKT_EXPERIMENT_APP=true
を指定しましょう。
まず空の Pod の作成です。CRI の RunPodSandbox
に相当する操作です。
$ sudo RKT_EXPERIMENT_APP=true rkt app sandbox (別ターミナルで) $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS c77b3f3b - - running 1 minute ago 1 minute ago default:ip4=172.16.28.2 $ ip netns list cni-a08f779f-ce1e-771b-b174-20ba662e6b7e (id: 0)
今までと異なり、APP
に何も登録されていない Pod が作られました。しかし NETWORK
欄や ip netns list
コマンドの結果を見ると、この段階ですでに namespace が先に作成されているのがわかります。
次に、この Pod の中にコンテナを追加してみます。CRI の CreateContainer
+ StartContainer
に相当します。
$ sudo RKT_EXPERIMENT_APP=true rkt app add c77b3f3b coreos.com/etcd:v3.1.7 $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS c77b3f3b etcd coreos.com/etcd:v3.1.7 running 7 minute ago 7 minute ago default:ip4=172.16.28.2 $ sudo RKT_EXPERIMENT_APP=true rkt app add c77b3f3b docker://redis:4.0.6 $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS c77b3f3b etcd coreos.com/etcd:v3.1.7 running 7 minute ago 7 minute ago default:ip4=172.16.28.2 redis registry-1.docker.io/library/redis:4.0.6
逆に特定のコンテナだけ終了させて Pod から外すことも可能です。CRI の StopContainer
+ RemoveContainer
に相当します。
$ sudo RKT_EXPERIMENT_APP=true rkt app rm c77b3f3b --app redis $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS c77b3f3b etcd coreos.com/etcd:v3.1.7 running 24 minutes ago 24 minutes ago default:ip4=172.16.28.2
表面上は全く同じように見えますが、rkt app
コマンドで作られた Pod は通常の rkt run
で作られた Pod とは別物です。例えば rkt run
で作られた Pod に後からコンテナを追加しようとするとエラーになります。
$ sudo rkt run coreos.com/etcd:v3.1.7 (別ターミナルで) $ sudo rkt list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS 5c786d20 etcd coreos.com/etcd:v3.1.7 running 3 minutes ago 3 minutes ago default:ip4=172.16.28.2 $ sudo RKT_EXPERIMENT_APP=true rkt app add 5c786d20 docker://redis:4.0.6 add: error adding app to pod: immutable pod
Pod が mutable であるかどうかは rkt cat-manifest
を用いて Pod の低レベルな情報を取得することで判断できます。Docker で言えば docker inspect
に相当するコマンドです。
$ sudo rkt cat-manifest 5c786d20 ... "annotations": [ { "name": "coreos.com/rkt/stage1/mutable", "value": "false" } ], ...
rktlet のインストール
さて、kubelet から gRPC を待ち受けて rkt app
を実行するのが rktlet の役目です。
Unix ソケットで通信している都合上、各 Node 上で(Kubelet と同じサーバで)rktlet が稼働している必要があります。こちらもバイナリがリリースされているのでダウンロードしてくればすぐ使えます。
$ wget https://github.com/kubernetes-incubator/rktlet/releases/download/v0.1.0/rktlet-v0.1.0.tar.gz $ tar xzvf rktlet-v0.1.0.tar.gz $ sudo mv rktlet-v0.1.0/rktlet /usr/local/bin/rktlet $ rktlet --version rktlet version: v0.1.0
直接フォアグラウンドで実行したまま実験してももちろん構いませんが、もし systemd に登録するのであればテスト用の最低限のサービス定義は以下のようになります。各 Node の /etc/systemd/system/rktlet.service
に配置してください。
[Unit] Description=rktlet: The rkt implementation of a Kubernetes Container Runtime Documentation=https://github.com/kubernetes-incubator/rktlet/tree/master/docs [Service] ExecStart=/usr/local/bin/rktlet Restart=always StartLimitInterval=0 RestartSec=10 [Install] WantedBy=multi-user.target
登録後、サービスとして起動しておきます。
$ sudo systemctl enable rktlet $ sudo systemctl start rktlet $ systemctl status rktlet ● rktlet.service - rktlet: The rkt implementation of a Kubernetes Container Runtime Loaded: loaded (/etc/systemd/system/rktlet.service; enabled; vendor preset: enabled) Active: active (running) since Fri 2017-12-22 17:52:06 UTC; 3s ago ...
Kubelet の設定
さて、次は呼び出す側の設定です。各 Node で稼働している Kubelet の実行時引数に、以下の四つの設定を入れてください。
--cgroup-driver=systemd --container-runtime=remote --container-runtime-endpoint=/var/run/rktlet.sock --image-service-endpoint=/var/run/rktlet.sock
--container-runtime-endpoint
CRI の RuntimeService に、--image-service-endpoint
が CRI の ImageService に、それぞれ対応していて、Unix ソケット経由で gRPC リクエストが送られるようになっています。
具体的に変更するファイルは Kubernetes をどうやって構築したかに依存するので何とも言えませんが、systemd サービスとして起動させているのであれば /etc/systemd/system/kubelet.service
内の ExecStart
もしくは EnvironmentFile
に記述があるはずです。
一旦 Kubelet を停止して、稼働している Docker コンテナをすべて止めておくのが安全です。その後、Kubelet を再起動して Node が Ready
になるまで待って確認してみると、Node のコンテナランタイム情報は狙い通り rkt に変わっています。
$ kubectl describe nodes/YOUR_NODE_NAME ... Container Runtime Version: rkt://0.1.0 ...
ただし rkt ではなく rktlet のバージョンが表示されてしまうようです。
実際に立ち上がっている rkt コンテナを確認してみましょう。rktlet はデフォルトの rkt とは別の場所、/var/lib/rktlet/data
以下にコンテナの情報を格納するようになっています。
クラスタ上に何がデプロイされているかによって細かい部分はもちろん違うと思いますが、おおむね以下のように Pod の一覧が表示されるはずです。
$ sudo rkt --dir=/var/lib/rktlet/data list UUID APP IMAGE NAME STATE CREATED STARTED NETWORKS 019e15b8 0-kubernetes-dashboard gcr.io/google_containers/kubernetes-dashboard-amd64:v1.6.3 running 3 minutes ago 3 minutes ago default:ip4=172.16.28.2 03183628 0-kube-proxy quay.io/coreos/hyperkube:v1.8.0_coreos.0 running 3 minutes ago 3 minutes ago 37bf1575 0-nginx-proxy registry-1.docker.io/library/nginx:1.11.4-alpine running 3 minutes ago 3 minutes ago 7996fe61 0-autoscaler gcr.io/google_containers/cluster-proportional-autoscaler-amd64:1.1.1 running 3 minutes ago 3 minutes ago default:ip4=172.16.28.5 abf84ed7 0-calico-node quay.io/calico/node:v2.5.0 running 3 minutes ago 3 minutes ago 1-calico-node quay.io/calico/node:v2.5.0 bf67a103 0-kubedns gcr.io/google_containers/k8s-dns-kube-dns-amd64:1.14.2 running 3 minutes ago 3 minutes ago default:ip4=172.16.28.4 0-dnsmasq gcr.io/google_containers/k8s-dns-dnsmasq-nanny-amd64:1.14.2 0-sidecar gcr.io/google_containers/k8s-dns-sidecar-amd64:1.14.2
この後は通常通り、Deployment やその他のリソースを作成すればマニフェストの記述に従って rkt のコンテナが立ち上がるはずです。
まとめ
今回の記事では、CoreOS 社が作ったシンプル指向のコンテナ技術 rkt の仕組み、および rktlet を用いた Kubernetes との連携について実際のコマンドを交えつつ説明しました。
- rkt は Docker とは別の Pod ネイティブな仕組みを採用した
- しかしそれが裏目に出て、CRI への対応が難しくなった
- kubelet と rkt コマンドの間に rktlet を置き、新しく実装された
app
サブコマンドを叩かせることで CRI 相当の動作を実現する
ところで、今回の記事では rkt の内部アーキテクチャにはそれほど深く踏み込めませんでした。従来の immutable な Pod と新しい mutable な Pod、それぞれがどうやって systemd 上に実装されているか、というのも興味深い話題ではあるのですが、それはまた別の話。
以上、Kubernetes Advent Calendar 2017 の 23 日目の記事でした。明日はクリスマスイブですね。担当は tkusumi さんです。