Language support for communicating transactions

Abstract

In the context of databases, a transaction is a sequence of data operations that are executed atomically and in isolation: either all operations are executed or none is; and their effects are visible to the environment only after the transaction commits. Database transactions are well-established abstractions that simplify concurrent data access in computer programming. Recently Software Transactional Memory (STM) has been proposed to extend the notion of transactions from databases to concurrent programming in shared-memory systems. STM has been likened to garbage collection for memory management in terms of cost and benefits: both of them provide modular abstractions that separate the specification of memory operations, which is delegated to the programmer, from its actual implementation and inherent complexity, which is delegated to an underlying management system. Few such abstractions currently exist for concurrent programming in distributed systems, where communication is based on message-passing rather than shared memory. Communicating transactions is one such abstraction that has been recently proposed to model automatic fault recovery in distributed systems. Dropping the isolation requirement from traditional transactions, communicating transactions allow groups of concurrent processes to interact and commit after reaching a consensus. When they fail to reach a consensus for any reason, including deadlock and unforeseen failures, all interactions are annulled and all side-effects are rolled back. This thesis focuses on the application of communicating transactions to concurrent programming languages for distributed systems. We explore the expressivity of communicating transactions in TCML, a novel transactional concurrent functional language inspired to CML. We review a powerful proof method based on bisimulations to reason about communicating transactions in the context of a new transactional calculus, TCCSm, and we present a new, equivalent bisimulation method that allows bisimulation equivalences between finite-state TCCSm processes to be calculated algorithmically. We study the performance of a TCML implementation using na¨ıve transaction scheduling policies. Our study shows that under such policies the creation of consensus groups decreases exponentially in proportion to the number of participants contending for the same resources. This points to the need of more sophisticated transaction analysis tools. A promising tool is session types, a recently proposed mechanism to statically verify the communication protocols employed by concurrent processes. We propose the first fully automatic, sound and complete session type inference algorithm that supports session delegation and recursion. We believe this mechanism to be the foundation for further development and performance enhancement in the realm of transactions scheduling.