目次

はじめに

これは「TLA+入門」コースのコンスペクトの一連のブログ投稿の第2回目です（第1回目はこちら[1]）。いつものように、すべての功績はレスリー・ランポートと彼のウェブサイトで見つけることができる彼のコースにあります。この部分では、_トランザクションコミット_と_ツーフェーズコミット_アルゴリズムを考察します。

トランザクションコミット

最初の部分では、_トランザクションコミット_アルゴリズム[3]（2～4ページ）を考察します。分散システムでは、トランザクションコミットには、異なるノード間で複数のリソースマネージャー（RM）が関与し、彼らは全員一致でトランザクションをコミットまたは中止することを決定しなければなりません。このプロトコルは、すべてのRMがコミット状態または中止状態に達することを保証し、安定性と一貫性の条件によってサポートされます。これらの条件は、RMがこれらの状態のいずれかに達したら戻れないこと、そしてどのRMも反対の状態になれないことを要求します。

データベーストランザクションは、_リソースマネージャー_と呼ばれるプロセスの集合によって実行されます。トランザクションは_コミット_または_中止_することができます。すべてのリソースマネージャーがコミットする準備ができている場合にのみコミットでき、いずれかのリソースマネージャーが中止したい場合は中止しなければなりません。

すべてのリソースマネージャーは、トランザクションがコミットされたか中止されたかについて合意しなければなりません。

pcwrooemrpmkaiirtneegddaborted

図1：各リソースマネージャーの状態/遷移図

次に、詳細を含むトランザクションコミット仕様を考察します。完全なテキストは以下の黒い三角形の下にあります。

完全なTCommit仕様のテキストはこちら
------------------------------ MODULE TCommit ------------------------------
(***************************************************************************)
(* この仕様は「トランザクションコミット」、TLA+ビデオコースのレクチャー5で説明されています。*)
(***************************************************************************)
CONSTANT RM       \* 参加するリソースマネージャーの集合

VARIABLE rmState  \* rmState[rm]はリソースマネージャーrmの状態を表す。
-----------------------------------------------------------------------------
TCTypeOK == 
  (*************************************************************************)
  (* 型の正当性の不変条件                                                *)
  (*************************************************************************)
  rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
            
TCInit ==   rmState = [r \in RM |-> "working"]
  (*************************************************************************)
  (* 初期述語。                                                          *)
  (*************************************************************************)

canCommit == \A r \in RM : rmState[r] \in {"prepared", "committed"}
  (*************************************************************************)
  (* すべてのRMが「prepared」または「committed」状態にある場合に真。     *)
  (*************************************************************************)

notCommitted == \A r \in RM : rmState[r] # "committed" 
  (*************************************************************************)
  (* どのリソースマネージャーもコミットを決定していない場合に真。       *)
  (*************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* 次に、RMが実行できるアクションを定義し、仕様の完全な次状態アクションを可能なRMアクションの選言と定義します。 *)
(***************************************************************************)
Prepare(r) == /\ rmState[r] = "working"
              /\ rmState' = [rmState EXCEPT ![r] = "prepared"]

Decide(r)  == \/ /\ rmState[r] = "prepared"
                 /\ canCommit
                 /\ rmState' = [rmState EXCEPT ![r] = "committed"]
              \/ /\ rmState[r] \in {"working", "prepared"}
                 /\ notCommitted
                 /\ rmState' = [rmState EXCEPT ![r] = "aborted"]

TCNext == \E r \in RM : Prepare(r) \/ Decide(r)
  (*************************************************************************)
  (* 次状態アクション。                                                   *)
  (*************************************************************************)
-----------------------------------------------------------------------------
TCConsistent ==  
  (*************************************************************************)
  (* 2つのRMが矛盾する決定に達していないことを主張する状態述語。これは仕様の不変条件です。 *)
  (*************************************************************************)
  \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted"
                       /\ rmState[r2] = "committed"
