Page 102 - My FlipBook
P. 102
Collaborative Projects所
內
合
作
計
畫
在我們的初步實驗（圖二），當底層的儲存系統使用 crash-deterministic 固態硬碟，上層檔案系統可以省
略掉紀錄日誌的動作 ( 用 ext2 取代 ext4)。上層資料庫 SQLite 提交 (commit) 的一筆交易 (transaction) 所
需要的 fsync 動作 ( 要求檔案系統清空目前的暫存狀態後並呼叫一次 SSD 的刷新動作 ) 也可以從 5 個減少
到 1 個。
Crash-deterministic 固態硬碟設計上唯一的缺點，就是它用了比較複雜的資料結構和演算法。這樣在韌體
實作上比較有可能出錯。一但發生錯誤，有時僅僅是一個位元的錯誤，也可能造成整個系統無法讀取。
為了確保我們的韌體實作沒有錯誤，我們用了形式化驗證的技術 (formal veri cation)。結合了多種的驗證
工具，包括 C 語言的驗證工具 Rosette+Serval，和定理證明器 Agda，我們開發了一個適用於檢驗 crash-
deterministic 性質的系統。這系統能自動檢查韌體設計師所寫的 C 程式，證明它是 crash-determinisitc，
或是找到一個它不是 crash-deterministic 的例子。
圖二：crash-deterministic SSD 儲存系統的優勢。
我們發現從儲存系統從一開始就設計整體系統的當機回復機制是一個好的選擇。近兩年 MIT 和華盛頓大
學也有相關的研究，但是他們的當機回復機制主要是從檔案系統開始。因為檔案系統的複雜度遠高於儲
存系統韌體的複雜度，其形式化驗證的成本極高。以 MIT 的檔案系統 DFSCQ 為例。其系統撰寫加上定理
證明就花了 10 人年，其檔案系統比標準的 ext4 慢了 3 倍。從 crash-determinisitc 固態硬碟出發，我們整
體儲存裝置的效能預計非但不會降低，反而會提高。驗證部分的自動化程度預計也會遠高於 MIT 的工作，
整體開發時間約可縮短至 2~4 人年。
100
內
合
作
計
畫
在我們的初步實驗（圖二），當底層的儲存系統使用 crash-deterministic 固態硬碟，上層檔案系統可以省
略掉紀錄日誌的動作 ( 用 ext2 取代 ext4)。上層資料庫 SQLite 提交 (commit) 的一筆交易 (transaction) 所
需要的 fsync 動作 ( 要求檔案系統清空目前的暫存狀態後並呼叫一次 SSD 的刷新動作 ) 也可以從 5 個減少
到 1 個。
Crash-deterministic 固態硬碟設計上唯一的缺點，就是它用了比較複雜的資料結構和演算法。這樣在韌體
實作上比較有可能出錯。一但發生錯誤，有時僅僅是一個位元的錯誤，也可能造成整個系統無法讀取。
為了確保我們的韌體實作沒有錯誤，我們用了形式化驗證的技術 (formal veri cation)。結合了多種的驗證
工具，包括 C 語言的驗證工具 Rosette+Serval，和定理證明器 Agda，我們開發了一個適用於檢驗 crash-
deterministic 性質的系統。這系統能自動檢查韌體設計師所寫的 C 程式，證明它是 crash-determinisitc，
或是找到一個它不是 crash-deterministic 的例子。
圖二：crash-deterministic SSD 儲存系統的優勢。
我們發現從儲存系統從一開始就設計整體系統的當機回復機制是一個好的選擇。近兩年 MIT 和華盛頓大
學也有相關的研究，但是他們的當機回復機制主要是從檔案系統開始。因為檔案系統的複雜度遠高於儲
存系統韌體的複雜度，其形式化驗證的成本極高。以 MIT 的檔案系統 DFSCQ 為例。其系統撰寫加上定理
證明就花了 10 人年，其檔案系統比標準的 ext4 慢了 3 倍。從 crash-determinisitc 固態硬碟出發，我們整
體儲存裝置的效能預計非但不會降低，反而會提高。驗證部分的自動化程度預計也會遠高於 MIT 的工作，
整體開發時間約可縮短至 2~4 人年。
100
