###### tags: `TransactionalInformationSystems`

# 13章-4 redo-historyアルゴリズム

ここまででredo-winnersアルゴリズムを導入してきたが、ここでもう一つのパラダイム、redo-historyを導入する。

これは、勝者と敗者を区別せず、全ての操作をredoし、ひとまずクラッシュ直前のキャッシュデータベースの状態まで戻すという考えである。

こちらの方がredoしてからundoしなおす二度手間が増えるが、それを補って余りある単純さとエレガントさが特徴であり、総合してみるとこちらの方が大抵優れている。

## 概要

- 分析パス：redoパスにおける勝者と敗者の区別が無いので、分析パスなしでも問題ない。その場合2パスアルゴリズムになる。だが一応、ここでDirtyPagesリストを作っておくことで後のredoパスを最適化可能である。
- redoパス：SystemRedoLSNから開始して、PSNやDirtyPagesの検証を通して反映されていない操作をredoしていく。ここで勝者か敗者かは区別しないので、終了時点でクラッシュ直前の状態に戻っている。
- undoパス：こうすることで、undoパスは極めて単純に取り扱える。クラッシュ時点でアクティブだったトランザクション(敗者)がundoパスの開始時点でアクティブなトランザクションと一致しているので、これらのトランザクションをabortしてロールバックするだけでよい。

---

redo-pass():
    min := LogSeqNo of oldest log entry in StableLog;
    max := LogSeqNo of most recent log entry in StableLog;
    // 全操作のredo
    for i := min to max do
        pageno := StableLog[i].PageNo;
        fetch(pageno);
        if DatabaseCache[pageno].PageSeqNo < i then
            read-and-write(pageno) according to StableLog[i].RedoInfo;
            DatabaseCache[pageno].PageSeqNo := i;
        end
    end

undo-pass():
    ActiveTrans := empty;
    for each t in losers do
        ActiveTrans += t;
        ActiveTrans[t].LastSeqNo := losers[t].LastSeqNo;
    end
    // 各敗者のロールバック
    while there exists t in losers s.t. losers[t].LastSeqNo <> nil do
        nexttrans := TransNo in losers s.t. losers[nexttrans].LastSeqNo = max{losers[x].LastSeqNo|x in losers};
        nextentry := losers[nexttrans].LastSeqNo;
        if StableLog[nextentry].ActionType in {write, compensation} then
            pageno := StableLog[nextentry].PageNo;
            fetch(pageno);
            if DatabaseCache[pageno].PageSeqNo >= nextentry.LogSeqNo then
                newlogentry.LogSeqNo := new sequence number;
                newlogentry.ActionType := compensation;
                newlogentry.PreviousSeqNo := ActiveTrans[transid].LastSeqNo;
                newlogentry.RedoInfo := inverse action of the action in nextentry;
                newlogentry.UndoInfo := inverse action of the inverse action of the action in nextentry;
                ActiveTrans[transid].LastSeqNo := newlogentry.LogSeqNo;
                LogBuffer += newlogentry;
                read-and-write(StableLog[nextentry].PageNo) according to StableLog[nextentry].UndoInfo;
                DatabaseCache[pageno].PageSeqNo := newlogentry.LogSeqNo;
            end
            losers[nexttrans].LastSeqNo := StableLog[nextentry].PreviousSeqNo;
        end
        if StableLog[nextentry].ActionType = begin then
            newlogentry.LogSeqNo := new sequence number;
            newlogentry.ActionType := rollback;
            newlogentry.TransId := StableLog[nextentry].TransId;
            newlogentry.PreviousSeqNo := ActiveTrans[transid].LastSeqNo;
            LogBuffer += newlogentry;
            ActiveTrans -= transid;
            losers -= transid;
        end
    end
    force();

---

### 定理13.7

単純3パスredo-historyアルゴリズムは正当な障害回復を達成する。

#### 証明

redoパスの後には以下の不変条件が成立。
$$
\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) \Rightarrow o\in \text{cached database }
$$

undoパスにおいては、
- 単純に11章のトランザクション復元を行うだけ。
- redoステップが全書き込みをredoしたことが分かっているので、ページ状態の検証を行う必要すらない。
- もとの履歴がCSRかつLRCなのでPRED、よって可換規則によって並び替えると敗者トランザクションは全て空トランザクションに変換される。

よってundoパス後には以下の不変条件が成り立つ。

$$
\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 \in \text{losers}) \Rightarrow o\notin \text{cached database }
$$

敗者による書き込みは全て勝者による書き込みの後に行われるので、勝者は敗者から全く影響を受けない。よって

$$
\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 \in \text{winners}) \Rightarrow o\in \text{cached database }
$$

$\square$

## 最適化

redo-winnersの文脈で導入されたログ切り捨て・チェックポイント・flushロギングなどの手法は全てredo-historyにもそのまま適用できる。

## ロールバックの完全な取り扱い

redoパス中にクラッシュが発生した場合には、再びredoパスを実行すればよいだけなので何も問題ない。

