A Specification of Open Transactional Memory for Haskell

TL;DR

This paper introduces Open Transactional Memory (OTM) for Haskell, enabling safe, data-driven interactions between transactions by allowing them to merge dynamically, extending traditional isolated transactional models.

Contribution

It formalizes OTM in Haskell, demonstrating it as a conservative extension of existing STM and proving it satisfies opacity.

Findings

OTM supports transaction merging based on shared data accesses.

Formal semantics of OTM are provided and verified.

OTM extends current STM models without sacrificing safety.

Abstract

Transactional memory (TM) has emerged as a promising abstraction for concurrent programming alternative to lock-based synchronizations. However, most TM models admit only isolated transactions, which are not adequate in multi-threaded programming where transactions have to interact via shared data before committing. In this paper, we present Open Transactional Memory (OTM), a programming abstraction supporting safe, data-driven interactions between composable memory transactions. This is achieved by relaxing isolation between transactions, still ensuring atomicity: threads of different transactions can interact by accessing shared variables, but then their transactions have to commit together-actually, these transactions are transparently merged. This model allows for loosely-coupled interactions since transaction merging is driven only by accesses to shared data, with no need to specify participants beforehand. In this paper we provide a specification of the OTM in the setting of Concurrent Haskell, showing that it is a conservative extension of current STM abstraction. In particular, we provide a formal semantics, which allows us to prove that OTM satisfies the \emph{opacity} criterion.