加筆中｡

p59「A schedule together ~」から「p62 Proposition 3.1 」まで読んだ。

Multiversion(Version funtionまで考慮したschedule)のcorrectnessを定義したり、storage costなどについて学んだ。storageコストは若干不評気味だった。

勉強会開始前にストーンブレーカーの最近のDB界隈への嘆き？のプレゼンについて話題になった。
http://www.jfsowa.com/ikl/Stonebraker.pdf
- 某slackの某先生の書き込みから

full scheduleのセマンティクス

version functionが定義されているscheduleをfull scheduleという
- full scheduleを(s,V)と表記する
scheduleに対してversion functionまで考えることでtransactionとentityの相互作用を決定できる*1
- 今まではfullでないスケジュールにstandard version functionを暗黙的に仮定してこの相互作用を扱っていた。
- version functionを含めたセマンティクスになるように修正・拡張する
  - 今まではInterpretation I、初期値Xの元でstep aがread,writeする内容(いわゆるherbrand semantics)を$a_s(I,X)$で表現していた
  - Version functionをここに加る
    - $a^V_s(I,X)$
      - 例:aをb,cをreadした上でのwrite stepだとすると
      - $a^V_s(I,X)=f_a(b^V_s(I,X),c^V_X(I,X))$
        
        直感的な意味:b,cのread結果に関数faを適用したものがaがwriteする値
        
        $a^V_S(I,X)=b^V_S(I,X) $のときb=V(a)である
        
        read aとherbrand semanticsが一致するbが存在している場合version functionがaに対応ずけるstepはwrite bになる。
    - 最終状態$s(I,X)$を$s^V(I,X)$で表現する
      - $w(x)∈A_0$の場合、$a^V_s=x∈X$
なおversion functionを考えないherbrand semanticsに関しては過去にこのエントリでまとめている。

https://yuyubu.hatenablog.com/entry/2019/07/04/interpretation

full scheduleについてのview equivalentを考える

(s,V)と(s',V')がview equivalentであるには以下の３要素が一致する必要がある
- 全てのinterpretation I
- 初期状態X
- 各readで読み取った値

we say that (s,V) and (s',V') are view equivalent if, for all interpretations I and inital states X, the values read by each transaction (includeing the final pseudotransaction ) in both schedules are identical.

Theorem 2.2に類似したfull scheduleのview equivalenceの条件を考えたい
- 備考:Threorem 2.2(p31)

Theorem 2.2 Two schedules s and s' are view equivalent if and only if the involve the same set of transactions and D(s) = D(s')

補足:D(s)というのはSchedule sのread-from関係を図示したDirected Graphのこと

non-full scheduleのequivalenceをfull suchedule向けに拡張

version functionを考えていかなった従来のequivalenceの定義を拡張しfull schedule (s,V)のequivalenceを考えていく。まずはTheorem 2.1(これは Final State equivalent だが)を拡張しview equivalentを考える。

なお以下の復習書は読書会の範囲を逸脱して私が個人的に自習したものです。

(復習)p23 Theorem 2.1 FS eq ↔︎ D1(s)=D1(s')

※FS eq:=final state equivalentです(長いので勝手に略した)

Theorem 2.1の証明まで軽くまとめています｡長いです。注意してください。

Theorem 2.1 sとs'がFS等価である ↔︎ D1(s)=D1(s')
- (p21)原文掲載

Theorem 2.1: Two schedules s and s' are final-state equivalent if and only if they involve the same transactions, and D1(s)=D1(s')

　#### 用語の解説

D1の定義
- D(s)から最終状態に到達しないnodeをすべて削除したもの
D(s)=(V,A)
- V=$\hat{s}$に含まれる全てのread/write step
- A:$\hat{s}$内のstepのタプルであり、2種類ある
  - case 1:(ai,aj)
    - 同一トランザクション内でread step aiとwrite step ajがi<jの順序で存在する場合(ai,aj)をAに追加する
  - case 2:(ai,bj)
    - ai,bjはそれぞれ異なるトランザクションに属する
    - ai,bjはそれぞれ同じentityに対するstepである
    - aiがwrite,bjがreadであり、$\hat{s}$においてaiの直後にbjが続いている
- つまりAのcase1はトランザクション内の、case2はトランザクション間のread-fromの依存関係を表現している
D1例

A0:(初期値writes略)
A1:R(x)R(y)    W(z)W(x)
A2:        R(y)                        W(y)W(x)
A3:                    R(z)W(z)R(x)W(y)
A∞:(最終値reads略)

W3(y)は直後のW2(y)に上書きされるためD1では削除される
- ※補足:A3のW(y)はW3(y)と表記する
- 同様にW0(z),W1(x),R3(x)は削除される
$pre_D(v)$
- node vとvに先行するnodeのみに限定したdirected graph Dのこと

Theorem2.1証明

