[TLA+] TLA+と形式仕様言語 [目的と準備]

こむろ＠札幌です。

今年も社内の人から「それ何の役に立つの？」「それXXで良くない？」と言われ、大体において理解されないニッチな分野で生きていきたいと思います。よろしくお願いします。

はじめに

仕様変更や改修によってプログラムにちょっとしたパラメータやフラグを追加したことはないでしょうか。僕はあります。そしてそれを追加するにあたって

• そのパラメータはどのような状態を持ち、状態を追加することで機能に影響はあるのか
• 追加したパラメータによってシステムの正常な動作が阻害されないか（もしくは破綻しないか）
• 取りうるパラメータのパターン全てで正しく動作するのか

これら全てに明確に問題ないと答えられるでしょうか。（僕は無理です）

設計レビューやテスト等で全てをチェックするのはなかなか大変です。何らかの明確な根拠をもって問題ないと言っている人がどの程度いるでしょうか。

人の手によるチェックは限界があります。往々にして仕様の検討漏れは実装フェーズになって気づいたり、リリース後の障害で発覚したりします。特にクリティカルなシステムの場合の障害は致命的です。生命に関わったり金銭に関わるものであればなおさらです。そこで仕様や設計が正しいことを保証するツールや手法（形式手法）が必要になります。自分はぼんやりとしか知らなかった分野なのですが、今回冬休みの宿題でTLA+という形式手法のツールの一つの調査を行いました。後述していますが、AWSのDynamoDB、EC2やS3（今はさらに増えている）といった数多くのサービスの仕様をこの言語で表記し、モデル検査によって矛盾や不整合がないかをチェックしているそうです。

今回から何回かに分けて調査した内容を書いていきます。まず今回は全般的なTLA+の紹介と手っ取り早く体験するためのIDEの準備です。

ちなみにわたしは形式手法及びモデル検査の分野の学術的な知識はあまり（ほぼ）ありません。論文や著書等を調べながら書いているため、素っ頓狂な記述や言い回しがおかしい箇所があるかと思います。その際はお手数ですがコメントいただけると幸いです。

TLA+の前に形式仕様言語とその目的

TLA+はデジタルシステムのモデリングを行うための形式仕様言語及びツールです。

デジタルシステムとは、いわゆるソフトウェアを構成するアルゴリズム、プログラム、コンピュータシステムと言ったものの総称です。

形式仕様言語は通常のプログラミング言語とは異なり、システムの仕様を数学的な記法で記述します。どのように実装するHOWではなく、何ができるかWHAT（つまりは仕様）を表現します。形式仕様言語によって記述された仕様は数学的な論理に基づいて検証します。モデル検査によってその仕様を満たせるかを確認し、正しく仕様を満たせない場合はその反証を具体的に提示します。そのため、実装に入る前の設計段階でその仕様が論理に矛盾がなく満たすことができるかを確認できます。

形式仕様言語で表現されたコードはシステムが満たすべき性質を表現します。新たに仕様を追加したり変更する場合に既存の性質を破綻させるものではないかを機械的にチェックすることができます。

状態を示す変数が多いほど、そのパラメータが取りうる値の集合が大きいほど試行すべきパラメータセットの数は膨大になっていきます。これらを手で再現しチェックするのは実質不可能です。そのため、コンピュータの力によって膨大なパラメータセットを試行し、それらの状態変数の組み合わせでシステムの性質が保たれることを保証できます。

普段行っているプログラミングとは全く異なるパラダイム（そもそも抽象度が全く違う）であるため、考え方根本をリセットしてから挑む必要があります。

TLA+

TLA+はLeslie Lamport先生が開発した形式仕様言語及び関連ツールです。この言語の特徴は、並行実行や分散システムをサポートしていることです。また他の形式手法のツールに比べて数学的な素養があまりないプログラマーでも容易に習得ができるのが特徴です。Eclipseベースの優れたIDEが提供されているため、導入のファーストステップのハードルが非常に低いのも特筆すべき特徴でしょうか。

AWSのサービスのいくつか（S3やDynamoDB）はTLA+を利用して仕様を記述しシステムの仕様を検証しています。その結果、仕様の不具合を検出し修正しています。

The Evolution of Testing Methodology at AWS: From Status Quo to Formal Methods with TLA+

AWSのサービスのように複雑なシステムの場合、人間の手で破綻なく仕様をチェックすることは現実的ではなく、また複雑な仕様への追加・変更を行う上で「正しさ」をチェックできるのは非常に大きいと思われます。

国内の事例では、SQUARE ENIXのFinal Fantasy 15 Pocket Editionの一部機能の仕様で利用されているようです。

