Let's write β

プログラミング中にできたことか、思ったこととか

TLA+, SPINをつかってAPIサーバーの仕様を検証した

バックエンドサーバーのAPIの仕様を決めるにあたって、レスポンスの結果が常にみたしていてほしい不変条件がありました。 ビジネスの詳細に触れてしまうので、抽象的に表現すると

内部データのある属性値が1以上になっているならば、かならずレスポンスにふくまれてほしい 逆に、その属性値が0のものは、レスポンスにふくまれてはならない

といった物でした。

システムのアクターが、APIのユーザー・社内メンバーの管理者・社外の管理者といった複数のロールがあり、 それぞれが固有のユースケースを通して、その内部データに干渉する事になるため、はたしてそのユースケースをサポートするにあたって、 どんな事前条件を考慮しておかないと上記の不変条件がみたされなくなるのか、という事を仕様を決めるにあたってはっきりさせておく必要がありました。

人間が考えるテストケースには抜け漏れが発生しがち

この不変条件はユーザー体験上非常に重要なものにかかわっていたため、テストはしっかり書きたいです。 しかし、テストはあくまでテストをしたケースについて動作する事を保証しているのみで、テストできていないケースについてはミスを検出できません。

そのため「どんなテストをする必要があるのか?」がより重要になります。 しかし、システムのユーザーのユースケースの数が10個以上あり、それぞれがAPIを通して実施される事になるため、 テストケースを人間が考えるというのでは漏れが発生する可能性があります。

これは、たとえテストでの行にたいするカバレッジが十分にあったとしても、そもそも適切な事前条件を設定できていなかったりする場合にはその行自体はテスト時には実行されているため検出できません。 そのため「どのようなユースケースの呼びだされ順序をとっても、不変条件が破れる事がない」という事を確認したいという事になります。

現に、システムの開発を進めていくなかで、ふと「あれ、これってこの操作をしたあとに、この操作をすると変なデータになるのでは?」という話が何度かあり、 そもそも仕様としてそういったケースでどう対処するのかについても未定義という事がわかって仕様を追加で定義したりしました。

モデル検査ツールの出番

こういったケースではモデル検査ツールが役に立つのではないかという風に私は考えました。 以前別のプロジェクトでAlloyをつかって機能の設計を個人的にした事があったため、簡素な物であってもモデル検査が仕様の穴を発見するのに役だつ事はしっていました。

そこでAlloyでの検証も検討したのですが、 今回のケースではさまざまなユースケースがランダムな順序で実行を試みられるとして、 どのような順序で実行されたとしても不変条件が破れている状況が発生しないという事を目的としていたため ステートのサイズがどのくらいになれば良いのか不明な状況の中での検証となるため、自動的に網羅的な検証をしてくれるツールに頼りたいと考えました。

TLA

TLA+は2015年にAWSがシステムの検証に利用している事を発表した事で話題になったモデル検査ツールです。 分散システムの研究でチューリング賞を受賞されているLeslie Lamportさんが開発しているツールで、 TLA+という構文と、PlusCalとよばれるTLA+に翻訳される構文の2つをサポートしています。

AWSが採用した背景にTLA+が一般のエンジニアでも学習がしやすかったという事があげられていたため、僕もまずはトライしてみました。

各APIがいくつかのアクターからランダムに実行されつづけるというのは以下のような形式になるとおもいます

---------------------- MODULE delivery_request_cancel ----------------------
EXTENDS Integers, TLC

(* --algorithm api_server
variables hoge = "fuge", foo = "bar", baz = 0; \* APIで変化する内部の状態をあらわす変数

process ActorOne = 1
begin
ActorOneMain:
    while TRUE do
        either
            ApiOne:
                if hoge = "moge" /\ baz = 1 then
                    foo := "qux";
                end if;
        or
            ApiTwo:
               foo := "corge";
         end either;
     end while;
end process

process ActorTwo = 1
begin
ActorTwoMain:
    while TRUE do
        either
            ApiThree:
                if hoge = "fuge" /\ baz = 0 then
                    foo := "foo";
                end if;
        or
            ApiFour:
               foo := "qux";
         end either;
     end while;
end process

end algorithm; *)
=============================================================================

これは構文としてPlusCalをつかっています。 PlusCalでは、複数のプロセスが並行して動作する状況をprocessとして表現でき、 かつランダムにどれかを選択して実行されるという状況をeitherとして表現でき、まさに検証したい複数のアクターがランダムに処理を実行する状況を表現できます。

learntla.com

このように、TLA+では、実行したいアルゴリズムを記述すると共に、 「モデル」とよばれる、何を不変条件として検証したいのかや、(このコードでは出てきませんが)アルゴリズムに外部から注入したい定数等の指定を分割して管理します。

