Reversible Communicating Processes
Reversible Communicating Processes
复制标题
DOI：
10.4204/eptcs.203.4
复制
发表时间：
2016-01-01
影响因子：
--
通讯作者：
Sabry, Amr
中科院分区：
文献类型：
--
作者：
Brown, Geoffrey;Sabry, Amr
可逆分布式程序具有中止非生产性计算路径和回溯的能力，同时取消在中止的路径中发生的通信。虽然人们很自然地认为可逆性意味着完全状态恢复(就像传统的回滚恢复协议一样)，但一个有趣的替代方案是将回溯与本地状态恢复分开。例如，这种模型可以用来从嵌套的可补偿事务中创建复杂的事务，其中程序员提供的补偿定义了“展开”事务所需的工作。可逆的分布式计算在理论上得到了相当大的关注，但在实践中几乎没有减少；支持可逆性的少数已发布的语言实现依赖于高度的中央控制。本文的目的是证明一种实用的可逆分布式语言能够以完全分布式的方式高效地实现。我们讨论了一种嵌入在Scala中的支持CSP风格的同步通信的语言。虽然这种语言为本文中描述的工作提供了动机，但我们的重点是分布式实现。特别是，我们演示了可以使用简单的点对点协议来实现“高级”语义模型。
Reversible distributed programs have the ability to abort unproductive computation paths and backtrack, while unwinding communication that occurred in the aborted paths. While it is natural to assume that reversibility implies full state recovery (as with traditional roll-back recovery protocols), an interesting alternative is to separate backtracking from local state recovery. For example, such a model could be used to create complex transactions out of nested compensable transactions where a programmer-supplied compensation defines the work required to "unwind" a transaction.Reversible distributed computing has received considerable theoretical attention, but little reduction to practice; the few published implementations of languages supporting reversibility depend upon a high degree of central control. The objective of this paper is to demonstrate that a practical reversible distributed language can be efficiently implemented in a fully distributed manner.We discuss such a language, supporting CSP-style synchronous communication, embedded in Scala. While this language provided the motivation for the work described in this paper, our focus is upon the distributed implementation. In particular, we demonstrate that a "high-level" semantic model can be implemented using a simple point-to-point protocol.