形式化建模運(yùn)行在NAND閃存上的DFTL算法

張必紅，郭 宇，李兆鵬

(中國(guó)科學(xué)技術(shù)大學(xué) 蘇州研究院軟件安全實(shí)驗(yàn)室，江蘇 蘇州 215123)

1 引 言

隨著科技和閃存技術(shù)的發(fā)展，閃存已經(jīng)是現(xiàn)代電子設(shè)備作為存儲(chǔ)的主要選擇之一了.但是，閃存固有的物理特性使它相對(duì)于傳統(tǒng)的磁性存儲(chǔ)介質(zhì)，有很大的區(qū)別.比如，閃存有“寫前擦除”的限定，所以在修改之前必須先要擦除，但是擦除卻是以塊為單位的，要比寫的單位頁大得多.因?yàn)檫@個(gè)局限以及磨損均衡，斷電保護(hù)等原因，在閃存的設(shè)計(jì)中，有個(gè)中間轉(zhuǎn)換層FTL(Flash Translation Layer)的概念被提了出來，F(xiàn)TL算法的核心是進(jìn)行邏輯地址到物理地址的映射，也就是說如果一個(gè)邏輯地址映射到一個(gè)物理地址，而這個(gè)物理地址已經(jīng)寫了數(shù)據(jù)了，而現(xiàn)在需要進(jìn)行更新，那只能寫到一個(gè)空白的頁，然后在映射表中把新的物理地址取代原來的舊的物理地址，映射到要修改的邏輯地址，這樣來完成更新操作.一般典型的FTL算法的功能除了地址映射，還包括垃圾回收，壞塊管理，斷電保護(hù)，磨損均衡等.常用的FTL算法有BAST算法，F(xiàn)AST算法，LAST算法，DFTL算法等[1-4].DFTL算法相比較于與其它算法，DFTL算法在企業(yè)級(jí)規(guī)模的工作負(fù)載中表現(xiàn)尤其優(yōu)異，特別在系統(tǒng)響應(yīng)時(shí)間，隨機(jī)讀寫，大規(guī)模負(fù)載中均表現(xiàn)出性能優(yōu)越.

我們可以看出DFTL算法很重要，但同時(shí)它也有著它的復(fù)雜性.為了保證閃存的性能，可靠，以及穩(wěn)定，這類算法通常比其他存儲(chǔ)介質(zhì)的管理軟件更為復(fù)雜，也更容易出現(xiàn)問題.在工業(yè)界SSD的各大廠商的競(jìng)爭(zhēng)中，F(xiàn)TL層的設(shè)計(jì)是體現(xiàn)核心競(jìng)爭(zhēng)力的地方.因?yàn)镕TL層設(shè)計(jì)包括元數(shù)據(jù)管理，數(shù)據(jù)布局映射、磨損均衡、垃圾回收、緩存策略等，由此可見，F(xiàn)TL算法的重要性和復(fù)雜性.

正是由于DFTL算法的復(fù)雜和重要性，安全性需要得到可靠的保證，我們就決定采用形式化建模的方法來建立一個(gè)可靠的形式化模型.而形式化驗(yàn)證存儲(chǔ)系統(tǒng)這方面的研究相當(dāng)火熱，一直以來，完全驗(yàn)證一個(gè)文件系統(tǒng)是個(gè)非常吸引人的目標(biāo)[5].在這方面，最接近目標(biāo)的努力由Schellhorn，Pfahler等在緩慢地進(jìn)步著[6-9].但是目前驗(yàn)證的文件系統(tǒng)，他們的底層只驗(yàn)證到了讀寫硬盤這一層，而作為閃存內(nèi)部算法的FTL層，則目前基本上沒有人研究.因?yàn)镈FTL算法適用于有大規(guī)模請(qǐng)求的NAND閃存(SSD)，有著廣闊的市場(chǎng)應(yīng)用場(chǎng)景，所以我們選擇對(duì)DFTL算法進(jìn)行形式化建模.

本文的貢獻(xiàn)點(diǎn)在于以下：

1)本文根據(jù)DFTL算法的基本性質(zhì)和操作，對(duì)DFTL算法的基本數(shù)據(jù)結(jié)構(gòu)，進(jìn)行了形式化建模.

2)本文根據(jù)DFTL算法讀寫操作的策略，對(duì)DFTL算法的讀寫操作和圾回收算法進(jìn)行了分層形式化的建模.

3)本文對(duì)DFTL算法的一些基本性質(zhì)進(jìn)行了驗(yàn)證.

