---
# System prepended metadata

title: 13章-2 redo-winnersアルゴリズム
tags: [TransactionalInformationSystems]

---

###### tags: `TransactionalInformationSystems`

# 13章-2 redo-winnersアルゴリズム

ここでredo-winnersアルゴリズムから記述する。

これは、回復に際して、勝者(winner)すなわちcommitされたトランザクションのみをredoしなおすようなアルゴリズム。

最初に、書き込みがfull-writeのみからなるようなモデルにおける最もシンプルな障害回復アルゴリズムから入り、それを徐々に洗練していく。

なお、通常動作中にabortされロールバックされたトランザクションへの対応は、いったん脇に置いておき、後で考える。


## 通常動作における手続き

全ページで定義した各データ構造について、サーバの通常動作中にどのように更新していくかを疑似コードで記述する。

Pascalライクな書き方だが、HackMDの疑似コードサポートにPascalが無かった。それっぽいハイライトをしてくれるverilogで代用している。

```verilog
write or full-write(pageno, transid, s):
    // データベースキャッシュへの書き込み
    DatabaseCache[pageno].Contents := modified contents;
    DatabaseCache[pageno].PageSeqNo := s;
    DatabaseCache[pageno].Status := dirty;
    // ログエントリの作成
    newlogentry.LogSeqNo := s;
    newlogentry.ActionType := write or full-write;
    newlogentry.TransId := transid;
    newlogentry.PageNo := pageno;
    newlogentry.UndoInfo := information to undo update
    newlogentry.RedoInfo := information to redo update
    newlogentry.PreviousSeqNo := ActiveTrans[transid].LastSeqNo;
    // トランザクション情報の更新
    ActiveTrans[transid].LastSeqNo := s;
    // ログバッファの更新
    LogBuffer += newlogentry;
    
fetch(pageno):
    DatabaseCache += pageno;
    DatabaseCache[pageno].Contents := StableDatabase[pageno].Contents;
    DatabaseCache[pageno].PageSeqNo := StableDatabase[pageno].PageSeqNo;
    DatabaseCache[pageno].Status := clean;
    
flush(pageno):
    if there is logentry in LogBuffer with logentry.PageNo = pageno
    then // 対応するログバッファを永続ログに書き出すのが先
        force();
    end
    // 永続データベースにページを書き戻す
    StableDatabase[pageno].Contents := DatabaseCache[pageno].Contents;
    StableDatabase[pageno].PageSeqNo := DatabaseCache[pageno].PageSeqNo;
    DatabaseCache[pageno].Status := clean;
    
force():
    StableLog += LogBuffer;
    LogBuffer := empty;

begin(transid, s):
    // アクティブなトランザクションの追加
    ActiveTrans += transid;
    ActiveTrans[transid].LastSeqNo := s;
    // ログエントリの作成
    newlogentry.LogSeqNo := s;
    newlogentry.ActionType := begin;
    newlogentry.TransId := transid;
    newlogentry.PreviousSeqNo := nil;
    LogBuffer += newlogentry;
    
commit(transid, s):
    // ログエントリの作成
    newlogentry.LogSeqNo := s;
    newlogentry.ActionType := commit;
    newlogentry.TransId := transid;
    newlogentry.PreviousSeqNo := ActiveTrans[transid].LastSeqNo;
    LogBuffer += newlogentry;
    // アクティブなトランザクションからの削除
    ActiveTrans -= transid;
    // 永続ログへの書き出し
    force();
```

この疑似コードで定義される動作は、12章で定義した3つのログ規則を満たす。

1. redoログ規則：履歴に$commit(t)$が含まれるようなトランザクション$t$に対し、$t$でのデータアクションが全て永続ログもしくは永続データベースに含まれる。
    - commitの最後にforceを実行するので、永続ログに含まれる。
2. undoログ規則：$commit(t)$も$rollback(t)$も履歴に含まれないようなトランザクション$t$のデータアクション$p$について、$p$が永続データベースに含まれる時には永続ログにも含まれる。
    - flushが行われたときには、そのページを操作したログが必ずforceされるので、永続ログに含まれる。
