作为适应过程的补偿原语
On Compensation Primitives as Adaptable Processes
摘要:
我们比较机制的补偿处理和动态更新演算的并发。这些机制在可靠通信系统的规范中越来越重要。补偿和更新在直观上是相似的:两者都指定并发系统的行为在运行时如何响应异常事件而改变。然而,具有补偿和更新的结石在技术上是完全不同的。我们调查这些结石的相对表现力:我们开发的核心过程语言的编码与补偿到一个适应性强的过程在以前的工作中开发的演算。我们的编码揭示了补偿处理及其关键结构的(复杂)语义。它们还可以将现有的验证和推理技术转移到具有补偿处理的核心语言中。
英文摘要:
We compare mechanisms for compensation handling and dynamic update in calculi for concurrency. These mechanisms are increasingly relevant in the specification of reliable communicating systems. Compensations and updates are intuitively similar: both specify how the behavior of a concurrent system changes at runtime in response to an exceptional event. However, calculi with compensations and updates are technically quite different. We investigate the relative expressiveness of these calculi: we develop encodings of core process languages with compensations into a calculus of adaptable processes developed in prior work. Our encodings shed light on the (intricate) semantics of compensation handling and its key constructs. They also enable the transference of existing verification and reasoning techniques for adaptable processes to core languages with compensation handling.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。