本文形式化建模的代碼為可機(jī)器檢查的代碼，源代碼已經(jīng)開源*源地址https://github.com/zbh24/formal_dftl.

2 背 景

2.1 NAND閃存及DFTL算法

NAND閃存是一種半導(dǎo)體存儲(chǔ)器，有讀，寫，擦除等基本操作，但擦除的單位是要比寫的單位頁大.相對(duì)于傳統(tǒng)的機(jī)械硬盤，具有隨機(jī)訪問快，功耗低，噪聲低等優(yōu)點(diǎn).但局限性也很明顯，就是有“寫前擦除”的限定.針對(duì)這種限制，有原地更新和異地更新兩種策略.原地更新就是：把當(dāng)前塊中合法的其他數(shù)據(jù)拷貝到緩存中，然后擦除整個(gè)塊兒，再對(duì)這個(gè)空白塊中相對(duì)應(yīng)的頁進(jìn)行更新，再把其他合法數(shù)據(jù)寫回.因?yàn)椴脸俣认鄬?duì)讀寫速度慢，代價(jià)大，現(xiàn)實(shí)中一般不會(huì)采用原地更新.而異地更新則是把當(dāng)前頁標(biāo)志為非法的(常用策略是把這種標(biāo)志記錄在OOB中)，再把更新的數(shù)據(jù)寫到新的頁中，而記錄這種映射關(guān)系就是在FTL中，而這種標(biāo)志為非法的垃圾塊在最后是需要進(jìn)行垃圾回收，從而重新變?yōu)楹戏ǖ目瞻讐K.

FTL設(shè)計(jì)有很多種，如果我們基于映射關(guān)系來進(jìn)行分類，我們可以分為基于塊映射的，基于頁映射的，和混合映射的.基于塊映射就是一個(gè)數(shù)據(jù)塊對(duì)應(yīng)一個(gè)日志塊，寫數(shù)據(jù)時(shí)向數(shù)據(jù)塊寫數(shù)據(jù)，而要更新數(shù)據(jù)時(shí)則向?qū)?yīng)的日志塊寫數(shù)據(jù)，典型的基于塊映射的有BAST算法.基于頁映射則是每一個(gè)頁對(duì)應(yīng)一個(gè)日志頁，更新數(shù)據(jù)時(shí)則寫到對(duì)應(yīng)的日志頁，典型的頁映射算法有DFTL算法.而把這兩種基于塊和基于頁進(jìn)行混合起來設(shè)計(jì)的算法，典型的有FAST算法.

DFTL算法是一種基于全相聯(lián)頁映射的FTL算法.它其實(shí)并沒有明確的日志塊的概念，它把所有的塊分為兩種，一種數(shù)據(jù)塊，即是記錄數(shù)據(jù)的塊，塊中只記錄數(shù)據(jù).一種為映射塊，即是記錄這種映射的塊，塊中只記錄映射數(shù)據(jù).DFTL不僅采用了基于頁映射的策略，它還利用了訪問數(shù)據(jù)的局部性原理，會(huì)在閃存內(nèi)存中記錄最近訪問的映射記錄，而全部的映射記錄則記錄在閃存的物理介質(zhì)上.另外，每頁的狀態(tài)可以分為擦除，數(shù)據(jù)頁，映射頁，非法頁.DFTL算法會(huì)在閃存內(nèi)存中保存兩張表，一張為CMT表(cache_mapping_table)，即為一張有固定容量的緩存表，來記錄最近訪問的這種映射關(guān)系，而淘汰時(shí)一般采用LRU(最近最久未使用)算法.另一張為GTD表(global_translation_table)，來記錄所有的邏輯地址到映射頁的這種映射.

這個(gè)讀算法流程如下，如果一個(gè)請(qǐng)求的邏輯地址在CMT中，那么就直接在CMT中找到對(duì)應(yīng)的物理塊和在其中的偏移，讀出相應(yīng)數(shù)據(jù).如果請(qǐng)求的邏輯地址沒有命中CMT，那么就需要查看CMT緩存表是否滿了，如果滿了，則犧牲一項(xiàng)并且同時(shí)判斷犧牲的這一項(xiàng)是不是最新的，最新的則需要寫回到映射塊中.然后，就把這條最新的映射記錄更新到CMT緩存表中，然后再從CMT中讀出相應(yīng)的物理塊和頁號(hào)，接著從物理塊中讀出數(shù)據(jù)來.

圖1 DFTL讀算法示例Fig.1 Example of DFTL read algorithm

