Edelweiss: 分布式编程的自动存储回收

论文地址：Edelweiss：分布式编程的自动存储回收 Conway et al. 2014

Edelweiss是一个非常令人兴奋的发展，是朝着更好的方式建立分布式系统的路标。

在我职业生涯的早期，我有幸被分配到一个优秀的技术团队中，其中包括两位我后来长期合作的工程师：格林·诺明顿（Glyn Normington）和史蒂夫·鲍威尔（Steve Powell）。我们正在进行的项目涉及到对TP监视器（良好的老式事务处理）的重大改进。Glyn和Steve在形式化方法的实际应用方面都非常有经验，在这个项目中发生了一些奇妙的事情（在我看来）：对于系统的一个关键部分，产生了一个简单的形式化规范（如果我记得正确的话，使用CSP），并显示出所需的行为。然后，这个简单的模型被逐步改进为一个更节省空间和时间的实现模型，显示了每个步骤的等价性，因此更复杂模型的持续正确性。

Edelweiss就是这么做的-但为了代码。您可以编写简单的代码来表示系统应该做什么，Edelweiss引入了一系列改进，这些改进保留了用户可见的行为并提高了效率（在本例中，是基于事件日志交换（ELE）的系统的效率）。

无论是从业者还是学者都提出了尽可能使用不可变状态的写作系统。进程不是直接修改共享状态，而是积累和交换不可变的消息或事件日志，我们称之为事件日志交换（ELE）。以前学到的信息永远不会被替换或删除，但可以通过记录新的事实来掩盖，这些事实表明以前的信息不再有用。

基于ELE的设计有很多优点，这使得我无法在这里进行探索，但同时也带来了事件日志不断增长的问题。

为了避免这种情况，ELE设计通常包括一个后台“垃圾收集”或“检查点”协议，该协议回收不再有用的信息。这种日志记录和后台回收模式广泛存在于分布式存储和数据管理文献中，已应用于许多核心技术，包括可靠的广播和更新传播、组通信、密钥值存储、分布式文件系统、因果一致性、仲裁一致性、事务管理，以及多版本并发控制。

这些方案通常是手工从头开始构建的，而且很微妙，很难实现。雪绒花是Bloom的一个子语言，它省略了用于变异和删除数据的原语（因为ELE应用程序不这样做）。

Edelweiss程序描述了局部知识对分布式计算的贡献。系统计算互补垃圾收集逻辑：也就是说，它自动安全地丢弃将来永远不会有用的数据。

作为阅读这篇论文的一个附带好处，你将得到一个关于Bloom本身的精彩而简洁的介绍，这是遵循示例所必需的。从一个不可靠消息传递的基线开始，我们接着处理一系列令人印象深刻的短程序，用于可靠的单播、可靠的广播、键值存储、因果一致的键值存储和原子寄存器。

其中最大的是具有因果一致性的分布式密钥值存储，它需要19行雪绒花规则。（由此产生的由雪绒花产生的高效实现相当于一个62行香草花程序）。比较两个最近的C++实现，需要大约13kLoc！

Edelweiss产生的垃圾收集方案通常与文献中针对每个设计提出的手写方案相似。此外，不需要手工编制的垃圾收集方案简化了程序设计——生成的程序更具声明性，程序员可以专注于解决其域问题，而不是担心存储问题。

Bloom和Edelweiss
Bloom集群是一组节点。每个节点都有集合和规则。集合有一个模式，由一组事实（元组）组成，就像数据日志中的一个关系。Bloom中有几种收集类型-table和channel是本文中最常见的两种。表是一个持久的集合，通道集合允许异步通信：插入通道的事实在未来的不确定时间传递到远程节点。

节点运行事件循环：在每个时间步中，都会接收入站消息并将其添加到本地集合。然后对这些集合计算规则以生成新值。如果这些表示出站消息（添加到通道的事实），则发送消息。然后节点返回到侦听入站消息。

让我们看看简单可靠的单播程序，它建立在底层未确认的异步通信之上。

状态块（第04-08行）定义集合，bloom块（第10-13行）定义规则。

chn集合（第05行）存储（id、addr、val）事实（元组）。id是键，addr前面的@符号表示此列指定将向其发送频道消息的位置。

sbuf集合（第06行）存储（id、addr、val）事实，并充当我们传输的信息的发送缓冲区。rbuf集合（第07行）是我们接收到的消息的接收缓冲区。

在每个时间戳中，我们匹配规则rhs上输入集合中的事实，并将新事实添加到规则lhs中命名的集合中。

在第11行，<~运算符表示rhs将在将来某个不确定的时间合并到lhs集合中。因此，此规则将事实从发送缓冲区复制到通道中以进行异步传递。

在第12行中，信道集合中接收到的任何传入消息（事实）都被添加到接收缓冲区中。