3. ガーベジコレクション規則：履歴内の全てのトランザクション$t$のデータアクション$p$に対し、$p$が永続ログに存在しない$\Longrightarrow$(履歴に$commit(t)$が含まれる$\Longleftrightarrow$ $p$が永続データベースに含まれる)
    - ここでは永続ログの削除を考えないので、自明に満たされる。


### forceのI/O負荷

永続ログへの書き出し操作force()が行われるのは、flushとcommit。

- 前者のflushは、キャッシュ管理機構を洗練することで問題ない頻度に抑えられる。
- 後者のcommitは、トランザクションの数だけforceが行われることを意味するため、I/Oへの負荷が無視できないものになる。

commitにおけるforceのI/O負荷を軽減するための技術としては、ログエントリの書き出しを延期し、一定のタイミングで溜まったエントリを一気に書き出すことで、必要な書き出し回数を減らすI/Oバッチがある。commitの文脈ではこれはグループコミットと呼ばれる。

実用的には、ログエントリの書き出し間隔は100ミリ秒程度がいい、とのこと。


## 3パス障害回復アルゴリズム、シンプルバージョン

ここまでで通常動作中の更新方法を述べてきたので、今度はいよいよ障害回復ステップにおける手順を述べる。

redo-winnersパラダイムにおける最も単純な障害回復アルゴリズムは、3つのフェーズからなる。それぞれのフェーズで永続ログを走査するため「3パスアルゴリズム」。

---

### 1. 分析パス

永続ログの始点から順に、LSNの昇順でログエントリを読んでいく。各ログエントリが属するトランザクションのidを照合し、勝者か敗者かを判定する。一般的に勝者の数は非常に多く、敗者は比較的少ないと期待されるため、敗者のリストだけを明示的に保持する。また、各敗者トランザクションについて、最後のデータ操作のLSN(最終LSN)も同時に追跡する。


ログの最も一般的な実装では、固定サイズのログファイルにリングバッファのごとくサイクリックに書き込み、古いものから削除されていく形態がとられる。このとき現在の永続ログがどこから始まるのか分からない問題がある。これに対処するため、永続データベース内のマスタレコードに現在の永続ログにおける最古のLSNを保存する。

逆に、永続ログの終点の判定は、LSNが減少したタイミングになる(LSNが減少=古いログエントリのため)。


### 2. redoパス

永続ログを順方向に読んでいく。勝者トランザクションに属するデータ操作のログエントリが見つかる度に、そのページをフェッチしてデータ操作を再実行する。

### 3. undoパス

永続ログを逆方向、LSNの降順に読んでいく。敗者トランザクションに属するデータ操作のログエントリが見つかる度に、そのページをフェッチしてデータ操作の逆を実行する。

実装にあたっては、敗者リストと各敗者の最終LSNを活用する。まず、全敗者の最終LSNのうち最大値をとるトランザクションtの逆操作を実行したのち、tの最終LSNをその直前のデータ操作のLSNに置き換え、この手順を全操作がundoされるまで繰り返す。

---

これら3パスの後に、変更された全ページをflushしなおせば回復ステップは完了となる。が、このflushのI/O負荷は大きすぎるため、後にこれを減らすための工夫を考えていくことになる。

まず、単純のため、書き込み操作をfull-writeのみに限定する。


### 疑似コード

```verilog
restart():
    analysis-pass() returns losers;
    redo-pass();
    undo-pass();
    for each page p in DatabaseCache do
        if DatabaseCache[p].Status = dirty then flush(p); end
    end
    reinitialize StableLog;
    
analysis-pass() returns losers;
    var losers: set of record
        TransId: identifier;
        LastSeqNo: identifier;
    end indexed by TransId;
    losers := empty;
    min := LogSeqNo of oldest log entry in StableLog;
    max := LogSeqNo of most recent log entry in StableLog;
    for i := min to max do
        case StableLog[i].ActionType:
            begin:
                losers += StableLog[i].TransId;
                losers[StableLog[i].TransId].LastSeqNo := nil;
            commit:
                losers -= StableLog[i].TransId;
            full-write:
                losers[StableLog[i].TransId].LastSeqNo := i;
        end
    end

redo-pass():
    min := LogSeqNo of oldest log entry in StableLog;
    max := LogSeqNo of most recent log entry in StableLog;
    for i := min to max do
        if StableLog[i].ActionType = full-write and StableLog[i].TransId not in losers then
            pageno = StableLog[i].PageNo;
            fetch(pageno);
            full-write(pageno) with contents from StableLog[i].RedoInfo;
        end
    end
    
undo-pass():
    while there exists t in losers s.t. losers[t].LastSeqNo <> nil:
        nexttrans = TransNo in losers s.t. losers[nexttrans].LastSeqNo = max{losers[x].LastSeqNo|x in losers};
        nextentry = losers[nexttrans].LastSeqNo;
        if StableLog[nextentry].ActionType = full-write then
            pageno = StableLog[nextentry].PageNo;
            fetch(pageno);
            full-write(pageno) with contents from StableLog[nextentry].UndoInfo;
            losers[nexttrans].LastSeqNo := StableLog[nextentry].PreviousSeqNo;
        end
    end
    
```

