Mobile process calculi for programming the new blockchain

David Currin, Joseph Denman, Ed Eykholt, Lucius Gregory Meredith

December 2016

介绍

从90年代早期开始，伴随着MCC的ESS技术以及其他一些新技术的兴起，分布式以及去中心化应用开始展露头脚。这其中的核心技术是基于一个虚拟机环境，在一个网络连通的物理环境中运行节点。这个想法为开发一个适合现有互联网模型的去中心化且可协调的应用程序提供了丰富的材料。在如此丰富的环境之上，应用程序开发的模式是一个值得深入研究的课题。

在这里，我们针对于去中心化应用的开发、部署做了一个简单且特殊的调研，并且基于这些调研结果抽象出了一个单一模型。值得注意的是，这个单一模型很好地适应了区块链的一些特点，并且包含了有关智能合约的概念。因此，这个总结可以作为RChain架构的设计原理以及区块链智能合约的rholang模型。

Actors, 元组和π演算

Rosette

MCC的Carnot研究小组在网景公司成名整整十年之前就已经预测到了互联网的商业化。然而，Carnot小组专注于去中心化、分布式的应用，并且研发出了一个称为可扩展服务网关(Extensible Services Switch,EXX)的网络应用结点，以及用于在这些结点之上编程的编程语言Rosette。 而Rosette/ESS的研究模型则是actor模型。在这里，我们特别讲述了由Carl Hewitt开发并由Gul Agha精炼的模型，Gul Agha之后为Rosette的设计提供了建议。

Rosette在作用域和优雅上的成果令人瞩目。尤其是，Rosette把一个actor分解为

  • 一个邮箱(一个接受actor客户端消息的队列)
  • 一个状态(许多值组成的元组)
  • 元信息(描述如何通过更抽象的关键字访问状态值)
  • 以及一个共享的行为对象(一个从消息类型到响应时需要运行的代码的映射，大致相当于C++语言中的vtable)

Actor的处理过程包括从邮箱中读取下一条信息，使用共享的行为对象(share behavior object, sbo)来确定使用哪些代码来执行而得到针对该消息的响应，然后在执行环境中运行代码，在该执行环境中元信息所引用的键被绑定到状态元组对应的位置。该代码主要将消息发给其他actor，之后可能在等待响应。

Actor通过更新在并发运行中提供一个一致的状态视图，更具体地说，一个actor直到它被更新之后才会处理邮箱中的下一条消息，并且当actor正在处理当前消息时，邮箱上锁并且将进来的客户端请求排队。当一个actor调用了更新操作，一个新的逻辑线程将被创建来处理邮箱队列中的下一条信息。线程对该actor状态的视图全部都提供给了该次更新。前面的线程可能仍然会对状态进行更改，但是这些对后面处理邮箱中后续消息的线程都是不可见的，因此对后续的客户端请求也是不可见的。这种方法提供了一种可伸缩的并发概念，从消息抵达顺序不确定的单线程容器，扩展到某些系统级支持逻辑线程映射的外部容器(例如虚拟机，操作系统或硬件本身)。

这已经是一个比当今大多数工业系统中存在的acotr模型（比如Scala的AKKA框架）更具表达能力的模型。然而，Rosette模型更加优雅的是它对元编程的全部承诺。在Rosette模型中，一切都是actor。特别是，actor的邮箱是actor，而邮箱，状态，元信息和sbo都是actor。值得注意的是，Rosette使得这个完全反射模型具备退化到与Java或C＃等语言相同或更好性能的可能性。

从某种意义上说，Rosette模型中的actor的结构化反射也在Java这样的语言中得到了体现，在这些语言中，类也可以通过编程方式探查和参与计算的对象。然而，Rosette将反射原理更进一步。该模型不仅提供了结构化反射，而且还提供了程序化反射，通过提供与模型中固有的并发性相一致的延续的概念。具体而言，就像移位复位风格的分隔延续表示中的使用移位块使得等待延续可用在代码块中一样，Rosette的反射方法使得等待延续可用作方法的参数。稍后再说。

结束这个简短的总结笔记：Rosette不仅仅是结构上和程序上的反射，更是词法上的反射。也就是说，Rosette程序中的所有句法结构也都是actor！反射式的底层构造为干净的宏系统、嵌入式领域特定语言以及其他语法和符号处理特性提供了基础，而这些是许多工业语言在Rosette完成20年后还难以提供的特性。

元组空间

大约在Rosette模型被研究用于在去中心化和分布式环境中开发应用的同时，Gelernter提出了Tuplespaces。他的想法是在互联网的物理层和通信层之上创建一个逻辑仓库。该仓库基本上被组织为分布式键值数据库，其中键值对被用作计算之间的通信和协调机制。 Gelernter描述了与元组空间交互的三个基本操作： out 用于在元组空间创建一个新的数据对象，in 从元组空间消费（移除）一个对象，以及 rd 读取一个对象并且不移除它

与消息传递系统不同的是，这种方法允许发送者和接收者在彼此不知情的情况下进行操作。当一个进程产生一个其他进程所需要的结果，它只是将新的数据转储到元组空间。需要数据的进程可以使用模式匹配在元组空间中查找它。

out("job", 999, "abc")

in("job", 1000, ?x) ; blocks because there is no matching tuple
in("job", 999, x:string) ; takes that tuple out of tuple space, assigning 'abc' to x

这引起了关于如何发布持久化数据的问题，以及进程悬停等待元组空间中不存在的键值对时会发生什么情况的问题。此外，元组空间机制对编程模型没有任何限定。使用元组空间的代理可以用各种各样编程模型来编写，这些编程模型对并发语义具有各种实现和解释器。这使得在由许多代理通过元组空间进行交互的应用程序中进行端到端语义的推理变得尤其困难。然而，模型在沟通和协调上的简单性已经引起了广泛的关注，在随后的几十年里，关于元组空间的实现产生了很多。

