ぱと隊長日誌

ブログ運用もエンジニアとしての生き方も模索中

well-formedなトランザクションとlegalなスケジュール

はじめに

Transaction management におけるwell-formedなトランザクションとlegalなスケジュールについて説明します。

主に以下の資料を参考にします。
http://www.dis.uniroma1.it/~rosati/gd/1-concurrency.pdf
P60付近を参照ください。
ここでは exclusive locks を前提としています。本エントリでもこれに倣います。
shared locks も含めた議論はもう少し後のページにあります。

"Transactional Information Systems"も参考にしています。

Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery (The Morgan Kaufmann Series in Data Management Systems)

Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control and Recovery (The Morgan Kaufmann Series in Data Management Systems)

well-formedなトランザクションの定義

read/write操作する対象をアイテムAとします。

トランザクションTiのアイテムAに対するread/write操作pi(A)が "critical section" に含まれるとき、そのトランザクションTiはwell-formedです。"critical section" とはAに対する一連の操作をlock/unlockのペアで区切ることを指します。

Ti: … li(A) … pi(A) … ui(A) ...

この説明だと、トランザクション内で同じアイテムの操作に対し、複数回に分けてlock/unlockすることが認められているかがあいまいです。

Ti: li(A) pi(A) ui(A) li(A) pi(A) ui(A)

この点について、トランザクション本では以下の定義がされています。

LR2: For each x accessed by ti, schedule s has at most one rli(x) and at most one wli(x) step; in other words, locks of the same type are set at most once per transaction and per data item.
※LR1, LR3は省略した
Transactional Information Systems, P132

ここでは read lock (shared) と write lock (exclusive) を区別して考えている点が異なりますが、各トランザクションの各アイテム毎に最大1回だけロックする、とあります。つまり、トランザクション内で同じアイテムの操作を異なる "critical section" に分けることは認めていないとわかります。

legalなスケジュールの定義

スケジュールSでトランザクションTiがアイテムAに対するロックを保持している間、他のトランザクションがAに対してロックを保持することがなければ、そのスケジュールSはlegalです。つまり、legalなスケジュールでは同じアイテムに対して異なるトランザクションが同時にロックを保持することを認めていません。

well-formedとlegalの関係

well-formedか否かはトランザクションに対してであり、legalか否かはスケジュールに対してです。よって、これは個別に判定する必要があります。

S1 : l1(A) r1(A) w1(B) u1(A)
T1はAに対するロックしか保持してないのにBに対する操作を行っています。よってこれはill-formed(well-formedではない)といえます。

S2 : l1(A) l1(B) r1(A) w1(B) l2(B) u1(A) u1(B) r2(B) w2(B) u2(B)
T1がBに対するロックを保持している間にT2もBに対するロックを保持しています。このスケジュールSは not legal です。
T1についてだけ見れば、well-formedといえます。

S3 : l1(A) r1(A) u1(A) l1(B) w1(B) u1(B) l2(B) r2(B) w2(B) u2(B)
T1, T2ともにwell-formedであり、S3はlegalといえます。

なお、well-formedなトランザクションで構成されたlegalなスケジュールであっても、serializabilityを保証することはできません(Ghost updateが起こりえます)。serializabilityを保証する手法として two-phase locking (2PL) protocol があります。

参考

別の資料にはwell-formedなトランザクションが同じアイテムに対して2回ロックしてはならない、と説明しています。

  • Well-formed transaction
    • locks data object before accessing it
    • does not lock the same data object twice
    • unlocks all the locked objects before completion
http://www.cs.virginia.edu/~son/662.pdffiles/cc06.pdf

記号論理学における論証(前提と結論)の妥当性

記号論理入門(金子 洋之・著)」は自然演繹による証明を学ぶための入門書としてお勧めできます。
ですが、いくつかわかりにくい点もあります。その一つが論証の妥当性についてです。このエントリでは本の解説の補足をしながら、論証の妥当性について説明を試みます。