圖1展示了一個(gè)具體的DFTL讀算法的例子，一個(gè)邏輯地址(lpn = 1234)訪問，首先，CMT里沒有找到，然后去GTD表查詢，找到這條記錄存儲(chǔ)在映射塊的第47頁中，然后在影射頁讀出相應(yīng)的映射記錄，然后去數(shù)據(jù)頁(Dppn = 704)讀出數(shù)據(jù)來，同時(shí)把這條最新的訪問記錄更新到CMT表中.

DFTL寫算法的邏輯相對(duì)簡(jiǎn)單，DFTL算法會(huì)一直保持兩個(gè)塊，current_data_blcok(當(dāng)前數(shù)據(jù)塊)和current_trans_block(當(dāng)前映射塊).寫算法是直接從current_data_block中分配一個(gè)空白頁，然后把數(shù)據(jù)寫進(jìn)去，然后再更新到CMT表.如果current_data_blcok滿了，則從自由塊中分配一個(gè)新塊來當(dāng)做新的current_data_blcok.

隨著讀寫的不斷進(jìn)行，非法頁會(huì)越來越多，為了使它們可以重新使用，就需要垃圾回收也就是擦除操作來進(jìn)行.垃圾回收對(duì)于數(shù)據(jù)塊和映射塊采用不同的策略.如果是映射塊，則把合法的映射頁復(fù)制到當(dāng)前映射塊，然后更新CMT.如果是數(shù)據(jù)塊，則把合法的數(shù)據(jù)頁復(fù)制到當(dāng)前數(shù)據(jù)塊，然后再更新對(duì)應(yīng)的映射頁和CMT表.具體算法的形式化定義會(huì)在后面進(jìn)行說明.下面的兩張圖分別展示了映射塊和數(shù)據(jù)塊的回收過程.

圖2 DFTL映射塊的垃圾回收Fig.2 Example of the translation block garage collection

圖2是一個(gè)具體的映射塊的回收例子，選中映射塊Block1，然后把合法的數(shù)據(jù)拷貝到當(dāng)前的映射塊Block2中，然后再去更新相應(yīng)的全局映射表(GTD)的記錄.

圖3的數(shù)據(jù)塊回收，首先選中一個(gè)數(shù)據(jù)塊，然后把合法的數(shù)據(jù)拷貝到當(dāng)前的數(shù)據(jù)塊，接著對(duì)于記錄這條映射記錄的映射塊也進(jìn)行回收，把含有這條記錄的映射塊標(biāo)記為非法，然后在當(dāng)前的映射塊里分配一頁，更新新的映射記錄，最后來更新GTD表和CMT表.

圖3 DFTL數(shù)據(jù)塊的垃圾回收Fig.3 Example of the data block garage collection

DFTL算法的主要操作流程，就是是由以上讀操作，寫操作，和針對(duì)映射塊和數(shù)據(jù)塊的垃圾回收算法構(gòu)成的.

2.2 形式化工具Coq

Coq是一個(gè)交互式的定理證明工具，在Coq里面可以形式化定義程序和程序規(guī)范，并且可以自動(dòng)或者半自動(dòng)地尋找證明項(xiàng).Coq是建立在構(gòu)造演算的基礎(chǔ)上的，雖然Coq并不是一個(gè)完全自動(dòng)的定理證明工具，但是它提供了一些尋找證明的策略，并提供了一種語言(Ltac)可以讓用戶自己定義證明策略.目前Coq在形式化領(lǐng)域已經(jīng)得到比較廣泛的應(yīng)用，比如一個(gè)已經(jīng)被形式化驗(yàn)證的C語言編譯器CompCert[10].

3 DFTL算法數(shù)據(jù)結(jié)構(gòu)的形式化定義

3.1 FTL的組成

根據(jù)DFTL算法提出者的設(shè)計(jì)，我們把DFTL算法形式化建模成以下6個(gè)部分：

Record FTL：Set：=

mk _FTL {

ftl_bi_table：block_info_table；

ftl_free_blocks：block_queue；

ftl_cmt_table：cache_mapping_table；

ftl_gtd_table：global_mapping_directory；

current_data_block：block_no；

current_trans_block：block_no

}.

這6個(gè)部分分別表示為所有的塊的信息表，所有空閑塊的列表，部分映射的緩存表，全局映射目錄表，當(dāng)前的數(shù)據(jù)塊號(hào)，當(dāng)前的映射塊號(hào).下面我們將分別建模每個(gè)模塊.

3.2 ftl_bi_table