元组空间概念与actor模型之间的显着区别在于actor模型基本端口的限制。一个actor有一个位置，即它的邮箱，监听世界其他地方的行为。现实中的系统和现实中的系统开发通常要求应用程序需要监听两个或更多的数据源并在它们之间进行协调。例如，Fork-join的程序，会spawn出多个程序对多个数据源请求信息，然后后续的计算过程将这些来自自动化数据源的结果信息流合并，这种算法是人类决策过程中一种常见的想法，应用于诸如从贷款处理，到学术论文的审查。当然，可以安排一个actor在多个actor之间进行协调，然后负责这些独立的数据源的处理。但这在应用程序中引入了开销，并打破了封装，因为参与者必须要知道他们正在被协调。

相比之下，元组空间模型非常适合协调跨多个自动化数据源的计算过程。

移动进程演算的分布式实现

Tomlinson，Lavender和Meredith等人提供了Rosette/ESS中的元组空间模型的实现，作为进行两种模型研究的手段，并比较两种风格所写出来的应用程序。正是在这项工作中，Meredith开始了对移动进程演算的深入研究，并把他作为actor模型和元组空间模型的第三个替代方案。主要需求之一是在具有一个统一的编程模型（如Rosette的actor模型）之间建立桥梁，通过元组空间模型提供的简单但灵活的通信和协调概念，使应用语义的推理变得容易得多。

在下面描述的代码中，方法名使用consume和produce来代替传统的Linda动词 in 和 out 。原因在于，一旦使用了反射法策略，然后使用划定的延续进行细化，这会导致与数据和延续生命周期相关的新的重要观测。

元组空间get语义的Rosette实现
(defRMethod NameSpace (consume ctxt & location)
 ;;; by makng this a reflective method - RMethod - we gain access to the awaiting continuation
 ;;; bound to the formal parameter ctxt
 (letrec [[[channel ptrn] location]
                ;;; the channel and the pattern of incoming messages to look for are destructured and bound
        [subspace (tbl-get chart channel)]
                ;;; the incoming messages associated with the channel are collected in a subtable
                ;;; in this sense we can see that the semantic framework supports a compositional
                ;;; topic/subtopic/subsubtopic/… structuring technique that unifies message passing
                ;;; with content delivery primitives
                ;;; the channel name becomes the topic, and the pattern structure becomes
                ;;; the subtopic tree
                ;;; this also unifies with the URL view of resource access
       [candidates (names subspace)]
       [[extractions remainder]
          (fold candidates
            (proc [e acc k]
                (let [[[hits misses] acc]
                [binding (match? ptrn e)]]
            (if (miss? binding)
                (k [hits [e & misses]])
                (k [[[e binding] & hits] misses])))))]
                  ;;; note that this is generic in the match? and miss? predicates
                  ;;; matching could be unification (as it is in SpecialK) or it could be
                  ;;; a number of other special purpose protocols
                  ;;; the price for this genericity is performance
                  ;;; there is decent research showing that there are hashing disciplines
                  ;;; that could provide a better than reasonable approximation of unification
       [[productions consummation]
            (fold extractions
              (proc [[e binding] acc k]
                (let [[[productions consumers] acc]
               [hit (tbl-get subspace e)]]
                  (if (production? hit)
               (k [[[[e binding] hit] & productions] consumers])
               (k [productions [[e hit] & consumers]])))))]]
                  ;;; this divides the hits into those matches that are data and
                  ;;; those matches that are continuations
                  ;;; and the rest of the code sends data to the awaiting continuation
                  ;;; and appends the continuation to those matches that are currently
                  ;;; data starved
                  ;;; this is a much more fine-grained view of excluded middle

   (seq
     (map productions
       (proc [[[ptrn binding] product]]
            (delete subspace ptrn)))
     (map consummation
          (proc [[ptrn consumers]]
            (tbl-add subspace
            ptrn (reverse [ctxt & (reverse consumers)]))))
     (update!)
     (ctxt-rtn ctxt productions))))
元组空间put语义的Rosette实现
;;; This code is perfectly dual to the consumer code and so all the comments
;;; there apply in the corresponging code sites
(defRMethod NameSpace (produce ctxt & production)
 (letrec [[[channel ptrn product] production]
        [subspace (tbl-get chart channel)]
       [candidates (names subspace)]
       [[extractions remainder]
          (fold candidates
            (proc [e acc k]
                (let [[[hits misses] acc]
                [binding (match? ptrn e)]]
            (if (miss? binding)
                (k [[e & hits] misses])
                (k [hits [e & misses]])))))]
       [[productions consummation]
            (fold extractions
              (proc [[e binding] acc k]
                (let [[[productions consumers] acc]
               [hit (tbl-get subspace e)]]
                  (if (production? hit)
               (k [[[e hit] & productions] consumers])
               (k [productions [[[e binding] hit] & consumers]])))))]]
   (seq
     (map productions
       (proc [[ptrn prod]] (tbl-add subspace ptrn product)))
     (map consummation
       (proc [[[ptrn binding] consumers]]
       (seq
            (delete subspace ptrn)
            (map consumers
              (proc [consumer]
                (send ctxt-rtn consumer [product binding])
                binding)))))
     (update!)
     (ctxt-rtn ctxt product))))

本质上，该问题是，在输入请求满足输出请求后数据和延续这两个中的一个或两个会发生什么。在传统的元组空间和π演算语义中，数据和连续都从仓库中移除。然而，事件发生后，完全有可能将其中一个或两个都留在仓库中。每个独立的选择都会导致不同的编程范式。

Traditional DB operations

