Database Concurrency Control Papadimitriou 読書会第5回議論メモ

勉強会について

Database Concurrency Control Papadimitriou 読書会第5回 - connpass の議論メモです。

自分のメモをベースにまとめています。発言の聞き間違い、解釈違いの可能性があることをご了承ください。

特記の無い引用は本で議論した箇所を示しています。

Theory of Database Concurrency Control

作者: Christos Papadimitriou
出版社/メーカー: Computer Science Pr
発売日: 1986/07/01
メディア: ハードカバー
この商品を含むブログを見る

[memo]は私のメモです。勉強会で議論された内容ではないことにご注意ください。

今回、エルブラン・セマンティクスで検証を行っています。エルブラン・セマンティクスの詳細は過去記事を参照ください。
エルブラン・セマンティクス(Herbrand Semantics)理解メモ - ぱと隊長日誌

2.3 THE CRITIQUE OF FINAL-STATE SERIALIZABILITY

Using Semantics

Final-State serializability is certainly "syntactic," in that it ignores the semantics of the transactions and the integrity constraints of the database.

final-state serializability (FSR) は意味論の観点では考えていないということ。

Commutativity

可換性のこと。

[memo]
交換法則 - Wikipedia

write steps がインクリメント（例：f(x) = x + 1）するだけとする。
A₁ : R(x)W(x)
A₂ : R(x)W(x)

この時、A₁A₂ も A₂A₁ も全体としては結果に変わりがない。だが、この2つのスケジュールは final-state equivalent とは言えない。

[memo]
ここではスケジュールが final-state serializability かではなく、2つのスケジュールが final-state equivalent であるかを確認していることに注意が必要です。

◆ A₁A₂ ⇒ R₁(x)W₁(x)R₂(x)W₂(x)
H(R₁(x)) = f_0x()
H(W₁(x)) = f_1x(f_0x())
H(R₂(x)) = f_1x(f_0x())
H(W₂(x)) = f_2x(f_1x(f_0x()))
----------
H(x) = f_2x(f_1x(f_0x()))

◆ A₂A₁ ⇒ R₂(x)W₂(x)R₁(x)W₁(x)
H(R₂(x)) = f_0x()
H(W₂(x)) = f_2x(f_0x())
H(R₁(x)) = f_2x(f_0x())
H(W₁(x)) = f_1x(f_2x(f_0x()))
----------
H(x) = f_1x(f_2x(f_0x()))

それぞれの H(x) が異なることから final-state equivalent でないとわかります。

Copiers

"f(...,x,...) = x" は恒等写像を意味している。

[memo]
恒等写像 - Wikipedia

恒等写像を考慮すれば、もっと緩い FSR が定義できるかもしれない。

[memo]
この節で例示されているスケジュールをエルブラン・セマンティクスから検証します。

◆ オリジナルのスケジュール
R₁(x)R₃(x)W₃(y)W₂(x)R₄(y)W₄(x)R₅(x)W₅(z)W₁(z)
H(R₁(x)) = f_0x()
H(R₃(x)) = f_0x()
H(W₃(y)) = f_3y(f_0x())
H(W₂(x)) = f_2x()
H(R₄(y)) = f_3y(f_0x())
H(W₄(x)) = f_4x(f_3y(f_0x()))
H(R₅(x)) = f_4x(f_3y(f_0x()))
H(W₅(z)) = f_5z(f_4x(f_3y(f_0x())))
H(W₁(z)) = f_1z(f_0x())
----------
H(x) = f_4x(f_3y(f_0x()))
H(y) = f_3y(f_0x())
H(z) = f_1z(f_0x())

