Lasp：一种用于分布式、无协作编程的语言

论文地址： Lasp：一种用于分布式、无协作编程的语言——Meiklejohn&Van Roy 2015

克里斯托弗·梅克勒约翰最近宣布，他将离开巴索，根据他在Lasp方面的研究成果攻读博士学位。对巴索来说是个不幸的消息，但对我们其他人来说，看到这些想法的发展是令人兴奋的。我祝你在新的事业中一切顺利，克里斯，不断创新！

Lasp建立在Derflow和CRDTs中的思想之上。

无冲突复制数据类型（CRDTs），提供形式化为强最终一致性的属性…强最终一致性（SEC）导致并发更新到复制状态的确定性解决方案。这种特性在分布式系统中是非常理想的，因为它不再将解析逻辑放在程序员的手中；程序员能够使用复制的数据类型，这些数据类型的功能就好像它们是顺序对应的一样。然而，已经证明，这些数据类型的任意组合是非常重要的。

使用CRDTs，我们已经开始为分布式、最终一致的数据类型创建一组构建块。研究继续扩展集合中的类型集，并改进其实现的效率。但是，我们显然需要释放它们的全部潜力的是组合这些类型并从这些组合（等等，无限期）中创建高阶抽象的方法。这与我们上周研究的Burckhardt等人关于云类型和全局序列协议的工作所面临的挑战是一样的。Lasp为我们提供了一个编程模型，它被实现为一个Erlang库，其主要数据类型是CRDT，并提供了组成这些原语的功能机制。

为了实现这一目标，我们提出了一个新的编程模型，旨在简化正确的、大规模的、分布式的编程，称为Lasp。此模型提供了使用函数式编程中的操作来确定地将crdt组合成观察SEC属性的更大计算的能力；这些应用程序支持使用其值在外部显示为非单调的数据结构进行编程，而在内部使用对象的单调元数据进行计算。

本文的第2节以观察到的移除集CRDT（或集）为中心，为问题空间提供了一个非常清晰和简洁的背景。

观察到的删除集CRDT单调地建模任意非单调操作，如同一元素的添加和删除，以保证在不同副本上并发操作的收敛性。

OR集不是简单地跟踪成员身份，而是为集合中的每个值保留一个“add Set”和一个“remove Set”。询问某个值v是否在集合中的查询的结果是非单调的，并且随着时间的推移而变化，但是执行add或remove操作的结果相对于集合的内部数据结构是单调的（分别导致add set或remove set的加法）。

但如果我们同时使用两个（或更多）或两个集，会发生什么呢？

CRDTs的收敛特性对于分布式系统的计算是非常理想的：这些数据结构对更新、重排序、复制和消息延迟具有弹性，这些都是在不可靠的异步网络上进行计算的相关问题。但是，这些收敛特性仅适用于单个复制对象，而不扩展到组成多个CRDT的计算。

作者给出了一个简单使用map的例子。我们想在一个集合上映射一个函数f来产生一个新的输出集合。假设我们有一个或集的两个副本r1和r2，并且在每个节点（副本）上，我们将f映射到集成员上，以生成输出集o1和o2。我们现在无法聚合输出集o1和o2的副本-我们通过映射到外部表示来丢失内部add-remove集中包含的关键信息。

Lasp解决了这个问题。

对于t型的每个CRDT，Lasp提供以下核心操作：

• declare（t）：声明t类型的变量
• 绑定（x，v）：将变量x绑定到值v。值v与前一个值连接以创建新值。
• 更新（x，op，a）：将op应用于由常数a标识的x
• 读（x，v）：单调读操作
• 严格读取（x，v）：严格单调读取操作

单调读取操作的工作方式是整洁的。在x的值大于（严格读取）或等于（正则读取）x上诱导的偏序关系中v的值之前，x的读取不会返回。偏序关系当然是CRDTs的连接半格的基础。