移除延续，但留下数据构成一个标准的数据库读取：

 

易失性的-data

易失性的-k

持久化-data

易失性的-k

易失性的-data

持久性的-k

持久化-data

易失性的-k
生产者 put store publish publish with history
消费者 get read subscribe subscribe

Traditional messaging operations

将数据移除的同时将延续保留，组成pub/sub模型中的订阅

 

易失性的-data

易失性的-k

持久化-data

易失性的-k

易失性的-data

持久性的-k

持久化-data

易失性的-k
生产者 put store publish publish with history
消费者 get read subscribe subscribe

Item-level locking in a distributed setting

标准的移动进程演算和元组空间语义将数据和延续都移除

 

易失性的-data

易失性的-k

持久化-data

易失性的-k

易失性的-data

持久性的-k

持久化-data

易失性的-k
生产者 put store publish publish with history
消费者 get read subscribe subscribe

在Tomlinson使用Rosette的反射方法来模拟元组空间语义（见上面的代码）的基础上，Meredith通过线性延续提供了从π演算到元组空间语义的直接编码。这种语义是微软BizTalk的Process Orchestration引擎的核心，微软的XLang可以说是第一个互联网规模的智能合约语言，而它正是由此产生的编程模型。这个模型直接影响到W3C标准，如BEPL和WS-Choreography，并催生了整整一代的业务流程自动化应用和框架。

与Rosette为actor模型带来的改进一样，π演算为应用程序提供了一个特定的本体论，这些应用程序是以通过消息传递信道进行通信的进程概念而构建的。重要的是要注意，进程是通道中的参数，而Meredith使用这个抽象层次为XLang中提供了各种信道类型，包括绑定到微软的MSMQ消息队列、COM对象和许多其他在当时的流行技术的接入点。也许当今互联网最核心的抽象在于，URI提供了一个自然的信道概念，允许通过URI感知通信协议（如http）实现编程模型。同样，就当今的存储地带而言，键值对存储(如nosql数据库)中的键也直接映射到π演算中的通道概念，而Meredith使用这个构想来提供π演算到元组空间语义的编码。

从元组空间到 π演算

π演算赢得了基于消息传递交互来构建的并发计算的核心模型。它在并发和分布式计算中所扮演的角色，就像lambda演算在函数式语言和函数式编程所扮演的一样，给出了计算的基本本质，并将其转化为可以执行计算的语法和语义。给定信道的一些概念，它构建起了一些基本的进程公式，其中前三个是关于I/O的，描述了消息传递的行为。

  • 0 表示惰性或已停止的进程，是模型的基础情况
  • x?( ptrn )P 表示输入看守进程正在监听信道 x ，等待与模式相匹配的消息，然后当接收到该信息后，会接着执行:code:P，其中模式中的所有变量被绑定到消息中对应的值。
  • x!( m ) 表示在信道 x 发送消息 m

接下来的三个表示进程的自然并发情况、信道创建和递归情形。

  • P|Q 表示由两个进程P和Q并行组成的进程，这两个进程是并发执行的。
  • (new x)P 表示一个执行子进程P的进程，在它的上下文中，x被绑定到一个新的信道，不同于所有其他正在被使用的信道
  • (def X( ptrn ) = P)[ m ] 和 X( m ) 表示进程的递归定义和执行

这些基本公式可以用元组空间里面的操作来模拟:

P,Q ::=                     [[-]](-) : π -> Scala =
    0                       { }
    | x?(prtn)P             { val ptrn = T.get([[x]](T)); [[T]](P) }
    | x!(m)                 T.put([[x]], m)
    | P|Q                   spawn{ [[P]](T)  }; spawn{ [[P]](T) }
    | (new x)P              { val x = T.fresh("x"); [[P]](T) }
    | (def X(ptrn) = P)(m)  object X { def apply(ptrn) = { [[P]](T) } }; X(m)
    | X(ptrn)               X(ptrn)

单子结构化的信道抽象

接着Meredith在两个方向上追求特性的提升。它们都与信道抽象有关。两者中的第一个将信道抽象与在反射编程范式中变得如此受欢迎的流抽象相关联。具体而言，很容易证明异步π演算中的信道对应于无限持久化队列。这个队列可以被视为一个流，并且是可以被单子化处理访问的流，就像在响应式编程范式中所做的那样。这为在前面提到的，支持人类决策应用的常见的fork-join并发模式添加了自然语法和语义的优势。

( let [[data (consume ns channel pattern)]] P)

for( data <- ns.consume(channel, pattern) ){ P }

这一点值得更详细的讨论。虽然π演算确实解决了actor模型的主要端口约束，但它并不为fork-join模式提供自然的语法和语义支持。π演算的一些变体，例如连接演算，已经被提出来解决这种困境，但可以说，这些提议深受一些特性纠缠，使得它们不适用于许多分布式和去中心化编程设计模式。同时，通道的单子解释提供了π演算语义中更为集中和基本的重构，这些与模型中所有现有的标志语义相一致，提供了fork-join的自然概念，同时也清晰地映射到响应式编程范式，从而使诸如Apache Spark等开发栈的集成相对简单。

如果我们从编程语言演化的角度来看待这个问题，我们首先看到的语义重构看起来像：

P,Q ::=                     [[-]](-) : π -> Scala =
    0                       { }
    | x?(prtn)P             for( ptrn <- [[x]](T) ){ [[P]](T) }
    | x!(m)                 T.put([[x]], m)
    | P|Q                   spawn{ [[P]](T)  }; spawn{ [[P]](T) }
    | (new x)P              { val x = T.fresh("x"); [[P]](T) }
    | (def X(ptrn) = P)(m)  object X { def apply(ptrn) = { [[P]](T) } }; X(m)
    | X(ptrn)               X(ptrn)

