Multiversion View Serializability の簡潔な定義

これは[自作DBMSアドベントカレンダー2020](https://adventar.org/calendars/5548)、5 日目の記事です。

こんにちは、starpoz です。DBMS を作る人が増えてきたかも！という状況を後押ししたいので、自作に必要な理論の話をしてみようと思います。


# はじめに

DBMS 自作したいですよね！私は元々トランザクション処理 (OLTP) に興味があり、2PL (Two Phase Locking) プロトロルにおける deadlock というものが嫌で、それをなんとかしたい、という動機から OLTP についての研究開発活動を始めました。その話はまたどこかでするとして、今日は **serializability (直列化可能性)** よくわかりません、という人のために、できるだけ簡潔だが正しい説明を試みます。え？DBMSの自作は？？？と思ったかも知れませんが、理論を知らないと作れないので遠回りですが仕方ないのです(半分くらい嘘)。

Serializability というのは、並行実行制御 (concurrency control、以後 CC) プロトコルが守るべきとされる性質で、ACID 特性の I (Isolation) とか C (Consistency) に絡む性質です。ひとことでいうと、trivial scheduler (素朴なスケジューラ) の実行すなわちトランザクションの直列実行を「正しい」(correct) と見做し、それと**「等価」(equivalent)**な実行であれば serializable といって、正しいものと等価なんだから正しいものと見做すということです。「等価」な実行とはなんでしょうか？色々あるのですが、ひとつ選ぶとするとそれはズバリ、**ビュー等価 (view equivalence)** です。Conflict equivalence だと思った方、ゴメンナサイ、でも view equivalence の方が広い空間なので今日覚えていってください。


# View serializability の定義

これから、定義を見せながらひとつひとつ説明していきます。集合や写像の記法が出てきますが、この記事では多少は説明を加えるようにしますので、不安な方でも大丈夫です。私もいい年したオッサンですが、ちょっと前まで全然このあたりの記法の意味するところを分かったようで分かってませんでした。必要なら教科書などで勉強すればいいのです。例えば [Mathematics for Computer Science](https://courses.csail.mit.edu/6.042/spring17/mcs.pdf) (ライセンス: CC BY-SA 3.0) などが利用できます。今回の話でいえば、4.1 Sets、4.3 Functions、10.6 Partial Orders あたりが関連すると思います。

さて、トランザクション処理ではデータを扱うわけですから、定義しましょう。

**定義 1.** データエンティティの集合を $\mathbb{D} := \\{x, y, z, \dots\\}$ とかく。

ただ、ひとつ集合を考えて $\mathbb{D}$ という記号で表しただけです。要素として $x, y$ などをよく使います。データエンティティはアクセスする単位を意味します。これ以上細かい単位ではアクセスしないものとします。たとえば、$x \in \mathbb{D}$ が実は 2 つに分かれて、半分だけアクセスする、なんてことは考慮しませんということです。

データを定義したので、それにどうアクセスするかを定義しましょう。

**定義 2.** オペレーションの集合 $\mathbb{O} := \\{r,w\\} \times \mathbb{D}$ とかく。$p \in \\{r,w\\}$、$x \in \mathbb{D}$ について、$(p,x) \in \mathbb{O}$ を $p(x)$ とかく。$type(p(x)) := p$、$entity(p(x)) := x$ とかく。

$\\{r, w\\}$ というのは、$r$ と $w$ の 2 つの要素を持つ集合で、それぞれ read と write を表します。そうです、読み書きです。え、insert は？ delete は？ ありません。許してください。今回のモデルでそこは扱いません。insert/delete に伴う phantom problem は興味深い問題なのですが、それもこのモデルではないことになっています。$\times$ は直積演算のことで、集合と集合からタプル集合を作ります。$r(x)$、$w(x)$ という書き方は業界の慣例みたいです。関数っぽく見えますが、気になさらないよう。要は $x$ を読む、書く、というオペレーションですね。これでデータの操作ができます。$type$ や $entity$ はオペレーションの中身を指す関数だと思ってください。

**定義 3.** $t \subset \mathbb{O}$ をトランザクションとよぶ。$t_0 := \\{w(x) \mid x \in \mathbb{D}\\}$ とする。トランザクション全体を $txset$ とかく。

はい、$\mathbb{O}$ の部分集合をトランザクションとここで定義します。トランザクションは複数の読み書き操作のことだったのです。Operation の order や sequence を考えることもあるのですが、今回は議論に関係ないので入っていません。注意点として、$t$ は operation の集合なので、$r(x) \in \mathbb{O}$ が $t$ に含まれるか含まれないか、しか表現できません。$x$ を複数回読んだり書いたりする操作はどう表現するの？という問いに対しては、このモデルでは表現できません、ということになります。トランザクション毎にキャッシュデータを用意すれば、複数回の read や write 操作をひとつにまとめることは可能なので、モデルに入ってなくても大丈夫です。$r(x),w(x) \in t$ のときは特別な意味を持っていて、read-modify-write (RMW) と呼びます。write が先で read が後 (self-read とでも呼ぶべき) という意味論も考えられますが、ここでは read が先で write が後とみなします。トランザクションというものは大雑把に捉えると、複数のデータエンティティを読んで、処理して、複数のデータエンティティを書くということをしていますので、このようなモデルでも現実をそれなりに表現できます。$t_0$ は初期状態を表すトランザクションです。集合の内包表記を使っていますが、要は全データエンティティになにかしら値を書いているという意味を持っています。$txset$ はトランザクションというものの全体からなる集合を指していますので、$\mathbb{O}$ のべき集合になります。

**定義 4.** トランザクションの列  $T = \\{t_i \in \mathbb{O} \mid i \in \mathbb{N}\_{1\le e}\\}$ を考える。

- $T^+ := T \cup \\{t\_0\\}$ とかく。
- $T' \subset T$ について、$op(T') := \\{(i,o) \mid t\_i \in T', o \in t\_i\\}$ とかく。
- $(i, r(x)), (i, w(x)) \in op(T')$ をそれぞれ $r\_i(x)$、$w\_i(x)$ とかく。
- $(i,o) \in op(T')$ について、$tid((i,o)) := i$、$type((i,o)) := type(o)$、$entity((i, o)) := entity(o)$ とかく。
- $rop(T') := \\{o \in op(T') \mid type(o) = r\\}$ とかく。
- $wop(T') := \\{o \in op(T') \mid type(o) = w\\}$ とかく。
- $T$ 全体を $\mathbb{T}$ とかく。


$T$ は本当は列なのですが、部分列などのために集合の操作を使いたいので、集合として定義しています。集合に対して列には、同じ内容の要素が複数回出てきても良いという違いがあります。たとえば、$t\_1 = t\_2 = \\{r(x), w(y)\\}$ でも大丈夫です。ただし、$t\_1$ と $t\_2$ は別物として扱います。$\mathbb{N}\_{b\le e}$ は $b$ 以上 $e$ 以下の整数の集合です。ただし $0 \le b < e$ とします。あとは、ちょっと多いですが、$T+$ や $T' \subset T$ や関連する集合およびその要素の表現についていくつか定義しています。たとえば、$r\_i(x)$ は、$T^+$ における $i$ 番目のトランザクションの $x$ を read するオペレーションを、$wop(T')$ は、どのトランザクション由来か分かるようにした $T'$ に含まれる write operation の集合、を意味します。$\mathbb{T}$ は、$T \in \mathbb{T}$ と書いたときに、$T$ はトランザクション列なんだよと簡潔に伝えるために導入した記号です。

ここまでで、データがあって、オペレーションがあって、オペレーションを複数含むトランザクションがあって、トランザクションの列があって、という状況までモデル化できました。あとは、トランザクション同士がどう関係しているかをモデルに入れてあげる必要があります。それが version function です。

**定義 5.** $T \in \mathbb{T}$ があったとき、写像 $V: rop(T) \rightarrow wop(T^+)$ について考える。$r\_i(x) \in rop(T)$ について、$V((r\_i(x)) = w\_j(y)$ とおく。任意の $r\_i(x)$ について $i \neq j$ および $x = y$ を満たすとき、$V$ は $T$ の version function と呼ぶ。

- $T$ の version function 全体を $ver(T)$ とかく。
- $T' \subset T$ および $V \in ver(T)$ について、$r\_i(x) \in rop(T')$ について $V'(r\_i(x)) = V(r\_i(x))$ であるような写像 $V': rop(T') \rightarrow wop(T^+)$ を、($V$ における) $T'$ の view と呼び、$V|\_{T'}$ とかく。

各 read operation が、どの write operation の書いた値を読んだか、という情報が version function です。他のトランザクションの書いた値を読むから $i \neq j$ ですし、同じデータエンティティの値を読むわけだから $x = y$ という制約がついているのですね。Version function の定義域 (つまり $rop(T')$ の元となる $T' \subset T$) を限定して考えることが多いので、それを view とする定義が便利です(この記事では使わないけど)。値域が $wop(T^+)$ となっており、$t\_0$ は任意の $x \in \mathbb{D}$ について $w(x) \in t\_0$ を満たしますので、どのような $T$ についても version function は必ず存在します。

**定義 6.** $T \in \mathbb{T}$、$V \in ver(T)$ について、$(T,V)$ を history と呼ぶ。History 全体を $\text{H}$ とかく。

トランザクション列 $T$ と version function $V$ の組(要素 2 のタプル)を history と呼びます。これが serializable かどうか、というのをこれから議論していくわけです。

**定義 7.** $T \in \mathbb{T}$ について、$T^+$ 上の全順序 $S \subset T^+ \times T^+$ を考える。ただし、任意の $t\_i \in T$ について $t\_0 <_S t\_i$ とする。このような $S$ の全体を $txseq(T)$ とかく。

$S$ は二項関係なので、トランザクションの組で表現します。$(t\_i, t\_j) \in S$ は、$t\_i <_S t\_j$ を意味します。$<\_S$ は $S$ における大小関係を表す二項演算子とします。$S$ は全順序なので、任意のトランザクション同士が比較可能です($\le\_S$ ではなく $<\_S$ を使っているところから分かるように、任意の $t\_i \in T^+$ について $(t\_i, t\_i) \notin S$ とします)。$t\_0$ は初期状態を表す特殊なトランザクションなので、一番小さいという制約を入れています。

やっと trivial scheduler の実行を表現できるところまできました。先程定義した全順序 $S$ を使います。

**定義 8.** $(T,V) \in \text{H}$ および $S \in txseq(T)$ について考える。$r\_i(x) \in rop(T)$ について、$C\_{i,x} = \\{t\_k \in T^+ \mid w(x) \in t\_k \wedge t\_k <\_S t\_i \\}$ を考える。$C\_{i,x}$ の $S$ における最大元を $t\_j$ とおく。任意の $r\_i(x)$ について $V(r\_i(x)) = w\_j(x)$ であるとき、$V$ は $T,S$ の correct version function と呼び、$corver(T,S)$ とかく。$corver(T) := \\{corver(T,S) \mid S \in txseq(T)\\}$ とかく。

「正しい」 (correct) version function を定義しています。トランザクションを直列実行するという trivial scheduler の振る舞いによって生み出される version function が $corver(T)$ に含まれているということです。$S$ の順序でトランザクションが実行され、「直前」に $x$ を書いたトランザクションの書いた値を読む、という振る舞いが前提となっています。$corver(T,S)$ と $corver(T)$ で同じ $corver$ が使われていますが、関数のオーバーロードと思って名前の再利用を許してください。型が違うので別の関数です。

**定義 9.** $h = (T,V) \in \text{H}$ について、$V \in corver(T)$ のとき、$h$ は view serializable であるという。view serializable な history の全体を $\text{MVSR}$ とかく。

Trivial scheduler の生成した version function が corver(T) に含まれているという定義になっています。trivial scheduler の生成するであろう history と view 等価であるときに、その history は view serializable である、ということです。multiversion という言葉がひとことも出てきてませんが、mono(single)version について議論するには、ここで定義した history にさらなる制約を加える必要があります。既存の定義との等価性については、別途証明が必要で、手元では確認していますが、ここに書くには長すぎるので興味がある人はやってみましょう。


# MVTO スケジューラの正しさを示す

定義 9 のままだと使いづらいので、もっと分かりやすいルールにしてあげる必要があります。たとえば、MVTO (Multiversion Timestamp Ordering) というスケジューラは、各トランザクションにユニークなタイムスタンプ $ts: T^+ \rightarrow \mathbb{N}$ ($i \neq j$ のとき $ts(t\_i) \neq ts(t\_j)$) を付与して、以下の 2 つのルールを守るように動作します。

- **rule-1**: $r\_i(x) \in rop(T)$ について、$V(r\_i(x)) = w\_j(x)$ とおいたとき、$ts(t\_j) < ts(t\_i)$。
- **rule-2**: $r\_i(x) \in rop(T)$ について、$V(r\_i(x)) = w\_j(x)$ とおき、$w(x) \in t\_k$ であるような $k \neq i,j$ について、$ts(t\_k) < ts(t\_j) \vee ts(t\_i) < ts(t\_k)$。

$ts(t\_0)$ は最小値を取るという制約は必要なので入れておきましょう。それでは、次の定理を証明してみましょう。

**定理 10.** MVTO スケジューラの生成する history は view serializable である。

**証明** $T \in \mathbb{T}$ について、定義 9 の rule-1 および rule-2 を満たす $V \in ver(T)$ と $ts: T^+ \rightarrow \mathbb{N}$ をとる。$ts(t_i)$ は $t_i \in T^+$ に対して unique だから、$ts(t\_i) < ts(t\_j) \Leftrightarrow t\_i <\_S t\_j$ であるような $S \in txseq(T)$ が存在する $\;$(1)。$r\_i(x) \in rop(T)$ について考える。$V(r\_i(x)) = w\_j(x)$ とおく。rule-1 より、$ts(t\_j) < ts(t\_i)$。これと (1) より $t\_j <\_S t\_i$ $\;$(2)。$w(x) \in t\_k \in T^+$ であるような $k \neq i,j$ を考える。そのような $k$ が存在した場合、rule-2 より、$ts(t\_k) < ts(t\_j) \vee ts(t\_i) < ts(t\_k)$。これと (1) より $t\_k <\_S t\_j \vee t\_i <\_S t\_k$ $\;$(3)。定義 8 の $C\_{i,x} = \\{t\_l \in T^+ \mid w(x) \in t\_l \wedge t\_l <\_S t\_i \\}$ について考える。(2) と (3) より、$t_j$ は $C\_{i,x}$ の $S$ における最大元。よって、$V = corver(T,S) \in corver(T)$。すなわち、$(T,V)$ は view serializable。



# おわりに

思ったより簡単でしょう？ここまで読んでくれたあなたは、今後新しい CC プロトコルを思いついたとき、それが view serializable であることを証明するための道具を手にいれたことになります。Serializability の理論、怖くないよということで、ひとつ皆さんも勉強してみましょう。

入手性を考えると、私が知る限りほぼ唯一の教科書は、[Transactional Information Systems](https://www.amazon.co.jp/dp/B01253U1BC/) ですが、適宜参照している論文にもあたる必要はあると思います。私はこの教科書の内容で自分の必要なところをもっとスッキリとさせたくて、このような定式化を自分でやり直しています。

ここ 10 年くらいは、特に In-memory DBMS と分散 DBMS の文脈で、新しい CC プロトコルがどんどん提案されています。一方で、背景にある理論は 1970〜1990 あたりのものがそのまま使われていることが多い印象があって、再構築およびさらなる発展が必要だと感じています。ということで、トランザクションの理論に興味が出てきた方は、是非一緒に頑張りましょう。

それでは、皆さん良いトランザクション人生を。

# 宣伝

[Project Tsurugi (劔)](https://project-tsurugi.connpass.com/) という DBMS 作ろうぜ、というプロジェクトがあります。
先日[経過報告会](https://project-tsurugi.connpass.com/event/191252/)が開催され、資料もたくさん置いてありますので、興味のある方は是非見てみてください。
プロジェクトがどのようなものかについては、1 年くらい前の記事になりますが、[Project Tsurugi(劔)とAsakusaについて](https://okachimachiorz.hatenablog.com/entry/2019/12/24/230908) あたりに中の人の考えや現状認識などがあります。


# 参考文献

- [Mathematics for Computer Science](https://courses.csail.mit.edu/6.042/spring17/mcs.pdf)
- [Transactional Information Systems](https://www.amazon.co.jp/dp/B01253U1BC/)