---
tags: 論文メモ
---

# 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