其中for-comprehension是使用延续单子的语法糖。这条成功的解析表明了对解释器中**源**的重构。

P,Q :: = 0
         | for (ptrn <- x)P
         | x!(m)
         | P|Q
         | (new x)P
         | (def X(ptrn) = P)[m]
         | X(ptrn)

这个重构出现在Meredith和Stay关于π演算的高阶范畴论语义的工作 [SM15] 中，之后在rholang设计中加入。需要注意的重要一点是，基于for-comprehension的输入现在可以平滑地扩展到来自多个源的输入，在继续被调用之前，每个或所有这些输入都必须通过一个过滤器过滤。

\[for( ptrn_{1} \leftarrow x_{1}; \dotso; ptrn_{n} \leftarrow x_{n} if cond )P\]

使用for-comprehension允许单子化使用的信道可以使用输入守护语义来规范参数，因此特定的join语义可以多形地提供。这个意义怎么强调都不为过。特别是:

  • 与join与递归不可分割地绑定在一起的join演算不同。单子守卫输入允许匿名的、一次性合并，这在人类决策过程中是非常标准的fork-join模式。
  • 它提供了用于模拟Kiselyov的LogicT单子转换器的适当配置。搜索每个输入源直到找到满足条件的输入元组，对每个输入源中的发散很敏感。更重要的是，公平的交叉是一个描述交织策略的编程算法，它对于可靠，可用和高性能的服务至关重要。这是LogicT的实际导入和在机器部署中的正确设置。
  • 我们现在有一个嵌套事务的语法形式。具体来说：P 只能在满足与输入源状态变更和条件相符的上下文中运行。此外， P 可以是又一个输入守护进程。因此程序员或程序分析器可以 依照句法地 检测事务的边界。这对涉及金融和其他关键任务的事务的合约至关重要。

前RChain智能合约模型

正如rholang设计中所规定的的那样，这是一个用于智能合约的RChain模型的前身。它为构造合约提供了迄今为止最丰富的通信原语集合，这是由理论和工业规模的开发和部署所共同推动的。然而，整套合约原语适合在一条线上。从基于PoW的区块链到EVM，在这个领域没有一个单一设计方案能够承受这个方案所经受的质量保证压力。具体来说，这个方案在所有使用Rosette、Tuplespaces和BizTalk的经验中都有所取舍，并将它们归结为一个单一的设计方案，该方案满足所有这些场景中发现的迫切需求。它只有七个原语，并且与当前市场的主要编程范例相符。然而，作为来自rholang规范的例子，以及用行为类型显示来防止 DAO bug的研究，现有区块链技术中可表达的全部合约范围都在此模型中被紧凑地表达。

然而, 正如在 rholang 设计中所看到的, 这只是故事的开始。为了理解在开发引入的这些概念，需要一些背景知识。在过去的20年里, 一场革命已在计算机科学和逻辑学中悄然发生。许多年来人们都知道, 对于函数式编程模型中的小而增长的代码片段中，类型对应于命题, 证明对应于编程。如果这种对应，五花八门地被称为类型即命题范式或Curry-Howard 同构, 可以被用来涵盖模型中的一个重要而实用的部分, 它对软件开发有着深远的影响。至少, 这意味着, 类型检查程序的标准实践与程序证明在执行过程中拥有一致的某些属性。与Curry-Howard 同构所覆盖的初始片段相关的属性，主要与相关形式的函数中输入输出数据有关, 通过编译时检查，有效地消除了这类内存访问违规的行为.

加上J-Y Girard的线性逻辑的发明，我们可以看到命题即类型范式的一个具体扩展。通过线性逻辑，我们看到了范围涵盖远远超过严格串行的函数式模型。类型检查所提供的作用范围从属性证明扩展到并发环境下的协议一致性检查。接着，Caires和Cardelli发现了空间逻辑，其进一步扩展了作用范围，包括程序内部形态的结构化属性。在这些发现的基础上，Stay和Meredith确定了一个算法，即LADL算法，来生成类型系统，带来了一系列从安全性、可用性到安全性质的结构化和行为化的特性。通过应用Stay和Meredith开发的LADL算法，这里介绍的无类型的合约原语模型被赋予了一个完备的类型系统，它足以提供一些编译时守护，保证处理金融财产和其他敏感内容的关键任务所要求的关键的安全性和可用性。一个在编译时守护的简单例子是足以在编译时去发现和防止在The DAO事件中引起5千万美元损失的bug。

SpecialK

信道语义的单子处理就是在SpecialK栈研究中的亮点。首先，它将信道访问映射到for-comprehension风格的单子结构化的响应式编程。其次，它将信道同时映射到与整个节点相关的本地存储，以及节点之间的基于AMQP服务提供商的通信基础设施中的队列。这提供了内容传送网络的基础，该网络可以在通信节点的网络上实现，其与基于π演算的编程模型集成。特别的，从以上代码的注释中可以看出，信道加模式的单子化对待统一了消息传递和内容交付编程范式。具体来说，信道可以被看作是主题提供者，而模式为消息流提供了嵌套的子主题结构。这整合了所有的标准内容寻址机制（例如URL + http），同时提供了一个查询模型。详细信息请参见下面的章节。

从SpecialK到RChain

正如我们将看到的，RChain合约模型继承了SpecialK对待内容交付的所有优点。但是，SpecialK所实现的前RChain合约模型是以嵌入领域专用语言作为Scala的一组类库，而RChain则将该模型实现为全面的编程语言，运行在区块链上复制的虚拟机上，极具以太坊的架构和设计理念。该选择解决了第一个Synereo白皮书中指出的几个Synereo 版本1中体系结构的缺点。特别是避免了为运转注意力经济学的财务能力而必须支付给其他区块链费用从而在注意力经济系统合约上遭受了许多基于经济上的攻击的问题。它还解决了与SpecialK语义中心的Scala有限的延续库有关的SpecialK技术栈中的技术债务问题，同时显着提高了其支持的智能合约的能力。

