Determinizing Crash Behavior with a Verified Snapshot-Consistent Flash Translation Layer

背景

問題意識

• storage stackにおけるcrash saftyの形式的検証
• prefix-preserving disk model
  • 最後のフラッシュ以降のある時点の状態に回復
• snapshot-consistent model
  • 最後のフラッシュ以前のある時点の状態に回復

問題への貢献

• SCFTL: snapshot-consistent flash translation layer
  • snapshot-consistent disk modelの実装
  • flush as a snapshot, 上のレイヤでアトミックな操作の実装が容易になる
• SCFTLの実装とその検証

具体的な手法など

• snapshot-consistency theoremはagda
• Cの実装をsybolic executerで論理式にしてsmtで処理してるっぽい
• agdaでsnapshot-consistencyを定式化して,それを満たす状態遷移機械を定義し,Cの実装がそれを満たすことをsymbolic executerとsmtで保証してる
• フラッシュが少ないシステムでは既存の実装と同等のパフォーマンス
• snapshot-consistencyの形式化
  • 2 arrayとカウンタを考慮
  • 複数のwrite間のatomicity