TIS Chapter 3

この章ではConcurrency Controlについて述べる．

3.1 Goals and OverView

ある一連の処理(Transaction)が他のTransactionにInterleaveされたとする．

このとき，処理の結果がSerial Exectuionの結果と等価であるかを証明する方法を説明する．

failure-free environmentを仮定して定式化を行う．

failureは往々にしてrecoveryの結果abortに帰結するがcounterintuitiveであるため．

ここではConcurrency Controlのみを扱うのでそうしている．

3.2 Canonical Concurrency Problems

Dirty Read, Inconsistent Read, Lost-update Anomalyの紹介．

既知かつ想像に容易いのでスキップ

一応，一例をあげる

たとえば r1(x) r2(x) w2(x) w1(x) C2 C1 とする

しかし結果は一回しか実行されていないものと同じとなる．

3.3 Syntax of Histories and Schedules

この節はterminologyの話なので，いっそ飛ばしても読める．

厳密な理解の助けにはなる．

ユーザがどんなときに「この処理結果は問題である」と考えるか，全パターンをすくい上げるのは無理だろう．

なのでここでは，Concurrency Problemsという概念そのものを定義する．

この関数は，とりあえず「Concurrency Problemsが起きているか？」を検証するboolだと思えばよい．

これで，強いcorrectnessを使えばあらゆるConcurrency Problemsは起こらないし，弱いcorrectnessがどのようなProblemsを含むのかも定義可能となる．

最も強いcorrectnessが「直列実行したか？」である，と考えるとわかりやすいだろう．

まず，全てのTxnsの述語が与えられていることを前提とする．

トランザクションの成功とはcommitを意味する

失敗とは，abortの呼出(いわゆるuser abort)か，concurrency controlの結果としてのabort(いわゆるsysabort)を指す

abortしたトランザクションの処理内容はDBに一切の影響を与えない

トランザクションとは，data opsの順序集合にtermination opsがくっついたものと定義できる．

次に，全てのトランザクションの処理内容(r,w,c,a)は他の全てのトランザクションから可視であるという前提を置く．

この前提を置かないと以降のhistory/scheduleの議論ができない

history: 処理の結果を示す．全てのtermination operationを含む．complete scheduleとも呼ぶ．

schedule: termination operationを含まず，実行中の処理が含まれていてもよい．

この二者を区別する理由は，静的ではなく動的にトランザクションを実行したいから．

アドホックなクエリが飛んでくること(当たり前だが)を想定している

ここでは半順序のみを考える．

historyとscheduleはトランザクションのopsを並べることで表記できる．

ここでいう並び順が，半順序を意味する．

たとえば r1(x) w2(x) c2 r2(y) a1 など．

集合論でかけるけど面倒なのでskip

r1(x) c1 r2(x) c2 はSerial.

r1(x) r2(x) r1(y) c2 c1 はnot Serial.

DAGを一度描いてしまえば，あとは任意の順番でトポロジカルソートすることで，任意の全順序が生成できる．

3.4 Correctness of Histories and Schedules

correct(S) < 0なら部分スケジュールのどれかがcorrect.

で，問題のcorrectかどうか？という議論については，「異論はあるかもしれないが」以下とする．

Assuming that schedules should maintain the integrity of the underlying data(i.e. keep it consistent) and assuming that each individual transaction is able to assure is, it is reasonable to conclude (by induction) that serial histories are correct.

すなわち直列実行した際に起こりうるスケジュールであるか?ということ．

半順序のDAGから生成した全順序が直列実行した際のものと等価であるか？ということ．

で，ここまで長々と定義したことは全て以下に帰結する:

define a notion of equivalence for schedules,

define serializability via equivalence to serial histories.

3.5 Herbrand Semantics of Schedules

では，correctness関数の一つを実際に考えてみる．

すなわち，ある時点での全てのタプルのエルブラン関数が直列実行した際と一致するかを調べる．

これによって，直列実行した際と同じ最終値が生成されているかがわかる．

文字だけだとやや厳しいので直感的な数式を．

ノリとしてはこんな感じ

code:FSR

x = 1; // w0(x)

Thread 1 do {

localx = x;

}

Thread 2 do {

localx = x;

x = localx + 1;

}

Thread 3 do {

x = 42;

}

4までは理解しやすいが，5が面白い．

エルブランセマンティクスがシンプルな関数一つに戻っている．

$ s = a_1a_2w_3(x) c_3

いきなり問答無用でT1とT2を殺してT3だけ実行してやるパターン．

なので，エルブラン関数をcorrectness関数に用いるという実際例は無い．

3.6 Final State Serializability

まず，readの結果は直前のwriteに依存する，という前提を置く．

これはエルブランセマンティクスの話と同じ．

以下のtermを整理する．

useful

または，あるトランザクションがread-writeをした場合．このreadステップもwriteステップもuseful．

useful closureは連鎖していく．この場合全ステップuseful.

alive

端的に言うと「今DBから読める値に影響を及ぼしているステップ」のこと