这是一个完整的程序，足以让您了解Bloom/Edelweiss的声明式编程风格。

Edelweiss源码（ruby写的而且已经不再更新-仅仅作为了解可以分析下。不知道当时为什么做分布式系统形式化证明竟然用ruby语言。在我看来最好的用haskell或者ocaml）

改进1：避免冗余消息
这个雪绒花项目的美妙之处在于，它是如何清晰和简单地推理行为。外部可见的行为正是我们想要的，但内部效率却留下了一些需要的东西。例如，我们真的需要无限期地扩展发送缓冲区，并在每个时间步将其中的每个事实插入到通信通道中吗？

Edelweiss的ARM（避免冗余消息）优化规则可以检测到这种低效率，并自动重写程序以避免重复传输。Edelweiss不能改变程序的语义（可靠）传递，因此需要引入ack机制。它可以推断acks只需要包含消息id（chn的键）。

这种Edelweiss精化的结果就好像程序员添加了以下两个集合：

table :chn_approx, [:id]
channel :chn_ack, [:@sender, :id]

更新了bloom规则如下：

bloom do
chn :id)
rbuf <= chn
chn_ack <~ chn {|c| [c.source_addr, c.id]}
chn_approx <= chn_ack.payloads
end

它已经明显比最初的程序复杂（尽管与非Bloom语言实现相比仍然令人印象深刻！）。

改进2：正差异回收（DR+）
ARM改进避免了重复传输，但发送缓冲区仍然无限增长——我们希望能够回收已确认的消息。

Edelweiss的正差异回收（DR+）改进能够推断sbuf仅被一个规则引用（应用ARM后重写的bloom块的第一行中的“notin”运算符语句）。sbuf位于该运算符的“积极”一侧（向chn_approx添加新事实不会导致以前发送的内容需要重新发送）。因此，DR+优化将以下规则添加到程序中：

sbuf <- (sbuf * chn_approx).lefts(:id => :id)

改进3：范围压缩
我们还可以减少chn U approx系列使用的存储空间。我们实际上不需要在集合中保留所有事实（id），只需要知道从发送缓冲区中删除哪些id是安全的。如果id是从一个完全有序的序列分配的，并且我们希望所有消息最终都能被传递，那么我们最终将得到一组从k（初始值）到n（最后发送值）不等的id。对于无序异步传递，这个范围在任何时间点都可能有间隙，因此我们通过存储成对集（k0，k1），…，（km，kn）来用范围树来表示它，其中每对表示一个无间隙序列。

Edelweiss会在“有利可图”时自动对出站通道消息应用范围压缩。程序员还可以使用新的“范围”集合类型显式地请求它进行集合。

改进4：标点符号
在本文中，您将看到可靠的单播节目扩展到可靠的广播。当ARM和range压缩应用到这个新的上下文中时，会发生一些非常有趣的事情：

回想一下，对于可靠的单播，chn_approx最终将被压缩到一个值，从而有效地产生一个逻辑时钟。对于广播，chn_approx将包含广播组中每个节点的单个“时钟”值，因此其行为类似于矢量时钟。也就是说，ARM和距离压缩的结合本质上“发现”了事件历史和逻辑时钟之间的关系！Edelweiss允许程序员简单地操作不可变事件集；然后它自动生成相应的“时钟”管理代码。

对于广播，从chn_approx回收存储器比较困难，因为我们需要每个收件人的ack才能安全地这样做。Edelweiss通过添加标点符号的概念来处理这个问题。标点符号保证集合中不再出现与谓词匹配的元组。雪绒花引入了一种新的密封集合类型，该类型指示在系统初始化后其内容固定的集合。这使雪绒花能够自动为集合发出标点符号。当集合未密封时，使用epoch可以启用相同的优化。

细化5：负差异回收

负差异回收应用于X.notin（Y，：A=>：B）形式的表达式，其中X和Y是持久的，A是X的键。它从X和Y回收匹配的元组，代价是保留一个范围压缩的X键集。有关详细信息，请参阅文件中的键值存储。

实践中的Edelweiss
请参阅整篇文章，了解一组很棒的Edelweiss示例程序，最终生成一个用于原子读/写寄存器的快照隔离程序。

虽然传统的设计使用可变存储，但我们展示了如何通过累加不可变事件日志的Edelweiss程序实现可变寄存器接口。然后，我们扩展程序以支持对多个寄存器的原子写入和反映一致快照的多个寄存器读取。对于所有这些程序，Edelweiss支持自动和安全的垃圾收集，生成与原始程序在语义上等价的节省空间的实现。

未来的方向包括将Edelweiss推广到连接半格，以捕获除集合中事实的累积之外的其他类型的增长——例如，单调递增的整数，或从false移动到true的布尔值。