单调读取操作确保读取操作在与先前读取的结果一起提供时始终读取相等或更大的值。在处理复制的数据以确保向前推进时，此行为对我们的系统非常重要。

考虑在节点a1、a2和a3上复制三次变量a。应用程序从a1读取a并对其进行修改。更新将异步传播到a2和a3。副本a1暂时无法访问，应用程序从a2读取a的值…

在本例中，在给定消息延迟、失败和异步复制的情况下，副本a2可能暂时具有比副本a1更早的状态。单调读取操作确保在基于触发值的给定副本处的a的晶格的部分顺序上定义的等效或更大状态可用之前，读取不会完成。

对于基础知识，现在对于组合功能来说，就到此为止了。我们可以将CRDT看作一系列状态更新：

正如我们将在第4节中证明的那样，Lasp中每个基于状态的CRDT都有一个单一的状态序列，随着时间的推移，随着更新操作的发布而单调地演化；这与前面提供的通胀定义（定义2.4）类似。CRDT的当前状态存储在变量中；变量的连续值构成CRDT的状态序列。

复合运算符创建（lightweight，Erlang）从不终止的进程，并处理对其输入和输出的更新序列。

• 映射（x，f，y）：将函数f应用于x到y
• filter（x，p，y）：在x上向y应用filter谓词p
• 折叠（x，op，y）：使用op将值从x折叠到y
• 积（x，y，z）：计算z中x和y的积
• 并（x，y，z）：计算z中x和y的并
• 交集（x，y，z）：计算x和y在z中的交集

或集合上的映射可能是这样的：

程序员可以将lasp应用程序当作未分发的应用程序进行推理：

在Lasp中编程有多容易？它能像用非分布式语言编程一样简单吗？是否可以忽略CRDTs的副本到副本通信和分发？由于CRDTs具有很强的语义特性，这是确实可能的。在这一节中，我们将Lasp程序的分布式执行形式化，并证明存在一个集中式执行，即一个状态序列，它产生与分布式执行相同的结果。这允许我们使用与集中程序相同的推理和编程技术。

Lasp的实现建立在Riak核心库的基础上，并使用Dynamo风格的分区来跨集群中的节点分发crdt副本，以确保高可用性和容错性。主动反熵协议确保所有副本都是最新的。Quorum用于系统操作：

在第4节中，我们概述了系统的三个特性：碰撞停止故障、反熵和正确性。虽然这些属性足以确保计算的汇合性，但它们并不保证如果CRDT的给定副本在将其状态与对等副本通信之前失败，将观察到所有更新。因此，为了保证安全性和容错性，对副本的仲裁执行读取和更新操作。

Quorums也用于所有合成操作：

给定对象本身的复制，为了保证容错性和高可用性，我们的函数编程操作和集合论操作也必须复制。为了实现这一点，仲裁复制用于联系输出CRDT附近的大多数副本，这些副本负责读取输入CRDT并执行转换。

举例说明了用Lasp建立的广告计数器和复制Key-value存储。

这个广告计数器的实现是完全单调和同步自由的。在活动进程连接的CRDTs中，ads的添加和删除、ads的添加和删除以及ads的视图数量达到契约数量时的禁用都被建模为状态的单调增长。程序员可见的非单调性由CRDTs中的单调元数据表示。

由于Christopher Meiklejohn将进一步研究Lasp作为其博士学位的一部分，因此本文的未来工作部分为我们提供了一个可能出现的线索：

我们对Lasp的未来计划包括将其扩展为一个成熟的语言和系统、确定更有效的状态传播的优化、探索更强大的一致性模型、优化分发和副本放置以获得更好的容错性和减少延迟。我们还计划对Lasp系统进行评估，并验证我们的假设，即Lasp的弱同步模型非常适合于可扩展的高性能应用，特别是在具有间歇性连接的设置中，例如移动应用和“物联网”。我们的最终目标是使Lasp成为一种通用语言，用于构建尽可能少使用同步的大规模分布式应用程序。