-----------------------------------------------------------------------------
(***************************************************************************)
(* 以下の部分はビデオレクチャー5では説明されていません。ビデオレクチャー8で説明されます。 *)
(***************************************************************************)
TCSpec == TCInit /\ [][TCNext]_rmState
  (*************************************************************************)
  (* 時相論理式として書かれたプロトコルの完全な仕様。                   *)
  (*************************************************************************)

THEOREM TCSpec => [](TCTypeOK /\ TCConsistent)
  (*************************************************************************)
  (* この定理は、状態述語TCTypeOK /\ TCInvariantが仕様TCSpecの不変条件であることを主張します。この連言の不変性は、TCTypeOKとTCConsistentの両方の不変性と同等です。 *)
  (*************************************************************************)

=============================================================================

$TLA^+$では、すべての値は集合ですが、$TLA^+$のセマンティクスは集合の要素が何であるかを示していません。 式 rmState \in [RM -> {"working", "prepared", "committed", "aborted"}] は、図1に従って rmState が取り得る可能な状態の集合を表しています。

TCInit は初期の rmState を宣言し、それはインデックス集合 RM を持つ配列で、各リソースマネージャー rm に対して $[r \in RM \mapsto working][rm]$ は配列であり、rm に適用されると文字列 $working$ となります。すべての $r$ が $RM$ において。

簡単に言えば：$\forall r \in RM, RM(rm) = working$。

$TLA^+$ の配列式の構文は次のとおりです：$[ \text{variable} \in \text{set} \mapsto \text{expression}]$、ここで $\mapsto$ はASCIIでは |-> のように見えます。

例：sqr = [ i \in 1..42 |-> i**2] は、sqr[i] = i**2 となるインデックス集合が1から42までの配列 sqr を定義します。

同じものに対してプログラミングと数学で使用される用語

プログラミング、数学、そして $TLA^+$ で使用される用語を考慮する必要があります。各行の用語は同等です。

プログラミング数学
配列関数
インデックス集合関数の定義域
$f[e]$$f(e)$

$TLA^+$ ではプログラムではなく式を書きますので、関数と定義域の用語を使用します。ただし、他の数学的操作とのあいまいさを避けるために $f[e]$ 記法が使用されます。

$TLA^+$ は、関数がその定義域として任意の集合を持つことを許します。たとえば、すべての整数の集合など、無限の集合でも可能です。

リソースマネージャーの状態遷移を定義する $Prepare$ と $Decide$ の式を含む一連の式を考えます。

式 $\exists r \in RM : Prepare(r) \lor Decide(r)$ は、$RM$ の集合にあるある $r$ が存在し、$Prepare(r) \lor Decide(r)$ が真である場合に真となります。

例えば、RM = { "r1", "r2", "r3", "r4" } とすると、この式は次の選言の集合に等しくなります。

\/ Prepare("r1") \/ Decide("r1")
\/ Prepare("r2") \/ Decide("r2")
\/ Prepare("r3") \/ Decide("r3")
\/ Prepare("r4") \/ Decide("r4")

$\exists$ は r を式に局所的に宣言します。

この式を $\exists r$ ではなく $\forall r$ で定義した場合は次のようになります：$\forall r \in RM : \text{Prepare}(r) \lor \text{Decide}(r)$。これは「すべての $r$ が $\text{RM}$ において…」と読みます。上記と同じ $\text{RM}$ の値に関する仮定で、この式は次のようになります。

/\ Prepare("r1") \/ Decide("r1")
/\ Prepare("r2") \/ Decide("r2")
/\ Prepare("r3") \/ Decide("r3")
/\ Prepare("r4") \/ Decide("r4")

RMの遷移グラフを思い出してください。 $Prepare(r)$ はリソースマネージャー $r$ の状態 $working \rightarrow prepared$ を記述します。 このステップは、$r$ の現在の状態が $working$ である場合にのみ行うことができます。 $Prepare(r) \equiv \land rmState[r] = working$ であり、$\land rmState[r] = working$ は真でなければなりません。

仕様は、新しい状態 $rmState’[r] = prepared$ が何であるかを述べることはできません。$rmState’$ 関数全体が何であるかを述べる必要があります。この関数の値は、次のような定義域 $RM$ の関数でなければなりません：$rmState’ = [s \in RM \mapsto …]$、ここで $…$ は各リソースマネージャー $s$ に対する $rmState[s]$ の新しい値で置き換える必要があります。

