执行模型

概论

每一个 Rho虚拟机 (RhoVM)实例都维护着一个环境,该环境重复应用底层Rho演算归约规则于持久性键值数据库中的元素,这些规则在高级Rholang合约语言中表达 [1]。 RhoVM的“状态”类似于区块链的状态。

../_images/execution_storage.png

图 - RhoVM作为联排式键值存储和执行引擎

合约的执行会影响RhoVM实例的 环境状态 。在这种情况下,所谓的“环境”不仅指的是执行环境,也包括键值结构的配置。环境和状态分别是名称到内存中的位置以及内存中的位置到值的映射。变量直接引用内存中的位置,这意味着环境相当于命名到变量的映射。程序通常在运行时修改这些关联中的一个或两个。环境的改变伴随着Rholang的词法作用域规则发生,它的值可能是简单或复杂,比如原始值或完整程序。

../_images/bindings_diagram.png

图 — 从名称到值的两阶段绑定

RhoVM针对键值数据库操作。RhoVM的状态变化是通过修改键映射到值关系的操作来实现的 因为像Rholang一样,RhoVM是从Rho演算计算模型中衍生的,那么操作就是底层的rho演算归约规则。卓有成效地,被称为“COMM”的归约规则是一种替代方案,它定义了如果在一个键上观察到新值,则要执行 P。键类似于一个名字,在该名字中它引用内存中持有将被替换的值的地址。在下面的例子中,key 是一个键, val 是被替换的值:

for ( val <- key )P | key! ( @Q ) -> P { @Q/val }

除了共识之外,这就是在区块链上存储合约的并发协议的计算模型。 在某个线程上,输出进程 key!,将合约 @Q 的代码存储在由 key 指示的位置。在另一个并发运行的线程上,输入进程 for ( val <- key )P 等待一个新的 val 出现在 key 上。 当在 key 上出现一些 val 时,在这种情况下, @QP 将在一个环境中被执行,在该环境中,出现的每个 val 都将被替换为 @Q。该操作修改了 key 所引用的值,比如说,key 先前映射到一般的 val, 而现在映射到合约 @Q 的代码,有资格作为RhoVM的状态转换的归约。

key 上的输入和输出进程的同步是通过触发RhoVM的状态转换的事件来实现。乍一看,将合约 @Q 存储到由 key 所表示的位置的输出进程,本身构成一个状态转换。但是,Rho演算归约语义要求具有 可观测性。对于任何未来将发生的计算 P,归约规则要求输入进程 for ( val <- key) P观察到key 上的赋值。这是因为只有输入项定义未来的计算,也就是说输出项本身在计算上是不重要的。 因此,直到输入和输出项在 key 上同步之后,才会出现 可观察 的状态转换。这个可观测性要求在编译时被强制执行,以防止通过重复调用输出 key!(@Q) 的DDoS攻击。

已经证明,将rho演算归约规则应用于键值数据存储的数据元素上,构成了RhoVM实例上的状态转换。但是,其目的是为了验证和维护实例上所执行的每个合约指定的所有状态转换。这意味着键值数据存储的配置历史记录必须通过修改来维护,因此它是一个可持久化的数据结构。 所以,每个key必须映射到在该位置发生的已验证的归约历史记录:

../_images/transaction_history.png

图 - 内存中某个位置的归约/转换历史

每个键映射到一个归约列表,它实际上是某个地址的“事务历史”。 事务 { for(val1 <- keyn).P1 | keyn!(@Q1), , for(valn <- keyn).Pn | keyn!(@Qn) } -> { P1{@Q1/val1}, , Pn{@Qn/valn} } 的历史意味着合约 @Q 已经做了的修改,其中 @Qn 是仓库中的最近版本。认识到这个方案是RChain平台上的最顶层事务是非常重要的。传递的消息本身就是合约,这通常发生在客户系统或系统间交互中。 但是,每个合约 @Q 本身也可以在更简单的值上执行许多底层事务。

在事务/归约应用之后,就要达成共识。共识验证在 keyn 上的事务历史,{ for(val1 <- keyn).P1 | keyn!(@Q1) for(valn <- keyn).Pn | keyn!(@Qn) } ,在所有运行RhoVM实例的节点上一致性地复制。一旦事务历史被验证,最近的事务就被添加到事务历史中。 当事务被提交到这些位置时,相同的共识协议会应用到一系列的键 { key1 -> val1 keyn -> valn }

拓展一下,事务块表示已经应用到持久化键值存储中元素的归约集合,而事务历史表示一个Rho虚拟机实例的状态配置和转换的可验证快照。请注意,当且仅当节点上提出冲突的归约历史时,共识算法才会被应用。

