###### tags: `TransactionalInformationSystems` # 3章-1 スケジュールの構文論/意味論的定義 ### 略称定義 Concurrency Control : CC ## 3章概要 - CCアルゴリズムの正当性を証明する技法 - 構文論的な正当性と意味論的な正当性の違い - スケジュール正当性のクラス階層 - 正当性判定の計算複雑性 といったことが述べられている ## 適切なCCが無いと起こる問題 ### Lost Update 更新が別トランザクションに上書きされて消える問題。 | $t_1$ | Time | $t_2$ | | - | - | - | | | $x=100$ | | | $r(x)$ | 1 | | | | 2 | $r(x)$ | | $x=x+30$ | 3 | | | | 4 | $x=x+20$ | | $w(x)$ | 5 | | | | $x=130$ | | | | 6 | $w(x)$ | | | $x=120$ | | 問題の原因となるパターン $$r_1(x)r_2(x)w_1(x)w_2(x)$$ ### Inconsistent Read 片方のトランザクションによる更新が中間状態の時点でもう一方がreadすることで、不正状態を読み込んでしまう問題。 | $t_1$ | Time | $t_2$ | | -------- | -------- | -------- | | | 1 | $r(x)$ | | | 2 | $x=x-10$ | | | 3 | $w(x)$ | | $sum=0$ | 4 | | | $r(x)$ | 5 | | | $r(y)$ | 6 | | | $sum=sum+x$ | 7 | | | $sum=sum+y$ | 8 | | | | 9 | $r(y)$ | | | 10 | $y=y+10$ | | | 11 | $w(y)$ | $x$と$y$の初期状態がそれぞれ50だったとすると、$t_1$が想定するものは合計値100の算出のはずだが、$t_2$による送金の途上で計算してしまったせいで90と出ている 問題の原因となるパターン $$r_2(x)w_2(x)r_1(x)r_1(y)r_2(y)w_2(y)$$ 以上の2つは、2つのトランザクションをシリアルに実行していれば避けられる問題 ### Dirty Read | $t_1$ | Time | $t_2$ | | -------- | -------- | -------- | | $r(x)$ | 1 | | | $x=x+100$ | 2 | | | $w(x)$ | 3 | | | | 4 | $r(x)$ | | | 5 | $x=x-100$ | | failure&rollback | 6 | | | | 7 | $w(x)$ | $t_1$がトランザクションに失敗してロールバックしたため、$t_2$が読み込んで使用した値がロールバック前の不正なものになってしまう問題。 問題の原因となるパターン $$r_1(x)w_1(x)r_2(x)a_1w_2(x)c_2$$ ## 履歴とスケジュールの構文論的な定義 CCの中核であるスケジューラーは、トランザクションをどの順で実行するかオンラインで決定していく必要がある。ということでまずスケジュールの定義をはっきりさせる また、スケジュールはトランザクションの成功/失敗にも依存するので、データの操作に加えてトランザクションの終了操作も定義しておく - commit ( $c$ ) : トランザクションは成功し、更新を永続化する - abort ( $a$ ) : トランザクションは失敗し、実行前の状態に戻る 現実にはトランザクションの成功/失敗が分かるのは過去についてのみなので、 - 全てのトランザクションの結果が分かっているスケジュールを履歴 - 一部もしくは全てのトランザクションの結果が不明であるスケジュールを改めてスケジュールと呼ぶことにする ### 定義:履歴とスケジュール (半順序による定義) トランザクションの集合を$T=\{t_1, \cdots, t_n \}$とし、各$t_i$は$t_i=(op_i,<_i)$という形をしているものとする。ここで$op_i$は操作の集合、$<_i$は操作間に定められた半順序である。 1. $T$の履歴(history)とは、ペア$s=(op(s),<_s)$で以下の条件を満たすものである。 a. $op(s)\subseteq \bigcup_{i=1}^nop_i\cup \bigcup_{i=1}^n\{c_i,a_i\}$ かつ $\bigcup_{i=1}^nop_i\subseteq op(s)$ である。つまり、$op(s)$は各トランザクションの操作とcommit/abortから成る。 b. $c_i\in op(s)\Leftrightarrow a_i\notin op(s)$ である。つまり、1つのトランザクションに対してcommitとabortはどちらかしかない。 c. $\bigcup_{i=1}^n <_i \subseteq <_s$である。つまり、履歴の半順序は各トランザクションの半順序を保存する。 d. $\forall p\in op_i,\ p<_s a_i$ or $p<_s c_i$ である。つまり、commit/abortはトランザクションの最終ステップに行われる。 e. 別のトランザクションに属するが、同じデータアイテムを操作するread/writeもしくはwrite/write操作 $p,q\in op(s)$ の間には順序($p<_sq$もしくは$q<_sp$)が付けられる。 2. スケジュール(schedule)とは履歴のprefixである。ここで半順序集合 $s=(op(s),<_s)$ におけるprefix $s'=(op_{s'},<_{s'})$ は以下を満たす。 1.$op_{s'}\subseteq op_s$ 2.$<_{s'}\: \subseteq\: <_s$ 3.$\forall p \in op_{s'}, \forall q \in op(s),\ q <_s p \Rightarrow q\in op_{s'}$ 4.$\forall p,q \in op_{s'},\ p <_s q \Rightarrow p <_{s'} q$ 履歴$s$における任意の2つの異なるトランザクションにおいて、一方の操作が全てもう一方のトランザクションの操作よりも小さい順序であるとき、その履歴は逐次的(serial)であるという。 ### 全順序による定義 $s'\in shuffle(T)$に、先述の1.b,1.dの定義を満たす$c,a$を混ぜた操作の列を履歴といい、そのprefixをスケジュールという。ここで$shuffle(T)$は、各トランザクションの操作列を、順序を保存しながら混ぜたような列の集合. ### 今後使う便利定義 sをスケジュールとする。 - trans(s) : s内で起こるトランザクションの集合。(sは履歴とは限らず、全トランザクションが行われるとは限らないため) - commit(s) : s内でコミットされるトランザクションの集合。 - abort(s) : s内で中断されるトランザクションの集合。 - active(s) : s内で起こるものの、コミットも中断もされないトランザクションの集合。$active(s)=trans(s)-(commit(s)\cup abort(s))$ なお本章では中断は取り扱わないので $abort(s)=\emptyset$ を想定する。 ## 履歴とスケジュールの「正当性」 スケジュールの正当性の基準を考えていく。 $S$を全てのスケジュールの集合としたとき、各スケジュールに真偽値をマッピングする関数 $$\sigma : S \rightarrow \{0,1\}$$を正当性の基準とする。 $$correct(S)=\{s\in S|\sigma(s)=1\} $$が正当なスケジュールの集合になる。 **$correct(S)$には少なくとも以下の条件を満たしてほしい** 1. 空集合ではない。正当なスケジュールは少なくとも1つある。 2. 「$s\in correct(S)$かどうか」は効率的に判定できる。スケジューラが永遠に待たされるようなことがない。 3. ある程度要素数が大きい方が良い。その方が並列実行の自由度が高まり、パフォーマンスが改善される。 本章でやることは、トランザクションの意味的な詳細が分からないという前提の下で、上の条件を満たせるような正当性基準を導出すること。 少なくとも逐次的な履歴は常に正当である。ただし、パフォーマンス的に逐次実行は最悪であるため、正当性の出発点、あるいは比較基準として用いる。アイディアの根底にあるものは、 1. スケジュール間のある種の同値性の概念を定義し、 2. 逐次的なスケジュールを代表元とする同値類を「serializable」なクラスと考える こと。同値性の種類によって、serializableの概念はいろいろ存在しうる ## スケジュールのHerbrandによる意味論 各操作のアプリケーションにおける実際的な意味を知らなければ、意味論的にスケジュールを捉えることはできない。 そこで、トランザクションにおける各ステップのセマンティクスをとりあえずふわっと以下のように定義してみる(後でさらに詰める)。スケジュールを$s$とする。 1. $r_i(x)\in s$ は、$r_i(x)$ の直前に登場する$x$への書き込み $w_j(x)\in s (i\neq j)$ によって保存された値を読み出す。 (スケジュールの定義から直前のwriterは一意に定まる) 2. $w_i(x)\in s$ により書き込まれる値は、$w_i(x)$の以前にトランザクション$t_i$がデータベースや$active(s)\cup commit(s)$に属するトランザクションから読みだしたデータアイテムの値に依存する。 全ての読み込みが書き込みの後にあるとは限らない。直前の書き込みが存在しない読み込みについても一意に定義するため、便宜的に全データアイテム初期化用トランザクション$t_0=w_0(x)w_0(y)\ldots c_0$を最初に配置する。 以上の定義でも、まだ読み込まれる値や適用される関数の中身は分からない。そこはHerbrandのセマンティクスを利用して論理学的に定義する。関数シンボルだけ利用し、それ以上の深追いはしない。 ### 定義:ステップのHerbrandセマンティクス $s$をスケジュールとする。$r_i(x), w_i(x)\in op(s)$のHerbrandセマンティクス$H_s$を以下のように定義する。 1.$H_s(r_i(x)):= H_s(w_j(x))$, ただしここで $w_j(x), j\neq i$ は$s$内で$r_i(x)$の直前に出現する書き込み。 2.$H_s(w_i(x)):= f_{ix}(H_s(r_i(y_1)),\ldots,H_s(r_i(y_m)))$, ただしここで $r_i(y_j) (1\leq j \leq m)$ は$w_i(x)$ 以前に現れる全ての読み込み操作を表し、$f_{ix}$は *uninterpreted m-ary function symbol* (解釈されていないm引数関数シンボル) トランザクションあたり同じデータアイテムへのwriteは1回しかないので$f_{ix}$はwell-defined。 #### セマンティクスの例 $$s=w_0(x)w_0(y)c_0r_1(x)r_2(y)w_2(x)w_1(y)c_2c_1$$ の各ステップのセマンティクスは $$H_s(w_0(x)) = f_{0x}() (初期化定数)\\ H_s(w_0(y)) = f_{0y}() (初期化定数)\\ H_s(r_1(x)) = H_s(w_0(x)) = f_{0x}()\\ H_s(r_2(y)) = H_s(w_0(y)) = f_{0y}()\\ H_s(w_2(x)) = f_{2x}(H_s(r_2(y))) = f_{2x}(f_{0y}())\\ H_s(w_1(y)) = f_{1y}(H_s(r_1(x))) = f_{1y}(f_{0x}())$$ のようになる。 ### 定義:Herbrand Universe $D=\{x, y, z ,\ldots \}$をデータアイテムの集合とする (同じサーバ上の)。トランザクション$t$内の操作ステップ集合を$op(t)$とする。トランザクション群 $t_i (i>0)$ についてのHerbrand Universeとは、以下の条件を満たす最小のシンボル集合とする。 1. 各$x\in D$に対して$f_{0x}()\in HU$ 2. $w_i(x)\in op(t_i),\ |\{r_i(y)\mid (\exists y \in D) r_i(y) <_{t_i} w_i(x)\}|=m$ のときに $v_1,\ldots,v_m \in HU$ であれば $f_{ix}(v_1,\ldots,v_m)\in HU$ (関数$f$群のみから計算することのできる値を集めた集合がHerbrand Universe) ### 定義:スケジュールのセマンティクス スケジュール$s$のセマンティクスは、関数 $$H[s] : D \rightarrow HU$$ であり、 $$H[s](x) := H_s(w_i(x))$$ で定義される。ここで$w_i(x)$はデータアイテム$x\in D$に対する最後の書き込みとする。 (つまり、スケジュール=関わったデータアイテムの全てに各ステップによる計算結果をマッピングする関数と意味付ける) #### スケジュールセマンティクスの例 $$s=w_0(x)w_0(y)c_0r_1(x)r_2(y)w_2(x)w_1(y)c_2c_1$$ のセマンティクスは $$H[s](x) = H_s(w_2(x)) = f_{2x}(f_{0y}()) \\ H[s](y) = H_s(w_1(y)) = f_{1y}(f_{0x}())$$ ###### メモ用テンプレート | $t_1$ | Time | $t_2$ | | -------- | -------- | -------- | | $$ | 1 | $$ |