もし $s$ がリソースマネージャー $r$ であれば、新しい状態での $RM$ の状態の値は $prepared$ でなければなりません。他のリソースマネージャーは新しい状態で古い状態と同じ値を持つべきです。

完全な定義は次のとおりです： $$ \begin{split} \text{Prepare}(r) \equiv & \land rmState[r] = \text{working} \\ & \land rmState' = [rmState \text{ EXCEPT } ![r] = \text{prepared}] \end{split} $$

$\text{Decide}(r)$ は、リソースマネージャー $r$ が $\text{committed}$ または $\text{aborted}$ 状態に達する可能なステップを記述します。これは2つの式の選言であり、$r$ が $\text{prepared}$ 状態にある場合にのみ起こり得る遷移 $\text{prepared} \rightarrow \text{committed}$ を記述しています。

$r$ は、すべてのリソースマネージャーが $\text{prepared}$ または $\text{committed}$ 状態にある場合にのみコミットできます。2番目の選言は、$\text{aborted}$ 状態への可能な遷移を記述しています。この遷移は、$r$ の状態が $\text{working}$ または $\text{prepared}$ 状態である場合に起こり得ます。$r$ は、他のリソースマネージャーが $\text{committed}$ でない場合にのみ中止できます。

$$ \begin{split} \text{Decide}(r) \equiv \lor & \land rmState[r] = \text{prepared} \\ & \land \text{canCommit} \\ & \land rmState' = [rmState \text{ EXCEPT } ![r] = \text{committed}] \\ \lor & \land rmState[r] \in \{ \text{working}, \text{prepared} \} \\ & \land \text{notCommitted} \\ & \land rmState' = [rmState \text{ EXCEPT } ![r] = \text{aborted}] \end{split} $$

ここで、2つの式 $\text{canCommit}$ と $\text{notCommitted}$ を定義できます。

すべてのリソースマネージャーが $\text{prepared}$ または $\text{committed}$ 状態にある場合にのみトランザクションをコミットできます：$\forall s \in \text{RM} : \text{rmState}[s] \in \{ \text{prepared}, \text{committed} \}$。 トランザクションは、すべてのリソースマネージャーの状態が $\text{committed}$ でない場合にコミットされません：$\forall s \in \text{RM} : \text{rmState}[s] \neq \text{committed}$。

モデルをチェックするには、チェックすべき不変条件（常に $true$ である式）を提供する必要があることを覚えておくことが重要です。この不変条件は次のように提示されます。

$$ \begin{split} TCConsistent \equiv \forall r1, r2 \in RM : & \neg \land rmState[r1] = \text{aborted} \\ & \land rmState[r2] = \text{committed} \end{split} $$

$TCommit$ 仕様を考察し、使用されている式とそのセマンティクスに慣れたところで、より高度な例である ツーフェーズコミット アルゴリズムを進めることができます。

ツーフェーズコミット

ツーフェーズコミット アルゴリズムを理解するために、関連する資料を読むことをお勧めします（[3]、5～7ページ）し、マーティン・クレップマンのビデオを見ることをお勧めします。これは彼の素晴らしい 分散システム コースの一部です。

要するに、分散システムにおける ツーフェーズコミット プロトコルは、トランザクションマネージャー（TM）がリソースマネージャー（RM）間のコミットプロセスを調整し、RMはトランザクションをコミットまたは中止するために2段階の通信プロセスに従います。プロトコルは、RMが準備状態に入り、TMに信号を送り、TMはすべてのRMに準備を指示します。すべてのRMが準備できていれば、TMは彼らにコミットを命じ、RMが準備できない場合は中止を命じます。この方法は一貫性を確保しますが、コストがかかり、TMが故障した場合にブロックされやすくなります。

ツーフェーズコミット アルゴリズムの仕様を考察する前に、$TLA^+$ における レコード の概念を理解する必要があります。