この回復アルゴリズムは完全に恒等であることに注意。つまり、回復の最中に再びクラッシュして回復をやり直しても、前回の回復と全く同じ手順が繰り返され、ここでページがflushされたかどうかは全く考慮されないということ。


### 定理13.2 full-write限定3パスアルゴリズムの正当性

データ操作をfull-writeに限定したとき、シンプル3パスアルゴリズムは正しい回復を達成する。

#### 証明

まず、クラッシュ前の履歴はconflict serializableかつログ復元可能であると仮定しているので、同じページへの異なるトランザクションの書き込み操作が、それらトランザクションの終了順を反映することに注意。

ここで、回復アルゴリズムが終了した時点で、キャッシュデータベースが履歴のうち勝者トランザクションのみserialに実行したような状態になることを示せばよい。

1. 分析パス：終了時点で、リストlosersは、永続ログにおいてcommitログエントリを持たないようなトランザクションからなる。あとは、これらがundoステップを必要とするトランザクションを過不足なく示していることを言えばよい。
    1. redoログ規則から、勝者トランザクションは絶対にcommitログエントリを永続ログに持つ。逆に言えば、losersのトランザクションは全てcommitされておらず、undoステップを必要とする。
    2. undoログ規則から、永続データベースに影響を与えたトランザクションは永続ログにエントリを記録しなければならない。したがって、losersに属さない敗者トランザクションは永続データベースに影響を与えておらず、undoステップを必要としない。
2. redoパス：勝者トランザクションの全full-write操作がやり直される。また、実行順は元の履歴と全く同じである。redoパスが終了した時点で各ページは最後のfull-write操作の後イメージになっており、これは元の履歴のserialな実行順を反映している。敗者トランザクションが存在しない場合、証明はこれで完了。敗者による書き込みしか行われていないページについては、クラッシュの直近のflush以前の書き込みが永続データベースに反映されている。
3. undoパス：敗者トランザクションが存在する場合、ログ復元可能性から、敗者による書き込みは全て勝者による書き込みの後に行われる。このことから、勝者による書き込みが行われたページは全て、undoの全実行後に結局最後の勝者による書き込みと同じ内容になっており、正当である。あとは、永続データベースに影響を与えた敗者による書き込みをundoパスが全て捉えられることを示す必要がある。そのような書き込みはlosersリストのLastSeqNoから始まる後方チェインに含まれており、確かにundoパスでカバーできる。あとは、もとの敗者による書き込みが永続データベースに反映されていないケースが特別の注意を要する。実のところ、そのような操作のundoを実行した時点で、実質的にその操作が実行されたことになっているため問題ない。

実のところ、この単純版のアルゴリズムではundoパスをredoパスより先に行っても問題ない。が、これから複雑化していった際にredo→undoという順番が必須になる。$\square$

## write操作を組み込む

full-writeと違って、必ずしも恒等でない一般のwrite操作も許した場合の障害回復アルゴリズムに拡張していく。

大事なのは、全てのwinner操作がただ一度だけ実行されるのを保証すること。複数回実行されてしまうと不正状態になりうる。

この保証のためにpage sequence number(PSN)を活用できる。redoパスの各ステップにおいて、その操作のLSNとページの現在のPSNを比較し、LSNがPSNより大きい(=ページにその操作が反映されていない)場合のみその操作をredoし、PSNをそのLSNで更新する。こうすれば一度redoされた操作が再びredoされてしまう事故を防げる。

