今日はCSRの定義が3つもあることを知ることができた。雑なので後日結構手を入れてfixするかも。

p46「Theorem 2.9」からp49「theorem 2.10」まで読んだ。次回p49「theorem 2.10のproof」から

Conflicts and Commutativity(可換を使ったCSRの2つ目の定義)

s
A1:R(x)        W(x)
A2:    R(x)W(y)

s'
s
A1:R(x)    W(x)
A2:    R(x)    W(y)

定理2.9`s~*s'`が成り立つ ↔︎s とs'がConflict equivalentである

Theorem 2.9 Two schedules s and s' are conflict equivalent if and only if s~*s'
証明
- if direction(←):任意の回数の~交換はCSRを違反しない(雑)
- Only if direction(→) :
  - 2つのスケジュールに出現する順序が違うstepのペアの数をkとする
  - k=0のとき、明らかにs~*s'
  - k>0のとき
    - s'で前後関係が異なるstepが2つ存在する
      - 英語Memo:out of order=順序が違う
      - ペアの順序関係が違うstepが隣接しているもののみの場合、明らかにs~*s
      - sと順序関係が違うs'のstep pairが隣接していないものがある場合、pairの間にあるstepとpairの少なくとも1要素とparitを作っているthird stepが必ず一つ存在する
        
        s'から~操作を実行して得られるorderをs''とする
        
        s''のout of order-step pair数は最大でk-1になる
        
        1回の交換の副作用で他のpairのorderも修正される可能性があるため
        
        この操作を繰り返していくことでs''~*sとすることができる推移的にこれはs'~*sである□

f:id:yuyubu:20191204210745j:plain

この新しい定義を使えばuniterpreted mdelのtransactionのserializabilityを検査することができる
- Readwrite,multiversionのセマンティクスを必要としない。
  - orderとconflict pairのみでschedulrのvalidationが可能である
Example 2.6
- s=a1b1a2c1a3b2c2c3a4c4b3
  - Transaction
    - A = a1,a2,a3,a4
    - B = b1,b2,b3
    - C = c1,c2,c3,c4
- Conflict c:{a2,b1},{a2,c1},{b1,c1},{b3,c4}

stepのconflict pairでdirected graphを作り、transactionの粒度にshrinkさせればb,c間にcycleがあることがわかる

View serializabilityは常にmonotonicな性質ではない
CSRはmonotonicな性質である
- G(s)でacyclicな場合、任意のprojection ででacyclicになる
  - CSRはVSRの中でmonotonicな性質を持つ最大の集合である。

Important concepts usually come in a number of alterative formulations