$r \equiv [ \text{prof} \mapsto \text{“Fred”}, \text{num} \mapsto 42]$ は、2つのフィールド $\text{prof}$ と $\text{num}$ を持つ レコード を定義します。これはおおよそ C の struct に対応します。

このレコードは、定義域が $\{\text{“prof”},\text{“num”}\}$ である関数 $f$ であり、$f[\text{“prof”}] = \text{“Fred”}$、$f[\text{“num”}] = 42$ となります。実際には、レコードのフィールドはドット記法 $f.\text{prof}$ でアクセスでき、これは $f[\text{“prof”}]$ の省略形です。

$[f \text{ EXCEPT } ![\text{“prof”}]=\text{“Red”}]$ は、$\text{“prof”}$ フィールドが $\text{“Red”}$ に等しいことを除いて $f$ と同じレコードに等しいです。この式は $[f \text{ EXCEPT } .\text{prof} = \text{“Red”}]$ とも書けます。

では、詳細を含む ツーフェーズコミット 仕様を考察します。完全なテキストは以下の黒い三角形の下にあります。

完全なTwoPhase仕様のテキストはこちら
------------------------------ MODULE twophase ------------------------------

(***************************************************************************)
(* この仕様は「ツーフェーズコミット」、TLA+ビデオコースのレクチャー6で議論されています。これは、トランザクションマネージャー（TM）がリソースマネージャー（RM）を調整してモジュールTCommitのトランザクションコミット仕様を実装するツーフェーズコミットプロトコルを記述しています。この仕様では、RMは自発的にPreparedメッセージを発行します。TMがRMに送るPrepareメッセージは無視します。*)
(* *)
(* 簡略化のため、RMが中止を決定したときに送信するAbortメッセージも省略します。そのようなメッセージは、TMがトランザクションを中止する原因となります。これはここではTMが自発的に中止を決定するイベントとして表現されます。*)
(***************************************************************************)
CONSTANT RM  \* リソースマネージャーの集合

VARIABLES
  rmState,       \* rmState[r] はリソースマネージャー r の状態。
  tmState,       \* トランザクションマネージャーの状態。
  tmPrepared,    \* TMが「Prepared」メッセージを受信したRMの集合。
  msgs           
    (***********************************************************************)
    (* プロトコルでは、プロセスはメッセージを送信することで互いに通信します。簡単のため、送信されたすべてのメッセージの集合である変数msgsでメッセージ送信を表現します。メッセージはmsgs集合に追加することで送信されます。実装では、特定のメッセージの受信によって有効になるアクションは、ここではmsgsにそのメッセージが存在することで有効になります。簡単のため、メッセージはmsgsから削除されません。これにより、単一のメッセージが複数の受信者によって受信されることが可能になります。同じメッセージを2回受信することも許されますが、この特定のプロトコルでは問題ありません。*)
    (***********************************************************************)

Messages ==
  (*************************************************************************)
  (* すべての可能なメッセージの集合。タイプが「Prepared」のメッセージは、そのメッセージのrmフィールドで示されるRMからTMに送信されます。タイプが「Commit」および「Abort」のメッセージはTMによってブロードキャストされ、すべてのRMが受信します。集合msgsにはそのようなメッセージの単一のコピーのみが含まれます。*)
  (*************************************************************************)
  [type : {"Prepared"}, rm : RM]  \cup  [type : {"Commit", "Abort"}]
   
TPTypeOK ==  
  (*************************************************************************)
  (* 型の正当性の不変条件                                                *)
  (*************************************************************************)
  /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
  /\ tmState \in {"init", "done"}
  /\ tmPrepared \subseteq RM
  /\ msgs \subseteq Messages

TPInit ==   
  (*************************************************************************)
  (* 初期述語。                                                          *)
  (*************************************************************************)
  /\ rmState = [r \in RM |-> "working"]
  /\ tmState = "init"
  /\ tmPrepared   = {}
  /\ msgs = {}
