形式化建模运行在NAND闪存上的DFTL算法

张必红，郭 宇，李兆鹏

(中国科学技术大学 苏州研究院软件安全实验室，江苏 苏州 215123)

1 引 言

随着科技和闪存技术的发展，闪存已经是现代电子设备作为存储的主要选择之一了.但是，闪存固有的物理特性使它相对于传统的磁性存储介质，有很大的区别.比如，闪存有“写前擦除”的限定，所以在修改之前必须先要擦除，但是擦除却是以块为单位的，要比写的单位页大得多.因为这个局限以及磨损均衡，断电保护等原因，在闪存的设计中，有个中间转换层FTL(Flash Translation Layer)的概念被提了出来，FTL算法的核心是进行逻辑地址到物理地址的映射，也就是说如果一个逻辑地址映射到一个物理地址，而这个物理地址已经写了数据了，而现在需要进行更新，那只能写到一个空白的页，然后在映射表中把新的物理地址取代原来的旧的物理地址，映射到要修改的逻辑地址，这样来完成更新操作.一般典型的FTL算法的功能除了地址映射，还包括垃圾回收，坏块管理，断电保护，磨损均衡等.常用的FTL算法有BAST算法，FAST算法，LAST算法，DFTL算法等[1-4].DFTL算法相比较于与其它算法，DFTL算法在企业级规模的工作负载中表现尤其优异，特别在系统响应时间，随机读写，大规模负载中均表现出性能优越.

我们可以看出DFTL算法很重要，但同时它也有着它的复杂性.为了保证闪存的性能，可靠，以及稳定，这类算法通常比其他存储介质的管理软件更为复杂，也更容易出现问题.在工业界SSD的各大厂商的竞争中，FTL层的设计是体现核心竞争力的地方.因为FTL层设计包括元数据管理，数据布局映射、磨损均衡、垃圾回收、缓存策略等，由此可见，FTL算法的重要性和复杂性.

正是由于DFTL算法的复杂和重要性，安全性需要得到可靠的保证，我们就决定采用形式化建模的方法来建立一个可靠的形式化模型.而形式化验证存储系统这方面的研究相当火热，一直以来，完全验证一个文件系统是个非常吸引人的目标[5].在这方面，最接近目标的努力由Schellhorn，Pfahler等在缓慢地进步着[6-9].但是目前验证的文件系统，他们的底层只验证到了读写硬盘这一层，而作为闪存内部算法的FTL层，则目前基本上没有人研究.因为DFTL算法适用于有大规模请求的NAND闪存(SSD)，有着广阔的市场应用场景，所以我们选择对DFTL算法进行形式化建模.

本文的贡献点在于以下：

1)本文根据DFTL算法的基本性质和操作，对DFTL算法的基本数据结构，进行了形式化建模.

2)本文根据DFTL算法读写操作的策略，对DFTL算法的读写操作和圾回收算法进行了分层形式化的建模.

3)本文对DFTL算法的一些基本性质进行了验证.

本文形式化建模的代码为可机器检查的代码，源代码已经开源*源地址https://github.com/zbh24/formal_dftl.

2 背 景

2.1 NAND闪存及DFTL算法

NAND闪存是一种半导体存储器，有读，写，擦除等基本操作，但擦除的单位是要比写的单位页大.相对于传统的机械硬盘，具有随机访问快，功耗低，噪声低等优点.但局限性也很明显，就是有“写前擦除”的限定.针对这种限制，有原地更新和异地更新两种策略.原地更新就是：把当前块中合法的其他数据拷贝到缓存中，然后擦除整个块儿，再对这个空白块中相对应的页进行更新，再把其他合法数据写回.因为擦除速度相对读写速度慢，代价大，现实中一般不会采用原地更新.而异地更新则是把当前页标志为非法的(常用策略是把这种标志记录在OOB中)，再把更新的数据写到新的页中，而记录这种映射关系就是在FTL中，而这种标志为非法的垃圾块在最后是需要进行垃圾回收，从而重新变为合法的空白块.

