MIT科學家打造電腦當掉資料也不會遺失的檔案系統

三名來自麻省理工學院（MIT）電子工程系（EECS）的研究人員利用形式驗證（formal verification）的程序建立了一個即使電腦突然當掉也不會造成資料遺失的檔案系統，相關研究成果並準備在今年10月舉行的作業系統學術會議ACM Symposium on Operating Systems Principles（SOSP）上發表。

MIT電子工程系副教授Nickolai Zeldovich表示，很多人都擔心檔案系統的穩定性，不論是在正常運作的狀況下，或是在電腦當機、電源故障、硬體故障，或是軟體出現臭蟲的時候，而且使用者還會發現，就算是經過嚴謹測試的檔案系統，其當機復原功能亦存在著許多臭蟲，因為這並不是件容易的事。

所謂的形式驗證是以數學方法描述電腦程式運作時可以接受的「綁定」（bounds），且證明它絕不會超出這些綁定。這是個複雜的程序，因此多半只應用在描繪程式功能的高階圖式（schema）上，將這些圖式轉換成程式碼可能會帶來相關驗證未能解決的各種複雜問題。

MIT研究人員則是直接驗證檔案系統的程式碼，而非高階圖式，他們透過名為Coq的驗證助理工具，以其形式語言描述電腦系統的各個組件與它們之間的關聯。由於此一形式驗證環境包含了程式語言，在此環境中以同樣的語言撰寫檔案系統，就能讓驗證程序檢查真正的程式碼而非圖式。

研究人員先以Coq的形式語言定義此一檔案系統的各種元件，然後還得描述這些元件在遭遇當機情況時的行為與彼此間的關聯，之後才進行系統驗證，並寫出相對應的檔案系統。

此一新的檔案系統將能保證使用者不會因為系統當掉而遺失資料，即使受限於今日的標準而使得該檔案系統運作緩慢，但研究人員宣稱他們所使用的技術將可適用於更精密的設計，形式驗證最終將讓打造可靠及有效率的檔案系統變得更容易。（編譯/陳曉莉）