undoパス中にクラッシュが発生した場合にも、最初のundoパス(ロールバック)中に生成された相殺ログエントリ(CLE)も含めて全てロールバックしなおせばよいので、正当性の観点では何も問題は生じない。

ただし、パフォーマンスの観点では問題が生じうる。undoパス中のクラッシュが繰り返されると、ロールバックしなければならないログエントリが雪だるま式に増えて行ってしまうため。このような現象はそうそう起きないとは思われるが、一応改善する方法があるので導入する。

まず、ある操作のログエントリl1に対するCLEl2が生成されたとき、l2によってl1の影響を打ち消し終わっているので、これらのログエントリのペアは一気に削除してしまって問題ないということが言える。
このようなペアを上手いこと判定できる方法が欲しい。

このような判定は、ログエントリ間のリンクに基づく後方連鎖を用いる。既にあるPreviousSeqNoリンクに加えて、NextUndoSeqNoリンクを追加する。これは以下の性質を満たす。

- CLEでない通常の操作については、NextUndoSeqNoの値はPreviousSeqNoと等しい。
- CLEについては、NextUndoSeqNoは、それが打ち消した通常操作ログエントリのPreviousSeqNoと等しい。

これを用いることで、undoしなければならないログエントリの加速度的な増加を防いだ以下のundoパスが実現する。

---

undo-pass():
    ActiveTrans := empty;
    for each t in losers do
        ActiveTrans += t;
        ActiveTrans[t].LastSeqNo := losers[t].LastSeqNo;
    end
    // 各敗者のロールバック
    while there exists t in losers s.t. losers[t].LastSeqNo <> nil do
        nexttrans := TransNo in losers s.t. losers[nexttrans].LastSeqNo = max{losers[x].LastSeqNo|x in losers};
        nextentry := losers[nexttrans].LastSeqNo;
        // CLEなら
        if StableLog[nextentry].ActionType = compensation then
            // NextUndoSeqNoまでは相殺が終わっているので飛ばしてもよい
            losers[nexttrans].LastSeqNo := StableLog[nextentry].NextUndoSeqNo;
        end
        // CLEでない(通常ログエントリ)なら
        if StableLog[nextentry].ActionType = write then
            pageno = StableLog[nextentry].PageNo;
            fetch(pageno);
            if DatabaseCache[pageno].PageSeqNo >= nextentry.LogSeqNo then
                newlogentry.LogSeqNo := new sequence number;
                newlogentry.ActionType := compensation;
                newlogentry.PreviousSeqNo := ActiveTrans[transid].LastSeqNo;
                // NextUndoSeqNoの追加
                newlogentry.NextUndoSeqNo := nextentry.PreviousSeqNo;
                newlogentry.RedoInfo := inverse action of the action in nextentry;
                newlogentry.UndoInfo := inverse action of the inverse action of the action in nextentry;
                ActiveTrans[transid].LastSeqNo := newlogentry.LogSeqNo;
                LogBuffer += newlogentry;
                read-and-write(StableLog[nextentry].PageNo) according to StableLog[nextentry].UndoInfo;
                DatabaseCache[pageno].PageSeqNo := newlogentry.LogSeqNo;
            end
            losers[nexttrans].LastSeqNo := StableLog[nextentry].PreviousSeqNo;
        end
        if StableLog[nextentry].ActionType = begin then
            newlogentry.LogSeqNo := new sequence number;
            newlogentry.ActionType := rollback;
            newlogentry.TransId := StableLog[nextentry].TransId;
            newlogentry.PreviousSeqNo := ActiveTrans[transid].LastSeqNo;
            LogBuffer += newlogentry;
            ActiveTrans -= transid;
            losers -= transid;
        end
    end
    force();

---

NextUndoSeqNoは、通常動作中のロールバックにも同様に追加する必要がある。よってabort操作は以下の感じになる。

---

abort(transid):
    logentry := ActiveTrans[transid].LastSeqNo;
    while logentry is not nil and logentry.ActionType = write or full-write do
        newlogentry.LogSeqNo := new sequence number;
        newlogentry.ActionType := compensation;
        newlogentry.PreviousSeqNo := ActiveTrans[transid].LastSeqNo;
        newlogentry.RedoInfo := inverse action of the action in logentry;
        // NextUndoSeqNoのセット
        newlogentry.NextUndoSeqNo := logentry.PreviousSeqNo;
        ActiveTrans[transid].LastSeqNo := newlogentry.LogSeqNo;
        LogBuffer += newlogentry;
        write(logentry.PageNo) according to logentry.UndoInfo;
        logentry := logentry.PreviousSeqNo;
    end
    newlogentry.LogSeqNo := new sequence number;
    newlogentry.ActionType := rollback;
    newlogentry.TransId := transid;
    newlogentry.PreviousSeqNo := ActiveTrans[transid].LastSeqNo;
    newlogentry.NextUndoSeqNo := nil;
    LogBuffer += newlogentry;
    ActiveTrans -= transid;
    force();

---