Zenn
💨

形式手法を学んでみた

2021/04/17に公開
形式手法
tla
idea

形式手法がバズってた

少し前？(2021/03頃)形式手法は役に立たないんだとか役に立つんだとかで盛り上がっていたので、勉強してみました（1ヶ月くらいかかりました）。
DeNAの方も入門記事を書かれているようですね。

AWS ペーパーを読んでみる

そもそも形式手法（formal methods)のなんたるかを知らないので、わかりやすい記事がないかなーと思っていたところ。「AWSのペーパーが〜」と言及されていることが多かったので、読んでみることに。
これは結構読み物として良くて、

  • システムの動作を定義するために（だから formal methods)
  • 既存の資産を最大限活用したく（だから tla+)
  • だいたいどのエンジニアも2週間くらいでキャッチアップして
  • S3とかでバグの発見に役だった

と、背景と具体例を交えていて面白かったですね。

Lamportから学ぶ

形式手法の言語は色々あるらしいのですが、上記でも言及されていたtla+はとっつきやすそうだったので、それで。
tla+の開発者であり数学者でありチューリング賞受賞者であるLeslie Lamportが、チュートリアルをはじめ頑張って色々リソースをまとめてくれているので、基本はそちらを参照。Hello World的な講義動画はYoutubeにも転載されていて、静かなユーモアがめちゃくちゃ面白いのでぜひ１話だけでも。

tla+の中身

中身はあんまり言及しませんが、ハイレベルでは "thoroughly testable psuedo code"と表現していました. 基本的には数式でシステムの状態をstringで定義してあげて、「次の状態」（x の次の状態はx' で表現）を状態遷移図を書くように定義してあげて、その中でおかしな挙動が無いかをチェックする、みたいな感じです（safety).

複数のリソースマネージャーがトランザクション可能な状態の定義

canCommit == \A rm \in RM : rmState[rm] \in {"prepared", "committed"}

これが次のような形で render されます（見た目の問題だけ）。

canCommit == \forall rm \in RM : rmState[rm] \in {"prepared", "committed"}

リソースマネージャーが状態遷移することの表現

or 条件 (\/ = \lor）と and 条件 (/\ = \land）の組み合わせ

Decide(rm)  == \/ /\ rmState[rm] = "prepared"
                  /\ canCommit
                  /\ rmState' = [rmState EXCEPT ![rm] = "committed"

注意事項

注意としては

  • 到達可能な状態を状態遷移の定義に沿って総当たりで計算していくので、簡単なアルゴリズムでもめちゃくちゃ時間がかかる。ちょっとモデルを大きくする（リソースマネージャーを3->5にする）といきなり2分->5時間とかになる（ので大きくできない）。
  • tex ぽく書かないとならないので、慣れていないとしんどいかも。
  • 見た目が似てる記号を ASCIIの中で代用してるのも若干癖がある(\neqが#とか).

Lamportの講義全１０話の中身

最初は motivation の説明から、TLA+ toolbox のダウンロードと使い方の説明、transaction commit などの簡単なアルゴリズムの実装と正しさの検証、をやっていきます。いちいち手を動かさないと理解できないので、動画の2倍〜5倍くらい時間がかかりました。

やってみた感想

集合と位相をなぜ学ぶのかとかを読んで、数学がどんな風に世界を抽象化、モデル化してるのかなんとなく興味があったので、システムってこんな風に記述できるのか、という部分は結構ワクワクしましたね。後10年ぶりにTexの知識が生きて少し嬉しかったり。

大規模開発とか、SLAがめちゃくちゃ厳しい（その分開発期間が長い）開発とかでは普通に使われてるんだろうな、という気がしました。

個人的つまづきポイント

  • メインのモジュール１個につき、.tla ファイルを１個作る。
  • .tla ファイルは先頭に ----- <module_name> -----, 末尾に ========= をつける
  • import は INSTANCE として定義して TC!TCConstant みたく活用する
  • "Download from the webpage"とか言われてもリンク無いんですがとなるけども、URLを直打ちすると見つかる e.g., https://lamport.azurewebsites.net/video/xxxx.tla, あるいは github にまとまっている。
  • tex のインストールに3時間くらいかかった。MacTex は悪さをするらしいので TexLiveで。

References

Discussion