◆ A₅A₁A₃A₂A₄ のスケジュール
R₅(x)W₅(z)R₁(x)W₁(z)R₃(x)W₃(y)W₂(x)R₄(y)W₄(x)
H(R₅(x)) = f_0x()
H(W₅(z)) = f_5z(f_0x())
H(R₁(x)) = f_0x()
H(W₁(z)) = f_1z(f_0x())
H(R₃(x)) = f_0x()
H(W₃(y)) = f_3y(f_0x())
H(W₂(x)) = f_2x()
H(R₄(y)) = f_3y(f_0x())
H(W₄(x)) = f_4x(f_3y(f_0x()))
----------
H(x) = f_4x(f_3y(f_0x()))
H(y) = f_3y(f_0x())
H(z) = f_1z(f_0x())

この2つのスケジュールで H(x), H(y), H(z) は一致しており、オリジナルのスケジュールが FSR にみえます。ですが、papa本ではオリジナルのスケジュールが FSR ではないとしています。

この疑問を解くヒントになりそうな資料がありました。

Copiers. Suppose we know that t3 and t4 simply copy their arguments via r(X)w(Y) and r(Y)w(X). Then, r1(X)r3(X)w3(Y)w2(X)r4(Y)w4(X)r5(X)w5(Z)w1(Z) is equivalent to t5t1t3t2t4 although it's not final state serializable. key- r5 read X0.
https://webcourse.cs.technion.ac.il/236510/Spring2018/ho/WCFiles/ch3.pdf

"key- r5 read X0" とあります。確かに2つのスケジュールで H(R₅(x)) は異なります。

もし A₃, A₄ が恒等写像であるとすれば、
H(R₅(x)) = f_4x(f_3y(f_0x())) = f_0x()
となります。これであれば2つのスケジュールで H(R₅(x)) が等しくなります。

ただ、最終状態のエルブラン・セマンティクスでなく、途中のエルブラン・セマンティクスが等しくないことで final-state equivalent でないといえるのかが確信を持てないでいます。

今回の記事では最終状態のエルブラン・セマンティクスが等しければ final-state equivalent であるとしました。Weikum本から定義を引用します。