ftl_bi_table的類型是block_info_table，block_info_table是所有塊詳細(xì)信息的列表，具體包括以下部分：每個(gè)塊的狀態(tài)，已經(jīng)使用了多少頁，擦除次數(shù)和每頁狀態(tài)的列表，這些頁的狀態(tài)包括擦除，數(shù)據(jù)頁，映射頁，非法頁.具體結(jié)構(gòu)如下：

Record block_info：Set：=

mk_bi {

bi_state：ftl_block_state；

bi_used_pages：nat；

bi_erase_count：nat；

bi_page_state：page_state_table

}.

Definition block_info_table：= list block_info.

3.3 ftl_free_blocks

ftl_free_blocks的類型是block_queue，block_queue是所有自由塊號(hào)的列表，它是一個(gè)先進(jìn)先出的隊(duì)列.每當(dāng)一個(gè)塊寫完時(shí)，需要申請(qǐng)新塊的時(shí)候，就從這個(gè)列表中出隊(duì)一個(gè)塊，當(dāng)一個(gè)塊被回收時(shí)，就加入到這個(gè)隊(duì)列中.具體結(jié)構(gòu)如下：

Definition block_queue：= list block_no.

3.4 ftl_cmt_table

ftl_cmt_table的類型是cache_mapping_table，cache_mapping_table是一個(gè)有固定長(zhǎng)度緩存記錄的列表，這些記錄的替換原則則遵循LRU算法.每條記錄包括：邏輯地址，物理地址(物理塊號(hào)和在塊內(nèi)偏移)，以及臟位(is_drity).如果標(biāo)志位為臟位，則在淘汰時(shí)需要到把這條記錄，寫回到相應(yīng)的塊中，否則淘汰時(shí)可以直接丟棄.具體定義結(jié)構(gòu)如下：

Inductive cmt_record：Set：=

| cmt_empty

| cmt_trans (lpn：page_no)(pbn：block_no)

(offset：nat)(is_dirty：flag).

Definition cache_mapping_table：= list cmt_record.

3.5 ftl_gtd_table

ftl_gtd_table的類型是global_mapping_directory，global_mapping_directory是所有映射塊的目錄表.每個(gè)合法的邏輯地址都有一個(gè)對(duì)應(yīng)的映射目錄號(hào)，而所有的映射目錄號(hào)都會(huì)給分配一個(gè)映射頁，這些映射頁里就寫著真正的映射記錄.全局映射目錄表的結(jié)構(gòu)如下：

Inductive gtd_record：Set：=

| gtd_empty

| gtd_trans(pbn：block_no)(offset：nat).

Definition global_mapping_directory：= list gtd_record.

3.6 current_data_block和current_trans_block

current_data_blcok和current_trans_block的類型都是自然數(shù)(nat)，分別代表著當(dāng)前的數(shù)據(jù)塊號(hào)和映射塊號(hào).當(dāng)需要寫一個(gè)數(shù)據(jù)頁時(shí)，先檢查當(dāng)前的數(shù)據(jù)塊是否還有空閑頁，有空閑頁就向里面寫入數(shù)據(jù)，沒有則分配一個(gè)新的數(shù)據(jù)塊，然后把這個(gè)新的數(shù)據(jù)塊號(hào)更新為當(dāng)前的數(shù)據(jù)塊號(hào).每當(dāng)需要寫一個(gè)映射頁時(shí)，映射塊也是執(zhí)行類似的操作過程.

4 DFTL算法的形式化定義

4.1 DFTL算法的讀過程

根據(jù)DFTL算法的原論文描述，我們形式化定義讀算法操作如圖4所示.

圖4 DFTL讀算法
Fig.4 DFTL read algorithm

根據(jù)DFTL算法的操作語義，我們進(jìn)行了分層次抽象，從最頂層的FTL讀函數(shù)接口到最底層調(diào)用NAND硬件接口.具體抽象定義如下，首先我們最頂層的DFTL讀算法函數(shù)簽名定義為：

Definition FTL_read(c：chip)(f：FTL)(lpn：page_no)：option(prod data(prod chip FTL)).

表示為輸入chip，F(xiàn)TL和邏輯頁號(hào)，輸出為數(shù)據(jù)，新的chip閃存和FTL.接下來，對(duì)于讀具體操作，我們會(huì)判斷當(dāng)前邏輯頁號(hào)是否在CMT中.當(dāng)邏輯頁號(hào)不在CMT中同時(shí)CMT也滿了的時(shí)候，采用LRU淘汰策略，我們形式化定義LRU淘汰策略時(shí)采用淘汰最久最未被使用，為此針對(duì)CMT，我們定義了如下四個(gè)函數(shù)remove_cmt，remove_head，insert_cmt，append_tail.