なお、引用元を明記していない箇所は本からの引用となります。

記号論理入門 (哲学教科書シリーズ)

記号論理入門 (哲学教科書シリーズ)

この本では妥当な論証について以下の説明をしています。

前提のすべてが正しく主張できるときには、結論もまた正しく主張できる
序章より

また以下のようにも言い換えています。

この条件が語っているのは、「前提のすべてが正しく主張できる」ときには、必ず「結論も正しく主張できる」、あるいは「前提のすべてが正しく主張できる」ことを認めたならば、「結論も正しく主張できる」ことを認めざるを得ない
序章より

以下の例が妥当な論証であることは先述の説明から理解できます。
「ある学生は論理学を学ぶ。論理学を学ぶものは誰も生物学を履修できない。ゆえに、学生の中には生物学を履修できないものがいる。」

ですが、以下の例は妥当な論証であるか否かがわかりにくいです。
「日本の首都は東京である。神奈川県の県庁所在地は横浜である。ゆえに北海道で一番大きな都市は札幌である。」

これを前提と結論に分けてみます。

  • 前提
    • 日本の首都は東京である。
    • 神奈川県の県庁所在地は横浜である。
  • 結論
    • ゆえに北海道で一番大きな都市は札幌である。

いずれの前提も結論も正しいのだから、これは妥当な論証といえるのでしょうか?実はこの論証が妥当とは言えません。

本ではこの論証について、前提と結論の間には何のつながりもないから「前提のすべてが正しく主張できるときには、結論もまた正しく主張できる」の条件を満たしているとは言えない、と解説しています。

これは「厳密含意 (strict implication)」を指しています。つまり、前提が成り立つようないかなる可能世界においても、結論が成り立つのでなければならない、ということです。

例えば、ある可能世界で北海道の一番大きな都市が函館になったとしたらどうでしょうか。前提は真だが結論が偽になってしまいました。これでは「前提のすべてが正しく主張できるときには、結論もまた正しく主張できる」といえず、妥当な論証といえないことがわかります。

論証の妥当性についてはWikipediaの説明のほうが納得しやすいかもしれません。

妥当な論証は前提が真であれば結論も必ず真となるもので、妥当な論証で前提が真で結論が偽となることはあり得ない。

論証 - Wikipedia

先ほどの例において、前提が真であるときに結論も必ず真であるとは言えませんでした。よって、妥当な論証とは言えないと説明することができます。

ただ、厳密含意でも論証に違和感のあるケースはあり、これを解消する「関連含意」が提唱されています。関連合意では「演繹可能性 (deducibility)」の概念を採用し、結論を導いた前提が演繹の過程で実際に使用されなければならない、としています。

厳密含意と関連含意については以下の資料を参照ください。
https://researchmap.jp/?action=multidatabase_action_main_filedownload&download_flag=1&upload_id=109558&metadata_id=39541

自然演繹による証明は与えられた論証が妥当であることを示します。逆に論証が妥当でないことを示すには反例を見つけます。これについては本の第11章を参照ください。

PostgreSQLマニュアルのトランザクション分離レベル表を参照する際の注意点

はじめに

PostgreSQLマニュアル「13.2. トランザクションの分離」にはトランザクション分離レベルの表が記載されています。この表の記載は9.4以前と9.5以降で変わっており、PostgreSQLの挙動が変わったと勘違いしてしまうかもしれません。ですが、マニュアルを注意深く読み解けば挙動に違いの無いことが分かります。本エントリではこれを解説します。

トランザクション分離レベルの表があらわすもの

注目すべきは表タイトルです。

バージョン 表タイトル
9.4 表 13-1. 標準SQLトランザクション分離レベル
9.5 表13.1 トランザクション分離レベル

9.4で記載されている表は「標準SQLトランザクション分離レベル」です。「PostgreSQLトランザクション分離レベル」ではありません。「標準SQLトランザクション分離レベル」とはANSI(米国国家規格協会)で定義されたトランザクション分離レベルのことです。