DEFINITION 3.6 Final State Equivalence
Let s and s' be schedules. s and s' are called final state equivalent, denoted s ≈_f s', if op(s) = op(s') and H[s] = H[s'], i.e., s and s' comprise the same set of operations and have the same Herbrand semantics.
Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery (The Morgan Kaufmann Series in Data Management Systems)

Integrity Constraints

この節は FSR の話と言うよりトランザクション (TX) の正しさとは何か、という話に近いのでは。一方で、全部終わった後に上手く行くなら良い（途中は無視！）ということから考えると FSR にもつながる。

Dead Transactions

TX を勝手に除いてはダメ、としているが、不要な制限ではないか？Integrity Constraints を守っていさえすればよいのでは？
だが、これを許すと初期状態＝最終状態、つまり「何もしない（全ての TX を取り除く）」ということを許してしまう。なのでそんなわけはない。

[memo]

Schedule s is not final-state serializable, as it can be easily checked. It is, however, final-state equivalent to the serial schedule consisting of the transaction A₂ alone!

これをエルブラン・セマンティクスから検証します。

◆ オリジナルのスケジュール
R₁(x)R₂(y)W₁(y)W₂(y)
H(R₁(x)) = f_0x()
H(R₂(y)) = f_0y()
H(W₁(y)) = f_1y(f_0x())
H(W₂(y)) = f_2y(f_0y())
----------
H(x) = f_0x()
H(y) = f_2y(f_0y())

◆ A₁A₂ のスケジュール
R₁(x)W₁(y)R₂(y)W₂(y)
H(R₁(x)) = f_0x()
H(W₁(y)) = f_1y(f_0x())
H(R₂(y)) = f_1y(f_0x())
H(W₂(y)) = f_2y(f_1y(f_0x()))
----------
H(x) = f_0x()
H(y) = f_2y(f_1y(f_0x()))

◆ A₂A₁ のスケジュール
R₂(y)W₂(y)R₁(x)W₁(y)
H(R₂(y)) = f_0y()
H(W₂(y)) = f_2y(f_0y())
H(R₁(x)) = f_0x()
H(W₁(y)) = f_1y(f_0x())
----------
H(x) = f_0x()
H(y) = f_1y(f_0x())

◆ A₂ のスケジュール
R₂(y)W₂(y)
H(R₂(y)) = f_0y()
H(W₂(y)) = f_2y(f_0y())
----------
H(x) = f_0x()
H(y) = f_2y(f_0y())

「オリジナルのスケジュール」と「A₂のスケジュール」で H(x), H(y) が一致することを確認できました。

最後の状態に影響するものを live とする。有向グラフ D(s) で A_∞ にリーチしていれば live ということ。

(a) A write step is live in s if either it is the last write step on this entity, or it is the last write step for that entity before a live read step for the entity.
(b) A read step is live in s if there is a subsequent live write step in the same transaction.

read only TX はdead TX と言えるのではないか？R_∞ に影響を与えないため。

FSR は途中の観測者を考えない。R_∞ つまり最後の観測者だけ考える。Read Only Anomaly も考えなくて良い。

We say a transaction is dead in s if all of its steps are dead in s.

全ての step が dead なら TX も dead だ。
一部の step が dead でも TX まで dead とは言えない。w(x)w(y) で w(x) が R_∞ につながり、w(y) が dead となるようなケースが考えられる。

[memo]

Yet s' is final-state serializable, and therefore correct from our point of view, since it is equivalent to the serial schedule A₁A₃A₂

これをエルブラン・セマンティクスから検証します。

◆ オリジナルのスケジュール
R₃(z)W₃(y)R₁(x)R₂(y)W₁(y)W₂(y)
H(R₃(z)) = f_0z()
H(W₃(y)) = f_3y(f_0z())
H(R₁(x)) = f_0x()
H(R₂(y)) = f_3y(f_0z())
H(W₁(y)) = f_1y(f_0x())
H(W₂(y)) = f_2y(f_3y(f_0z()))
----------
H(x) = f_0x()
H(y) = f_2y(f_3y(f_0z()))

◆ A₁A₃A₂ のスケジュール
R₁(x)W₁(y)R₃(z)W₃(y)R₂(y)W₂(y)
H(R₁(x)) = f_0x()
H(W₁(y)) = f_1y(f_0x())
H(R₃(z)) = f_0z()
H(W₃(y)) = f_3y(f_0z())
H(R₂(y)) = f_3y(f_0z())
H(W₂(y)) = f_2y(f_3y(f_0z()))
----------
H(x) = f_0x()
H(y) = f_2y(f_3y(f_0z()))

「オリジナルのスケジュール」と「A₁A₃A₂のスケジュール」で H(x), H(y) が一致することを確認できました。

s' は s に A₃ を入れたことで FSR になった。A₃ を入れたことで A₁ を無効にした。

Strict Serializability

s = R₁(x)R₂(x)W₂(x)R₃(y)W₃(y)W₁(y)
このスケジュール s は s' = A₃A₁A₂ と final-state serializable だ。

s で A₂ の終了後に A₃ が開始している。一方 s' ではこれが逆順になっている。このような "inversion" が発生しないことを strictly serializable という。これはリカバリのコンテキストで議論されることが多い。

This is not a serious problem. The serial schedule s' should be regarded merely as a proof of the correctness of s, and as a proof it is certainly a valid one.

これはシリアスな問題ではない。シリアライザブルの判定に使っているだけだからだ。

Incorrect Views

以下のスケジュールを考える。
s = R₁(x)W₁(x)R₂(x)R₂(y)W₂(y)W₁(y)

It is final-state serializable, because it is equivalent to A₂A₁.
（中略）
Now A₂ reads x after it is updated, and yet reads an unupdated version of y: It saw an "inconsistent view," in which possibly the integrity constraint is violated.

s は FSR だが VSR ではないということだ。