再接著，我們會(huì)進(jìn)行判斷，被淘汰的這條記錄的標(biāo)志位是否為臟位，如果是臟位，則我們需要將被淘汰的記錄寫回到NAND物理介質(zhì)中去.關(guān)于寫回去這個(gè)函數(shù)，我們抽象出它的操作語義，定義函數(shù)簽名如下：

Definition copy_trans_page(c：chip)(f：FTL)(lpn：page_no)(trans_pbn：block_no)(trans_off：nat)(pbn：block_no)(off：nat)：option(prod chip FTL).

分別表示為輸入NAND，F(xiàn)TL，邏輯頁號(hào)以及它對(duì)應(yīng)的映射塊和在映射塊中的偏移，以及對(duì)應(yīng)新的數(shù)據(jù)塊和在數(shù)據(jù)塊中的偏移，輸出為新的chip和FTL.這個(gè)函數(shù)具體形式化語義為，當(dāng)這條最新的映射記錄被寫回NAND物理介質(zhì)中時(shí)，如果對(duì)應(yīng)的映射頁里沒有時(shí)，則我們把這條映射記錄添加到對(duì)應(yīng)的映射頁里，否則我們就把最新的映射記錄更新到對(duì)應(yīng)的映射頁里.

再往下，我們需要對(duì)GTD和CMT進(jìn)行查找，更新，插入等操作.所以我們對(duì)GTD和CMT這類數(shù)據(jù)結(jié)構(gòu)都定義了查找，更新，插入等操作.

最后，我們得到了邏輯頁號(hào)對(duì)應(yīng)的物理頁號(hào)時(shí)，調(diào)用read_block函數(shù)，在這個(gè)函數(shù)里調(diào)用了一個(gè)已經(jīng)被形式化建模的NAND閃存模型的接口[11]，從而讀出數(shù)據(jù)來，我們的DFTL算法是運(yùn)行在這個(gè)已經(jīng)被形式化定義的NAND閃存模型上，這就是整個(gè)DFTL讀算法分層次形式化定義的基本結(jié)構(gòu).

4.2 DFTL算法的寫過程

DFTL算法的寫操作形式化定義如下：首先直接檢測(cè)當(dāng)前數(shù)據(jù)塊是否滿了，如果滿了則申請(qǐng)新的一塊，然后分配一個(gè)新的數(shù)據(jù)頁，直接把數(shù)據(jù)寫進(jìn)數(shù)據(jù)頁里面，接著再把這條記錄寫到對(duì)應(yīng)的CMT中，對(duì)CMT進(jìn)行更新操作.具體邏輯見圖5.

圖5 DFTL寫算法
Fig.5 DFTL write algorithm

和FTL讀函數(shù)一樣，我們也采用了分層形式化建模，首先最頂層FTL寫函數(shù)的函數(shù)簽名如下：

Definition FTL_write(c：chip)(f：FTL)(lpn：page_no)(d：data)：option(prod chip FTL).

分別表示為輸入chip，F(xiàn)TL，邏輯頁號(hào)和數(shù)據(jù)，操作完成以后，輸出一個(gè)新的chip閃存和FTL.

然后，在FTL_write函數(shù)中需要對(duì)CMT進(jìn)行更新，關(guān)于CMT的更新比較復(fù)雜.具體的形式化定義如下：CMT表是一個(gè)固定長(zhǎng)度的先進(jìn)先出的隊(duì)列，每次讀或者寫都算作一次訪問.在隊(duì)尾的是最新訪問的記錄，在隊(duì)頭的是最久沒有被訪問的記錄.替換的時(shí)候，我們根據(jù)不同情況，形式化定義了以下這4種替換策略：

1.CMT滿了且CMT里面沒有對(duì)應(yīng)記錄：去掉第一項(xiàng)，把當(dāng)前記錄添加到隊(duì)列末尾.

2.CMT滿了且CMT有對(duì)應(yīng)的記錄：則把當(dāng)前記錄移除，添加到隊(duì)列末尾.

3.CMT未滿且CMT里面沒有對(duì)應(yīng)記錄：則從頭直接找到第一個(gè)空白項(xiàng)，把當(dāng)前記錄寫進(jìn)去.

4.CMT未滿且CMT有對(duì)應(yīng)的記錄：則把當(dāng)前記錄移除，從頭找到第一個(gè)空白項(xiàng)，把當(dāng)前記錄寫進(jìn)去.

具體可參考cmt_update_when_ftl_write函數(shù)，函數(shù)簽名如下：