Rho演算

尽管单子抽象提供了在信道上用于内容流流动的结构，但更基本的观察提供了支持工业级元编程的必要结构。我们知道几乎所有的主要编程语言都支持元级编程。原因很简单，程序员不写程序，程序编写程序，程序员编写写程序的程序。这就是为何能在互联网规模上完成如此巨大的编程任务的原因，使用计算机尽可能地自动完成任务。从文本编辑器到编译器，到代码生成器，到AI，这些都是生产出互联网规模上运行的服务代码的基本生态系统的一部分。

从更狭隘的角度来看，观察到Scala在语言设计之后艰难的添加元编程特性的教训是很有用的。在Scala中的反射甚至在好几年间都不是线程安全。可以说，这次教训，再加上类型系统的问题，都是其设计之初不定的编译器和新语言设计的原因。这些以及其他经过深入探索的努力清楚地表明，从编程语言的核心设计开始时就提供元编程模型原语，对其寿命和实际应用都是很重要的。简而言之，一个实际上支持元编程的设计在想要获得与Java，C#或者Scala等同的生产完备特性的项目中更具成本效应。

从Rosette对元编程设计的总体承诺中得到一个线索，高阶反射π(r-eflective h-igher o-rder π-calculus,简写为rho-演算)，引入反射作为其核心模型的一部分。它提供了两个基本原语，反射和修改，允许正在进行的计算将进程转变为一个通道，将一个从进程修改后得到的信通转变回它所修改的进程。该模型在过去的十年间经历过多次同行评审。原型系统已有将近十年的历史，清晰得演示了其健壮性。它采用总数达到了9个的合约构建原语集合，远远少于以太坊智能合约语言Solidity，然而这个模型比Solidity更具表达能力。特别是基于Solidity的智能合约不享有内在并发。

资源地址、内容传递、查询和分片的启示

在深入研究模型与资源寻址，内容交付，查询和分片的关系之前，让我们先快速地看一下基于路径的寻址。请注意，路径并不总是能够合并。比如`/a/b/c`和`/a/b/d`。这些不会自然地合并成一条路径。然而，每一条路径都是一棵树，而这些树合并了一棵新的树`/a/b/c+d`。换句话说，树为资源寻址提供了一个可组合的模型。这也可以作为查询模型。要看到这个声明的后半部分，让我们用这种形式重写我们的树：

\[/a/b/c \mapsto a(b(c))\]
\[/a/b/c+d \mapsto a(b(c, d))\]

接着注意到统一可作为匹配和分解树的一种自然的算法，基于统一的匹配和分解为查询提供了基础。

根据这个讨论，我们来看看π演算中的I/O行为：

input: x?(a(b(X,Y)))P ↦ for(a(b(X,Y)) <- x)P
output: x!(a(b(c,d)))

当这些被置于并发执行中，我们有

for(a(b(X,Y)) <- x)P | x!(a(b(c,d)))

它被求解为 P{ X := c, Y := d }，也就是说，我们在某个环境中开始执行 P，在该环境中 X 被绑定为 c ， Y 被绑定为 d 。我们用符号写下求解过程:

for(a(b(X,Y)) <- x)P | x!(a(b(c,d))) → P{ X := c, Y := d }

这引起了一个非常自然的解释：

  • 输出将资源置于对应位置：
x!(a(b(c,d)))
  • 输入查询在位置上的资源
for(a(b(X,Y)) <- x)P

这只是故事的开始。通过反射，我们允许信道的名称自身也是结构，比如上面例子中的x。这允许我们通过命名空间来细分存储资源的空间。命名空间是从安全到分片的各种特性的基础。

RChain智能合约模型

现在我们对RChain智能合约模型已经有一个完整的描述。它编纂在rholang的设计中。它从反射所得到的特性数量，从宏到协议适配器，足以值得引起重视。然而，退一步说，我们将看到

  • 它有一个健全和正确的类型系统
  • 一份形式化规范
  • 将形式化规范渲染为能工作的代码
  • 它决定了一份构建时正确的虚拟机的形式化规范
  • 这决定了一个清晰的编译策略，一系列构建时正确的到虚拟机字节码的转换规则，该虚拟机已经被现场测试了达20年之久。

现在，以这个出发点和以太坊中Solidity和EVM的当前状态做比较。如果目的是产生一个可信的时间线，通过它我们可以得到一个区块链节点网络，在其上面运行形式验证、构建时正确的代码，那么与以太坊网络相比，这种方法也有明显的优势。显然，有足够的市场兴趣来支持这两种选项的发展。

[SM15]Mike Stay and Lucius Gregory Meredith. Higher category models of the pi-calculus. CoRR, 2015. URL: http://arxiv.org/abs/1504.04311.

进入区块链

用一句简单的话来解释，区块链是一项去中心化的多冗余技术。状态可以备份在多个网络节点，并且不需要任何中心化的机构来管理备份。多冗余机制和基于经济学的安全之间微妙的相互作用有时候使多冗余本身的基本价值被模糊化。这个机制下的多备份已经成为一个高影响力的价值主张。以太坊的见证提议，它的精髓是在区块链上备份虚拟机的状态，而不是账本的状态。这不仅提供了一个智能合约系统，同时还有全网公开、无法被关闭的计算资源。

不仅仅是华尔街引起了注意，亚马逊的AWS，Google的云服务，Microsoft的Azure，所有这些业务深深地被以太坊所影响。事实上，账本（多冗余状态的经济学说法）可以被用作一个经济上的安全实体，可以抗衡基于全球计算资源的DoS攻击，加强了协议的健壮性。它也从本质上地改变了使用这些服务的生态系统。