总结:

  1. RhoVM虚拟机由Rholang表达的Rho演算归约规则,以及一个持久化的键值数据存储组成。
  2. .Rho演算归约规则将一个键的值替换为另一个值,其中一个命名频道对应于一个键,并且值可以是简单或复杂的。
  3. 替换就是事务,表现为存储在键中的字节码的差异。这些字节码差异在所有运行该RhoVM实例的结点上的精确复制,是通过共识算法验证的。
[1]RhoVM“执行环境”之后将作为“Rosette VM”引入。选择使用Rosette虚拟机的原因取决于两个因素。首先,Rosette系统已经在生成环境中应用了超过20年。 其次,Rosette VM的内存模型,计算模型和运行时系统为RhoVM所需的并发提供了支持。RChain已经承诺将以Scala语言对Rosette VM进行现代化的重新实现,以作为最初的RhoVM执行环境。

可扩展性简介

从传统软件平台的角度来看,“并发”虚拟机实例的概念是多余的。虚拟机实例都被假设为独立运行。因而,不存在所谓的“全局”的RhoVM虚拟机。相反,在任意给定的时刻,存在多路在跨网络的结点上独立运行的RhoVM,各自在相关的分片(即我们已经提到的命名空间)上执行和验证交易。

这个设计选择形成了RChain平台上的系统级并发,而指令级的并发由Rholang提供。 因此,当本文引用RhoVM的单个实例时,都假定有多路RhoVM实例同时在不同的命名空间执行不同的合约集合。

执行环境

Rosette是什么?

Rosette是一种反射式,面向对象的语言,通过actor语义实现并发。Rosette系统(包括Rosette虚拟机)在1994年已经部署到生成环境中,应用在自动取款机上。 由于Rosette展示出来的可靠性,RChain Cooperative已经承诺会在Scala(针对JVM)完成Rosette VM彻底的重新实现。 这样做有两个主要的好处。 首先,Rosette语言满足Rholang中表达的指令级并发语义。 其次,Rosette VM被有意设计成支持在任意数量的处理器上运行的多计算机(分布式)系统。 有关更多信息,请参阅 Mobile Process Calculi for Programming the Blockchain

模型校验与理论证明

在RhoVM和其他潜在的上游合约语言中,有许多技术和检查会被应用在编译时和运行时。这些有助于解决让诸如开发者和系统本身,能够提早知道类型良好的合约将终止的需求。 形式化验证将通过模型检查(如SLMC)和理论证明(如Pro Verif)来确保端到端的正确性。此外,这些相同的检查也可以运行时应用,当新提出组装的合约被运行的时候。

发现服务

一个先进的发现特性将最终被实现,从而能够从其他合约中搜索兼容的合约,并合并成一个新的复合合约。通过形式化验证技术,新合约的作者可以得到保证,当工作合约被合并在一起时执行时,与单独合约执行的效果相同。

编译

为了允许客户端在RhoVM上执行合约,RChain开发了一个以Rholang源代码为起点的编译器流水线。 Rholang源代码首先经过转译,变成Rosette源代码。经过分析,Rosette源代码被编译成一个Rosette中间状态(IRs),它将被优化。从Rosette IR中,Rosette字节码被合成并传递给VM用于本地执行。编译流水线中的每个转换步骤要么是可证明正确的,要么在生产系统中经过了商业测试,或者两者兼而有之。这个流水线如下图所示:

../_images/compilation_strategy.png

图 - RChain编译策略

  1. 分析:从Rholang源代码或者编译到Rholang的另一个智能合约语言,这一步包括:

    1. 计算复杂度分析
    2. 注入速率限制机制的代码
    3. 事务语义的形式化验证
    4. 解语法糖
    5. 等价函数的简化
  2. 转译 :从Rholang的源代码,编译器:

    1. 执行从Rholang到Rosette源代码的源代码到源代码的转换。
  3. 分析 :从Rosette源代码,编译器执行:

    1. 依照Rosette语法进行词法、语法和语义分析,构建AST; 和
    2. 合称为Rosette中间表示
  4. 优化:从Rosette 中间表示(IR),编译器:

    1. 通过冗余消除,子表达消除,无用代码消除,常量折叠,变量推理和抢断简化来优化IR
    2. 合成由Rosette VM执行的字节码

限速机制

The compilation pipeline will implement a rate-limiting mechanism that is related to some calculation of processing, memory, storage, and bandwidth resources. Because the rho-calculus reduction rule is the atomic unit of computation on the RChain platform, the calculation of computation complexity is necessarily correlated to the amount of reductions performed per contract. This mechanism is needed in order to recover costs for the hardware and related operations. Although Ethereum (Gas) has similar needs, the mechanisms are different. Specifically, the metering will not be done at the VM level, but will be injected in the contract code during the analysis phase of compilation. For more details visit the `developer wiki`_. Compiler work can be seen on GitHub.