FTL设计有很多种，如果我们基于映射关系来进行分类，我们可以分为基于块映射的，基于页映射的，和混合映射的.基于块映射就是一个数据块对应一个日志块，写数据时向数据块写数据，而要更新数据时则向对应的日志块写数据，典型的基于块映射的有BAST算法.基于页映射则是每一个页对应一个日志页，更新数据时则写到对应的日志页，典型的页映射算法有DFTL算法.而把这两种基于块和基于页进行混合起来设计的算法，典型的有FAST算法.

DFTL算法是一种基于全相联页映射的FTL算法.它其实并没有明确的日志块的概念，它把所有的块分为两种，一种数据块，即是记录数据的块，块中只记录数据.一种为映射块，即是记录这种映射的块，块中只记录映射数据.DFTL不仅采用了基于页映射的策略，它还利用了访问数据的局部性原理，会在闪存内存中记录最近访问的映射记录，而全部的映射记录则记录在闪存的物理介质上.另外，每页的状态可以分为擦除，数据页，映射页，非法页.DFTL算法会在闪存内存中保存两张表，一张为CMT表(cache_mapping_table)，即为一张有固定容量的缓存表，来记录最近访问的这种映射关系，而淘汰时一般采用LRU(最近最久未使用)算法.另一张为GTD表(global_translation_table)，来记录所有的逻辑地址到映射页的这种映射.

这个读算法流程如下，如果一个请求的逻辑地址在CMT中，那么就直接在CMT中找到对应的物理块和在其中的偏移，读出相应数据.如果请求的逻辑地址没有命中CMT，那么就需要查看CMT缓存表是否满了，如果满了，则牺牲一项并且同时判断牺牲的这一项是不是最新的，最新的则需要写回到映射块中.然后，就把这条最新的映射记录更新到CMT缓存表中，然后再从CMT中读出相应的物理块和页号，接着从物理块中读出数据来.

图1 DFTL读算法示例Fig.1 Example of DFTL read algorithm

图1展示了一个具体的DFTL读算法的例子，一个逻辑地址(lpn = 1234)访问，首先，CMT里没有找到，然后去GTD表查询，找到这条记录存储在映射块的第47页中，然后在影射页读出相应的映射记录，然后去数据页(Dppn = 704)读出数据来，同时把这条最新的访问记录更新到CMT表中.

DFTL写算法的逻辑相对简单，DFTL算法会一直保持两个块，current_data_blcok(当前数据块)和current_trans_block(当前映射块).写算法是直接从current_data_block中分配一个空白页，然后把数据写进去，然后再更新到CMT表.如果current_data_blcok满了，则从自由块中分配一个新块来当做新的current_data_blcok.

随着读写的不断进行，非法页会越来越多，为了使它们可以重新使用，就需要垃圾回收也就是擦除操作来进行.垃圾回收对于数据块和映射块采用不同的策略.如果是映射块，则把合法的映射页复制到当前映射块，然后更新CMT.如果是数据块，则把合法的数据页复制到当前数据块，然后再更新对应的映射页和CMT表.具体算法的形式化定义会在后面进行说明.下面的两张图分别展示了映射块和数据块的回收过程.

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

图2是一个具体的映射块的回收例子，选中映射块Block1，然后把合法的数据拷贝到当前的映射块Block2中，然后再去更新相应的全局映射表(GTD)的记录.

图3的数据块回收，首先选中一个数据块，然后把合法的数据拷贝到当前的数据块，接着对于记录这条映射记录的映射块也进行回收，把含有这条记录的映射块标记为非法，然后在当前的映射块里分配一页，更新新的映射记录，最后来更新GTD表和CMT表.

图3 DFTL数据块的垃圾回收Fig.3 Example of the data block garage collection

DFTL算法的主要操作流程，就是是由以上读操作，写操作，和针对映射块和数据块的垃圾回收算法构成的.

2.2 形式化工具Coq

Coq是一个交互式的定理证明工具，在Coq里面可以形式化定义程序和程序规范，并且可以自动或者半自动地寻找证明项.Coq是建立在构造演算的基础上的，虽然Coq并不是一个完全自动的定理证明工具，但是它提供了一些寻找证明的策略，并提供了一种语言(Ltac)可以让用户自己定义证明策略.目前Coq在形式化领域已经得到比较广泛的应用，比如一个已经被形式化验证的C语言编译器CompCert[10].

