Transactional Information Systems 3章 3.1〜3.6まで

先週は全然読めなかった。。3章が長めで、3.7はちょっと重そうなので、前半をまとめてみる。

3章はPage model(read/write model)のトランザクションに対して、トランザクションを並列実行したときの「正しさ」を定義することを目標にしている。トランザクションが失敗するケースを考え始めると大変なので、まずは失敗がないことを前提に話を進めていく。失敗するケースはPart III、11章から扱い始める。

3.2では、lost-update,inconsistent-read,dirty-readという良くある問題を軽く説明。

3.3ではhistoryとscheduleを定義している。"A schedule is a prefix of a history"という記述があって良く意味がわからなかった。でも、とりあえず読み進めていったら後で分かった。厳密な定義を書き始めるときりがないので雰囲気で書いてみる。scheduleもhistoryも結局は複数のトランザクションが混ざったようなもの。ただし、historyには、abortかcommitで完了したトランザクションしか含まれていない。なのでhistoryはcomplete scheduleとも呼ばれるらしい。対して、scheduleは完了していないトランザクションも含む。scheduleの末尾に色々追加して全部のトランザクションが完了してしまえばhistoryになる。なので、prefixという事らしい。このあとはorderに関しての話題などを取り扱った。どんどん表現と説明が簡潔なのに分かりやすくなっていく様は格好良かった。

3.4は「正しさを定義するためにはこんな事が必要」という話と、今後の流れの説明。とりあえず、scheduleの等価性を定義する。その後、serial historyとの等価性を利用して、serializabilityというものを定義。

3.5は等価性を定義するために便利なHerbrand semanticsというものを定義。今まで、「w_i(x)の結果は、それまでトランザクションiが読み込んだすべての値に依存する」みたいに言葉で表現していたものを、全部数式っぽいもので表現できるようになった。

3.6はfinal state equivalenceというものを定義。2個のhistory(schedule)があったときに、データの流れ方が同じかどうかを判定しているのだと思う。それを厳密に説明するために、reads-from relationやaliveなどの関係・概念を定義した。その後、それを使ってfinal state serializabilityというものを定義。final state serializableなhistoryはFSRというクラスに属する。

FSRは定義できたけど、あるhistoryがFSRに含まれるかどうかはどうやったらチェックできるのか。3.7からはその話。定理ばっかりなので、ちょっと休憩してから読む。