###### tags: `TransactionalInformationSystems` # 11章-2 復元可能なページモデルスケジューラ いよいよ前ページで議論してきた復元可能性を実現するためのCCアルゴリズムを考えていく。復元可能性としては3つ、STとRGとPREDに着目する。 ## 2PLのStrictnessとRigorousnessによる拡張 前ページより$RG\subset COCSR$であり、また$Gen(SS2PL)\subset COCSR,\ Gen(SS2PL)\subset Gen(S2PL) \subset Gen(2PL)$は4章で分かっている。実はこれよりも踏み込んだことが言えて、 ### 定理11.6 $Gen(SS2PL)=RG$ #### 証明 SS2PLによって生成されるスケジュールを考える。SS2PLは、かけたロックをトランザクション終了時まで保持する。したがって、書き込んだアイテムは、そのトランザクションが終了するまで他のトランザクションからは読み書きできず(Strictness)、読み込んだアイテムは、そのトランザクションが終了するまで上書きできない(Rigorousness)。よって$Gen(SS2PL)\subseteq RG$。 逆に$s\in RG$を考えると、これはStrictnessとRigorousnessを満たしているため、ロックの競合によるブロックが発生しない($wr,ww$の衝突はStrictness, $rw$の衝突はRigorousnessによって競合しないようになっている)。そのためスケジュールはそのままSS2PLから出力され、したがって$RG \subseteq Gen(SS2PL)$。$\square$ ### 定理11.7 $Gen(S2PL)\subseteq CSR \cap ST$ #### 証明 $Gen(S2PL)\subseteq CSR$は既に示されている。S2PLは、write lockをトランザクション終了時まで保持するので、書き込んだアイテムはそのトランザクションが終了するまで他のトランザクションから読み書きできず(Strictness)、よって$Gen(S2PL)\subseteq ST$。$\square$ ## Serialization Graph Testingのログ復元可能性への拡張 CSR性を保証するために、リアルタイムで衝突グラフを保持して閉路判定を行う悲観的なプロトコル、Serialization Graph Testing(SGT)を4章で記述していた。 これを拡張してPREDを保証できるようなグラフ検証プロトコルを考える。 $PRED=CSR\cap LRC$ であることを踏まえると、まずいったん普通の衝突グラフを保持することを考える。その上で、各衝突辺に$rw,wr,ww$のラベルで注釈をつけて、LRC性に関わる$wr,ww$の辺のみを残した部分注釈グラフも同時に考えることにする。衝突グラフの非閉路性と、加えて部分注釈グラフのなんらかの性質を検証すればよい。 基本的な考え方としては、部分注釈グラフに$(t_i,t_j)$という辺があったとき、$t_i$がcommitするなら$t_j$のcommitよりも先であり、また$t_i$がabortするなら$t_j$が先にabortするか、$t_i,t_j$がグループで同時にabortしなければならないという性質が成り立つ。 部分注釈グラフにおいて、$t_j$へ向かう辺を持つノード集合を$precede(t_j)$、$t_j$から到達可能な全てのノード集合を$follow(t_j)$と表記すると、**拡張SGT(ESGT)** は以下の手順で実現される。 1. データ操作$o_i$が到着したとき、ノード$t_i$がないなら新たに作り、関連する$ww,wr,rw$辺を全て加える。閉路が生じたら$t_i$はabortされる、すなわち$a_i$が実行される。 2. commit操作$c_i$が到着したとき、$precede(t_i)$が空かチェックする。空集合なら$c_i$は直ちに実行され、$t_i$を待っていた全てのcommit操作が実行スケジュールされる。その後、$t_i$が全てのpredecessorリスト/successorリストから削除される。$t_i$がグラフのソース(入次数が0)ならノード$t_i$を削除してよい。$precede(t_i)$が空でなければ、$t_i$はcommit待ちのキューに入れる。 3. abort操作$a_i$が到着したとき、$follow(t_i)$が空かチェックする。空集合なら$a_i$は直ちに実行される。空でなければ、$t_j\in follow(t_i)$の$a_j$が全て実行スケジュールされる。その後、abortされたトランザクションが全てcommit待ちトランザクションキューから削除され、グラフからも削除され、predecessorリスト/successorリストからも削除される。 ### 定理11.8 $Gen(ESGT)\subseteq PRED$ #### 証明 ESGTの規則1より、CSR性は保証される。 次にLRC性を見ていく。 $w_i(x)r_j(x)$という形の衝突があったときに$c_i<c_j$となることは規則2より保証される。 $w_i(x)w_j(x)$という形の衝突があったときには、以下の4つのいずれかになる。 1. $c_i<c_j$ (規則2より) 2. $c_i<a_j$ ($t_i$がいったんcommitしたら$t_j$は自由なため) 3. $a_j<c_i$ (規則3のabort伝播は祖先側には影響しないため) 4. $a_j<a_i$ (規則3より) 従ってLRC性を満たし、以上より$Gen(ESGT)\subseteq PRED$。$\square$ ### その他のプロトコルの拡張 SGT系列は非常にオーバヘッドが大きいプロトコルなので、できれば他の軽いプロトコルを拡張することでLRCを保証したい。 例えば、2PLをベースに拡張したいときは、commitとabortに関する順序制約も設けることになる。$precede, follow$集合をESGTと同様に維持し、2PL+規則2+規則3のようにした形が拡張2PL(E2PL)。E2PLはLRCのスケジュールを全て生成できないことに注意。 同様に、Timestamp ordering(TO)を拡張したETOも考えられる。
×
Sign in
Email
Password
Forgot password
or
By clicking below, you agree to our
terms of service
.
Sign in via Facebook
Sign in via Twitter
Sign in via GitHub
Sign in via Dropbox
Sign in with Wallet
Wallet (
)
Connect another wallet
New to HackMD?
Sign up