Title: Communicating Transactions (a Survey)

Speaker: Matthew Hennessy (Trinity College Dublin, Ireland)

         https://www.scss.tcd.ie/Matthew.Hennessy 

Time: 12th December 2014, 14:30

Venue: Seminar Room (334), Level 3, Building 5, Institute of Software, CAS

Abstract:

The advent of multi-core computing has lead to a new software crisis: modern high-level languages do not contain adequate programming constructs which can harness the computing power of mult-cores. In this talk we propose a novel language construct called communicating transactions, obtained by dropping the isolation requirement from classical transactions, which can be used to model automatic error recovery in distributed systems. We show how, when added to a standard functional language, this construct can be used to describe simple and elegant solutions to difficult distributed synchronisation problems.

In the second part of the talk we outline a formal logical theory which can be used to reason about the behaviour of communicating transactions. We extend the well-known process calculus CCS with this construct and give a simple semantics for the extended calculus, called TransCCS. We outline how a sound and complete theory of bisimulations can developed for TransCCS, thereby laying the foundation for viable verification techniques for communicating transactions.

Joint work with Edsko de Vries, Vasileios Koutavas and Carlo Spaccasassi.

References:

Vasileios Koutavas, Carlo Spaccasassi and Matthew Hennessy.

Bisimulations for Communicating Transactions (Extended Abstract)

FOSSACS 2014.

Edsko de Vries, Vasileios Koutavas and Matthew Hennessy.

Communicating Transactions (Extended Abstract).

CONCUR 2010.

Edsko de Vries, Vasileios Koutavas and Matthew Hennessy.

Liveness of Communicating Transactions (Extended Abstract).

APLAS 2010.