-----------------------------------------------------------------------------
(***************************************************************************)
(* 次に、プロセスが実行できるアクションを定義します。まずTMのアクション、次にRMのアクションです。 *)
(***************************************************************************)
TMRcvPrepared(r) ==
  (*************************************************************************)
  (* TMがリソースマネージャーrから「Prepared」メッセージを受信します。既にtmPreparedにrが含まれている場合、このアクションを無効にする追加の有効化条件r \notin tmPreparedを追加することもできます。しかし、その必要はありません。その場合、アクションは効果がなく、状態は変更されません。*)
  (*************************************************************************)
  /\ tmState = "init"
  /\ [type |-> "Prepared", rm |-> r] \in msgs
  /\ tmPrepared' = tmPrepared \cup {r}
  /\ UNCHANGED <<rmState, tmState, msgs>>

TMCommit ==
  (*************************************************************************)
  (* TMがトランザクションをコミットします。TMが初期状態にあり、すべてのRMが「Prepared」メッセージを送信した場合に有効です。*)
  (*************************************************************************)
  /\ tmState = "init"
  /\ tmPrepared = RM
  /\ tmState' = "done"
  /\ msgs' = msgs \cup {[type |-> "Commit"]}
  /\ UNCHANGED <<rmState, tmPrepared>>

TMAbort ==
  (*************************************************************************)
  (* TMが自発的にトランザクションを中止します。                        *)
  (*************************************************************************)
  /\ tmState = "init"
  /\ tmState' = "done"
  /\ msgs' = msgs \cup {[type |-> "Abort"]}
  /\ UNCHANGED <<rmState, tmPrepared>>

RMPrepare(r) == 
  (*************************************************************************)
  (* リソースマネージャーrが準備します。                                 *)
  (*************************************************************************)
  /\ rmState[r] = "working"
  /\ rmState' = [rmState EXCEPT ![r] = "prepared"]
  /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]}
  /\ UNCHANGED <<tmState, tmPrepared>>
  
RMChooseToAbort(r) ==
  (*************************************************************************)
  (* リソースマネージャーrが自発的に中止を決定します。上記で述べたように、この仕様ではrはメッセージを送信しません。*)
  (*************************************************************************)
  /\ rmState[r] = "working"
  /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
  /\ UNCHANGED <<tmState, tmPrepared, msgs>>

RMRcvCommitMsg(r) ==
  (*************************************************************************)
  (* リソースマネージャーrがTMからコミットするように指示されます。     *)
  (*************************************************************************)
  /\ [type |-> "Commit"] \in msgs
  /\ rmState' = [rmState EXCEPT ![r] = "committed"]
  /\ UNCHANGED <<tmState, tmPrepared, msgs>>

RMRcvAbortMsg(r) ==
  (*************************************************************************)
  (* リソースマネージャーrがTMから中止するように指示されます。         *)
  (*************************************************************************)
  /\ [type |-> "Abort"] \in msgs
  /\ rmState' = [rmState EXCEPT ![r] = "aborted"]
  /\ UNCHANGED <<tmState, tmPrepared, msgs>>

TPNext ==
  \/ TMCommit \/ TMAbort
  \/ \E r \in RM : 
       TMRcvPrepared(r) \/ RMPrepare(r) \/ RMChooseToAbort(r)
         \/ RMRcvCommitMsg(r) \/ RMRcvAbortMsg(r)
-----------------------------------------------------------------------------
(***************************************************************************)
(* 以下の部分はビデオレクチャー6では説明されていません。ビデオレクチャー8で説明されます。 *)
(***************************************************************************)

TPSpec == TPInit /\ [][TPNext]_<<rmState, tmState, tmPrepared, msgs>>
  (*************************************************************************)
  (* ツーフェーズコミットプロトコルの完全な仕様。                        *)
  (*************************************************************************)

THEOREM TPSpec => []TPTypeOK
  (*************************************************************************)
  (* この定理は、型の正当性の述語TPTypeOKが仕様の不変条件であることを主張します。 *)
  (*************************************************************************)