Definition cmt_update_when_ftl_write(c：chip)(f：FTL)(lbn：block_no)(loff：nat)：option(prod chip FTL).

最后，我們需要把數(shù)據(jù)寫進(jìn)數(shù)據(jù)塊中，我們抽象出write_data_block函數(shù)，這個(gè)函數(shù)里面會(huì)直接調(diào)用NAND閃存模型提供的接口.如果當(dāng)前數(shù)據(jù)塊滿了，則需要分配新的塊，我們形式化定義了alloc_block，free_block等函數(shù)，這些函數(shù)的實(shí)現(xiàn)涉及下文的垃圾回收算法，我們將在下節(jié)中描述，整個(gè)FTL讀函數(shù)的形式化定義流程基本就如上所述.

5 DFTL的垃圾回收算法的形式化定義

首先我們定義的垃圾回收過程是發(fā)生在申請(qǐng)分配塊的時(shí)候，當(dāng)且僅當(dāng)剩余塊的數(shù)量低于閾值時(shí)才會(huì)發(fā)生調(diào)用.至于申請(qǐng)塊的函數(shù)形式化定義如下：

Definition alloc_block(c：chip)(f：FTL)(flag：alloc_block_type)：option(prod chip FTL).

它的函數(shù)簽名表示如下，輸入chip，F(xiàn)TL，和申請(qǐng)的塊類型，輸出新的chip和FTL.它的操作語義表示：如果剩余塊的數(shù)量大于閾值時(shí)，則正常分配塊.否則開始進(jìn)行垃圾回收操作.垃圾回收的函數(shù)的簽名如下：

Definition gc(c：chip)(f：FTL)(flag：alloc_block_type)：option(prod chip FTL).

函數(shù)的操作語義如下：首先是選擇出要回收的塊，接著對(duì)要回收的塊的類型進(jìn)行判斷，然后再進(jìn)行垃圾回收操作，數(shù)據(jù)塊和映射塊對(duì)應(yīng)著不同的垃圾回收策略，下面將分別說明.

5.1 映射塊的垃圾回收

對(duì)于映射塊的垃圾回收形式化定義為以下幾個(gè)步驟和層次：首先給當(dāng)前的映射塊分配一個(gè)新的塊，注意這個(gè)申請(qǐng)操作不受閾值的影響，是總是可以進(jìn)行的，即不通過調(diào)用alloc_block函數(shù)來申請(qǐng)塊的.接著從所有的塊中選擇一個(gè)映射塊進(jìn)行垃圾回收，注意選擇哪個(gè)回收塊大概要考慮兩個(gè)方面，第一這個(gè)塊中至少有一個(gè)非法的頁，否則沒有必要進(jìn)行回收操作.第二要注意負(fù)載均衡，因?yàn)橐粋€(gè)塊的擦寫次數(shù)是固定的，這里為了簡(jiǎn)化操作，只考慮了前者.接著當(dāng)選擇一個(gè)映射塊進(jìn)行回收時(shí)，依次對(duì)每個(gè)頁進(jìn)行掃描，如果這個(gè)頁是合法的，則從當(dāng)前映射塊申請(qǐng)一個(gè)新的映射頁，把這塊數(shù)據(jù)復(fù)制進(jìn)去，同時(shí)更新GTD，并把這頁設(shè)置為非法的，重復(fù)以上操作直到這個(gè)回收塊的所有頁都被掃描完以后，則可以把這塊映射塊標(biāo)志為非法塊，擦除后加入自由塊的隊(duì)列中，這樣一次對(duì)映射塊的垃圾回收操作完成.同時(shí)注意，對(duì)于原來申請(qǐng)新塊的操作，經(jīng)過垃圾回收過后，因?yàn)樾律暾?qǐng)塊的空閑頁數(shù)大于等于需要回收塊的合法頁數(shù)，所以不難證明原來的讀寫操作是總是可以進(jìn)行下去的.

圖6 映射塊的垃圾回收
Fig.6 Translation block GC

5.2 數(shù)據(jù)塊的垃圾回收