云服务基础设施提供商的价值主张非常依赖于微交易，这些微交易与计算资源的使用息息相关。以太坊在最底层的执行和存储中集成了微交易，在一定程度上对系统的安全至关重要。它比当前的云解决方案更好、更优雅。更重要地是，它被开源地实现了。具有这种新兴形式的一些特点的革命之一，离我们最近的，还是由互联网导致的通信方式的转移。电话业务提供商知道，互联网将改变人们的通讯方式，从而不得不争先恐后地适应这样的场景——超过半数的长距离通讯都将趋于使用像Skype, zoom和Google Hangouts这样的免费服务。云基础服务提供商，以及整个跑在云上的互联网络，都将不得不转变成一个精致的加密货币市场。它在最底层了全球可用的、公开的计算资源。

Casper

在2万英尺的高度上看，这是一个深奥的想法，但在生产环境系统执行的角度上看，它突出了几个要求。首先，它需要一个不同的备份技术。为了使得以太坊的想法在互联网规模的生产环境系统上仍然可行，这项促使以太坊协议诞生的技术是我们首先需要重新思考的。工作量证明过于消耗能源。社区对此的争议很大，并且以太坊开发者社区的所有主要利益相关方都在积极参与这些讨论。取而代之地，一个被称为Casper的新的“付费参与”算法，正在由一个小团队负责进行开发，成员包括Buterin, Zamfir和Meredith。

下注区块VS下注提案

Casper共识算法的核心是参与复制协议验证者的一个消息交换周期。在消息交换周期中各个验证者最终能够趋于收敛达成共识。Casper协议设计特点是共识周期，有时被称为博彩周期与验证者正在使用的共识算法的状态无关。它可以用来在单个布尔值上（例如硬币翻转的结果）达成共识，或者像状态机那样复杂地达成共识。在本文中进一步阐明了共识的状态该如何封装。具体而言，区块链这个名词指代的就是一系列状态被封装成区块并串联成链式的结构。因此，对于一个共识周期而言，需要达成共识的目标就是一个区块。通俗一点来说，验证者在一轮验证的过程中相互交换信息，使得对于区块链上下一个区块的内容达成共识。

在这一章节中，我们将逐步自然地从PoW算法切换到Casper算法上。但是值得注意的是，共识周期的长短直接限制了区块产生的速率。由于交易是被封装在区块当中的，因为我们可以用区块产生的速度大致估量系统处理交易的速率。Vitalik的试验性Casper实现已经说明采用casper算法，区块链的执行效率比采用PoW算法要提高许多。但是Casper算法最终的目的是让交易处理的吞吐量达到4w笔每秒，基本接近于金融网络的处理速率，例如Visa。为了实现如此高的交易处理速率，我们做了两个基本的观察。第一个是一个生活的常识：绝大多数交易都是相互独立的，在上海的一名用户发起一笔交易去购买一辆汽车与在西雅图的一名用户发起一笔交易去购买一杯咖啡是完全独立的。多个并发交易的隔离性需要遵循与多车道高速公路一样的原则，在高速公路上汽车不变道就是我们所说的独立性。按照这个比喻，我们将一个区块比做一条有多条车道的高速公路，期间的汽车几乎没有变道行为。

另一个观察是更微观的，它与可编程的数据压缩有关。有一个贴切的比喻来自于计算机图形学。对于许多图像，例如蕨类图像，绘制图像有两种根本不同的方式，其中一种方式是由渲染器提供与像素对应的大量数据点来进行图形绘制。据推测，这个数据集是通过数据采样获得的，例如可能通过扫描实际的蕨类植物获取。另外一种绘制方式是通过获取一个与蕨类植物相关联的算法模型，通过这个算法模型计算产生一系列的像素点来完成图形绘制。从这个角度上来看，这个算法模型其实代表了一种数据的压缩形式。相较于一份数据量很大的像素数据传递给渲染器进行渲染，使用算法模型生成像素数据来绘制图形的效率显然会高很多。

因此，我们可以对交易数据采用类似的方式压缩成一个提案。Stay和Meredith的LADL算法精确地描述了如何绑定一个提案与一批交易之间的映射关系，剩下的部分就是如何建立不同验证者与他们提出的提案之间的映射关系。具体来说，假设验证者Abed正在检测网络产生的一部分交易，而验证者Troy正在检测网络产生的另外一部分交易。假设Abed和Troy使用提案来完成这些交易信息的交互，那我们如果保证不同的提案所包含的交易信息是一致的呢？这就是由LADL算法提出的提案具备压缩交易信息的能力。

通过逻辑层次的推理，可以确定一组提案是否一致。在LADL算法中提出，两组提案当且仅当它们的组合（比如并集）（即它们表示的集合）的含义不是空的，则这两组提案是相同的；当他们的组合是空的时候，则表明这两组提案不是一致的。从这个角度来看，验证者在Casper的验证周期中从提案的最大一致性性子集中挑选出一个作为验证区块。一旦共识周期开始收敛，被确定的区块就会以一致的提案集合的形式产生，然后扩展到一个更大的交易集合，就像蕨类植物从由模式算法产生一些列的像素点绘制出图像一样。

RChain模型中从数据存储到区块存储

基于对内容存储和查询部分的观察，我们可以将JSON的直接表示形式细化为rholang的相关语法片段（见下图RHOCore部分）。

_images/rhocore-1.png

RSON: RChain数据表示形式

这说明了一个关于数据存储的元级别的观点。这种数据格式的存储和访问语义，与自托管的序列化格式是一致的，并用于将状态渲染到磁盘或电线中。实际上，无论编程者将什么序列化成JSON并存入像mongodb这样的数据库，它们可以呈现为rholang语法片段中的同构表达式的形式。它的执行将会影响存储。此外，这种格式的复杂度与JSON相差无几。然而，rholang的空间类型为一个类型提供了直接数据验证机制，用于序列化与反序列化数据。