9.4の「標準SQLトランザクション分離レベル」を引用します。

分離レベル ダーティリード 反復不能読み取り ファントムリード
リードアンコミッティド 可能性あり 可能性あり 可能性あり
リードコミッティド 安全 可能性あり 可能性あり
リピータブルリード 安全 安全 可能性あり
リアライザブル 安全 安全 安全

これに対し、9.5で記載されている表は「トランザクション分離レベル」です。これは標準SQLPostgreSQLで実装されているトランザクション分離レベルをまとめて記載しています。

9.5の「トランザクション分離レベル」を引用します。

分離レベル ダーティリード 反復不能読み取り ファントムリード 直列化異常
リードアンコミッティド 許容されるが、PostgreSQLでは発生しない 可能性あり 可能性あり 可能性あり
リードコミッティド 安全 可能性あり 可能性あり 可能性あり
リピータブルリード 安全 安全 許容されるが、PostgreSQLでは発生しない 可能性あり
リアライザブル 安全 安全 安全 安全
13.2. トランザクションの分離

この表には「許容されるが、PostgreSQLでは発生しない」という記載があります。これは標準SQLがそれぞれの分離レベルで提供しなくてはならない最小の保護のみを示しており、PostgreSQLは標準SQLより厳密な動作で実装しているということです。つまり先ほどの記載は「(標準SQLでは)許容されるが、PostgreSQL(の実装)では発生しない」といえます。

このことはマニュアルにも記載されています。

より厳密な動作をすることは標準SQLでも許されています。 つまり、この4つの分離レベルでは、発生してはならない事象のみが定義され、発生しなければならない事象は定義されていません。

13.2. トランザクションの分離

この結果として、PostgreSQLでは4つの標準SQLトランザクション分離レベルを全て要求することができますが、PostgreSQLのリードアンコミッティドモードは標準SQLのリードコミッティドに相当する挙動を示すため、実質的に3つのトランザクション分離レベルしか存在しないことになります。また、リピータブルリードモードではファントムリードが発生せず、標準SQLが求めるよりも厳密な動作で実装されています。

直列化異常とはなにか?

直列化異常について、マニュアルでは以下の説明をしています。

直列化異常
複数のトランザクションを正常にコミットした結果が、それらのトランザクションを1つずつあらゆる可能な順序で実行する場合とは一貫性がない。

13.2. トランザクションの分離

直列化異常の具体例としてマニュアルには2つ記載されています。

  1. 「13.2.2. リピータブルリード分離レベル」制御レコード
  2. 「13.2.3. シリアライザブル分離レベル」mytabテーブル

制御レコードの例はマニュアルの記載だとわかりにくいため、以下のエントリも併せて参照ください。
PostgreSQLマニュアルの「リピータブルリード分離レベル」における「制御レコード」とはなにか? - ぱと隊長日誌

トランザクション分離レベルの表には9.5から「直列化異常」が追加されています。ですが、9.4以前でもこの事象は発生します。これは先に挙げた直列化異常の例が9.4のマニュアルにも記載されていることからわかります。

なお、同時実行トランザクションを一度に一つずつ実行することについて、日本語版マニュアルの9.5以前で「並列」と記載していた箇所が9.6以降は「直列」となっています。これは英語版マニュアルで以前から"serial"と記載されており、「直列」との記載が正しいです。

しかし、このビューは常にいくつかの同じレベルの同時実行トランザクション並列(一度に一つずつの)実行で一貫性を持つ必要はありません。
※9.5より引用

13.2. トランザクションの分離

しかし、このビューは常にいくつかの同じレベルの同時実行トランザクション直列(一度に一つずつの)実行と一貫性を持つとは限りません。
※9.6より引用

13.2. トランザクションの分離

However, this view will not necessarily always be consistent with some serial (one at a time) execution of concurrent transactions of the same level.
※9.6英語版より引用。なお、9.5英語版でも同じ記載となっている。

PostgreSQL: Documentation: 9.6: Transaction Isolation