和映射塊類似，對(duì)于數(shù)據(jù)塊的垃圾回收形式化定義也分為幾層.當(dāng)需要分配數(shù)據(jù)塊的時(shí)候，剩余塊的數(shù)量低于閾值值時(shí)，則進(jìn)行數(shù)據(jù)塊的垃圾回收操作.首先給當(dāng)前的數(shù)據(jù)塊分配一個(gè)新的塊，這個(gè)操作跟映射塊的垃圾回收第一步是一樣的.接著對(duì)數(shù)據(jù)塊的垃圾回收也是要選擇一個(gè)合法的回收塊，依次對(duì)每個(gè)數(shù)據(jù)頁進(jìn)行掃描，如果被掃描的數(shù)據(jù)頁是非法的數(shù)據(jù)頁，則跳過這頁并繼續(xù)掃描，否則一旦被掃描到的是合法的數(shù)據(jù)頁，則首先從當(dāng)前數(shù)據(jù)塊分配一個(gè)新的數(shù)據(jù)頁，然后把這塊合法的數(shù)據(jù)頁的數(shù)據(jù)復(fù)制到新的空白數(shù)據(jù)頁，直到把整個(gè)回收塊的數(shù)據(jù)頁掃描完.注意在這個(gè)過程中，如果CMT中有相應(yīng)的記錄，則進(jìn)行CMT的更新，并且還要進(jìn)行映射頁和GTD表的更新.另外也可能會(huì)發(fā)生當(dāng)前的映射塊滿了，需要再次申請(qǐng)新的映射塊.所以在數(shù)據(jù)塊的垃圾回收中可能會(huì)多次發(fā)生對(duì)映射塊的垃圾回收.最后當(dāng)所有的頁都被掃描完成以后，則標(biāo)志當(dāng)前塊為非法，擦除后加入自由塊的隊(duì)列中了，至此對(duì)數(shù)據(jù)塊的垃圾回收操作完成.同樣的原來申請(qǐng)的新的數(shù)據(jù)塊的操作，經(jīng)過數(shù)據(jù)塊的垃圾回收過后，總是可以繼續(xù)進(jìn)行下去的.

關(guān)于垃圾回收的形式化模型，有兩點(diǎn)需要說明一下：

1)這個(gè)垃圾回收的觸發(fā)閾值是剩余塊一旦小于等于2塊，則進(jìn)行垃圾回收操作.因?yàn)樵跀?shù)據(jù)頁的垃圾回收操作時(shí)，可能會(huì)發(fā)生嵌套1層的映射塊的垃圾回收操作，所以剩余的自由塊的數(shù)量必須至少大于等于2，才能使垃圾回收繼續(xù)進(jìn)行下去，否則小于2塊時(shí)才進(jìn)行垃圾回收，則有可能會(huì)使操作卡死.

2)關(guān)于數(shù)據(jù)塊的回收操作，我們可以采取批量更新的策略，提高效率，不過這不影響垃圾回收算法的語義，因此我們的形式化時(shí)沒有采取這種優(yōu)化.

圖7 數(shù)據(jù)塊的垃圾回收
Fig.7 Data block GC

6 形式化模型的基本性質(zhì)

因?yàn)樾问交FTL算法是為了保證DFTL算法的正確性，所以我們首先必須正確地描述運(yùn)行著DFTL算法的NAND閃存的性質(zhì).首先我們定義了一個(gè)簡(jiǎn)單的硬盤模型，然后定義了R關(guān)系來保持硬盤和運(yùn)行DFTL算法的NAND閃存具有一致性，接著定義Inv關(guān)系來保證NAND閃存運(yùn)行過程中的一致性，具體定義如下：

R：?sec,hddreadhdd sec=fldreadfldsec

Inv：?c f,Finvf∧ Rinvc f

以上R表示對(duì)于任意一個(gè)地址，閃存和硬盤讀出來的數(shù)據(jù)都是一樣的.Inv表示在運(yùn)行過程中，F(xiàn)TL軟件的一些性質(zhì)會(huì)始終保持不變并且FTL軟件層和硬件層的一致性也始終保持不變.運(yùn)行著DFTL算法的NAND閃存具體有以下性質(zhì)(由于篇幅所限，僅列上部分性質(zhì))：

性質(zhì)1.

Rinit:=R hddinitfldinit

性質(zhì)1表示一開始整個(gè)NAND閃存都是空白的，在任意和硬盤同樣的位置讀出的數(shù)據(jù)都是一樣的，即是NONE或者0.

性質(zhì)2.

Writepreservel:= ? c f lpn d,Inv c f

→validlogic_page_no lpn

→?c′ f′,FTLwritec f lpn d

