TLA+
TLA+
TLA+は、Leslie Lamportによって開発された形式仕様言語。並行システムと分散システムの設計、モデル化、文書化、および検証に使用される。 TLA+は、網羅的にテスト可能な擬似コードとして説明されており、その使用はソフトウェアシステムの設計図を描くことに喩えられる。  TLAはTemporal Logic of Actionsの頭字語である。
設計と文書化に関して、TLA+ は非公式の技術仕様と同じ目的を果たす。ただし、TLA+の仕様は論理学と数学の形式言語で記述されており、この言語で記述された仕様の精度は、システムの実装が始まる前に設計上の欠陥を明らかにすることを目的としている。
TLA+のコードは形式言語で記述するため、有限モデル検査に適する。モデルチェッカーは、いくつかの実行ステップまでのすべての可能なシステム動作を見つけ、安全性や活性などの望ましい不変性プロパティの違反を調べる。 TLA+のコードでは、基本的な集合論を使用して安全性(悪いことが起こらない事)を定義し、時相論理を使用して活性(良いことがいずれ起こる事)を定義する。
TLA+は、アルゴリズムと数学的定理の両方について、マシンでチェックされた正確性の証明を作成するためにも使用される。証明は、単一の定理証明者バックエンドに依存しない宣言型の階層スタイルで記述される。公式および非公式の構造化された数学的証明は、TLA+で記述できる。言語はLaTeXに似ており、TLA+のコードをLaTeXドキュメントに翻訳するためのツールが存在する。
TLA+は、並行システムの検証方法に関する数十年の研究の後、1999年に公開された。その後、IDEや分散モデルチェッカーなどのツールチェーンが開発された。擬似コードのような言語PlusCalは2009年に作成され、TLA+にトランスパイルされ、シーケンシャルアルゴリズムを記述する際に有用とされる。 TLA+2は2014年に発表され、プルーフコンストラクトの言語サポートを拡張した。現在のTLA+リファレンスは、LeslieLamportによるTLA+Hyperbookである。
現代の時相論理は、1957年にアーサー・プライアーによって開発され、当時は時制論理と呼ばれていた。アミール・プヌーリが、コンピュータサイエンスへの時相論理の適用を真剣に研究した最初の人物だったが、アーサー・プライアーは1967年の10年前に既にその使用について予測していた。
プヌーリは、コンピュータープログラムの指定と推論における時相論理の使用を研究し、1977年に線形時相論理を導入した。 線形時相論理は、排他制御やデッドロックの解決などの特性を簡単に表現する、並行プログラムの分析のための重要なツールとなった。
プヌーリの線形時相論理に関する研究と同時に、学者はマルチプロセスプログラムの検証のためにホーア論理を一般化するために取り組んでいた。レスリー・ランポートは、ピアレビューで相互排除について提出した論文に誤りが見つかった後、この問題に関心を持つようになった。 Ed Ashcroftは、1975年の論文「Proving Assertions About Parallel Programs」で不変性を紹介した。これは、Lamportが1977年の論文「Proving Correctness of Multiprocess Programs」でFloydの方法を一般化するために使用した。ランポートの論文はまた、部分正当性と終了の一般化として、それぞれ安全性と活性を紹介した。 この方法は、EdsgerDijkstraによる1978年の論文で最初の同時ガベージコレクションアルゴリズムを検証するために使用された。
ランポートは、スーザンオウィッキが主催したスタンフォードでの1978年のセミナーで、プヌーリのLTLに最初に遭遇しました。ランポートによると「時相論理は、実用化されそうもなく抽象的で無意味だと確信していたが、楽しそうだったので参加した。」 との事であったが、1980年に彼は「'Sometime' is Sometimes 'Not Never'」を出版し、時相論理の文献で最も頻繁に引用される論文の1つとなった。  ランポートは、SRI在籍中に時相論理仕様の作成に取り組んだが、このアプローチは実用的ではないとわかった。
彼が実用的な仕様方法を模索した結果として1983年に論文「Specifying Concurrent Programming Modules」が生まれた。この論文では、状態遷移をプライム変数と非プライム変数のブール値関数として記述するというアイデアが導入されている。 その模索は1980年代に継続され、ランポートは1990年にアクションの時相論理に関する論文群の発表を開始した。しかし、1994年に「アクションの時相論理」が発表されるまでは正式には導入されなかった。 TLAは、時間式でのアクションの使用を可能にした。これは、ランポートによれば、「並行システム検証で使用されるすべての推論を形式化および体系化するための洗練された方法を提供する。」とされている。
TLAの仕様は、ほとんどが通常の非時相論的数学で構成されていたが、Lamportは、純粋な時間的仕様よりも煩わしさが少ないと発見した。 TLAは、1999年に論文「Specifying Concurrent Systems with TLA+」で紹介され、TLA+の仕様記述言語としての数学的基礎を提供した。同じ年の後半に、YuanYuはTLA+仕様のTLCモデルチェッカーを作成した。 TLCは、Compaqマルチプロセッサのキャッシュコヒーレンスプロトコルのエラーを見つけるために使用された。
ランポートは、2002年に「Specifying Systems:TLA+ Language and Tools for Software Engineers」というタイトルの+に関する完全な教科書を発行した。  PlusCalは2009年に導入され 、TLA+プルーフシステム(TLAPS)は2012年、 TLA+2は2014年に発表され、いくつかの言語構造が追加され、プルーフシステムの言語内サポートが大幅に増加した。  ランポートは、更新されたTLA+のリファレンスである「The TLA+ Hyperbook」の作成に取り組んでいる。未完成な作品は彼の公式ウェブサイトから入手できる。Lamportは、TLA+ビデオコースも作成している。このコースでは、「プログラマーとソフトウェアエンジニアにTLA+コードの記述方法を教える入門から始まる一連のビデオレクチャーを作りかけている」と説明されている。
TLA+コードは複数のモジュールからなる。モジュールは、他のモジュールを拡張(インポート)して、その機能を使用できる。 TLA+標準はタイプセット数学記号で指定されているが、既存のTLA+ツールは、ASCIIでLaTeXのような記号定義を使用する。 TLA+では、定義が必要ないくつかの用語を使用する。
State – 変数への値の代入
Behaviour – 連続したState
Step – Behaviourでの連続したStateのペア
Shuttering step – 変数が変更されないStep
Next-state relation – 変数が任意のStepでどのように変化するかを説明する関係
State function – Next-state relationではない変数と定数を含む式
State predicate – ブール値の状態関数
Invariant – 到達可能なすべてのStateで真とする状態述語
Temporal formula – 時相論理のステートメントを含む式
TLA+は、すべての正しいシステム動作のBehaviorを定義することを目的としている。例えば、0と1の間で際限なく刻々と変化する1ビットクロックは、次のように記述できる。Relation Tickはクロックが1であればclock'(次のStateにおけるclockの値)は0、0であれば1を設定する。clockの値が0または1の場合、State PredicateであるInitはtrueである。 Specは、1ビットクロックのすべてのBehaviorが最初にInitを満たし、すべてのStepがTickに一致するか、Shuttering stepである必要があることをアサートするTemporal formulaである。そのような2つの動作は次の通りである。1ビットクロックの安全性は –到達可能なシステム状態の集合 –という仕様によって適切に説明される。
上記の仕様では、1ビットクロックの奇妙な状態は許可されていないが、クロックが常に変化するとは言っていない。たとえば、次のような永続的なShuttering stepが起こりうる。変化しない時計は役に立たないので、これらの振る舞いは禁止されるべきである。 1つの解決策はShuttering stepを無効にする事であるが、TLA+では常にShutteringを有効にする必要がある。Shuttering stepは、仕様に記載されていないシステムの一部への変更を表し、改良に有用である。最終的にTickしなければならないクロックを確保するために、弱い公平性がTickのためにアサートできる。アクションに対する公平性が弱いということは、そのアクションが継続的に有効になっている場合は、最終的に実行する必要があることを意味する。Tickの公平性が弱いため、ティック間で許可されるShuttering stepの数は限られている。 Tickに関するこの時相論理ステートメントは、活性アサーションと呼ばれる。一般に、活性アサーションはマシンで閉じる必要がある。到達可能な状態のセットを制約するのではなく、可能な動作のセットのみを制約する必要がある。
ほとんどの仕様では、活性の表明は必要ない。安全性特性だけでモデル検査とシステム実装の両方に対して事足りる。
TLA+はZFに基づいているため、変数の操作にはセット操作が含まれる。言語には、集合元、和集合、共通部分集合、差集合、べき集合、および部分集合演算子が含まれる。 ∨ 、 ∧ 、 ¬ 、 ⇒ 、 ↔ 、 ≡などの一階述語論理演算子、および全称記号および存在記号∀と∃も含まれている。ヒルベルトのεは、任意の集合要素を一意に選択するCHOOSE演算子として提供される。実数、整数、自然数の算術演算子は、標準モジュールから利用可能である。
時相論理演算子はTLA+に組み込まれている。時間式では\Box P を"Pが常に真である"を意味し、 \Diamond Pを "Pが最終的に真となる"を意味するという使い方をする。演算子は結合され\Box \Diamond Pは"Pが無限に頻繁に真である"を意味する、または\Diamond \Box Pは、"最終的にPは常に真になる"という意味となる。他の時相演算子には、弱い公平性と強い公平性が含まれる。弱い公平を表すWFe(A)は、アクションAが連続して(つまり絶え間なく)有効になっている場合、それが最終的に実施される事を意味する。強い公平を表すSFe(A)アクションAは、(中断の有無にかかわらず、繰り返し)継続的に有効になっている場合は、それが最終的に実施される事を意味する。
ツールからのサポートはないが時相論的な存在記号と全称記号はTLA+に含まれている。
ユーザー定義の演算子はマクロに似ている。演算子は、ドメインが集合である必要がないという点において関数とは異なる。たとえば、集合のメンバーシップ演算子は、そのドメインとして集合の圏を持つが、これはZFCでは有効な集合ではない(その存在はラッセルのパラドックスにつながるため)。再帰的で匿名のユーザー定義演算子がTLA+2に追加された。
TLA+の基本的なデータ構造とは集合である。集合は、明示的に列挙されるか、演算子を使用するか、  (pはxの条件)または (eはxの関数)を使用して他の集合から構築される。一意の空集合は{}として表される。
TLA+の関数は、ドメイン内の各要素集合に値を割り当てる。 [S -> T]は、定義域集合Sの各xについて、Tにf [x]を持つすべての関数の集合である。例えばTLA+関数Double[x \in Nat] == x*2 とは集合 [Nat -> Nat]の一要素であるため、 Double \in [Nat -> Nat]はTLA+の真のステートメントである。関数は、一部の式e [x \in S |-> e]を使用するか、既存の関数を変更することによっても定義される[f EXCEPT ![v 1 ] = v 2 ] 。
レコードはTLA+の関数の一種である。レコード[name |-> "John", age |-> 35]は、フィールドnameとageを持つレコードであり、 r.nameやr.ageでアクセスされ、レコードの集合[name : String, age : Nat]に所属する。
タプルはTLA+に含まれている。 <<e>>は明示的に定義されるか、標準のシーケンスモジュールの演算子で構成される。タプルの集合は、デカルト積によって定義される。たとえば、自然数のすべてのペアの集合は、 Nat \X Natとして定義される。
TLA+には、一般的な演算子を含む一連の標準モジュールがある。それらは構文アナライザーで配布される。 TLCモデルチェッカーは、パフォーマンスを向上させるためにJava実装を使用する。
FiniteSets :有限集合を扱うためのモジュール。 IsFiniteSet(S)およびCardinality(S)演算子を提供する。
Sequences: Len(S)、Head(S)、Tail(S)、Append(S、E) 、連結、フィルターなどのタプルの演算子を定義する。
Bags: 多重集合を扱うためのモジュール。プリミティブな集合演算の類似物と重複カウントを提供する。
Naturals: 不等式および算術演算子とともに自然数を定義する。
Integers:整数を定義する。
Reals:実数と除算と無限大を定義する。
RealTime:リアルタイムのシステム仕様で役立つ定義を提供する。
TLC :ロギングやアサーションなど、モデルでチェックされた仕様のユーティリティ関数を提供する。
標準モジュールはEXTENDSまたはINSTANCEステートメントでインポートされる。
TLA+ Toolbox
統合開発環境はEclipseの上に実装されている。これには、エラーとシンタックスハイライトを備えたエディターに加えて、他のいくつかのTLA+ツールへのGUIフロントエンドが含まれる。
SANY構文アナライザー。仕様を解析して構文エラーをチェックする。
pretty-printされた仕様を生成するためのLaTeXトランスレータ。
PlusCalトランスレータ。
TLCモデルチェッカー。
TLAPSプルーフシステム。
IDEはTLAツールボックスで配布される。
TLCモデルチェッカーは、不変性プロパティをチェックするためのTLA+コードの有限状態モデルを構築する。 TLCは、仕様を満たす初期状態のセットを生成し、定義されたすべての状態遷移に対して幅優先探索を実行する。すべての状態遷移がすでに検出された状態につながると、実行は停止する。 TLCがシステム不変条件に違反する状態を検出すると、TLCは停止し、問題のある状態への状態トレースパスを提供する。 TLCは、組み合わせ爆発を防ぐためにモデルの対称性を宣言する方法を提供する。また並列計算状態探索ステップを並列化し、分散モードで実行して、ワークロードを多数のコンピューターに分散させる事もできる。
徹底的な幅優先探索の代わりに、TLCは深さ優先探索を使用するか、ランダムな動作を生成できる。 TLCはTLA+のサブセットで動作する。モデルは有限で列挙可能でなければならず、一部の時相演算子はサポートされていない。分散モードでは、TLCは活性特性をチェックすることも、ランダムまたは深さ優先の動作をチェックすることもできない。 TLCは、コマンドラインツールとして、またはTLAツールボックスにバンドルされて利用できる。
TLA+プルーフシステム(TLAPS)は、TLA+で記述されたプルーフを機械的にチェックする。これは、Microsoft Research - INRIA Joint Centerで開発され、並行アルゴリズムと分散アルゴリズムの正確性を証明する。証明言語は、特定の定理証明者から独立するように設計されており、証明は宣言型で記述され、複数の個別の義務として変換されバックエンドの証明者に送信される。主なバックエンドの証明者はIsabelleとZenonであり、 SMTソルバーCVC3 、 Yices 、およびZ3定理証明者にフォールバックする。 TLAPSプルーフは階層構造になっているため、リファクタリングが容易になり、非線形開発が可能となる。前のすべてのステップが検証される前に、後のステップで作業を開始でき、難しいステップはより小さなサブステップに分解される。モデルチェッカーは検証が開始される前に小さなエラーをすばやく見つけるため、TLAPSはTLCとうまく連携する。同様にしてTLAPSは、有限モデル検査の機能を超えるシステムプロパティを証明できる。
TLAPSは現在、実数による推論も、ほとんどの時間演算子もサポートしない。 IsabelleとZenonは通常、算術証明の義務を証明できないため、SMTソルバーを使用する必要がある。  TLAPSは、ビザンチンPaxos 、Memoirセキュリティアーキテクチャ、およびPastry分散ハッシュテーブルのコンポーネントの正当性を証明するために使用されている。
これは他のTLA+ツールとは別に配布され、BSDライセンスの下で配布されるフリーソフトウェアである。  TLA+2は、プルーフコンストラクトの言語サポートを大幅に拡張した。
Microsoftでは、TLA+で仕様を作成する過程で、 Xbox 360メモリモジュールに重大なバグを発見した。  TLA+は、ビザンチンPaxosおよびPastry分散ハッシュテーブルのコンポーネントの正式な証明を作成するために使用された。
アマゾンウェブサービスは2011年からTLA+を使用している。TLA+モデル検査によってDynamoDB 、 S3 、 EBS、および内部分散ロックマネージャーでバグを発見。一部のバグには、35ステップの状態トレースが必要であった。モデル検査は、積極的な最適化を検証するためにも使用された。さらに、TLA+仕様は、文書化および設計支援としての価値があることを確認した。
MicrosoftのAzureは、TLA+を使用して5つの異なる一貫性モデルをもち世界規模に分散したデータベースであるCosmos DBを設計した。