これは全ステップalive.

この場合先ほどのステップがusefulであることは変わらない．

dead

aliveでないこと．

エルブランセマンティクスで言い換えてもよい．

その値を再現するために必要な関数群に含まれないステップはdead.

含まれるならalive.

あまりにしんどいので擬似コードで示す．

code: useful, alive, dead

x = 1; // useful dead

x += 1; // useful dead

x = 2; // useful alive

x += 1; // useful alive

さて，reads-from relationは以下と定義する．

$ RF(s) := \{(t_i, x, t_j)| an\ r_j(x)\ reads\ x\ from\ a\ w_i(x)\}

$ LRF(s) := \{(t_i, x, t_j) | an\ r_j(x)\ alive \ reads\ x\ from\ a\ w_i(x)\}

で以下のスケジュールを考える

$ s = r_1(x) r_2(y) w_1(y) w_2(y) c_1 c_2

$ s' = r_1(x) w_1(y) r_2(y) w_2(y) c_1 c_2

でReads-fromをやってみる．

$ RF(s) = \{(t_0, x, t_1), (t_0, y, t_2), (t_0, x, t_\infty), (t_2, y, t_\infty)\}

$ RF(s') = \{(t_0, x, t_1), (t_1, y, t_2), (t_0, x, t_\infty), (t_2, y, t_\infty)\}

このことをLRFで示す．

$ LRF(s) = \{(t_0, y, t_2), (t_0, x, t_\infty), (t_2, y, t_\infty) \}

$ LRF(s') = \{(t_0, y, t_2), (t_1, x, t_2), (t_0, x, t_\infty), (t_2, y, t_\infty) \}

つまりひとつステップがdeadになっている．

だから何だ？ということになるが，要するにこの２つのスケジュールはLRFが一致しないのである．

つまり異なるDBの状態となる．

最終状態が一致することはLRFの比較で確認できるというわけである．

つまり，FSRのためのcorrectness関数にLRFの比較演算を用いることができる．

Serializable historyを用意し，そのLRFと比較すればよい．

これはエルブランセマンティクスというcorrectness関数と同じ機能を果たす．

3.7 View Serializability

FSRのスケジュールでは最終状態が一致していても途中のトランザクションがなんかおかしくなるということは示した．

なんかおかしくなる == Anomalyが発生するということはわかる．

が，まだAnomalyとは何か，ということについて定式化できていない．

つまりトランザクションは無限にありますと考える．

このためエルブランセマンティクスによる検証が不可となる．

LRFもなにそれ？という話になる．今aliveでも今後deadになるかもしれない．

逆に言うと，dead stepもaliveだった時代はあったのだ．

この状況化でのcorrectness関数を考える．

そうすると，常に，今aliveなステップがcorrectnessであることが望ましい．

やっと実用的になってきた．

writeの内容は直前のreadに依存するという前提を置いていることは先に述べた．

この特性は非常に重要．

株式なり検索なりどんなアプリケーションでもいいが，読み書きがView Serializableなら，プログラムは直列実行した際と並列実行した際で同じセマンティクスを得られる．

実際，コンパイラは未使用の変数や使われない代入文を最適化で潰すことがあるが，プログラマはそれで困っていないわけだし，ここは異論が(最大公約数的に)ないだろう．

だから，readが間違っているときAnomalyだとよばれる．

3.7.1 View Equivalence and the Resulting Correctness Criterion

これは実用上最も有効なcorrectness関数となりうる．

そのReadに至った全てのread and writeステップが一致しているということ．

すなわち処理されるwriteも一致する．

で，このcorrectness関数は多項式時間で解ける．つまりVSRの検証はNP-Complete.

ちなみにFSRの検証も同じく(まあロジックほぼ同じですし)NP-Complete.

以下証明．

ありうるSerial Orderは以下

alive && usefulだけを洗い出しているのでこうなる．

だが当然RFは違う．

$ RF(s) = \{(t_2, x, t_1), (t_0, y, t_1)\}

$ RF(s'_1) = \{(t_1, x, t_2), (t_1, y, t_2)\}

$ RF(s'_2) = \{(t_0, x, t_2), (t_0, y, t_2)\}

つまりanomalyが何がしかあるということになる．

3.7.2 On the Complexity of Testing View Serializability

では実際にVSRであることを検証するアルゴリズムはどう書けるだろうか？

まして100万TPSとか言う時代に，1Tx追加するたびにこれをやるのは無理.

この計算はいわゆるNP完全である．

マジメに説明するとpolygraphというものを作ってやるのだが一旦割愛

3.8 Conflict Serializability

これについては今回は飛ばす．

実際的に最も使われているSerializabilityであり，correct関数であるが，考える必要はない．

より具体的にいうと，MVSR等価が必ず保証されるVersion Functionの一例がCSRなのである．

この説明で腑に落ちるようになったほうがCSRを理解するより健全なので，ここは飛ばす．

要約すると，

こうするとVSRよりありうるscheduleは狭くなるが，簡単にonline schedulerを実装できる．