3 DFTL算法数据结构的形式化定义

3.1 FTL的组成

根据DFTL算法提出者的设计，我们把DFTL算法形式化建模成以下6个部分：

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个部分分别表示为所有的块的信息表，所有空闲块的列表，部分映射的缓存表，全局映射目录表，当前的数据块号，当前的映射块号.下面我们将分别建模每个模块.

3.2 ftl_bi_table

ftl_bi_table的类型是block_info_table，block_info_table是所有块详细信息的列表，具体包括以下部分：每个块的状态，已经使用了多少页，擦除次数和每页状态的列表，这些页的状态包括擦除，数据页，映射页，非法页.具体结构如下：

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是所有自由块号的列表，它是一个先进先出的队列.每当一个块写完时，需要申请新块的时候，就从这个列表中出队一个块，当一个块被回收时，就加入到这个队列中.具体结构如下：

Definition block_queue：= list block_no.

3.4 ftl_cmt_table

ftl_cmt_table的类型是cache_mapping_table，cache_mapping_table是一个有固定长度缓存记录的列表，这些记录的替换原则则遵循LRU算法.每条记录包括：逻辑地址，物理地址(物理块号和在块内偏移)，以及脏位(is_drity).如果标志位为脏位，则在淘汰时需要到把这条记录，写回到相应的块中，否则淘汰时可以直接丢弃.具体定义结构如下：

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是所有映射块的目录表.每个合法的逻辑地址都有一个对应的映射目录号，而所有的映射目录号都会给分配一个映射页，这些映射页里就写着真正的映射记录.全局映射目录表的结构如下：

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的类型都是自然数(nat)，分别代表着当前的数据块号和映射块号.当需要写一个数据页时，先检查当前的数据块是否还有空闲页，有空闲页就向里面写入数据，没有则分配一个新的数据块，然后把这个新的数据块号更新为当前的数据块号.每当需要写一个映射页时，映射块也是执行类似的操作过程.

4 DFTL算法的形式化定义

4.1 DFTL算法的读过程

根据DFTL算法的原论文描述，我们形式化定义读算法操作如图4所示.

图4 DFTL读算法
Fig.4 DFTL read algorithm

根据DFTL算法的操作语义，我们进行了分层次抽象，从最顶层的FTL读函数接口到最底层调用NAND硬件接口.具体抽象定义如下，首先我们最顶层的DFTL读算法函数签名定义为：

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

表示为输入chip，FTL和逻辑页号，输出为数据，新的chip闪存和FTL.接下来，对于读具体操作，我们会判断当前逻辑页号是否在CMT中.当逻辑页号不在CMT中同时CMT也满了的时候，采用LRU淘汰策略，我们形式化定义LRU淘汰策略时采用淘汰最久最未被使用，为此针对CMT，我们定义了如下四个函数remove_cmt，remove_head，insert_cmt，append_tail.

再接着，我们会进行判断，被淘汰的这条记录的标志位是否为脏位，如果是脏位，则我们需要将被淘汰的记录写回到NAND物理介质中去.关于写回去这个函数，我们抽象出它的操作语义，定义函数签名如下：

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，FTL，逻辑页号以及它对应的映射块和在映射块中的偏移，以及对应新的数据块和在数据块中的偏移，输出为新的chip和FTL.这个函数具体形式化语义为，当这条最新的映射记录被写回NAND物理介质中时，如果对应的映射页里没有时，则我们把这条映射记录添加到对应的映射页里，否则我们就把最新的映射记录更新到对应的映射页里.

再往下，我们需要对GTD和CMT进行查找，更新，插入等操作.所以我们对GTD和CMT这类数据结构都定义了查找，更新，插入等操作.

最后，我们得到了逻辑页号对应的物理页号时，调用read_block函数，在这个函数里调用了一个已经被形式化建模的NAND闪存模型的接口[11]，从而读出数据来，我们的DFTL算法是运行在这个已经被形式化定义的NAND闪存模型上，这就是整个DFTL读算法分层次形式化定义的基本结构.

4.2 DFTL算法的写过程

