- TLA+ は、コードレベルではなくより高いレベルで ソフトウェアをモデリングし、回路レベルではなくより高いレベルで ハードウェアをモデリングするための言語
- モデルを作成し、それを検査できる統合開発環境(IDE)を提供
- エンジニアが最も多く使うツールは TLC モデルチェッカーであり、証明チェッカーも提供
- TLA+ は数学に基づいており、どのプログラミング言語とも似ていない
- ほとんどのエンジニアにとっては、TLA+ よりも PlusCal から始めるほうが簡単
- TLA+ モデルは一般に「仕様（Specification）」と呼ばれる。以下の紹介では
モデル と呼ぶ
PlusCal
- PlusCal はアルゴリズム、特に 並列および分散アルゴリズムを書くための言語
- 疑似コードの代わりに、テスト可能な正確なコードでアルゴリズムを書くために使われる
- シンプルなプログラミング言語のように見え、並行性と非決定性を表現できる構文を提供する
- 数学的な式を式として使えるため、非常に表現力が高い
- PlusCal アルゴリズムは TLA+ モデルに変換され、TLA+ ツールで検証可能
- プログラミング言語のように見えるので学びやすいが、複雑なモデルの構造化には TLA+ のほうが適している
モデルとは何か
- コンピュータやネットワークは連続的な物理法則に従うが、その動作は離散的な出来事の集合としてモデル化するのが自然
- 実際のシステムを完全に記述するモデルはなく、モデルは特定の目的のためにシステムの一部の側面を記述する
- TLA+ は 状態ベースのモデリング言語であり、システムの実行を状態の列として表現する
- 出来事は連続する 2 つの状態の組で表現され、これを「ステップ（step）」と呼ぶ
- システムは、あり得るすべての実行を記述する動作の集合としてモデル化される
コードレベルを超えたモデリング
- TLA+ はコードレベルを超えたシステムモデリングに使われる
- 例えばユークリッドのアルゴリズムは、コードではなく手続きとして最大公約数（GCD）を計算する方法として説明できる
- 変数 x を M、y を N に設定する
- x と y のうち 小さい値を大きい値から繰り返し引く
- x と y が 等しくなるまで繰り返し、その値が GCD になる
- このような説明は、変数の型や例外処理のような詳細を省き、本質的なアルゴリズムの概念だけを表現する
- コーディングだけに集中すると良いアルゴリズムを見つけにくい → 抽象的な思考が必要
- ほとんどのプログラマは高水準モデルなしにコーディングを始め、その結果として設計ミスが発生する
- TLA+ は コードの振る舞いと方法を明確に記述できる高水準モデル言語
- 複雑なシステムほど単純化が重要であり、これはコード記述の技術ではなく高次の思考によって達成される
- ある産業プロジェクトでは、TLA+ モデリングによってリアルタイムオペレーティングシステムのコードサイズを 10 分の 1 に減らした事例がある
- モデリングは設計ミスを事前に見つけるのに効果的であり、テストやコード修正よりも信頼性が高い
並列システムのモデリング
- 並列システムは、同時に動作する複数のコンポーネント（プロセス）で構成される
- 分散システムは、空間的に分離されたプロセス同士がメッセージを通じて通信する
- TLA+ は システム全体の状態をグローバル状態としてモデル化する
- 40 年以上の経験によれば、分散システムをグローバル状態ベースでモデル化することが最も一般的に有用である
状態機械（State Machine）
- TLA+ は次の 2 つの要素で動作の集合を定義する:
- 初期条件: 可能な開始状態を指定
- 次状態関係: 可能なステップ（連続する状態の組）を指定
- この 2 つの条件を満たす動作の集合がモデル
- このようなモデルは状態機械（state machine）と呼ばれる
- 有限状態機械（finite-state machine）は、状態数が有限の状態機械
- チューリングマシンは状態機械の例であり、決定的チューリングマシンでは各状態に対して次状態が高々 1 つ
- プログラミング言語の意味を正確に説明する実用的な方法は、状態機械へ変換する操作的意味論である
- 次状態の動作は、発生し得るステップだけを指定し、必ず発生しなければならないことを意味しない
- ステップの必須発生を明示するには、公平性条件（fairness property）を追加する必要がある
- 公平性がなくても誤り（commission）を見つけるには十分だが、欠落による誤り（omission）は検出されない
- 多くの場合、誤りは commission のほうが多く、初心者は初期条件と次状態関係を書くことから始めるべき
性質の検証
- システムが望む通りに動作するかを確認するためにモデルを書く
- モデルが、あり得るすべての動作に対して特定の性質を満たすかどうかを TLA+ ツールで検証できる
- 例: 99% の初期状態で動作が正常終了しても、すべての動作が正常終了しなければならないことを検証する
- 最も一般的な性質は不変性（invariance property）で、すべての状態で常に真でなければならない
- 公平性条件があるモデルでは、ライブネス性質（liveness property）も検証する必要がある → 例: 実行が必ず終了する
- より複雑な性質は状態機械で表現でき、別の状態機械がそれを実装しているかを検証できる
- TLA+ では状態機械と性質の形式的な区別はなく、どちらも同じ数式として表現される
- ある状態機械が別の状態機械を実装するとは、その数式が論理的に包含されることを意味する
- 実際には多くの場合、不変性と単純なライブネス性質だけを調べるが、より複雑な概念を理解することもコードの誤り防止に役立つ
TLA+ 言語そのもの
- TLA+ は 数学ベースの言語であり、プログラミング言語のようには見えない
- プログラマは数学表現よりもプログラミング言語に慣れているため、最初は難しく感じることがある
- しかし実際には、数学はプログラミング言語よりも表現力に優れている
- 例: GCD を 2 つの数を割り切る最大の正の整数として定義できる（計算方法は省略可能）
- 数学的定義は、目的に必要な核心だけを残し、不要な実装詳細を抽象化できる
- 手続き化は抽象化を提供するのではなく、単に別の場所にコードを隠すだけ
- PlusCal は TLA+ 入門に適しており、熟練者でも簡単なモデルには PlusCal を好む
- しかし、数学的に考え高水準モデリングを行うには、TLA+ そのものを学ぶことが重要
3件のコメント
https://cacm.acm.org/research/… AWSでもうまく活用されていますね。
コーディングはプログラミングではありません
この記事で言及されていたので調べてみました。
私もこの記事で初めて見て、調べていましたね