-----------------------------------------------------------------------------
(***************************************************************************)
(* 次に、ツーフェーズコミットプロトコルがモジュールTCommitのトランザクションコミットプロトコルを実装していることを主張します。以下の文は、モジュールTCommitからすべての定義を現在のモジュールにインポートします。 *)
(***************************************************************************)
INSTANCE TCommit 

THEOREM TPSpec => TCSpec
  (*************************************************************************)
  (* この定理は、ツーフェーズコミットプロトコルの仕様TPSpecがトランザクションコミットプロトコルの仕様TCSpecを実装していることを主張します。 *)
  (*************************************************************************)
(***************************************************************************)
(* このモジュールの2つの定理は、6つのRMでTLCによってチェックされ、50816の到達可能な状態を持つ構成が1GHzのPCで約1分で完了しました。 *)
(***************************************************************************)
=============================================================================

この仕様では $CONSTANT RM$ と $VARIABLES rmState$ は前の仕様と同じです。 変数 $tmState$ と $tmPrepared$ はトランザクションマネージャーの状態を示し、$RM$ の状態を追跡します。トランザクションマネージャーは、リソースマネージャーがどの状態で $\text{“committed”}$ であるかを記憶し、すべてのリソースマネージャーから $\text{“committed”}$ 状態を受信するとトランザクションを実行します。$msgs$ は転送中のメッセージを記述します。

$$ \begin{split} TPTypeOK \equiv & \land \text{rmState} \in [RM \rightarrow \{ \text{"working"}, \text{"prepared"}, \text{"committed"}, \text{"aborted"} \}] \\ & \land \text{tmState} \in \{ \text{"init"}, \text{"done"} \} \\ & \land \text{tmPrepared} \subseteq \text{RM} \\ & \land \text{msgs} \subseteq \text{Messages} \end{split} $$

$TPTypeOK$ の定義は、それぞれ $rmState$ と $tmState$ の可能な値の集合を示します。$\text{tmPrepared}$ の値は $RM$ からのものでなければならず、$msgs$ は $\text{Messages}$ からのものでなければなりません。

この仕様の目的は、メッセージの送信を記述することです。メッセージが送信される実際のメカニズムを指定するのではなく、メッセージ送信に必要なものだけを指定します。

仕様には1つの簡略化が導入されています：ツーフェーズコミットアルゴリズムはメッセージの順序に依存しないため、既に取り出したメッセージを $msgs$ から削除しません。したがって、$msgs$ にはこれまでに送信されたすべてのメッセージが含まれ、受信者はそれからメッセージを読むことができます。これは現実に実際に起こり得ることなので、この場合でもアルゴリズムが機能することを確認する必要があります。

$Messages$ の定義。

$\text{Messages} \equiv [type : \{\text{“Prepared”}, rm : RM\}] \cup [type : \{\text{“Commit”}, \text{“Abort”}\}]$

和集合の左側は、$type$ フィールドが単一の要素 $\text{“Prepared”}$ を含む集合の要素であり、$rm$ が $RM$ の要素からなるレコードの集合です。これは $[type \mapsto \text{“Prepared”}, rm \mapsto r]$ と書くことができ、$r$ からトランザクションマネージャーに送信される prepared メッセージを表します。

和集合の右側は、トランザクションマネージャーからすべてのリソースマネージャーに送信されるメッセージを表す集合です。この集合は2つの要素 $\{[type \mapsto \text{“Commit”}],[type \mapsto \text{“Abort”}]\}$ を含む集合に等しいです。

$$ \begin{split} TPInit \equiv & \land rmState = [r \in RM \mapsto \text{"working"}] \\ & \land tmState = \text{"init"} \\ & \land tmPrepared = \{\} \\ & \land msgs = \{\} \end{split} $$

$TPInit$ 式では、$rmState$ はすべてのリソースマネージャーに文字列 $\text{“working”}$ を割り当てる式です。

$$ \begin{split} TMRcvPrepared(r) \equiv & \land tmState = \text{"init"} \\ & \land [type \mapsto \text{"Prepared"}, rm \mapsto r] \in msgs \\ & \land tmPrepared' = tmPrepared \cup \{r\} \\ & \land UNCHANGED \left \langle rmState, tmState, msgs \right \rangle \end{split} $$

