The Software Transactional Memory (STM) model is an original approach for controlling concurrent accesses to ressources without the need for explicit lock-based synchronization mechanisms. A key feature of STM is to provide a way to group sequences of read and write actions inside atomic blocks, similar to database transactions, whose whole effect should occur atomically. In this paper, we investigate STM from a process algebra perspective and define an extension of asynchronous CCS with atomic blocks of actions. Our goal is not only to set a formal ground for reasoning on STM implementations but also to understand how this model fits with other concurrency control mechanisms. We also view this calculus as a test bed for extending process calculi with atomic transactions. This is an interesting direction for investigation since, for the most part, actual works that mix transactions with process calculi consider compensating transactions, a model that lacks all the well-known ACID properties. We show that the addition of atomic transactions results in a very expressive calculus, enough to easily encode other concurrent primitives such as guarded choice and multiset-synchronization ( a la join-calculus). The correctness of our encodings is proved using a suitable notion of bisimulation equivalence. The equivalence is then applied to prove interesting laws of transactions'' and to obtain a simple normal form for transactions.
Linked to the upsurge of works on Web Services (and on long running Web transactions), a larger body of works is concerned with formalizing . In this context, each transactive block of actions is associated with a compensation (code) that has to be run if a failure is detected. The purpose of compensation is to undo most of the visible actions that have been performed and, in this case, atomicity, isolation and durability are obviously violated. We give a brief survey of works that formalize compensable processes using process calculi. These works are of two types: (1) @cite_19 @cite_4 @cite_2 , which are extensions of process calculi (like @math or join-calculus) for describing transactional choreographies where composition take place dynamically and where each service describes its possible interactions and compensations; (2) @cite_22 @cite_17 @cite_11 @cite_20 , where ad hoc process algebras are designed from scratch to describe the possible flow of control among services. These calculi are oriented towards the orchestration of services and service failures. This second approach is also followed in @cite_21 @cite_12 where two frameworks for composing transactional services are presented.
@cite_11 @cite_4 @cite_22 @cite_21 @cite_19 @cite_2 @cite_12 @cite_20 @cite_17
2150864072 1974168649 1587877137 1580055894 2460103410
In global computing applications the availability of a mechanism for some form of committed choice can be useful, and sometimes necessary. It can conveniently handle, e.g., distributed agreements and negotiations with nested choice points. We propose a linguistic extension of the Join calculus for programming nested commits, called Committed Join (cJoin). It provides primitives for explicit abort programmable compensations and interactions between negotiations. We give the operational semantics of cJoin in the reflexive CHAM style. Then we discuss its expressiveness on the basis of a few examples and encodings. Finally, we provide a big-step semantics for cJoin processes that can be typed as shallow and we show that shallow processes are serializable. A key aspect when aggregating business processes and web services is to assure transactional properties of process executions. Since transactions in this context may require long periods of time to complete, traditional mechanisms for guaranteeing atomicity are not always appropriate. Generally the concept of long running transactions relies on a weaker notion of atomicity based on compensations. For this reason, programming languages for service composition cannot leave out two key aspects: compensations, i.e. ad hoc activities that can undo the effects of a process that fails to complete, and transactional boundaries to delimit the scope of a transactional flow. This paper presents a hierarchy of transactional calculi with increasing expressiveness. We start from a very small language in which activities can only be composed sequentially. Then, we progressively introduce parallel composition, nesting, programmable compensations and exception handling. A running example illustrates the main features of each calculus in the hierarchy. We study long-running transactions in open component-based distributed applications, such as Web Services platforms. Long-running transactions describe time-extensive activities that involve several distributed components. Henceforth, in case of failure, it is usually not possible to restore the initial state, and firing a compensation process is preferable. Despite the interest of such transactional mechanisms, a formal modeling of them is still lacking. In this paper we address this issue by designing an extension of the asynchronous π-calculus with long-running transactions (and sequences) – the πt -calculus. We study the practice of πt-calculus, by discussing few paradigmatic examples, and its theory, by defining a semantics and providing a correct encoding of πt-calculus into asynchronous π-calculus. A timed extension of π-calculus with a transaction construct – the calculus Webπ – is studied. The underlying model of Webπ relies on networks of processes; time proceeds asynchronously at the network level, while it is constrained by the local urgency at the process level. Namely process reductions cannot be delayed to favour idle steps. The extensional model – the timed bisimilarity – copes with time and asynchrony in a different way with respect to previous proposals. In particular, the discriminating power of timed bisimilarity is weaker when local urgency is dropped. A labelled characterization of timed bisimilarity is also discussed. A long-running transaction is an interactive component of a distributed system which must be executed as if it were a single atomic action. In principle, it should not be interrupted or fail in the middle, and it must not be interleaved with other atomic actions of other concurrently executing components of the system. In practice, the illusion of atomicity for a long-running transaction is achieved with the aid of compensation actions supplied by the original programmer: because the transaction is interactive, familiar automatic techniques of check-pointing and rollback are no longer adequate. This paper constructs a model of long-running transactions within the framework of the CSP process algebra, showing how the compensations are orchestrated to achieve the illusion of atomicity. It introduces a method for declaring that a process is a transaction, and for declaring a compensation for it in case it needs to be rolled back after it has committed. The familiar operator of sequential composition is redefined to ensure that all necessary compensations will be called in the right order if a later failure makes this necessary. The techniques are designed to work well in a highly concurrent and distributed setting. In addition we define an angelic choice operation, implemented by speculative execution of alternatives; its judicious use can improve responsiveness of a system in the face of the unpredictable latencies of remote communication. Many of the familiar properties of process algebra are preserved by these new definitions, on reasonable assumptions of the correctness and independence of the programmer-declared compensations.