闪存存储抽象层

规范

该store在存储接口之上提供了一个从键到值的部分函数。存储的总容量取决于存储的大小。存储更新可以捆绑在事务中。可变操作是原子的，包括在中断时。

存储在闪存效率方面是高效的，因为它有效地使用存储寿命。对于每一页，所有单词在擦除周期之间至少写入一次，所有擦除周期都被使用。然而，并非所有写入的单词都是用户内容：寿命还消耗在元数据和压缩中。

存储可以通过除了键值之外的其他条目进行扩展。它本质上是一个框架，提供对存储寿命的访问。部分函数只是最常见的用法，可以用来编码其他用法。

定义

一个 条目 是一个键和值的对。一个 键 是一个介于0和4095之间的数字。一个 值 是一个长度介于0和1023字节之间的字节数组（对于足够大的页面）。

存储提供了以下 更新

• 给定一个键和一个值，StoreUpdate::Insert 更新存储，使值与键关联。其他键的值保持不变。
• 给定一个键，StoreUpdate::Remove 更新存储，使键不与任何值关联。其他键的值保持不变。此外，如果键关联了值，该值将从存储中擦除（所有位都被设置为0）。

该存储提供以下只读操作

• Store::iter遍历存储，返回所有条目恰好一次。迭代顺序未指定，但在可变操作之间是稳定的。
• Store::capacity返回在存储满之前可以存储多少单词。
• Store::lifetime返回在存储寿命耗尽之前可以写入多少单词。

该存储提供以下可变操作

• 给定一组独立的更新，Store::transaction应用更新序列。
• 给定一个阈值，Store::clear删除所有键值大于或等于阈值的条目。
• 给定一个单词长度，Store::prepare进行一次压缩步骤，除非可以在不进行压缩的情况下写入这么多单词。此操作对存储没有影响，但可能仍然会修改其存储。特别是，存储具有相同的容量，但可能的寿命可能减少。

如果操作过程中断电，可变操作是原子性的，则存储要么被更新（就像操作成功一样），要么保持不变（就像操作未发生一样）。如果存储保持不变，寿命可能仍然会被消耗。

存储依赖于以下存储接口

• 可以读取字节切片。该切片不会跨越多个页面。
• 可以写入单词切片。该切片不会跨越多个页面。
• 可以擦除一个页面。
• 页面按顺序从0索引。如果实际底层存储是分段的，那么存储层应将这些索引转换为实际页面地址。

存储的总容量为C = (N - 1) * (P - 4) - M - 1单词，其中

• P是每页的单词数
• N是页数
• M是值的最大长度（对于足够大的页面为256）

每个可变操作使用的容量如下（瞬态单词仅在操作期间使用容量）

*如果更新是事务中唯一的，则0，否则1。

存储的总寿命在L = ((E + 1) * N - 1) * (P - 2)以下和L - M单词以上，其中E是最大擦除周期数。寿命在包括瞬态使用容量以及进行压缩时使用。压缩频率和寿命消耗与存储负载因子（使用容量与总容量之比）正相关。

可以通过容量来近似瞬态词的成本：L 个瞬态词相当于 C - x 个容量单位，其中 x 是操作的平均容量（包括瞬态）。

先决条件

以下假设需要成立，否则存储可能会以意外的方式运行

• 一个字可以在擦除周期之间写入 两次。
• 在存储器的第一次启动后，一个页可以擦除 E 次。
• 当在写入一个切片或擦除一个页时断电，下一次读取会返回一个切片，其中应该被修改的子集（可能没有任何或全部）的位已经被修改。
• 读取一个切片是确定的。当在写入一个切片或擦除一个切片（擦除包含该切片的页）时断电，重复读取该切片会返回相同的结果（直到它被覆盖或其页被擦除）。
• 要判断一个页是否被擦除，只需要测试它的所有位是否都等于 1。
• 当在写入一个切片或擦除一个页时断电，该操作不计入限制。然而，完成该写入或擦除操作将计入限制，就像每字写入次数和擦除周期次数可以是分数一样。
• 存储仅由存储修改。请注意，支持完全擦除存储，实际上会丢失所有内容和生命周期跟踪。为了保持生命周期跟踪，建议使用 Store::clear 并将阈值设置为 0。