形式手法(TLA+)でトランザクションのないDynamoDBで一貫性のある実装ができているかをチェックしている / “『FINAL FANTASY XV POCKET EDITION』を支える AWS サーバーレス技術” https://t.co/oPdw1GX3e1

— fujiwara (@fujiwara) October 25, 2018

FINAL FANTASY XV POCKET EDITIONを支える AWS サーバーレス技術

DynamoDBにはトランザクションがなく複数レコードの一貫性が保たれないのを許容したとして、本当に一貫性が許容されなくても問題か？

上記をTLA+を使って確認をしているとのこと。

悪魔の証明にも見える命題ですが、状態変数を定義し変数の取りうる全てのパラメータセットを検証し総当たりでチェック。これによりDynamoDBの特性によってシステムの性質が破綻することがないということを確認しているようです。用途としてはシステムすべての仕様を記述するというよりは、一部分のクリティカルな処理を行う上での状態や遷移で表現したシステムの「性質」を記述し、状態のパラメータセットの組み合わせを持って自動的に検証、その仕様が正しいことを確認することが多いようです。

モデル検査

TLA+では記述された仕様が正しいかをチェックするために、TLC Model Checkerというツールを提供しています。Model Checkerに「どのような仕様であるか」「何をチェックすべきか」「記述された仕様で外部から与えられるパラメータ（定数パラメータ）に代入する値を指定」といった情報を与えるモデルを作成します。この作成したモデルに基づいてModel Checkerがモデル検査を実行します。

モデル検査は、形式仕様記述で仕様を記述したモデルを取りうる値のすべてを網羅的にかつ自動的に検証し、そのモデルが正しいことを数学的に証明する手法です。

Wikipedia - Model_checking

TLA+は状態遷移を主とした仕様モデルを扱います。そのため、TLA+ではState machineを表現し記述することになります。システムが扱う状態は状態変数によって表現され、それらの変数が変化することで様々な状態に遷移していきます。

検証ではそれぞれの状態変数の取りうる値（定義に基づいて）を網羅的に調べることで、未知の状態や不正な遷移が存在しないかをチェックできるようです。記述された仕様を満たせない状態があった場合は、それをエラーとして反証と共に提示します。モデル検査はハードウェア設計の検証等でよく利用されているようです。

こちらの資料がとても良くわかりやすくまとまっていました。

教材について

TLA+は作者のLeslie Lamport先生がVideo Lectureを公開しています。

非常に聞き取りやすい英語ですし、比較的容易な言い回しをしてくれているので英語が苦手な自分でもそこまで苦労なく聞き取れます。さらに資料にはScriptも用意されており、動画の中で喋っている内容は全て追えるようになっています。そのため、このVideo Lectureを全て見るだけでTLA+の一通りの使い方については理解できるようになります。

ただし、はじめは比較的優しいのですが後半加速度的に難易度が増していきます。 ^*1

The TLA+ Video Course

陽気なLeslie先生

TLA+ IDEのインストール

Eclipseベースで作成されています。基本的に対象環境のZIPをダウンロードして展開するのみです。

github - tlaplus/tlaplus release

Specの作成

Specというモジュールを作成します。これはtlaという拡張子になります。仕様はこのモジュールに抽象コードとして表現していきます。

モデルの作成

記述した仕様を検証するためにモデルを作成します。

基本はこの２つのファイルがベースになります。

Hello TLA+

TLA+は通常のプログラム言語と同じパラダイムではないので単純なHello Worldはかけません。

そこでLecture 1で紹介されているシンプルなC言語のプログラムと、それに対応する仕様を抽象コードで表現したコードを見比べます。

C言語のプログラム

簡単なC言語のプログラムを想定します。しかし一部のメソッド動作が不明です。

int i ;
void main()
{
i = someNumber();
i = i + 1 ;
}

TLA+で記述するにおいてsomeNumber() の実装詳細については必要ありません。ただしそのメソッドが何をするかを記述する必要があります。ここではsomeNumber() は0から1000までの任意の値を何らか返却すると仮定します。 このとき i を状態変数とします。するとステップごとに以下のように状態が変更するのがわかります。

1. i=0
2. i=42
3. i=43

当然ながらこれは例の一つです。しかし、iが取りうる全ての値のパターンを書き下して本当に問題がないかを確かめるのは大変です。

TLA+で表現

TLA+で上記のプログラムの仕様を記述してみます。

まずは上記のプログラムを抽象コードへ変換します。このプログラムは3つのStateが必要なようです。そこでStateを表すために pc という現在の状態を示すパラメータを導入します ^*2

int i;
void main()
{ i = someNumber(); // pc = "start"
i = i + 1 ; // pc = "middle"
} // pc = "done"

先程の例に当てはめてみます。