undoパスも同様に考慮する必要がある。もとの操作が反映されていないのにundoしてしまうケースや、既にundoされているのにundoしてしまうケースを避ける必要がある。この場合にもPSNと考えている操作のLSNを比較すればよい。LSNがPSN以下である(=ページにその操作が反映されている)場合のみその操作をundoし、PSNをそのLSNの値-1で更新する。-1にしておくことで、再びクラッシュしてundoパスをやり直したときにundoの重複を防げる。

### 一般のwriteを組み込んだ疑似コード

```verilog
redo-pass():
    min := LogSeqNo of oldest log entry in StableLog;
    max := LogSeqNo of most recent log entry in StableLog;
    for i := min to max do
        if StableLog[i].ActionType = full-write and StableLog[i].TransId not in losers then
            pageno = StableLog[i].PageNo;
            fetch(pageno);
            // PSN < LSNのときのみredo
            if DatabaseCache[pageno].PageSeqNo < i then
                read-and-write(pageno) according to StableLog[i].RedoInfo;
                // PSN <- LSN
                DatabaseCache[pageno].PageSeqNo := i;
            end
        end
    end
    
undo-pass():
    while there exists t in losers s.t. losers[t].LastSeqNo <> nil:
        nexttrans = TransNo in losers s.t. losers[nexttrans].LastSeqNo = max{losers[x].LastSeqNo|x in losers};
        nextentry = losers[nexttrans].LastSeqNo;
        if StableLog[nextentry].ActionType = full-write then
            pageno = StableLog[nextentry].PageNo;
            fetch(pageno);
            // PSN >= LSNのときのみredo
            if DatabaseCache[pageno].PageSeqNo >= nextentry.LogSeqNo then
                read-and-write(pageno) according to StableLog[nextentry].UndoInfo;
                // PSN <- LSN - 1
                DatabaseCache[pageno].PageSeqNo := nextentry.LogSeqNo -1;
            end
            losers[nexttrans].LastSeqNo := StableLog[nextentry].PreviousSeqNo;
        end
    end
```

---

### 定理13.3 PSN検証を組み込んだ単純な3パスアルゴリズムの正当性

PSNの検証を備えた単純な3パスアルゴリズムは、一般のwrite操作について正当な障害回復を達成する。

#### 証明

示す必要があるのは

1. 全勝者操作がただ一度だけ、もとの履歴と同じ順に実行されること
2. 全敗者操作がただ一度だけ、もとの履歴の逆順にundoされること

1については、redoパスが以下の不変条件を満たす。

$$\forall \text{ log sequence numbers } s \text{ such that } \\
\text{the log has been processed for redo up to but excluding } s:\\
\forall \text{ pages } p: \\ \forall \text{ transactions } t: \\
(s \text{ belongs to } t \text{ and refers to } p \land t \text{ is a winner }) \\ \Rightarrow (s \text{ is redone } \Leftrightarrow s\notin \text{ stable database })$$

つまり、winnerの操作のうち、永続データベースに反映されていないもののみredoが実行される、という関係が成り立つ。

操作がredoされた後にはそれはキャッシュデータベースに含まれているので、定理13.2と同様にredoに関する不変条件が成り立つ。

$$\forall \text{ log sequence numbers } s \in \text{stable log such that } \\ \text{the log has been processed for redo up to and including } s: \\ \forall \text{ pages } p: \\ \forall \text{ transactions } t: \\ \forall \text{ operations } o\in \text{stable log}: \\ 
(o \text{ belongs to } t \text{ and refers to } p \land t \text{ is a winner } \land o\leq s)\\
\Rightarrow
o\in \text{cached database}$$

キャッシュデータベースはクラッシュの後、永続データベースをベースに初期化され、各winner操作をただ一度だけredoする。

2のundoについても同様に、loserの操作がもれなくただ一度ずつ逆順にundoされていく。PSN検証でundoが抑止された場合には、キャッシュデータベースはその操作を既に含んでいる。その操作が既にflushされたものであるなら永続データベースのPSNにも反映されているため、その操作は二度とundoされることがない。一方、まだflushされておらず、再度のクラッシュで消えた際には、次の回復ステップで再びundoされることが保証される。 $\square$

---