=Some(c′，f′)∧(?c",f",

FTLreadc′f′lpn

=Some(d,(c",f"))

性質(zhì)2表示，對(duì)于任意一個(gè)chip，ftl，page_no，data，只要chip和 ftl滿足Inv關(guān)系并且這個(gè)page_no是合法的，那么就一定可以把數(shù)據(jù)寫進(jìn)去，并且在寫過后的閃存同樣的地址讀出的數(shù)據(jù)和寫進(jìn)去的數(shù)據(jù)是一樣的.

性質(zhì)3.

Writepreserve2:= ? c f lpn d,Inv c f

→validlogic_page_nolpn

→? c′ f′,FTLwritec f lpn d

=Some(c′，f′)∧(? lpn′，

=lpn′<>lpn→FTLreaddatac f lpn′

=FTLreaddatac′ f′ lpn′

性質(zhì)3表示，對(duì)于在任意一個(gè)合法的邏輯地址lpn寫入數(shù)據(jù)之后，在任意的lpn’不等于lpn的地址上讀出的數(shù)據(jù)跟寫入數(shù)據(jù)之前是一樣的，即表示DFTL算法在一個(gè)邏輯地址寫入數(shù)據(jù)后，不影響另一個(gè)邏輯地址的數(shù)據(jù).

以上這些基本性質(zhì)均在Coq中得到了證明.

7 結(jié)束語以及未來工作方向

閃存設(shè)備現(xiàn)在使用的已經(jīng)越來越普遍了，在存儲(chǔ)系統(tǒng)中扮演著一個(gè)非常重要的地位，但是閃存設(shè)備的復(fù)雜性和頻繁出現(xiàn)問題的危害性需要得到重視.本文就是針對(duì)閃存中使用的一種比較經(jīng)典的DFTL算法進(jìn)行了形式化的建模.首先我們針對(duì)DFTL的基本構(gòu)成和性質(zhì)，對(duì)DFTL的基本數(shù)據(jù)結(jié)構(gòu)進(jìn)行了形式化建模，其次我們對(duì)DFTL算法的讀操作和寫操作也進(jìn)行了分層次的形式化定義，再接著我們針對(duì)DFTL算法一定會(huì)出現(xiàn)的非法塊，也定義了垃圾回收的形式化算法.最后，我們對(duì)DFTL算法的一些基本性質(zhì)在我們的模型上的正確性進(jìn)行了驗(yàn)證.我們未來的工作，就是在已經(jīng)形式化定義好的DFTL模型的基礎(chǔ)上，對(duì)DFTL算法的一些更復(fù)雜的性質(zhì)，在一個(gè)描述正確性的框架下，進(jìn)行形式化驗(yàn)證，來保證DFTL算法的行為約束來符合我們的要求.

[1] Chung T，Park D，Park S，et al.System software for flash memory：a survey[C].In Proceedings of the International Conference on Embedded and Ubiquitous Computing，2006：394-404.

[2] Lee S，Park D，Chung T，et al.A log buffer based flash translation layer using fully associative sector translation[J].IEEE Transactions on Embedded Computing Systems，2007，6(3)：18.

[3] Lee S，Shin D，Kim Y J，et al.LAST：locality-aware sector translation for NAND flash memory-based storage systems[J].ACM SIGOPS Operating Systems Review，2008，42(6)：36-42.

[4] Gupta A，Kim Y，Urgaonkar B.DFTL：a flash translation layer employing demand-based selective caching of page-level address mappings[J].ACM Sigplan Notices，2009，44(3)：229-240.

[5] Joshi R，Holzmann G J.A mini challenge：build a verifiable filesystem[J].Formal Aspects of Computing，2007，19(2)：269-272.

[6] Ernst G，Pfahler J，Schellhorn G，et al.Inside a verified flash file system：Transactions and garbage collection[C].In Proceedings of the 7th Working Conference on Verified Software：Theories，Tools and Experiments.Springer International Publishing，2015：73-93.

[7] Pfahler J，Ernst G，Schellhorn G.Crash-safe refinement for a verified flash file system[R].Technical Report 2014-02，University of Augsburg，2014.

[8] Schellhorn G，Ernst G，Pfahler J，et al.Development of a verified flash file system[C].International Conference on Abstract State Machines，Alloy，B，TLA，VDM，and Z.Springer Berlin Heidelberg，2014：9-24.

[9] Schierl A，Schellhorn G，Haneberg D，et al.Abstract specification of the ubifs file system for flash memory[M].Formal Methods.Springer Berlin Heidelberg，2009：190-206.

[10] Leroy X.Formal verification of a realistic compiler[J].Communications of the ACM，2009，52(7)：107-115.

[11] Yang Long-ying，Guo Yu.Formal modeling for NAND flash hardware[J].Computer Engineering，2015，41(11)：94-99.

附中文參考文獻(xiàn)：

[11] 楊龍嬰，郭 宇.針對(duì)NAND閃存硬件的形式化建模[J].計(jì)算機(jī)工程，2015，41(11)：94-99.