DFTL算法的写操作形式化定义如下：首先直接检测当前数据块是否满了，如果满了则申请新的一块，然后分配一个新的数据页，直接把数据写进数据页里面，接着再把这条记录写到对应的CMT中，对CMT进行更新操作.具体逻辑见图5.

图5 DFTL写算法
Fig.5 DFTL write algorithm

和FTL读函数一样，我们也采用了分层形式化建模，首先最顶层FTL写函数的函数签名如下：

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

分别表示为输入chip，FTL，逻辑页号和数据，操作完成以后，输出一个新的chip闪存和FTL.

然后，在FTL_write函数中需要对CMT进行更新，关于CMT的更新比较复杂.具体的形式化定义如下：CMT表是一个固定长度的先进先出的队列，每次读或者写都算作一次访问.在队尾的是最新访问的记录，在队头的是最久没有被访问的记录.替换的时候，我们根据不同情况，形式化定义了以下这4种替换策略：

1.CMT满了且CMT里面没有对应记录：去掉第一项，把当前记录添加到队列末尾.

2.CMT满了且CMT有对应的记录：则把当前记录移除，添加到队列末尾.

3.CMT未满且CMT里面没有对应记录：则从头直接找到第一个空白项，把当前记录写进去.

4.CMT未满且CMT有对应的记录：则把当前记录移除，从头找到第一个空白项，把当前记录写进去.

具体可参考cmt_update_when_ftl_write函数，函数签名如下：

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

最后，我们需要把数据写进数据块中，我们抽象出write_data_block函数，这个函数里面会直接调用NAND闪存模型提供的接口.如果当前数据块满了，则需要分配新的块，我们形式化定义了alloc_block，free_block等函数，这些函数的实现涉及下文的垃圾回收算法，我们将在下节中描述，整个FTL读函数的形式化定义流程基本就如上所述.

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

首先我们定义的垃圾回收过程是发生在申请分配块的时候，当且仅当剩余块的数量低于阈值时才会发生调用.至于申请块的函数形式化定义如下：

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

它的函数签名表示如下，输入chip，FTL，和申请的块类型，输出新的chip和FTL.它的操作语义表示：如果剩余块的数量大于阈值时，则正常分配块.否则开始进行垃圾回收操作.垃圾回收的函数的签名如下：

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

函数的操作语义如下：首先是选择出要回收的块，接着对要回收的块的类型进行判断，然后再进行垃圾回收操作，数据块和映射块对应着不同的垃圾回收策略，下面将分别说明.

5.1 映射块的垃圾回收

对于映射块的垃圾回收形式化定义为以下几个步骤和层次：首先给当前的映射块分配一个新的块，注意这个申请操作不受阈值的影响，是总是可以进行的，即不通过调用alloc_block函数来申请块的.接着从所有的块中选择一个映射块进行垃圾回收，注意选择哪个回收块大概要考虑两个方面，第一这个块中至少有一个非法的页，否则没有必要进行回收操作.第二要注意负载均衡，因为一个块的擦写次数是固定的，这里为了简化操作，只考虑了前者.接着当选择一个映射块进行回收时，依次对每个页进行扫描，如果这个页是合法的，则从当前映射块申请一个新的映射页，把这块数据复制进去，同时更新GTD，并把这页设置为非法的，重复以上操作直到这个回收块的所有页都被扫描完以后，则可以把这块映射块标志为非法块，擦除后加入自由块的队列中，这样一次对映射块的垃圾回收操作完成.同时注意，对于原来申请新块的操作，经过垃圾回收过后，因为新申请块的空闲页数大于等于需要回收块的合法页数，所以不难证明原来的读写操作是总是可以进行下去的.

图6 映射块的垃圾回收
Fig.6 Translation block GC

5.2 数据块的垃圾回收

