On Compensation Primitives as Adaptable Processes

TL;DR

This paper explores the relationship between compensation mechanisms and dynamic updates in concurrent process calculi, developing encodings to compare their expressiveness and facilitate verification techniques transfer.

Contribution

It introduces encodings of compensation mechanisms into adaptable process calculi, clarifying their semantics and enabling the application of existing verification methods.

Findings

Encodings reveal the semantic differences between compensations and updates.

The work facilitates transferring verification techniques from adaptable processes to compensation handling.

It provides a formal comparison of the expressiveness of these calculi.

Abstract

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.