1. i=0, pc="start" // 初期状態
2. i=42, pc="middle" // 何かの数値がセットされて、middleへ
3. i=43, pc="done" // 何かの数値に +1 をして doneへ

つまり書き下すと以下のようになります(Lecture 1のスライドから引用)。

if current pc value equals "start"
then next value of i choose {0..1000} // 0から1000までの集合から任意の一つを選ぶ
next value of pc equals "middle" // middleへ遷移
else if current pc value equals "middle"
then next value of i equals current value i + 1 // i = i + 1
next value of pc equals "done" // doneへ遷移
else no next values // "done"まで遷移したのでその後の遷移はない

これをTLA+の形に変換すると以下のようになります。ひとまず細かい解説は抜いて全体像を記述します。

上記の抽象コードをTLA+で記述すると以下のとおり。

--------------------------- MODULE SimpleProgram ---------------------------
EXTENDS Integers

VARIABLES i, pc

Init == (pc = "start") /\ (i = 0)

Pick == /\ pc = "start"
/\ i' \in 1..1000
/\ pc' = "middle"

Add1 == /\ pc = "middle"
/\ i' = i + 1
/\ pc' = "done"

Next == \/ Pick \/ Add1
=============================================================================
\* Modification History
\* Last modified Fri Jan 25 11:34:26 JST 2019 by komurohiraku
\* Created Fri Jan 25 11:18:28 JST 2019 by komurohiraku

ずいぶんと見慣れない表記や記号が見られます。前述の通り、数学的な表現をそのまま記述しているためです。

それぞれの細かい解説は次回。

Latexで数学的な記号を正確に表示したい

ご存知の通りLeslie Lamport先生はLaTeXの原開発者として有名です。Wikipedia - LaTeX

そしてTLA+の抽象コードは数学的な表記が多くあります。LaTeXさえ入っていれば以下のようにきちんと数学的な記号を表示することができます。

ちゃんとした数学の記号が表示されました。

pdflatexがない場合

pdflatexがインストールされていない場合、このようなエラーが表示されます。

Macの場合、mactexというパッケージが公開されています。こちらを利用します。インストール方法についてはこちらが非常に詳しくかかれています。こちらを参考にします。

以下のページからpkgファイルを取得します。

mactex - The MacTeX-2018 Distribution

ダウンロードしたpkgファイルをインストール

3.2GBほどあるのでじっと待ちましょう。インストールが完了したら、Terminalを起動します。すでに起動している場合は再起動します。

以下のコマンドを入力しパッケージを更新します。700パッケージ以上が更新・インストールされるのでじっと待ちましょう。

$ sudo tlmgr update --self --all
Password:
Sorry, try again.
Password:
tlmgr: package repository http://ftp.yz.yamagata-u.ac.jp/pub/CTAN/systems/texlive/tlnet (not verified: gpg unavailable)
tlmgr: saving backups to /usr/local/texlive/2018/tlpkg/backups
[1/2, ??:??/??:??] update: texlive.infra [394k] (47457 -> 49228) ... done
[2/2, 00:03/00:05] update: texlive.infra.x86_64-darwin [345k] (43815 -> 47820) ... done
Restarting tlmgr to complete update ...
....
....
tlmgr: package log updated: /usr/local/texlive/2018/texmf-var/web2c/tlmgr.log
$ which pdflatex
/Library/TeX/texbin/pdflatex

pdflatex がインストールされました。続いてIDEの設定を変更します。

設定メニューから PDF Viewer の項目を探します。

Specify platex command の値を pdflatex コマンドのフルパスへ書き換えます。これでpdflatexで出力ができるようになります。

まとめ

TLA+という仕様を検証する言語・ツールについて調べてみました。AWSのサービスの非常に複雑な仕様がこれで表現されていることで、サービスの追加機能の際のトラブルの少なさや不具合の少なさに貢献しているとのことでした。非常に興味深いツールでしたがまだまだ日本では実際に使われている箇所は非常に少ないようです（単に公開していないだけかも）

複雑なシステムを設計や改修するにおいて、こういった数学的な裏付けのある手法が利用できるのは開発者にとても非常にメリットの大きいことだと思います。なかなか学術的な分野でもあるようなので時間は掛かりそうですが少しずつ調べて理解していきたい。そしてきちんと現場にフィードバックしていきたいと思います。

次回はTLA+の抽象コードの内容を解説をしていきたいところです。ではまた。

参照

• SlideShare - モデル検査入門 #wacate
• The TLA+ Video Course
• FINAL FANTASY XV POCKET EDITIONを支える AWS サーバーレス技術
• Mac OS X(Mojave)にLaTeX環境を構築する[VSCode版]

脚注