theorem 2.1再掲 :FS eq ↔︎ D1(s)=D1(s')

if direction (←)

D1(s)=D1(s')→FSRを証明すれば良いが、今回はより強い帰納的主張$pre_D(v)=pre_D(v')→v_s(I,X)=v_{s'}(I,X)$を証明する
強い命題:s,s'中のstep vの$pre_D(s)=pre_D(s')$が成り立つ場合、任意のI,Xで$v_s(I,X)=v_s'(I,X)$
- 証明
  - case1:$ pre_D(s)$が一つのstep vしか含まない場合、vは必ずwrite step $w \in A_0$である
    - 先行するreadが存在せず,function f ∈ Iのargumentは0,であり、vはIまたはXに依存する定数である
  - $pre_D(s)$が一つ以上のstepを含む場合
    - v=s中の唯一のread stepである場合
      - 仮定より$pre_D(s)=pre_D(s')$である
        
        wからなる$pre_D$グラフは同一のものになる
        
        vより先行するwの$pre_D(w)$グラフは小さくなりvを含まない(非循環)
        
        $w_s(I,X)=w_{s'}(I,X)$が成り立つ
        
        wが$pre_D(s)$の最終ステップである場合、sがreadする値である
        
        $v_s(I,X)=w_s(I,X)$が成り立つ
        
        同様に$v{s'}(I,X)=w{s'}(I,X)$である
    - v=s中の唯一のwrite stepである場合
      - $pre_D(v)$は全てreadである
        
        vに先行する任意のread step $rⁱ$で$pre{D_1(s)}(rⁱ)=pre{D_1(s')}(rⁱ)$が任意のiで成り立つ
        
        note:特に説明はないが、おそらく全ての$rⁱ$が初期値Xを読むからだと思われる
        
        vのinterpretationは任意のI,Xで一致する
        
        $v_s(I,X)=f(r¹_s(I,X),...,r^k_{s}(I,X))$
        
        $=f(r¹{s'}(I,X),...,r^k{s'}(I,X))=v_{s'}(I,X)$
    - note:if向きの証明はここで終わっている。(かなり不十分な気がする)
      - only one なread/write stepがある時の$pre_D$の一致→s,s'のintepretationの一致までしか証明できていない。
        
        2個以上writeやreadが混ざってる時の$v(I,X)$の一致が言えてないと思う。
      - only one stepの$pre_D$の一致、2個目の$pre_D$の一致,...n個目の$pre_D$ が一致することを証明して任意のvで一致するという風に証明するのかな。

only if direction(→)

only ifの向きではsとs'がFS eqと仮定し、その場合に必ずs,s'から成るDが一致することを証明する
- final-state equivalentであるということは以下のことが言える
  - 任意のentityのdomainが一致
  - 任意のwrite stepのinterpretationが一致
    - もちろん最終状態も一致
- 外向きのエッジの出次数(out of degree)が0のノード(sink)を持つグラフGを考える
  - fはk個の$G_i=(V_i,E_i),i=1,...,k$をsink $v_i$のGに割り当てる関数である
  - $G=f(G_1,...,G_k)$
  - Gの定義　
    - 前提(直接本に書かれていいないが解説として書き残しておく　)
      - i:G中のnode個数
      - j:G中のtransaction個数
    - (a):Gの全node $\bigcup^k_{i=1}V_i$は sinkとなる$A_j:W(x)$とそのトランザクション内のW(x)以前の全てのR(y)である
    - (b):Gの全arc $\bigcup^k_{i=1}$は以下の２種類になる
      - $(v_i,Aj:R(y_i))$
        
        ※ここの$v_i$はGの single sink nodeではなく、$R(y_i)$がreadしている何らかのwrite結果⊇$A_0$の意味。
        
        シンタックスがややこしいが、おそらく各readは対象entityに体操するin-degreeが必ず1になる(ようなwriteが存在する)ことを示したいものと思われる
      - $(A_j:R(y_i),A_j:W(x))$
        
        read からsingle sinkとなるwriteへのarc
    - 具体例は箇条書きブロックの末尾に示した。
    - Gを組み合わせてD1(s)を再構築することが可能である
    - s中の任意のwrite step vで$v_s(I,X)=pre_{D(s)}(v)$であり､これをwriteの最終stepに適用すると
      - $pre{D(s)}(v)=v_s(I,X)=v{s'}(I,X)=pre_{D(s')}(v)$
        
        $pre{D(s)}(v)=pre{D(s')}(v)$の等価性は上記のGの性質より得られる
        
        中間の$v_s(I,X)=v{s'}(I,X)$の性質は$A\infty$が読むreadによって保証される｡
        
        only if側の仮定がFS eqなのでs,s'の最終readが読む値は同一である｡
        
        D1はA∞のreadより前にある全てのGの合体したものなのでD1(s)=D1(s')が言える□

Theorem 3.1 view equivalence (theorem 2.1の拡張)

Theorem 3.1:(s,V)と(s',V')がview equivalent ↔︎ s-s'のトランザクションが同一かつV'が全てのread stepで同じ値の場合

Theorem 3.1: Two full schedules (s,V) and (s',V') are view equivalent if and only if s and s' have the same transactions , and V and V' agree on all read steps.