![[TLA+] Transaction Commitの仕様を表現する](https://devio2023-media.developers.io/wp-content/uploads/2019/01/TLA_logo_splash_image_3.png){kind=logo}
[TLA+] Transaction Commitの仕様を表現する
はじめに
こむろです。今回から情報科学を題材とした仕様を記述する講義になりました。まだまだ単純な例ですが、徐々に難易度が上がっている感じがしています。
今回の TLA+ Video Lectures - Transaction Commit も非常にわかりやすいLeslie Lamport先生の解説を聞けるのでおすすめです。情報科学を学習したい、興味がある、学生時代情報科学の基礎はやったなぁ、という人にとっては情報科学、数学の断片、そしてテクニカルな英語（とても聞き取りやすい）を聞ける講座になっているので、とてもオススメです。
ただし、集合論／論理演算あたりのちょっとした数学的な話は少なからず出てきてしまうので、数学を見ただけで目眩がするみたいな人にはオススメできません。厳密な数学の細かい話は出てこないのでご安心を。
今回は、パートナー同士の婚姻関係成立を例にTransaction Commitの仕様を考えます。ここでも中心となる考え方は（TLA+おいては） How は議論せずに What を仕様として表現することです。それではやっていきます。
婚姻関係の成立から考える状態遷移
結婚（入籍？）は二人のパートナーが互いの関係を婚姻関係にあると認め、それを法律として認める制度です。そのため、基本的には互いの合意がないと関係を結ぶことができません。 *1
そこで婚姻関係を結ぶにあたっての教会等でのそれぞれの誓い（宣言？）を状態遷移で表現します。婚姻関係を結ぶ人をそれぞれリソースとし、それぞれが状態を持つオブジェクトであるとします。関係を結ぶまで複数の状態を遷移します。
- 意思を確認していない状態（unsure）
- 関係を受け入れる状態（prepared）
- 関係を拒否する状態（aborted）
- 両者の関係が成立した状態（committed）
この状態を表現します。
この状態遷移において、最終的にそれぞれのリソースの状態が committed と aborted で混在することはありません。双方いずれかが aborted となれば関係は結べず、committed に遷移することはありません。committed に遷移できる（つまり関係を成立できる）のは双方ともに prepared となった時だけです。
Transaction Commit
婚姻関係を例に、オブジェクト同士の関係の状態遷移について確認しました。これをほぼそのまま情報科学の世界のTransaction Commitに置き換えて考えます。先程はそれぞれ関係を結ぶパートナーをそれぞれ状態を持つリソース（オブジェクト）と表現しました。これを Resource Manager に置き換えます。ここにおけるResource Managerとは何らかのデータを管理するものと思っておけば良さそうです（データベースとか）
例におけるTransaction Commitのざっくりした動きについて確認します。
- 複数のデータリソースへ変更を依頼する
- 全てのデータリソースへの変更が完了したら、全てのリソースへCommitを指示する
- Commitされ、すべてのデータリソースが正常に更新される
正常系の動作は以上です。いわゆるデータベースのTransaction処理と見てもらって良いかと思います（簡易的ではありますが）
先程の例をTransactionの例へ置き換えます。 *2
| 婚姻関係の例 | Transaction Commitの例 | 役割 |
|---|---|---|
| unsure | working | 初期状態 |
| parepared | prepared | 書き込み可能状態 |
| committed | committed | 正常に完了 |
| aborted | aborted | 中止 |
状態遷移図も変更しておきます。
しかしながら、複数のデータリソースを操作する際には、必ずしも全てが成功するとは限りません。何らかの（内的・外的）要因により一部のデータリソースの操作に失敗する場合があるでしょう。
その場合、処理の途中でAbortすることになるため、データリソースの操作を一度実行前まで戻す必要があります。関係のあるデータリソースへの操作を打ち消し、処理途中の中途半端な状態を維持せず、操作前の状態へ自動的に復元させます。つまり
- 関係するすべてのデータリソースは、操作が正常に行われすべて操作の結果が反映される
- 関係するすべてのデータリソースは、操作が中断され、すべて操作の結果が反映されていない
のいずれか のみ であることが求められます。
TLA+で仕様を記述する
TLA+でTransaction Commitの仕様を記述します。モジュール名は TCommit です。
変数・定数定義
まずはこの仕様において利用する変数及び定数を宣言します。
------------------------------ MODULE TCommit ------------------------------ CONSTANT RM VARIABLES rmState =============================================================================
CONSTANT はその名の通り定数を表します。すべてのステップにおいて値が変更することはありません。 RM は Resource Manager の集合を表します。この集合がTransactionの対象になります。
次に変数 rmState を定義します。この rmState は、RM 集合の要素それぞれのStateを集合として表します。具体的にどういうことかというと、辞書のような形で保持しているようなイメージです（あくまでイメージです）
RM から取り出した任意の要素のステータスは rmState に任意の要素をキーとして与えると取得できます。
型検査と初期評価
型検査と初期評価を定義します。
まずは変数の取りうる値の型検査から定義します。
今までは TypeOK と定義していましたが、今回は別の名前で式 TCTypeOK を定義します。変数 rmState の取りうる値の可能性を検査します。 rmState は集合 RM 各要素のステータスを管理する集合であり、そのステータスは4つの可能性で構成されます。
- working
- prepared
- aborted
- committed
全てのステップにおいて、上記が満たされていることが必要です。いずれの値にも合致しない場合は検査に失敗し、反例として直ちにエラーとして出力されます。式の定義は以下の通り。
------------------------------ MODULE TCommit ------------------------------
TCTypeOK == rmState \in [RM -> {"working", "prepared", "aborted", "committed"}]
=============================================================================
rmState は RM の各要素のステータスが {"working", "prepared", "aborted", "committed"} のいずれかで構成される集合に含まれます。
続いて初期状態を定義。
------------------------------ MODULE TCommit ------------------------------ TCInit == rmState \in [r \in RM |-> "working"] \* rmStateの状態を検査してAssertion =============================================================================
初期状態では、RM の要素全てが初期状態になっている必要があります。そこでMapのような機能を利用して集合の全ての要素に初期値を設定します。
[variable \in set |-> expression]
たとえば全てを2乗する式は以下のように定義できます。
sqr == [i \in 1..42 |-> i^2]
これを実行すると以下のような集合を得ることができます。
[1^2, 2^2, 3^2, 4^2, ... 42^2]
次状態を式で表現する
続いて全ての状態を検証するため、次状態の式を定義します。
TCNext == \E r \in RM : Prepare(r) \/ Decide(r)
\E は存在を示す記号です。数学記号だと ∃ となります。したがって、 \E r \in RM で RM の中のある 1 要素を式のローカル変数 r で示したことになります。そのローカル変数を使い、後半の式を評価します。
Prepare(r) \/ Decide(r)
当然ながら、ローカル変数の定義なので名前は任意で決めることができます。(r にこだわるひつようはない)
RM の集合を {"r1", "r2", "r3", "r4"} とした時に上記の式は以下のように展開されます。
\/ Prepare("r1") \/ Decide("r1")
\/ Prepare("r2") \/ Decide("r2")
\/ Prepare("r3") \/ Decide("r3")
\/ Prepare("r4") \/ Decide("r4")
Prepare(r) は初期状態(working) からの遷移を、 Decide(r) は最終状態(committed もしくは aborted) への遷移をそれぞれ制御します。
TLA+ではすべてが集合で表現されます。そのため、abc も 42 も [1, 2, 3] もすべて集合として扱われます。そのため、TLA+で宣言した値は全て集合演算の対象とすることが可能です。
Prepare(r)を定義する
まずは初期状態からの遷移を考えます。現在の状態が working であることが条件です。すでに TCInit で全ての対象のステータスは working です。これらをすべてのステータスを prepared に変更します。
Parepare(r) == /\ rmState[r] = "working" \* 指定された要素の状態が "working" となっていること
/\ rmState'[r] = "prepared" \* 次状態は、"prepared" に変更
今までの経験からすると上記のように書けてよいはずです。が、これは間違いです。以下のような式で表現するのが正しいとのことです。
Prepare(r) == /\ rmState[r] = "working"
/\ rmState' = [s \in RM |-> IF s = r THEN "prepared"
ELSE rmState[s]]
rmState[r] の1要素だけを見るのではなく、 s = r となる要素のみを "prepared" に変更し、それ以外の要素は変更前の値をそのまま残し、新たに集合を作成しています。そして集合を rmState の次状態として割り当てています。
つまり任意の1つの要素のみの変更であっても、他の要素に変更がないことを明示的にその式の中で明らかにする必要があるようです。しかしこの表記は少々長い。そこで以下のような省略の形で記述することができます。
/\ rmState' = [rmState EXCEPT ![r] = "prepared"]
ぱっと見、全く同じ式には見えません。が、新たに集合を作っている式と同じ意味になります。したがって、 Prepare(r) の式の最終的な形は以下の通りです。
Prepare(r) == /\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "prepared"]
Decide(r)を定義する
続いて committed, aborted を判定する式について定義します。
この式では 2 つの状態へ遷移させる必要があるので、 2 つの式を定義します。
- "prepared" から "committed" へ遷移する式
- "working", "prepared" のいずれかから "aborted" へ遷移する式
いくつか未定義の式がありますが以下のようになります。
Decide(r) == \/ /\ rmState[r] = "prepared"
/\ canCommit \* 未定義
/\ rmState' = [rmState EXCEPT ![r] = "committed"] \* Committedステータスへの遷移
\/ /\ rmState[r] \in {"working", "prepared"}
/\ notCommitted \* 未定義
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
committedステータスへの遷移
まずは "prepared" から "committed" へ遷移する式について。
/\ rmState[r] = "prepared" \* 1 /\ canCommit \* 2 /\ rmState' = [rmState EXCEPT ![r] = "committed"] \* 3
1, 2はいずれもこの式に合致する条件を表します。指定された要素が "prepared" のステータスであることは必須条件です。そして canCommit に合致する必要があります。では、この未定義の式をどのようにすれば committed に遷移できるでしょうか。
- 全ての
RMの要素のステータスがpreparedかcommittedである
上記を式では以下のように表現します。
canCommit == \A r \in RM: rmState[r] \in {"committed", "prepared"}
\A は「全ての」を表現する ∀ です。この式の意味するところは、RM に含まれる 全ての 要素のステータスが "prepared" か "committed" であれば真となります。
1, 2 の条件が真であれば指定された要素 r のステータスを "committed" へ変更します。（3 の式に相当）
abortedステータスへの遷移
続いて "aborted" へ遷移する式について。
/\ rmState[r] \in {"working", "prepared"} \* 1
/\ notCommitted \* 2
/\ rmState' = [rmState EXCEPT ![r] = "aborted"] \*3
こちらも先程と同じように、 1, 2 が現在の状態を評価します。"aborted" とするためには以下になります。
- 全ての
RMの要素のステータスがcommittedを含まない
上記を式で表現すると以下の通り。
notCommitted == \A r \in RM: rmState[r] /= "committed"
/= は Not Equal を表す記号です。≠ のTLA+上での表現になります。
こちらも1, 2の条件が真であれば指定された要素 r のステータスを "committed" へ変更します。(3 の式に相当)
notCommittedについて
notCommitted は全ての要素において committed が存在しないこと、という非常に単純な式です。果たしてこれで十分なのでしょうか？いまいち確信が持てません。
例で考えてみます。 RM に 3 つの要素がある時。初期状態は以下のとおりです。
RM = {"r1", "r2", "r3"}
rmState["r1"] = "working"
rmState["r2"] = "working"
rmState["r3"] = "working"
状態遷移図を思い出してみると、 working から遷移できる可能性は prepare か aborted のいずれかです。集合の中からr1 を対象とした時を考えてみます。r1 は working からの遷移なので
RM = {"r1", "r2", "r3"}
rmState["r1"] = "prepared"
rmState["r2"] = "working"
rmState["r3"] = "working"
もしくは
RM = {"r1", "r2", "r3"}
rmState["r1"] = "aborted"
rmState["r2"] = "working"
rmState["r3"] = "working"
となる可能性があります。r1 はステータス working であるため、Prepare(r) によって prepared となる可能性と DecideA(r) によって aborted になる可能性です。
さらに
RM = {"r1", "r2", "r3"}
rmState["r1"] = "prepared"
rmState["r2"] = "prepared"
rmState["r3"] = "working"
となっている場合は、全ての要素が prepared か committed になっていなければ canCommit の状態には合致しないため、可能性としては Prepare(r) か DecideA(r) のいずれかしかありません。
全てが prepared となると
RM = {"r1", "r2", "r3"}
rmState["r1"] = "prepared"
rmState["r2"] = "prepared"
rmState["r3"] = "prepared"
初めて canCommit の状態に合致する状態となり、DecideC(r) の遷移が可能となり、committed となるかもしくは DecideA(r) によって aborted となる可能性が考えられます。
1 つでも committed になってしまえば
RM = {"r1", "r2", "r3"}
rmState["r1"] = "prepared"
rmState["r2"] = "prepared"
rmState["r3"] = "committed"
notCommitted の状態には合致しなくなるため、以降 aborted へ遷移することはなくなります。そのため、 notCommitted の式は rmState の集合の中に committed が存在しないという条件だけで十分ということになります。
Transaction CommitのSpec
では今までの式をまとめます。
------------------------------ MODULE TCommit ------------------------------
CONSTANT RM
VARIABLE rmState
\* rmStateがいずれかのステータスStringである. Invariantで評価
TCTypeOK == rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
\* RMに含まれる全てを "workking" にする. Mapping処理. 初期化
TCInit == rmState = [r \in RM |-> "working"]
Prepare(r) == /\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "prepared"]
canCommit == \A r \in RM: rmState[r] \in {"committed", "prepared"}
notCommitted == \A r \in RM: rmState[r] /= "committed"
Decide(r) == \/ /\ rmState[r] = "prepared"
/\ canCommit
/\ rmState' = [rmState EXCEPT ![r] = "committed"] \* Committedステータスへの遷移
\/ /\ rmState[r] \in {"working", "prepared"}
/\ notCommitted
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
\* ∃は存在. あるrに対して Prepare(r), Decide(r) を評価した和集合
TCNext == \E r \in RM: Prepare(r) \/ Decide(r)
=============================================================================
Decide(r) の中の式がそれなりに複雑でなかなか読むのが大変そうです。canCommit と notCommitted の2つの和集合を取っているのでここも式に分割します。
\* Committedへ遷移
DecideC(r) == /\ rmState[r] = "prepared"
/\ canCommit
/\ rmState' = [rmState EXCEPT ![r] = "committed"]
\* Abortedへ遷移
DecideA(r) == /\ rmState[r] \in {"working", "prepared"}
/\ notCommitted
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
最終的なTransaction CommitのSpec
分割した式に変形し、記述し直します。
------------------------------ MODULE TCommit ------------------------------
CONSTANT RM
VARIABLE rmState
\* rmStateがいずれかのステータスStringである. Invariantで評価
TCTypeOK == rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
\* RMに含まれる全てを "workking" にする. Mapping処理. 初期化
TCInit == rmState = [r \in RM |-> "working"]
Prepare(r) == /\ rmState[r] = "working"
/\ rmState' = [rmState EXCEPT ![r] = "prepared"]
canCommit == \A r \in RM: rmState[r] \in {"committed", "prepared"}
notCommitted == \A r \in RM: rmState[r] /= "committed"
\* Committedへ遷移
DecideC(r) == /\ rmState[r] = "prepared"
/\ canCommit
/\ rmState' = [rmState EXCEPT ![r] = "committed"]
\* Abortedへ遷移
DecideA(r) == /\ rmState[r] \in {"working", "prepared"}
/\ notCommitted
/\ rmState' = [rmState EXCEPT ![r] = "aborted"]
\* ∃は存在. あるrに対して Prepare(r), Decide(r) を評価した和集合
TCNext == \E r \in RM: Prepare(r) \/ DecideC(r) \/ DecideA(r)
=============================================================================
Specの検査
まずはいつもどおりModelを作成します。今回は Init, Next をそれぞれ TC をPrefixにつけているため、明示的に指定します。
今回は CONSTANT RM がコードの中では未定義です。これはモデルとして外部から値を指定する必要があります。What is the model というセクションをダブルクリックして値を直接入力します。
型検査の式は TCTypeOK で与えています。こちらをInvariantに指定。
こちらを実行してみます。
No errors でFinishするはず。
abortedとcommittedが混在することがないかをチェックする
今回の仕様では RM の集合の要素のステータスは、全てのステップにおいて、決して aborted と committed が混在することはあり得ません。こちらを検査する式を追加します。
TCConsistant == \A r1, r2 \in RM : ~ /\ rmState[r1] = "aborted"
/\ rmState[r2] = "committed"
「RM の集合に含まれる任意の r1, r2 のステータスはそれぞれ "aborted" かつ "committed" となることはない(~)」という式になります。 ~ は否定となります。この式をInvariantに追加します。
再度実行しても結果に変化はありません。従って、記述したSpecは "aborted" と "committed" が混在した状態にならないということが検査できたということになります。
まとめ
婚姻関係の例からTransaction Commitの仕様をTLA+で記述し、動作を確認しました。このようにあらゆる状態の組み合わせを試行した結果、最終的なデータの不整合が存在しないかを検証することができます。
実際に導入する際には、全ての仕様を記述するのではなく一部のクリティカルな箇所に特化してモデル化し、全ての状態を検査するのが現実的なようです。ソフトウェアでどのように利用するかの一端が見えた気がします。
次回はかなり複雑な対象です?
