一種對NAND閃存硬件和閃存轉(zhuǎn)換層軟件的形式化建模.pdf

1、NAND閃存已經(jīng)成為主流的存儲介質(zhì)，并被廣泛地應(yīng)用到嵌入式、桌面、服務(wù)器以及數(shù)據(jù)中心等各種計算機(jī)系統(tǒng)中，并仍迅速地擠占傳統(tǒng)純磁性材料存儲介質(zhì)的市場。與此同時，在航空航天、國防軍工，核電，醫(yī)療設(shè)備等一些安全攸關(guān)領(lǐng)域，NAND閃存也因其存儲密度高、抗震性好、低功耗等特點得到了越來越多的應(yīng)用。然而NAND閃存的一些獨有的物理特性導(dǎo)致了其與傳統(tǒng)機(jī)械硬盤相比，具有天然的存儲不穩(wěn)定性。例如NAND閃存存在著磨損的問題，即經(jīng)過多次讀寫之后的閃存單元會

2、變得越來越不穩(wěn)定，而且超過一定的擦除次數(shù)之后，存儲單元就會徹底報廢。又例如閃存單元讀寫會引入電流干擾，即在寫一個存儲單元時，電流引起相鄰的存儲單元的位翻轉(zhuǎn)。NAND閃存的這些物理特性就對管理NAND的軟件提出了更高的要求。一種較為常見的解決方案引入一個被稱為閃存轉(zhuǎn)換層（Flash Translation Layer, FTL）的軟件層，用以隱藏這些物理特性，使得NAND閃存可以像傳統(tǒng)的機(jī)械硬盤一樣進(jìn)行任意讀寫。在過去的十多年里，有大量F

3、TL軟件相關(guān)的算法被提出。為了兼顧穩(wěn)定性、性能，可靠性，這類算法通常比其他存儲介質(zhì)的管理軟件更為復(fù)雜，也更容易出現(xiàn)問題。為了構(gòu)建高可信的基于NAND閃存存儲的系統(tǒng)軟件，通過嚴(yán)格的形式化方法對NAND閃存硬件進(jìn)行建模，對管理NAND閃存的FTL軟件層的行為進(jìn)行正確性驗證具有一定的理論和實際意義。
　　首先，本文根據(jù)一個被眾多閃存生產(chǎn)廠商廣泛接受認(rèn)可的NAND閃存接口標(biāo)準(zhǔn)ONFI3.0，采用形式化語言對NAND閃存硬件的真實語義進(jìn)行形

4、式化建模。本文提出的形式化模型包括ONFI所定義的NAND閃存硬件的存儲層次結(jié)構(gòu)、閃存硬件芯片處理命令的內(nèi)部工作流程、閃存硬件的命令集，以及在此基礎(chǔ)之上定義的閃存的基本操作。本文的NAND閃存形式化模型在定理證明工具Coq中定義實現(xiàn)。在Coq工具中，該模型的一些性質(zhì)也得到了完整地證明。該模型可以直接被用來作為驗證基于NAND閃存硬件的存儲系統(tǒng)軟件的基礎(chǔ)。
　　其次，本文使用基于不變式的證明方法建立了一個通用的、可以驗證各種閃存轉(zhuǎn)換

5、層正確性的形式化框架。所謂的正確性是指:在正確的初始條件下，一個運行著正確的閃存轉(zhuǎn)換層算法的NAND閃存與一塊傳統(tǒng)機(jī)械硬盤在相同的讀寫命令序列之后將輸出同樣的數(shù)據(jù)。在該形式化框架中，本文首次定義了一個經(jīng)典的閃存轉(zhuǎn)換層算法(BAST)，并證明了算法的正確性。本文所建立的形式化NAND閃存模型和閃存轉(zhuǎn)換層算法證明框架為驗證其上運行的嵌入式操作系統(tǒng)及其它嵌入式軟件提供了嚴(yán)格的形式化模型，并將為基于NAND閃存的高可信嵌入式軟件的開發(fā)提供一個堅