和映射块类似，对于数据块的垃圾回收形式化定义也分为几层.当需要分配数据块的时候，剩余块的数量低于阈值值时，则进行数据块的垃圾回收操作.首先给当前的数据块分配一个新的块，这个操作跟映射块的垃圾回收第一步是一样的.接着对数据块的垃圾回收也是要选择一个合法的回收块，依次对每个数据页进行扫描，如果被扫描的数据页是非法的数据页，则跳过这页并继续扫描，否则一旦被扫描到的是合法的数据页，则首先从当前数据块分配一个新的数据页，然后把这块合法的数据页的数据复制到新的空白数据页，直到把整个回收块的数据页扫描完.注意在这个过程中，如果CMT中有相应的记录，则进行CMT的更新，并且还要进行映射页和GTD表的更新.另外也可能会发生当前的映射块满了，需要再次申请新的映射块.所以在数据块的垃圾回收中可能会多次发生对映射块的垃圾回收.最后当所有的页都被扫描完成以后，则标志当前块为非法，擦除后加入自由块的队列中了，至此对数据块的垃圾回收操作完成.同样的原来申请的新的数据块的操作，经过数据块的垃圾回收过后，总是可以继续进行下去的.

关于垃圾回收的形式化模型，有两点需要说明一下：

1)这个垃圾回收的触发阈值是剩余块一旦小于等于2块，则进行垃圾回收操作.因为在数据页的垃圾回收操作时，可能会发生嵌套1层的映射块的垃圾回收操作，所以剩余的自由块的数量必须至少大于等于2，才能使垃圾回收继续进行下去，否则小于2块时才进行垃圾回收，则有可能会使操作卡死.

2)关于数据块的回收操作，我们可以采取批量更新的策略，提高效率，不过这不影响垃圾回收算法的语义，因此我们的形式化时没有采取这种优化.

图7 数据块的垃圾回收
Fig.7 Data block GC

6 形式化模型的基本性质

因为形式化建模DFTL算法是为了保证DFTL算法的正确性，所以我们首先必须正确地描述运行着DFTL算法的NAND闪存的性质.首先我们定义了一个简单的硬盘模型，然后定义了R关系来保持硬盘和运行DFTL算法的NAND闪存具有一致性，接着定义Inv关系来保证NAND闪存运行过程中的一致性，具体定义如下：

R：∀sec,hddreadhdd sec=fldreadfldsec

Inv：∀c f,Finvf∧ Rinvc f

以上R表示对于任意一个地址，闪存和硬盘读出来的数据都是一样的.Inv表示在运行过程中，FTL软件的一些性质会始终保持不变并且FTL软件层和硬件层的一致性也始终保持不变.运行着DFTL算法的NAND闪存具体有以下性质(由于篇幅所限，仅列上部分性质)：

性质1.

Rinit:=R hddinitfldinit

性质1表示一开始整个NAND闪存都是空白的，在任意和硬盘同样的位置读出的数据都是一样的，即是NONE或者0.

性质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"))

性质2表示，对于任意一个chip，ftl，page_no，data，只要chip和 ftl满足Inv关系并且这个page_no是合法的，那么就一定可以把数据写进去，并且在写过后的闪存同样的地址读出的数据和写进去的数据是一样的.

性质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′

性质3表示，对于在任意一个合法的逻辑地址lpn写入数据之后，在任意的lpn’不等于lpn的地址上读出的数据跟写入数据之前是一样的，即表示DFTL算法在一个逻辑地址写入数据后，不影响另一个逻辑地址的数据.

以上这些基本性质均在Coq中得到了证明.

7 结束语以及未来工作方向

闪存设备现在使用的已经越来越普遍了，在存储系统中扮演着一个非常重要的地位，但是闪存设备的复杂性和频繁出现问题的危害性需要得到重视.本文就是针对闪存中使用的一种比较经典的DFTL算法进行了形式化的建模.首先我们针对DFTL的基本构成和性质，对DFTL的基本数据结构进行了形式化建模，其次我们对DFTL算法的读操作和写操作也进行了分层次的形式化定义，再接着我们针对DFTL算法一定会出现的非法块，也定义了垃圾回收的形式化算法.最后，我们对DFTL算法的一些基本性质在我们的模型上的正确性进行了验证.我们未来的工作，就是在已经形式化定义好的DFTL模型的基础上，对DFTL算法的一些更复杂的性质，在一个描述正确性的框架下，进行形式化验证，来保证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.

附中文参考文献：

[11] 杨龙婴，郭 宇.针对NAND闪存硬件的形式化建模[J].计算机工程，2015，41(11)：94-99.