今回のモデルでは、僕たちは検証したい

内部データのある属性値が1以上になっているならば、かならずレスポンスにふくまれてほしい
逆に、その属性値が0のものは、レスポンスにふくまれてはならない

という内容を、モデルで検証したい不変条件として実行しました。

検証の結果

検証の結果としては、まず僕たちが自力で気がついた不具合が検出され、追加した仕様を設定するとその穴がうまる事が確かめられました。 これによって、正しくシステムをモデル化できている事がたしかめられました(ほんとうはもっと厳密にやるべきですが)

さらに、僕たちが気がつけていなかった別の実行過程でも不変条件が破られる事がわかり、こちらについても対応を決める事ができました。 対応を決める中でも、どのような仕様にすると穴がうまるのかを確かめられたため、設定した仕様に自信が持てました。

SPINでのリライトと比較

TLA+というモデル検査ツールですが、モデル検査ツールではほかにメジャーなツールとしてSPINというツールが存在します。

spinroot.com

SPINはTLA+よりも歴史が長くリリースが最近もおこなわれているため、SPINの使用感も検証する必要があると考えました。

SPINでは、PromelaとよばれるC言語に似た構文の言語を利用して記述します。 SPINではデフォルトで複数のプロセスによる協調動作を前提として記述するので、上の例をSPINにあわせてみると

mtype:hoge_t = {fuge, moge};
mtype:foo_t {foo, bar, qux, corge};

hoge_t hoge;
foo_t foo;
bool baz = 0;

active proctype actor_one() {
    do
        :: hoge == moge && baz == 1 ->
             foo = qux;
        :: foo = corge;
    od;
}

active proctype actor_two() {
        do
        :: hoge == fuge && baz == 0 ->
             foo = foo;
        :: foo = qux;
    od;
}

ltl p0 {[]((foo == foo && hoge == moge) || (baz == 0 && foo == qux))};

このように、proctypeという形でプロセスを表現する事ができます. SPINでは、doという形式が、eitherと同様に実行可能な物をどれか実行するという事になっています。

ツールとしての使いやすさ

個人には、言語の構文はC言語ににており、慣れしたしんだ記号で比較や論理演算ができるため、SPINの方が使いやすいなと感じました。 一方で、SPINの公式のGUIフロントエンドはTcl/Tkで実装されており、UIの挙動としてちょっと古い感じがあり、最近のTCLで動かすには一部リライトする必要等がありました。 なので、私は利用する時はVSCodeでコードを書いてCLIでSPINを呼びだすように今後は使うかとおもいます。

一方、TLA+はTLAがかなりシンプルな機能しか提供していないため、 PlusCalで記述しなければ今回のようなケースでは記述量が多くなったりミスをしやすくなってしまうかと感じますが、 PlusCalの記法はTLA+よりはわかりやすく、PlusCalからTLAへの変換はToolKitが自動的にやってくれます。

また、GUIとしての使いやすさはTLA+はシンプルとはいえEclipseベースのIDEが提供されSPINと比較して馴染みやすさを感じました。

検査したい抽象度に応じた記法の調整

WebAPIを実装するにあたって、モデルによって検証したい事が何なのかによってどこまで詳細に記述するのかを考える必要があります。

仕様レイヤーのみの検証

今回の場合は「仕様」のレイヤーにおいて矛盾が生じない事を検討したかったため、 各APIの実行におけるロックや排他処理は適切に実施されているという前提で一つのサーバーというプロセスがどれかの処理を実施するという風にシンプルに記述する事が可能です:

active proctype Server() {
  do
  :: (API 1の事前条件) -> API 1の処理
  :: (API 2の事前条件) -> API 2の処理
  od;
}

すこし実装に踏みこんだ、マルチプロセスでの検証

よりもうすこし詳細に、実装についても検証を深めたいとなると以下のように複数のアクターが並行してサーバーにアクセスしてくる状況として記述できます:

proctype ActorOne() {
  do
  :: (API 1の事前条件) -> API 1の処理
  od;
}

proctype ActorTwo() {
  do
  :: (API 2の事前条件) -> API 2の処理
  od;
}

init {
  atomic {
    run ActorOne();
    run ActorTwo();
  }
}

このようにしておくと、たとえば「API1の処理の途中でAPI2の実行がされた時に、API 1の処理の途中結果がAPI2に見えしまって異常なデータが発生する」といった事が検出されます。

処理をatomicにして排他制御

atomicに実行する事によって一方の途中結果がAPI2に見えないようにトランザクションにしたり:

proctype ActorOne() {
  do
  :: (API 1の事前条件) -> atomic { API 1の処理 }
  od;
}

