Loading article…
TLA + は、レスリー・ランポートによって開発された形式仕様言語です。これは、特に並行システムや分散システムなどのプログラムの設計、モデリング、ドキュメント作成、検証に使用されます。TLA + は、徹底的にテスト可能な擬似コードと考えられており、[ 4 ]その使用はソフトウェアシステムの設計図を描くことに例えられています。[ 5 ] TLAは、Temporal Logic of Actionsの頭文字をとったものです。
設計と文書化に関しては、TLA + は非公式の技術仕様と同じ目的を果たします。ただし、TLA +仕様は論理と数学の形式言語で記述され、この言語で記述された仕様の精度は、システムの実装が始まる前に設計上の欠陥を明らかにすることを目的としています。[ 6 ]
TLA +仕様は形式言語で記述されているため、有限モデル検査に適しています。モデルチェッカーは、一定数の実行ステップまでのシステム動作をすべて検出し、安全性や活性などの望ましい不変性特性の違反がないか検査します。TLA +仕様では、基本的な集合論を用いて安全性（悪いことは起こらない）を定義し、時相論理を用いて活性（良いことが最終的に起こる）を定義します。
TLA + は、アルゴリズムと数学定理の両方について、機械検証済みの正当性証明を作成するためにも使用されます。証明は、特定の定理証明バックエンドに依存しない宣言的かつ階層的なスタイルで記述されます。形式的および非形式的な構造化された数学的証明の両方を TLA +で記述できます。この言語はLaTeXに似ており、TLA +仕様を LaTeX 文書に変換するツールが存在します。[ 7 ]
TLA +は、並行システムの検証手法に関する数十年にわたる研究を経て、1999年に発表されました。以来、IDEや分散モデルチェッカーを含むツールチェーンが開発されてきました。擬似コードのような言語であるPlusCalは2009年に作成され、 TLA +にトランスパイル可能で、逐次アルゴリズムの記述に役立ちます。TLA +2は2014年に発表され、証明構造に対する言語サポートが拡張されました。現在のTLA +のリファレンスは、Leslie Lamport著の『The TLA + Hyperbook』です。
現代の時相論理は、1957年にアーサー・プライアーによって開発され、当時は時制論理と呼ばれていた。アミール・プヌエリが時相論理のコンピュータ科学への応用を本格的に研究した最初の人物であったが、プライアーはそれより10年前の1967年にその利用について考察していた。
離散時間に関するこのようなシステムの有用性は、時間が離散的であるという深刻な形而上学的仮定に依存するものではありません。これらのシステムは、離散的な状態のシーケンスにおいて次に何が起こるかのみに関心があるような、限られた議論の分野、例えばデジタルコンピュータの動作において適用可能です。
プヌエリは、コンピュータプログラムの仕様記述と推論における時相論理の使用について研究し、 1977年に線形時相論理を導入した。LTLは並行プログラムの解析のための重要なツールとなり、相互排他性やデッドロックからの解放などの特性を容易に表現できるようになった。[ 8 ]
Pnueli の LTL に関する研究と並行して、研究者たちはマルチプロセス プログラムの検証のためにHoare 論理を一般化することに取り組んでいた。Leslie Lamport は、相互排他に関する論文を投稿した際に査読で誤りが見つかったことをきっかけに、この問題に興味を持つようになった。Ed Ashcroft は 1975 年の論文「Proving Assertions About Parallel Programs」で不変性を導入し、Lamport はこれを用いて1977 年の論文「Proving Correctness of Multiprocess Programs」でFloydの方法を一般化した。Lamport の論文では、部分的な正しさと終了性の一般化として、安全性と活性も導入された。[ 9 ]この方法は、 Edsger Dijkstraとの 1978 年の論文で、最初の並行ガベージ コレクションアルゴリズムの検証に使用された。[ 10 ]
ランポートは、1978年にスーザン・オウィッキがスタンフォード大学で開催したセミナーで、プヌエリのLTLに初めて出会った。ランポートによれば、「時間論理は実用的な応用が全くない抽象的なナンセンスだと確信していたが、面白そうだったので参加した」。1980年に彼は「『Sometimes』は『Not Never』であることもある」を発表し、これは時間論理の文献で最も頻繁に引用される論文の1つとなった。[ 11 ]ランポートはSRI在籍中に時間論理の仕様書の作成に取り組んだが、そのアプローチは非実用的であると気づいた。
しかし、シュワルツ、メリアー・スミス、フリッツ・フォークトが単純なFIFO キューの 仕様を定めるために何日も費やし、列挙した特性が十分かどうかを議論しているのを見て、私は時間論理に幻滅しました。時間特性の論理積として仕様を記述することは、見た目には魅力的でも、実際にはうまくいかないことに気づきました。[ 12 ]
実用的な仕様記述方法を模索した結果、1983 年の論文「Specifying Concurrent Programming Modules」が発表され、状態遷移をプライム付き変数とプライムなし変数のブール値関数として記述するというアイデアが導入された。[ 12 ]研究は 1980 年代を通して続けられ、ランポートは1990 年にアクションの時間論理に関する論文を発表し始めたが、正式には 1994 年に「The Temporal Logic of Actions」が出版されるまで発表されなかった。TLAにより、アクションを時間式で使用できるようになり、ランポートによれば「並行システム検証で使用されるすべての推論を形式化および体系化する洗練された方法を提供する」という。[ 13 ]
TLA 仕様は主に通常の非時間的な数学で構成されており、ランポートは純粋に時間的な仕様よりも扱いやすいと考えた。TLA は、 1999 年に論文「Specifying Concurrent Systems with TLA + 」で紹介された仕様言語 TLA +の数学的基盤を提供した。 [ 1 ]同年後半、ユアン・ユーはTLA +仕様用の TLCモデルチェッカーを作成した。TLC は、 Compaqマルチプロセッサのキャッシュコヒーレンスプロトコルのエラーを検出するために使用された。[ 14 ]
ランポートは、2002 年に「Specifying Systems: The TLA + Language and Tools for Software Engineers」というタイトルの TLA +に関する完全な教科書を出版しました。 [ 15 ] PlusCal は2009 年に導入され、[ 16 ] TLA +証明システム (TLAPS) は 2012 年に導入されました。 [ 17 ] TLA +2は 2014 年に発表され、いくつかの追加の言語構造が追加され、証明システムの言語内サポートが大幅に強化されました。[ 2 ]ランポートは、更新された TLA +リファレンス「The TLA + Hyperbook」の作成に取り組んでいます。未完成の作業は、彼の公式 Web サイトから入手できます。ランポートはまた、「プログラマーやソフトウェア エンジニアが独自の TLA +仕様を作成する方法を教えるための一連のビデオ講義の開始部分からなる進行中の作業」と説明されているThe TLA + Video Course も作成しています。
TLA +仕様はモジュールに整理されています。モジュールは他のモジュールを拡張（インポート）してその機能を利用できます。TLA +標準は組版された数式記号で規定されていますが、既存の TLA +ツールはLaTeXのようなASCII 形式の記号定義を使用しています。TLA + では、定義が必要な用語がいくつかあります。
TLA + は、すべての正しいシステム動作の集合を定義することに関係しています。たとえば、0 と 1 の間を無限に刻み続ける 1 ビットのクロックは、次のように指定できます。
可変時計 Init == clock \in {0, 1} ティック == IF clock = 0 THEN clock' = 1 ELSE clock' = 0 Spec == Init /\ [][Tick]_<<clock>> 次の状態関係Tick は、 clockが 0 の場合はclock ′ (次の状態におけるclockの値) を 1 に、 clockが 1 の場合は 0 に設定します。状態述語Initは、 clockの値が 0 または 1 の場合に真となります。Specは、1 ビット clock のすべての動作が最初にInit を満たし、すべてのステップがTickに一致するか、または途切れ途切れのステップである必要があることを主張する時間式です。そのような動作の 2 つは次のとおりです。
0 -> 1 -> 0 -> 1 -> 0 -> ... 1 -> 0 -> 1 -> 0 -> 1 -> ... 1ビットクロックの安全特性 （到達可能なシステム状態の集合 ）は、仕様書で適切に説明されています。
上記の仕様では、1ビットクロックの異常な状態は禁止されていますが、クロックが常にカチカチと音を立てるとは規定されていません。例えば、以下のような断続的な動作は許容されます。
0 -> 0 -> 0 -> 0 -> 0 -> ... 1 -> 1 -> 1 -> 1 -> 1 -> ... クロックが刻まないのは役に立たないため、このような動作は禁止されるべきです。解決策の一つはスタッタリングを無効にすることですが、TLA + ではスタッタリングを常に有効にする必要があります。スタッタリングのステップは仕様に記載されていないシステムの一部の変更を表し、改良に役立ちます。クロックが最終的に刻むことを保証するために、Tickに対して弱い公平性が主張されます。
Spec == Init /\ [][Tick]_<<clock>> /\ WF_<<clock>>(Tick) アクションに対する弱い公平性とは、そのアクションが継続的に有効になっている場合、最終的には実行される必要があることを意味します。Tick に対する弱い公平性では、ティック間のスタッタリング ステップは有限個しか許可されません。Tick に関するこの時間的な論理ステートメントは、ライブネス アサーションと呼ばれます。一般に、ライブネス アサーションはマシン クローズであるべきです。つまり、到達可能な状態の集合を制約するのではなく、可能な動作の集合のみを制約するべきです。[ 18 ]
ほとんどの仕様では活性特性の表明は要求されていません。安全性特性は、モデル検査とシステム実装のガイダンスの両方に十分です。[ 19 ]
TLA +はZF をベースとしているため、変数に対する演算には集合操作が含まれます。この言語には、集合のメンバーシップ、和集合、積集合、差集合、冪集合、部分集合演算子が含まれています。∨ 、∧ 、 ¬ 、 ⇒、↔、≡などの一階述語論理演算子、および全称量化子∀と存在量化子∃も含まれています。ヒルベルトのεは CHOOSE 演算子として提供され、任意の集合要素を一意に選択します。実数、整数、自然数に対する算術演算子は、標準モジュールから利用できます。
時間論理演算子は TLA +に組み込まれています。時間式はPは常に真であり、Pが最終的に真であることを意味する。演算子は次のように組み合わされる。Pが無限に真であることを意味する、または最終的にP が常に真になることを意味します。その他の時間演算子には、弱い公平性と強い公平性があります。弱い公平性 WF e ( A ) は、アクションA が継続的に有効になっている場合(つまり、中断がない場合)、最終的に実行される必要があることを意味します。強い公平性 SF e ( A ) は、アクションA が継続的に有効になっている場合(繰り返し、中断の有無にかかわらず)、最終的に実行される必要があることを意味します。
TLA +には時間的存在量化と全称量化が含まれていますが、ツールによるサポートはありません。
ユーザー定義演算子はマクロに似ています。演算子は、定義域が集合である必要がないという点で関数とは異なります。たとえば、集合メンバーシップ演算子の定義域は集合のカテゴリですが、これはZFC では有効な集合ではありません(その存在がラッセルのパラドックスにつながるため)。再帰的および匿名のユーザー定義演算子は TLA +2で追加されました。
TLA +の基本データ構造は集合です。集合は明示的に列挙するか、演算子を使用して他の集合から構築されます。ここでpはxに関する何らかの条件、またはeはxに関する何らかの関数です。唯一の空集合は として表されます。{x \in S : p}{e : x \in S}{}
TLA +の関数は、定義域である集合の各要素に値を割り当てます。は、定義域集合Sの各xに対して、f[ x ]がT[S -> T]に含まれるすべての関数の集合です。たとえば、TLA +関数は集合 の要素であるため、 はTLA +では真のステートメントです。関数は、何らかの式eに対して で定義することも、既存の関数 を変更することによって定義することもできます。Double[x \in Nat] == x*2[Nat -> Nat]Double \in [Nat -> Nat][x \in S |-> e][f EXCEPT ![v1] = v2]
レコードは TLA +における関数の一種です。レコード[name |-> "John", age |-> 35]は、name と age というフィールドを持つレコードで、 と でアクセスされr.name、r.ageレコードのセット に属します。[name : String, age : Nat]
タプルは TLA +に含まれています。タプルは明示的に定義されるか、標準の Sequences モジュールの演算子を使用して構築されます。タプルの集合はデカルト積によって定義されます。たとえば、すべての自然数のペアの集合は次のように定義されます。<<e1,e2,e3>>Nat \X Nat
TLA +には、一般的な演算子を含む標準モジュール群が用意されています。これらは構文解析器とともに配布されます。TLCモデルチェッカーは、パフォーマンス向上のためJavaによる実装を使用しています。
標準モジュールは、EXTENDSまたはINSTANCEステートメントを使用してインポートされます。
Eclipse上に統合開発環境が実装されています。これには、エラーと構文のハイライト表示機能を備えたエディタに加え、他のいくつかのTLA +ツールへのGUIフロントエンドが含まれています。
このIDEはTLAツールボックスに同梱されています。
TLCモデルチェッカーは、不変性をチェックするための TLA +仕様の有限状態モデルを構築します。TLC は仕様を満たす一連の初期状態を生成し、定義されたすべての状態遷移に対して幅優先探索を実行します。すべての状態遷移が既に発見された状態につながる場合、実行は停止します。TLC がシステム不変条件に違反する状態を発見した場合、TLC は停止し、違反状態への状態トレースパスを提供します。TLC は、組み合わせ爆発を防ぐためにモデルの対称性を宣言する方法を提供します。[ 14 ]また、状態探索ステップを並列化し、分散モードで実行してワークロードを多数のコンピュータに分散させることができます。[ 20 ]
網羅的な幅優先探索の代替として、TLCは深さ優先探索を使用したり、ランダムな動作を生成したりできます。TLCはTLA +のサブセット上で動作します。モデルは有限かつ列挙可能である必要があり、一部の時間演算子はサポートされていません。分散モードでは、TLCは活性特性をチェックしたり、ランダムな動作や深さ優先の動作をチェックしたりすることはできません。TLCはコマンドラインツールとして、またはTLAツールボックスに同梱されて利用できます。
TLA +証明システム、または TLAPS は、 TLA +で記述された証明を機械的にチェックします。これは、並行および分散アルゴリズムの正当性を証明するために、 Microsoft Research - INRIA共同センターで開発されました。証明言語は、特定の定理証明器に依存しないように設計されており、証明は宣言的なスタイルで記述され、バックエンド証明器に送信される個々の義務に変換されます。主要なバックエンド証明器はIsabelleと Zenon で、SMTソルバーCVC3、Yices、およびZ3にフォールバックします。TLAPS 証明は階層的に構造化されているため、リファクタリングが容易になり、非線形開発が可能になります。すべての前のステップが検証される前に後のステップの作業を開始でき、難しいステップはより小さなサブステップに分解されます。TLAPS は TLC とうまく連携し、モデルチェッカーは検証が開始される前に小さなエラーを迅速に検出します。その結果、TLAPS は有限モデル検査の能力を超えるシステム特性を証明できます。[ 17 ]
TLAPS は現在、実数やほとんどの時間演算子による推論をサポートしていません。Isabelle と Zenon は一般的に算術証明義務を証明できないため、SMT ソルバーを使用する必要があります。[ 21 ] TLAPS は、 Byzantine Paxos、Memoir セキュリティ アーキテクチャ、Pastry 分散ハッシュ テーブルのコンポーネント、[ 17 ]および Spire コンセンサス アルゴリズムの正当性を証明するために使用されています。 [ 22 ] TLA +ツールの他の部分とは別に配布されており、 BSD ライセンスの下で配布されるフリー ソフトウェアです。[ 23 ] TLA +2では、証明構造に対する言語サポートが大幅に拡張されました。
Microsoftでは、TLA +で仕様を記述する過程でXbox 360メモリ モジュールに重大なバグが発見されました。[ 24 ] TLA + は、ビザンチン PaxosとPastry 分散ハッシュ テーブルのコンポーネントの正当性の形式的証明を記述するために使用されました。[ 17 ]
Amazon Web Services は2011 年以来TLA + を使用しています。TLA +モデルチェックにより、 DynamoDB、S3、EBS 、および内部分散ロックマネージャのバグが発見されました。一部のバグでは、35 ステップの状態トレースが必要でした。モデルチェックは、積極的な最適化の検証にも使用されました。さらに、TLA +仕様はドキュメントおよび設計支援として価値があることがわかりました。[ 4 ] [ 25 ]
Microsoft Azure は、 5 つの異なる整合性モデルを備えたグローバル分散データベースであるCosmos DBを設計するためにTLA +を使用しました。[ 26 ] [ 27 ]
Altreonic NVはTLA +を使用してOpenComRTOSのモデルチェックを 行いました。
スナップショット分離度を持つキーバリューストア：
--------------------------- モジュール KeyValueStore --------------------------- 定数 Key、\* すべてのキーのセット。 Val、\* すべての値の集合。 TxId * すべてのトランザクション ID のセット。 VARIABLES store、* キーを値にマッピングするデータストア。 tx、* オープン状態のスナップショットトランザクションのセット。 snapshotStore、* 各トランザクションのストアのスナップショット。 書き込み、* 各トランザクション内で実行された書き込みのログ。 見逃された* 各トランザクションから見えない書き込みのセット。 ---------------------------------------------------------------------------- NoVal == \* 値がないことを示すものを選択してください。 v を選択 : v \notin Val Store == \* すべてのキーバリューストアの集合。 [キー -> Val \cup {NoVal}] Init == \* 初期述語。 /\ store = [k \in Key |-> NoVal] \* すべてのストア値は最初は NoVal です。 /\ tx = {} \* オープン トランザクションのセットは最初は空です。 /\ snapshotStore = \* すべての snapshotStore の値は最初は NoVal です。 [t \in TxId |-> [k \in Key |-> NoVal]] /\ written = [t \in TxId |-> {}] \* すべての書き込みログは最初は空です。 /\ missed = [t \in TxId |-> {}] \* ミスした書き込みはすべて最初は空です。 TypeInvariant == \* 型不変条件。 /\ ストア \in ストア /\ tx \subseteq TxId /\ snapshotStore \in [TxId -> Store] /\ [TxId -> SUBSET Key] に書き込まれました /\ が [TxId -> SUBSET Key] で見つかりませんでした TxLifecycle == /\ \A t \in tx : \* ストアがスナップショットではなく、書き込みが行われていない場合、書き込みを逃した可能性があります。 \A k \in Key : (store[k] /= snapshotStore[t][k] /\ k \notin written[t]) => k \in missed[t] /\ \A t \in TxId \ tx : \* トランザクションが破棄後にクリーンアップされていることを確認します。 /\ \A k \in Key : snapshotStore[t][k] = NoVal /\ written[t] = {} /\ missed[t] = {} OpenTx(t) == \* 新しいトランザクションを開きます。 /\ t \notin tx /\ tx' = tx \cup {t} /\ snapshotStore' = [snapshotStore EXCEPT ![t] = store] /\ 変更なし <<書き込み、見逃し、保存>> Add(t, k, v) == \* トランザクション t を使用して、キー k の下にあるストアに値 v を追加します。 /\ t \in tx /\ snapshotStore[t][k] = NoVal /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v] /\ written' = [written EXCEPT ![t] = @ \cup {k}] /\ 変更なし <<tx、欠落、ストア>> Update(t, k, v) == \* トランザクション t を使用して、キー k に関連付けられた値を v に更新します。 /\ t \in tx /\ snapshotStore[t][k] \notin {NoVal, v} /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v] /\ written' = [written EXCEPT ![t] = @ \cup {k}] /\ 変更なし <<tx、欠落、ストア>> Remove(t, k) == \* トランザクション t を使用して、ストアからキー k を削除します。 /\ t \in tx /\ snapshotStore[t][k] /= NoVal /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = NoVal] /\ written' = [written EXCEPT ![t] = @ \cup {k}] /\ 変更なし <<tx、欠落、ストア>> RollbackTx(t) == \* ストアへの書き込みをマージせずにトランザクションを閉じます。 /\ t \in tx /\ tx' = tx \ {t} /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]] /\ written' = [written EXCEPT ![t] = {}] /\ missed' = [missed EXCEPT ![t] = {}] /\ 変更なしストア CloseTx(t) == \* トランザクション t を閉じ、書き込みをストアにマージします。 /\ t \in tx /\ missed[t] \cap written[t] = {} \* 書き込み競合の検出。 /\ store' = \* snapshotStore の書き込みを store にマージします。 [k \in Key |-> IF k \in written[t] THEN snapshotStore[t][k] ELSE store[k]] /\ tx' = tx \ {t} /\ missed' = \* 他のオープン トランザクションの書き込み漏れを更新します。 [otherTx \in TxId |-> IF otherTx \in tx' THEN missed[otherTx] \cup written[t] ELSE {}] /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]] /\ written' = [written EXCEPT ![t] = {}] Next == \* 次の状態の関係。 \/ \E t \in TxId : OpenTx(t) \/ \E t \in tx : \E k \in Key : \E v \in Val : Add(t, k, v) \/ \E t \in tx : \E k \in Key : \E v \in Val : Update(t, k, v) \/ \E t \in tx : \E k \in Key : Remove(t, k) \/ \E t \in tx : RollbackTx(t) \/ \E t \in tx : CloseTx(t) Spec == \* Init で状態を初期化し、Next で遷移します。 初期化 /\ [][次へ]_<<ストア、トランザクション、スナップショットストア、書き込み済み、欠落>> ---------------------------------------------------------------------------- 定理仕様 => [](TypeInvariant /\ TxLifecycle) ============================================================================= デザインを正確に説明しようとすると、見落としがちな微妙な相互作用や「特殊なケース」といった問題点が明らかになることが多い。
もし書いてしまったとしたら、それはたいてい間違いです。
実際、[ほとんどのエンジニア]は、安全性の特性のみを表し、変数を隠蔽しない形式(8.38)の仕様で十分うまくやっていける。
{{cite AV media}}: CS1メンテナンス: 場所 (リンク)