然而，这仅仅使用了输出端（生产者）。通过包含输入端（消费者），我们也可以提供一个正确、高效的区块结构表示。首先注意输入端的保留格式。这个持续过程被确保是在观测到值的通道上下文中执行的。

_images/rhocore-2.png

RSON: RChain数据表示形式

这恰恰是一个交易上的保证。从此，我们可以创建一个恰好与编程语法相关的正确的区块结构表现形式。

_images/rhocore-3.png

RSON: RChain数据表示形式

区块的表现形式也直接嵌入了RHOCore中。

Sharding（分片）

另一个使得以太坊提案得以实践的要求是摆脱全网的电脑设备。以太坊真正需要的是一个虚拟机集群，每个虚拟机服务于一个客户端过程的分片，而不是只在区块链上运行单个虚拟机。在某种意义上，这标志着我们重新回到了Rosetee/ESS设计被提出时，互联网最初的愿景。然而这里面有一些关键的不同点。首先，每个虚拟机的状态是被存储在区块链上的。其次，尽管每个虚拟机都是来自同一个部分，但仍然需要一个规则来控制它们的交互。具体来说，尽管它们都是同一个VM的有效副本，每个虚拟机操作特定的虚拟地址空间，或者是我们调用它时所处的命名空间。当它们在操作同一个命名空间时，我们已经确保了每个副本的状态都是强一致的。这是共识算法的目的。

在以太坊的虚拟机设计中，一个很关键的成分缺陷在于虚拟机之间协调某一命名空间下组合账户的使用。而主要的原因是：它并不是组合的。另一个核心变化是，类似Rosette/SEE的设计，RChain的虚拟机被设计成在根本上是并行的。RChain的智能合约，也跟Rosette/ESS中的参与者一样，在执行期享受着细粒度的并行性。以下两个关键因素使得这种并行性在金融交易中很安全。

并行性、非确定性与安全性

在分布式环境中，有两种使得细粒度并行执行变得安全的机制，它们根本上是运行在不同层的。一个是在运行期，另一个是在编译期。运行期是比较好理解的。而合约相关的并行执行所引起的不确定性，总是以下面的竞争形式出现：

  • 两个输出竞争服务于同一个输入请求
x!( v1 ) | for( y <- x )P | x!( v2 )
  • 两个输入请求竞争同一个输出
for( y <- x )P1 | x!( v ) | for( y <- x )P2

这种竞争要么出现在合约内部的计算，要么在合约与其运行环境之间。无论是哪一种可能情况，为了让合约能继续运行，我们需要一个消除的手段，其中之一是交易。这就是前文所述的交易边界的意义。因此，这些交易正是Casper共识算法想要复制的。所以，尽管会出现内部的不确定性，但复制的状态是确定性的。在同一个分片上的所有节点都会看到同样的状态。

但我们依然可能敲下错误的代码。抛开EVM的确定性不谈，DAO的bug的出现，说明了在调度有关维护新用户请求的状态更新上存在一些不公正；而且，当它以rholang合约的形式表示时，会产生多余的竞争条件。那就是，考虑到合约真正想要表达的语意，合约中所允许的一定程度的不确定性存在着安全隐患。在大多数实际情况下，这些问题可以被检测到，并且在编译期使用rholang的空间行为类型来预防。在攻击DAO所找到的bug的特例中便是如此。

虚拟机是什么？

让我们短暂回顾一下，什么是虚拟机。每个虚拟机相当于一张表格。表格列出了一个交易的集合。这些交易按如下形式：

<byte code, machine state> -> <byte code’, machine state’>

交易明确指出了一个在给定状态下的机器运行一串特殊字节码指令后会发生什么：