proctype ActorTwo() {
  do
  :: (API 2の事前条件) -> atomic { API 2の処理 }
  od;
}

init {
  atomic {
    run ActorOne();
    run ActorTwo();
  }
}

する事もできます。 しかし、たとえばこれでは

API 1とAPI 2の処理はAtomicに実施されるが、事前条件の判定はAtomicに実施されていないため、 本来API 1の処理をした後にはAPI 2の事前条件が満されなくなるべきだが、条件確認だけ事前に並行しAPI1の後にAPI 2が実施されてしまう

という事事が検出されます

事前条件の確認もふくめて全体で排他制御

そのような場合には条件のチェックもふくめてAtomicに実施する事で

proctype ActorOne() {
  do
  :: atomic { 
    if
    :: API 1の事前条件 -> atomic { API 1の処理 }
    fi;
  }
  od;
}

proctype ActorTwo() {
  do
  :: atomic { 
    if
    :: API 2の事前条件 -> atomic { API 2の処理 }
    fi;
  }
  od;
}

init {
  atomic {
    run ActorOne();
    run ActorTwo();
  }
}

という事をして、条件確認もふくめて排他的にチェックする事で回避できる事が確認できます。 しかし、このように処理全体をロックするという事は、システム全体を止めて一つの処理だけを実行している事に近く、ロックの範囲が大きすぎるように感じます。

ロックの取得待ちで排他制御

そこで、一つのデータをロックとして利用する事で排他制御するように記述する事も可能です。

bool data_locked = 0;
proctype ActorOne() {
  do
  :: atomic { data_locked == 0; data_locked = 1; }
    if
    :: API 1の事前条件 -> atomic { API 1の処理 }
    fi;
    data_locked = 0;
  od;
}

proctype ActorTwo() {
  do
  :: atomic { data_locked == 0; data_locked = 1; }
    if
    :: API 2の事前条件 -> atomic { API 2の処理 }
    fi;
    data_locked = 0;
  od;
}

init {
  atomic {
    run ActorOne();
    run ActorTwo();
  }
}

といった事も確認できます。

おそらくですが、 全体をAtomicでロックする事はいわば、DBへのアクセスを一つのプールに制限したりDB全体にロックをかけるような処理に該当し、 後者のロック取得は、行ロックにような必要最小限の反映でのロックに該当するかと思われます。

このように、不変条件が破られない事を確認しながら、リファクタリングをするように排他制御のプランを変更したりする事ができます。

より詳細な検証もできるが、システムへの理解と翻訳の難易度が高くなる

このように、段々とモデリングを詳細化していく事によって仕様検証ができるモデル検査ツールですが、 たとえばRDBMSのトランザクション分離レベルでのファントムリードに起因する問題であったり、そういった物は上記の記述ではカバーできていません。 最初のアクセスがあった時点でのスナップショットをとって、そこから読みとられる事になるといった挙動がモデルに表現できていないからです。 このようにより実装の検証に入っていくとより詳細なシステムの動作への理解とそれをモデル検査ツールの言語に翻訳する能力がもとめられます。

TLA+ではラベルの配置が重要になる

上記の例はSPINのPromela言語での記載ですが、PlusCalでもおそらく同じような検証は可能だと思います。 しかし、TLAでは、デフォルトで構文上の分岐の枝が一つのかたまりとして実行されるため、後半で触れていたような条件チェックのインターリーブのような物は コード上にラベルを配置して、細かく処理の最小単位を設定してやる必要があります。

Checking a Multithreaded Algorithm with +CAL

その点SPINではatomicで囲われていないコードは、デフォルトでインタリーブされる可能性があるとして取りあつかわれるため、 わざわざラベルを記述しなくても逆にナイーブな実装をしてしまっている時にミスに気がつきやすいと感じました。

まとめ

今回の検証では仕様のレベルでの矛盾の発見を目的として、TLA+とSPINという二つのツールを利用して検証を実施しました。

モデル検査をしていくにあたっては、どの領域まで検証するのか(されているのか)という認識をきちんと理解して 利用しなければ結果を過信しすぎてしまったりする事になると思います。 しかし、人間が考えるテストケースにとらわれずにシステムが網羅的に検証してくれる事によって、より自信をもって作業を進められるようになり、その効果は非常に大きいと感じました。

また、ツール選択においてはどちらのツールにもそれぞれの個性がありますが、PlusCalとSPINのデフォルトの処理単位の挙動などを含めると、 個人的には、より手さぐりでつくっていく時にはSPINで記述してミスに気がつく事のほうが楽で、 逆に設計したアルゴリズムについてきちんと理解した上で記述していくならば、データ構造等が豊富に存在するPlusCalのほうが使いやすそうだなと感じました。