即使在这些假设之外，存储属性也可能仍然保持，但失败的可能性会越来越大。

实现

我们定义以下常量

• E <= 65535，一个页可以擦除的次数。
• 3 <= N < 64，存储中页的数量。
• 8 <= P <= 1024，一个页中的字数。
• Q = P - 2，虚拟页中的字数。
• M = min(Q - 1, 256)，值的最大长度（字为单位）。
• W = (N - 1) * Q - M，窗口大小。
• V = (N - 1) * (Q - 1) - M，虚拟容量。
• C = V - N，用户容量。

我们使用每个页的前两个字从物理存储构建一个虚拟存储。

• 第一个字包含页被擦除的次数。
• 第二个字包含在压缩过程中此页将要移动到的起始字。

虚拟存储的长度为 (E + 1) * N * Q 个字，并代表存储的生命周期。（我们预留最后 Q + M 个字以支持添加紧急生命周期。）这个虚拟存储具有线性地址空间。

我们在每个 Q 对齐边界定义一组重叠的 N * Q 个字的窗口。我们称 i 为从 i * Q 到 (i + N) * Q 的窗口。只有那些实际存在于底层存储中的窗口。我们使用压缩将当前窗口从 i 移动到 i + 1，保留存储的内容。

对于虚拟存储的给定状态，我们定义 h_i 为窗口 i 中第一个条目的位置。我们称之为窗口 i 的头部。因为条目最多有 M + 1 个字，它们最多可以重叠 M 个字。因此，我们有 i * Q <= h_i <= i * Q + M。由于在第一页之前没有条目，我们有 h_0 = 0。

我们定义t_i为窗口i中最后一个条目之后的一个位置。如果没有条目在该窗口中，我们设t_i = h_i。我们称t_i为窗口i的尾部。我们定义紧缩不变量为t_i - h_i &leq V，窗口不变量为t_i - h_i &leq W。紧缩不变量可能在最多N - 1次紧缩的序列中暂时被破坏。

我们定义|x|为位置x之前的容量。我们有|x| &leq x。我们定义容量不变量为|t_i| - |h_i| &leq C。

使用这种虚拟存储，只要既有虚拟容量来保留紧缩不变量，又有容量来保留容量不变量，条目就会被追加到尾部。当虚拟容量耗尽时，窗口的第一页被紧缩，窗口移动。

条目通过位的前缀进行识别。前缀必须包含至少一个设置为0的位，以与尾部区分。条目可以是以下之一

• 填充：第一个位设置为0的词。其余部分是任意的。这个条目用于标记操作中断后部分写入的词作为填充，以便它们被未来的操作忽略。
• 头部：第二个位设置为0的词。它包含以下字段
  • 一个位，指示条目是否被删除。
  • 一个位，指示值是否与词对齐并且其最后一词的所有位都设置为1。条目的最后一词用于检测条目是否已完全写入。因此，它必须包含至少一个位等于0。
  • 条目的键。
  • 值的字节数长度的长度。值跟随头部。如果值不是与词对齐的，则条目是词对齐的。
  • 条目第一个和最后一个词的校验和。
• 擦除：在紧缩过程中使用的词。它包含要擦除的页面和校验和。
• 清除：在清除操作期间使用的词。它包含阈值和校验和。
• 标记：在事务期间使用的词。它包含标记之后的更新数量和校验和。
• 删除：在事务内部使用的词。它包含要删除的条目的键和校验和。

校验和是等于0的位的数量。

证明

紧缩

设I是一个所有不变量都成立的窗口。我们将证明在每次紧缩之后，下一N - 1次紧缩将保持窗口不变量（容量不变量显然被保持） 。我们还将证明在N - 1次紧缩之后，紧缩不变量被恢复。