rosette> (code-dump (compile '(+ 1 2)))
litvec:
   0: {RequestExpr}
codevec:
   0: alloc 2
   1: lit 1, arg[0]
   2: lit 2, arg[1]
   3: xfer global[+],trgt
   5: xmit/nxt 2
rosette>

上面的例子包含往一个寄存器中加载一个字面量，或是取出寄存器的值并求和。寄存器、堆、栈，这些都是组成机器状态的一些例子。在RhoVM中，最重要的状态转移是关于I/O的：

for( y <- x )P | x!( Q ) -> P{ @Q / y }

这个转移表达式的意思是，当虚拟机中的一个输入守卫线程正在等待x上的输入，与一个正在提交输出到x上的另一个线程并行运行，这时数据会通过x传递，最终在持续过程P中与变量y绑定。这是一个包含了很多低层级状态变化的更高层级的状态转移。理解这个很重要。这是因为x与多种通道绑定，从本地存储的表格，到AMQP队列，再到tcp/ip的套接字。每个通道都有一种与更高层转移规则进行平滑互操作的自然语义。高层转换规则和不同通道语义之间的互操作，恰好是元组空间的语义所能提供的。

然而，在这次讨论中，对于给定虚拟机实例的识别是很重要的。换句话说，一个虚拟机表格的副本，加上一个特定的机器状态配置，可以被限制在特定命名集合上进行操作。这个命名集合（也称为命名空间），可以编程的方式指定，因此也不一定是有限的。

在这个架构中，一个分片大致相当于一个命名空间，一个机器实力以及部署在虚拟机状态所存储的网络上的RChain节点。我们只敢说“大致”，因为分片也可能由分片组成，这意味着给定的、在命名空间的子空间中复制机器状态的分片中，存在着节点的子群。同样地，因为虚拟机只有在他们有重合的命名空间时才可以互操作，多个分片可以存储在相同的节点上。这提供了可用性与安全性，因为对于使用虚拟机、节点和命名空间之间的关系，以及寻找节点的物理地址与命名空间的相关性，这些可以根据需要在计算量上做得足够困难。

结论以及将来的工作

我们简要地回顾了一下这个技术，这个技术可以将移动处理算法有效地呈现为分布式可编程虚拟机网络的编程模型和执行引擎。 我们已经逐步地描述了这个过程，通过存储虚拟机的状态以在区块链上实现这一特点。我们已经提供了这种方法的背景和设计原理，能够实现基于区块链的公共经济、计算资源的基础设施。

文献

[AH87]Gul Agha and Carl Hewitt. Actors: A conceptual foundation for concurrent object-oriented programming. In Research Directions in Object-Oriented Programming, pages 49–74. 1987.
[Cai04]Lu’ıs Caires. Behavioral and spatial observations in a logic for the pi-calculus. In Foundations of Software Science and Computation Structures, 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings, 72–89. 2004. URL: http://dx.doi.org/10.1007/978-3-540-24727-2_7, doi:10.1007/978-3-540-24727-2_7.
[FG00]Cédric Fournet and Georges Gonthier. The join calculus: A language for distributed mobile programming. In Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures, 268–332. 2000. URL: http://dx.doi.org/10.1007/3-540-45699-6_6, doi:10.1007/3-540-45699-6_6.
[GZ97]David Gelernter and Lenore D. Zuck. On what linda is: formal description of linda as a reactive system. In Coordination Languages and Models, Second International Conference, COORDINATION ‘97, Berlin, Germany, September 1-3, 1997, Proceedings, 187–204. 1997. URL: http://dx.doi.org/10.1007/3-540-63383-9_81, doi:10.1007/3-540-63383-9_81.
[HWT14]Jiansen He, Philip Wadler, and Philip W. Trinder. Typecasting actors: from akka to takka. In Proceedings of the Fifth Annual Scala Workshop, SCALA@ECOOP 2014, Uppsala, Sweden, July 28-29, 2014, 23–33. 2014. URL: http://doi.acm.org/10.1145/2637647.2637651, doi:10.1145/2637647.2637651.
[KSFS05]Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry. Backtracking, interleaving, and terminating monad transformers: (functional pearl). In Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, Tallinn, Estonia, September 26-28, 2005, 192–203. 2005. URL: http://doi.acm.org/10.1145/1086365.1086390, doi:10.1145/1086365.1086390.
[MB03]Greg Meredith and Steve Bjorg. Contracts and types. Commun. ACM, 46(10):41–47, 2003. URL: http://doi.acm.org/10.1145/944217.944236, doi:10.1145/944217.944236.
[MR05a]L. Gregory Meredith and Matthias Radestock. A reflective higher-order calculus. Electr. Notes Theor. Comput. Sci., 141(5):49–67, 2005. URL: http://dx.doi.org/10.1016/j.entcs.2005.05.016, doi:10.1016/j.entcs.2005.05.016.
[MR05b]L. Gregory Meredith and Matthias Radestock. Namespace logic: A logic for a reflective higher-order calculus. In Trustworthy Global Computing, International Symposium, TGC 2005, Edinburgh, UK, April 7-9, 2005, Revised Selected Papers, 353–369. 2005. URL: http://dx.doi.org/10.1007/11580850_19, doi:10.1007/11580850_19.
[Mer15]Lucius Gregory Meredith. Linear types can change the blockchain. CoRR, 2015. URL: http://arxiv.org/abs/1506.01001.
[MSD13]Lucius Gregory Meredith, Mike Stay, and Sophia Drossopoulou. Policy as types. CoRR, 2013. URL: http://arxiv.org/abs/1307.7766.
[Mil92]Robin Milner. The polyadic pi-calculus (abstract). In CONCUR ‘92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings, 1. 1992. URL: http://dx.doi.org/10.1007/BFb0084778, doi:10.1007/BFb0084778.
[SMTA95]Munindar P. Singh, Greg Meredith, Christine Tomlinson, and Paul C. Attie. An event algebra for specifying and scheduling workflows. In Database Systems for Advanced Applications ‘95, Proceedings of the 4th International Conference on Database Systems for Advanced Applications (DASFAA), Singapore, April 11-13, 1995, 53–60. 1995.
[SM15]Mike Stay and Lucius Gregory Meredith. Higher category models of the pi-calculus. CoRR, 2015. URL: http://arxiv.org/abs/1504.04311.
[SM16]Mike Stay and Lucius Gregory Meredith. Logic as a distributive law. CoRR, 2016. URL: http://arxiv.org/abs/1610.02247.
[TKS+89]Chris Tomlinson, Won Kim, Mark Scheevel, Vineet Singh, B. Will, and Gul Agha. Rosette: an object-oriented concurrent systems architecture. SIGPLAN Notices, 24(4):91–93, 1989. URL: http://doi.acm.org/10.1145/67387.67410, doi:10.1145/67387.67410.
[TCMW93]Christine Tomlinson, Philip Cannata, Greg Meredith, and Darrell Woelk. The extensible services switch in carnot. IEEE P&DT, 1(2):16–20, 1993. URL: http://dx.doi.org/10.1109/88.218171, doi:10.1109/88.218171.
[WAC+93]Darrell Woelk, Paul C. Attie, Philip Cannata, Greg Meredith, Amit P. Sheth, Munindar P. Singh, and Christine Tomlinson. Task scheduling using intertask dependencies in carot. In Proceedings of the 1993 ACM SIGMOD International Conference on Management of Data, Washington, D.C., May 26-28, 1993., 491–494. 1993. URL: http://doi.acm.org/10.1145/170035.170150, doi:10.1145/170035.170150.