永続化に関する正当性の検証

[ban-nobuhiro]

永続化に関する正当性を検証する

• e, e' ∈ epoch, l ∈ log_channel, d ∈ data
• write_log(e, d) : (PWALファイル) epoch e としてデータ d が ディスクに書き終わる
• write_epoch(e) : (メタ情報ファイル) epoch e がディスクに書き終わる

検証項目

• add_entry して end_session をしたらいつかは durable 通知が発生するかクラッシュする
• add_entry して end_session したらいつかは ディスクに永続化されるかクラッシュする
• durable 通知 e が発生したら、それ以後に e 以下の epoch のデータがディスクに永続化されることも メタ情報ファイル epoch に e 以下(未満?)の値が記録されることもない

CTL:

• ∀l∀e; l.add_entry(d) → AG(l.end_session(e) → AF(∃e'≧e;inform_durable(e') ∨ crash))
• ∀l∀e; l.add_entry(d) → AG(l.end_session(e) → AF((write_log(e, d) ∧ AF∃e'≧e;write_epoch(e')) ∨ crash))
• ∀e∀e'≦e∀d; inform_durable(e) → ￢EF(write_log(e', d) ∨ write_epoch(e'))

LTL のほうが楽か??

リカバリまで含めての系列で検証すべきかもしれない

[ban-nobuhiro]

FIXME: end_session() は epoch e を取らないので、switch_epoch(e) からの系列に組み立てなおさなければならない

[ban-nobuhiro]

追加: write_epoch(e) が e'≦e; write_log(e', d) より前にきてはならない。
それを満たせないと、write_epoch と write_log の間でクラッシュした後のリカバリで、pwal が一部欠損した状態になる。
∀e∀e'≦e∀d; write_epoch(e) → ￢EF write_log(e', d)