我们考虑完全紧缩后的虚拟存储上的所有符号。我们将使用|x|符号，尽管我们更新虚拟存储的状态。这是可以的，因为紧缩不会改变现有词的状态。

我们首先证明在每次紧缩之后，窗口不变量被保持。

for all (1 <= i <= N - 1)   t_{I + i} - h_{I + i}  <=  W

我们假设i在1和N - 1之间。

紧缩的一步将尾部推进了多少个词，最后一页可能重叠在下一页。

for all j   t_{j + 1}  =  t_j + |h_{j + 1}| - |h_j| + 1

通过归纳，我们有

t_{I + i}  =  t_I + |h_{I + i}| - |h_I| + i

我们有以下属性

t_I  <=  h_I + V
|h_{I + i}| - |h_I|  <=  h_{I + i} - h_I

将它们替换到我们之前的等式中，我们可以得出结论

t_{I + i}  =  t_I + |h_{I + i}| - |h_I| + i
          <=  h_I + V + h_{I + 1} - h_I + i
iff
t_{I + i} - h_{I + 1}  <=  V + i
                       <=  V + N - 1
                        =  W

一个重要的推论是尾部保持在窗口内

t_{I + i}  <=  (I + i + N - 1) * Q

我们具有以下属性

h_{I + i}  <=  (I + i) * Q + M

根据W的定义，我们得出以下结论

t_{I + i}  <=  h_{I + i} + W
           <=  (I + i) * Q + M + (N - 1) * Q - M
            =  (I + i + N - 1) * Q

经过N - 1次压缩后，压缩不变性得以恢复。特别是，剩余容量在不需要压缩的情况下可用。

V - (t_{I + N - 1} - h_{I + N - 1})  >=  C - (|t_{I + N - 1}| - |h_{I + N - 1}|) + 1
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~      ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~   ~
        immediate capacity                         remaining capacity              |
                                                                         reserved for clear

我们可以替换C的定义并简化

V - (t_{I + N - 1} - h_{I + N - 1})  >=  V - N - (|t_{I + N - 1}| - |h_{I + N - 1}|) + 1
iff  t_{I + N - 1} - h_{I + N - 1}  <=  |t_{I + N - 1}| - |h_{I + N - 1}| + N - 1

我们有以下属性

t_{I + N - 1}  =  t_I + |h_{I + N - 1}| - |h_I| + N - 1
|t_{I + N - 1}| - |h_{I + N - 1}|  =  |t_I| - |h_I|
|h_{I + N - 1}| - |t_I|  <=  h_{I + N - 1} - t_I

由此我们得出以下结论

     t_{I + N - 1} - h_{I + N - 1}  <=  |t_{I + N - 1}| - |h_{I + N - 1}| + N - 1
iff  t_I + |h_{I + N - 1}| - |h_I| + N - 1 - h_{I + N - 1}  <=  |t_I| - |h_I| + N - 1
iff  t_I + |h_{I + N - 1}| - h_{I + N - 1}  <=  |t_I|
iff  |h_{I + N - 1}| - |t_I|  <=  h_{I + N - 1} - t_I

校验和

我们想要的主要属性是，所有部分写入/擦除的单词要么是初始单词，要么是最终单词，要么是无效的。

我们说一个位序列TARGET可以从一个位序列SOURCE到达，如果两者具有相同的长度，并且SOURCE & TARGET == TARGET，其中&是该长度位序列上的按位与运算。换句话说，当SOURCE有一个位等于0时，TARGET也有那个位等于0。

唯一写入的条目以101或110开头，并且从擦除的单词写入。将条目标记为填充或已删除是一个单比特操作，因此该属性显然成立。对于这些情况，证明依赖于事实，即前3位中恰好有一个位等于0。要么这3位仍然是111，在这种情况下我们希望剩余的位等于1。否则，我们可以使用给定类型的条目的校验和，因为这两种类型的条目不能从对方到达。以下是基于前3位的分区可视化