$TMRcvPrepared(r)$ サブ式は、トランザクションマネージャーがリソースマネージャー $r$ からの $Prepared$ メッセージを受信することを記述します。

メッセージは、トランザクションマネージャーが $init$ 状態にあり、送信されたメッセージの集合 $msgs$ にリソースマネージャー $r$ からの $Prepared$ メッセージが存在する場合にのみ受信できます。

新しい値 $\text{tmPrepared’}$ は、その値と要素 $r$ との和集合に等しく、つまり $\text{tmPrepared}$ に $r$ を追加します。

全体の $UNCHANGED$ 式は、$\land rmState’ = rmState \land tmState’ = tmState \land msgs’ = msgs$ と等しく、$rmState$、$tmState$、$msgs$ の値が変更されないことを主張します。

この式では、最初の2つの結合はプライムがありません。これはステップの最初のステップに関する条件であり、有効化条件と呼ばれます。それらは式の冒頭に置くべきです。

結合の順序には意味があります。ここでは、3番目の結合が $\text{tmPrepared’}$ 集合に要素 $r$ を追加することを宣言しており、以降のステップでは $\text{tmPrepared}$ に $r$ が含まれているため $\text{tmPrepared}$ は変更されないと暗に示しています。なぜなら、それが要素を含むか含まないかを示しており、$r$ の2つのコピーを含むことはできないからです。つまり、このステップで $r$ は $\text{tmPrepared}$ 集合ではなく $\text{tmPrepared’}$ 集合に移動し、その後 $\text{tmPrepared’}$ に代入されます。

ツーフェーズコミットでは、すべてのリソースマネージャーは同一の役割を持ち、相互に置き換えることができます。TCLでは、可能な置換の集合を対称性集合と呼びます。TLCは、モデルがモデル値の集合に対称性集合を設定すると、より少ない状態をチェックします。

対称性集合でない集合を対称性集合と主張すると、TLCはエラーを見逃す可能性があることに注意してください。

ツーフェーズコミットが実際のトランザクションコミットプロトコルであることを確認するために、$TCommit$ 仕様の式 $TCConsistent$ が、あるリソースマネージャーが中止した場合に別のリソースマネージャーがコミットできないことを主張し、仕様の不変条件であることを確認する必要があります。

INSTANCE TCommit ステートメントは、$TCommit$ からの定義をモジュール $TwoPhase$ にインポートします。

したがって、仕様にエラーがないことを確認するためには、$TPTypeOK$ と $TCConsistent$ の両方の不変条件を TLA+ Toolbox に追加する必要があります。

結論

このブログ投稿では、トランザクションコミット と ツーフェーズコミット アルゴリズムを考察しました。マルチパーティプロトコル、レコード、および対称性集合の定義方法を学びました。次のブログでは、パクソス アルゴリズムを説明する Learning $TLA^+$ コースの部分をカバーします。

注意事項

モデルを実行しようとしたときに（「未知の演算子 TPInit」のような）エラーが発生した場合は、このスレッドをチェックしてください：https://groups.google.com/u/1/g/tlaplus/c/REfGFm9bJMU/m/BuJ9N8NnGwAJ

ただし、上記は私には役立ちませんでしたので、問題を解決するために行ったことは：

  1. 新しい仕様を作成する（ツリービューを右クリック -> new specification）
  2. $TwoPhase$ 仕様を貼り付ける
  3. 現在のものの中に新しい仕様を作成する（modules を右クリック -> new specification with the root module file as the current one）
  4. 新しく作成した仕様に $TCommit$ 仕様を貼り付ける（INSTANCE TCommit 式に従って名前を一貫させる）。

おそらく奇妙な解決策ですが、動作します 🐦‍⬛。

参考文献

このブログ記事の議論に参加してください:

x
discord
telegram

この記事は AI 搭載の翻訳ツールによって翻訳されました。翻訳に誤りがある場合はご容赦ください。すぐに校正し、考えられる誤りを修正します。誤りを見つけた場合は、GitHub で問題を作成してください。