# Open Transactions on Shared Memory

Marino Miculan, Marco Peressotti, Andrea Toneguzzo

► To cite this version:

Marino Miculan, Marco Peressotti, Andrea Toneguzzo. Open Transactions on Shared Memory. 17th International Conference on Coordination Languages and Models (COORDINATION), Jun 2015, Grenoble, France. pp.213-229, 10.1007/978-3-319-19282-6_14. hal-01774945

HAL Id: hal-01774945

https://inria.hal.science/hal-01774945

Submitted on 24 Apr 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Open transactions on shared memory

Marino Miculan, Marco Peressotti, and Andrea Toneguzzo

Laboratory of Models and Applications of Distributed Systems
Department of Mathematics and Computer Science, University of Udine
{marino.miculan, marco.peressotti}@uniud.it

**Abstract.** *Transactional memory* has arisen as a good way for solving many of the issues of lock-based programming. However, most implementations admit *isolated* transactions only, which are not adequate when we have to coordinate *communicating* processes. To this end, in this paper we present *OCTM*, an Haskell-like language with *open* transactions over shared transactional memory: processes can *join* transactions at runtime just by accessing to shared variables. Thus a transaction can co-operate with the environment through shared variables, but if it is rolled-back, also all its effects on the environment are retracted. For proving the expressive power of *OCTM* we give an implementation of *TCCS*<sup>*m*</sup>, a CCS-like calculus with *open* transactions.

## 1 Introduction

Coordination of concurrent programs is notoriously difficult. Traditional fine-grained lock-based mechanisms are deadlock-prone, inefficient, not composable and not scalable. For these reasons, *Software Transactional Memory* (STM) has been proposed as a more effective abstraction for concurrent programming [1,9,17]. The idea is to mark blocks of code as “atomic”; at runtime, these blocks are executed so that the well-known ACID properties are guaranteed. Transactions ensure deadlock freedom, no priority inversion, automatic roll-back on exceptions or timeouts, and greater parallelizability. Among other implementations, we mention *STM Haskell* [7], which allows atomic blocks to be composed into larger ones. STM Haskell adopts an *optimistic* evaluation strategy: the blocks are allowed to run concurrently, and eventually if an interference is detected a transaction is *aborted* and its effects on the memory are rolled back.

However, standard ACID transactions are still inadequate when we have to deal with *communicating* processes, i.e., which can exchange information *during* the transactions. This is very common in concurrent distributed programming, like in service-oriented architectures, where processes dynamically combine to form a transaction, and all have to either commit or abort together. In this scenario the participants cannot be enclosed in one transaction beforehand, because transactions are formed at runtime. To circumvent this issue, various forms of *open transactions* have been proposed, where the Isolation requirement is relaxed [2-4,10,12]. In particular, *TransCCS* and *TCCS*<sup>*m*</sup> are two CCS-like calculi recently introduced to model communicating transactions [4, 5, 10]. These calculi offer methodologies for proving important properties, such as fair-testing for proving liveness and bisimulations for proving contextual equivalences.
Now, if we try to implement cross-transaction communications *a la TCCS*<sup>*m*</sup> in STM Haskell or similar languages, it turns out that isolated transactions are not expressive enough. As an example, let us consider two *TCCS*<sup>*m*</sup> transactions $\langle \bar{c}.P \blacklozenge 0 \rangle | \langle c.Q \blacklozenge 0 \rangle$ synchronizing on a channel *c*. Following the standard practice, we could implement this synchronization as two parallel processes using a pair of semaphores *c1*, *c2* (which are easily realized in STM Haskell):

$$ \langle \bar{c}.P \blacklozenge 0 \rangle = \begin{array}{l} \text{atomic} \{ \\ \quad \text{up } c1 \quad -- 1.1 \\ \quad \text{down } c2 \quad -- 1.2 \\ \quad P \\ \} \end{array} \quad \left| \quad \begin{array}{l} \langle c.Q \blacklozenge 0 \rangle = \begin{array}{l} \text{atomic} \{ \\ \quad \text{down } c1 \quad -- 2.1 \\ \quad \text{up } c2 \quad -- 2.2 \\ \quad Q \\ \} \end{array} \\ \end{array} $$

This implementation is going to deadlock: the only possible execution order is 1.1-2.1-2.2-1.2, which is possible outside transactions but it is forbidden for ACID transactions<fnref n="1" />. The problem is that ordinary STM transactions are kept isolated, while in *TCCS*<sup>*m*</sup> they can merge at runtime.

In order to address this issue, in this paper we introduce software transactional memory with *open* transactions: processes can *join* transactions and transactions can *merge* at runtime, when they access to shared variables. To this end, we present *OCTM*, a higher-order language extending the concurrency model of STM Haskell with composable *open (multi-thread)* transactions interacting via *shared memory*. The key step is to separate the isolation aspect from atomicity: in *OCTM* the *atomic* construct ensures “all-or-nothing” execution, but not isolation; when needed, isolated execution can be guaranteed by a new constructor *isolated*. An *atomic* block is a *participant* (possibly the only one) of a transaction. Notice that transaction merging is implicitly triggered by accessing to shared memory, without any explicit operation or *a priori* coordination. For instance, in *OCTM* the two transactions of the example above would merge becoming two participants of the same transaction, hence the two threads can synchronize and proceed. In order to prove formally the expressivity of *open memory transactions*, we define an implementation of *TCCS*<sup>*m*</sup> in *OCTM*, which is proved to correctly preserve behaviours by means of a suitable notion of simulation. We have based our work on STM Haskell as a paradigmatic example, but this approach is general and can be applied to other STM implementations.

Lesani and Palsberg [12] have proposed transactions communicating through transactional message-based channels called *transactional events*. These mechanisms are closer to models like TransCCS and *TCCS*<sup>*m*</sup>, but on the other hand they induce a *strict coupling* between processes, which sometimes is neither admissible nor easy to implement (e.g., when we do not know all transaction's participants beforehand). In fact, most STM implementations (including STM Haskell) adopt the shared memory model of multi-thread programming; this model is also more amenable to implementation on modern multi-core hardware architectures with transactional memory [8]. For these reasons, in *OCTM* we have preferred to stick to *loosely coupled* interactions based on shared memory only.

<footnote n="1">¹ This possibility was pointed out also in [7]: “two threads can easily deadlock if each awaits some communication from the other”.</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1. Syntax of OCTM values and terms.</figcaption></figure>

The rest of the paper is structured as follows. In Section 2 we describe the syntax and semantics of OCTM. The calculus TCCS<sup>m</sup>, our reference model for open transactions, is recalled in Section 3. Then, in Section 4 we provide an encoding of TCCS<sup>m</sup> in OCTM, proving that OCTM is expressive enough to cover open transactions. Conclusions and directions for future work are in Section 5. Longer proofs are in the extended version of this paper [15].

## 2 OCTM: Open Concurrent Transactional Memory

In this section we introduce the syntax and semantics of OCTM, a higher-order functional language with threads and open transaction on shared memory. The syntax is Haskell-like (in the wake of existing works on software transactional memories such as [7]) and the semantics is a small-step operational semantics given by two relations: $\beta \to$ models transaction auxiliary operations (e.g. creation) while $\to$ models actual term evaluations. Executions proceeds by repeatedly choosing a thread and executing a single (optionally transactional) operation; transitions from different threads may be arbitrarily interleaved as long as atomicity and isolation are not violated where imposed by the program.

### 2.1 Syntax

The syntax can be found in Figure 1 where the meta-variables *r* and *x* range over a given countable set of locations *Loc* and variables *Var* respectively. Terms and values are inspired to Haskell and are entirely conventional<sup>2</sup>; they include abstractions, application, monadic operators (*return* and **=>**), memory operators (*newVar*, *readVar*, *writeVar*), forks, transactional execution modalities (*atomic* and *isolated*) and transaction operators (*abort* and *retry*).

Effectfull expressions such as *fork* or *isolated* are glued together by the (overloaded) monadic bind **=>** e.g.:

$$ \mathit{newVar} \ 0 \Longrightarrow \lambda x. (\mathit{fork} \ (\mathit{writeVar} \ x \ 42)) \Longrightarrow \lambda y. (\mathit{readVar} \ x) $$

whereas values are “passed on” by the monadic unit *return*.

Akin to Haskell, we will use underscores in place of unused variables (e.g. `\lambda_0`) and `M >> N` as a shorthand for `M >>= \lambda_.N`, and the convenient *do-notation*:

$$ \begin{align*} \mathit{do}\{x \leftarrow M; N\} &\equiv M &\Longrightarrow& (\lambda x. \mathit{do}\{N\}) \\ \mathit{do}\{M; N\} &\equiv M &\Longrightarrow& (\lambda_. \mathit{do}\{N\}) \\ \mathit{do}\{M\} &\equiv M \end{align*} $$

<footnote n="2">² Although we treat the application of monadic combinators (e.g. `return`) as values in the line of similar works [7].</footnote>
possibly trading semicolons and brackets for the conventional Haskell *layout*. For
instance, the above example is rendered as

```
do
  x ← newVar 0
  fork (writeVar x 42)
  readVar x
```

## 2.2 Operational Semantics

We present the operational semantics of *OCTM* in terms of an abstract machine
whose states are triples $\langle P; \Theta, \Delta \rangle$ formed by

- thread family (process) *P*;

- heap memory $\Theta: \text{Loc} \to \text{Term}$;

- distributed working memory $\Delta: \text{Loc} \to \text{Term} \times \text{TrName}$

where *Term* denotes the set of *OCTM* terms (cf. Figure 1) and *TrName* denotes the set of names used by the machine to identify active transactions. We shall denote the set of all possible states as *State*.

*Threads* Threads are the smaller unit of execution the machine scheduler operates on; they execute OCTM terms and do not have any private transactional memory. Threads are given unique identifiers (ranged over by *t* or variations thereof) and, whenever they take part to some transaction, the transaction identifier (ranged over *k*, *j* or variations thereof). Threads of the former case are represented by $([M])_t$ where *M* is the term being evaluated and the subscript *t* is the thread identifier. Threads of the latter case have two forms: $([M] \triangleright [M'] ; N)_{t,k}$, called and $([M] \triangleright [M'])_{t,k}$ where:

- *M* is the term being evaluated inside the transaction *k*;

- *M'* is the term being evaluated as *compensation* in case *k* is aborted;

- *N* is the term being evaluated as *continuation* after *k* commits or aborts.

Threads with a continuation are called *primary participants (to transaction k)*, while threads without continuation are the *secondary participants*. The former group includes all and only the threads that started a transaction (i.e. those evaluated in an *atomic*), while the latter group encompasses threads forked inside a transaction and threads forced to join a transaction (from outside a transactional context) because of memory interactions. While threads of both groups can force a transaction to abort or restart, only primary participants can vote for its commit and hence pass the transaction result to the continuation.

We shall present thread families using the evocative CCS-like parallel operator $|$ (cf. Figure 2) which is commutative and associative. Notice that this operator is well-defined only on operands whose thread identifiers are distinct. The notation is extended to thread families with *0* denoting the empty family.
Thread $T_t ::= (M)_t | ((M \triangleright M'; N)_{t,k} | ((M \triangleright M')_{t,k})$

Thread family $P ::= T_{t_1} \parallel \cdots \parallel T_{t_n} \quad \forall i, j, t_i \neq t_j$

Expressions $\mathbb{E} ::= [-] | \mathbb{E} >>= M$

Processes $\mathbb{P}_t ::= (\mathbb{E})_t$

Transactions $\mathbb{T}_{t,k} ::= ((\mathbb{E} \triangleright M; N)_{t,k} | ((\mathbb{E} \triangleright M)_{t,k}))$

<caption>Fig. 2. Threads and evaluation contexts.</caption>

$$ \frac{M \not\equiv V \quad \mathcal{V}[M] = V}{M \to V} \quad \text{(EVAL)} \qquad \frac{\text{return } M \gg= N \to NM}{\mathbb{M}} \quad \text{(BINDRETURN)} \\ \frac{\text{retry } \gg= M \to \text{retry}}{\mathbb{M} \to \text{retry}} \quad \text{(BINDRETRY)} \qquad \frac{\text{abort } N \gg= M \to \text{abort } \mathbb{N}}{\mathbb{N}} \quad \text{(BINDABORT)} $$

<caption>Fig. 3. OCTM semantics: rules for term evaluation.</caption>

*Memory* The memory is divided in the heap $\Theta$ and in a distributed working memory $\Delta$. As for traditional closed (acid) transactions (e.g. [7]), operations inside a transaction are evaluated against $\Delta$ and effects are propagated to $\Theta$ only on commits. When a thread inside a transaction $k$ accesses a location outside $\Delta$ the location is claimed for $k$ and remains claimed for the rest of $k$ execution. Threads inside a transaction can interact only with locations claimed by their transaction. To this end, threads outside any transaction can join an existing one and different active transactions can be merged to share their claimed locations.

We shall denote the pair $(\Theta, \Delta)$ by $\Sigma$ and reference to each projected component by a subscript e.g. $\Sigma_{\Theta}$ for the heap. When describing updates to the state $\Sigma$, we adopt the convention that $\Sigma'$ has to be intended as equal to $\Sigma$ except if stated otherwise, i.e. by statements like $\Sigma'_{\Theta} = \Sigma_{\Theta}[r \mapsto M]$. Formally, updates to location content are defined on $\Theta$ and $\Delta$ as follows:

$$ \Theta[r \mapsto M](s) \triangleq \begin{cases} M & \text{if } r = s \\ \Theta(s) & \text{otherwise} \end{cases} \quad \Delta[r \mapsto (M, k)](s) \triangleq \begin{cases} (M, k) & \text{if } r = s \\ \Delta(s) & \text{otherwise} \end{cases} $$

for any $r, s \in \text{Loc}$, $M \in \text{Term}$ and $k \in \text{TrName}$. Likewise, updates on transaction names are defined on $\Sigma$ and $\Delta$ as follows:

$$ \Sigma[k \mapsto j] \triangleq (\Theta, \Delta[k \mapsto j]) \quad (\Delta[k \mapsto j])(r) \triangleq \begin{cases} \Delta(r) & \text{if } \Delta(r) = (M, l), l \neq k \\ (M, j) & \text{if } \Delta(r) = (M, k) \end{cases} $$

for any $r \in \text{Loc}$, $M \in \text{Term}$ and $k, j \in \text{TrName}$. Note that $j$ may occur in $\Delta$ resulting in the fusion of the transactions denoted by $k$ and $j$ respectively. Finally, $\emptyset$ denotes the empty memory (i.e. the completely undefined partial function).

*Behaviour* Evaluation contexts are shown in Figure 2 and the transition relations are presented in Figures 3, 4, 5. The first (cf. Figures 3) is defined on terms only and models pure computations. In particular, rule (EVAL) allows a term $M$ that is not a value to be evaluated by an auxiliary (partial) function, $\mathcal{V}[M]$ yielding the value $V$ of $M$ whereas the other three rules define the semantic of the monadic bind. The transition relation modelling pure computations can be thought as accessory to the remaining two for these model transitions between the states of the machine under definition.
$$
\begin{align*}
& M \to N \qquad \frac{M \to N}{\langle \mathbb{P}_t[M] \| P; \Sigma \rangle \to \langle \mathbb{P}_t[N] \| P; \Sigma \rangle} \quad (\text{TERMP}) \\
& \phantom{M \to N} \frac{M \to N}{\langle \mathbb{T}_{t,k}[M] \| P; \Sigma \rangle \to \langle \mathbb{T}_{t,k}[N] \| P; \Sigma \rangle} \quad (\text{TERMT}) \\
& t' \notin \text{threads}(P) \quad t \neq t' \\
& \frac{\langle \mathbb{P}_t[\text{fork } M] \| P; \Sigma \rangle \to \langle \mathbb{P}_t[\text{return } t'] \| (M) \rangle_{t'} \| P; \Sigma \rangle}{\langle \mathbb{T}_{t,k}[\text{fork } M] \| P; \Sigma \rangle \to \langle \mathbb{T}_{t,k}[\text{return } t'] \| (M \triangleright \text{return}) \rangle_{t',k} \| P; \Sigma \rangle} \quad (\text{FORKP}) \\
& t' \notin \text{threads}(P) \quad t \neq t' \\
& \frac{\langle \mathbb{T}_{t,k}[\text{fork } M] \| P; \Sigma \rangle \to \langle \mathbb{T}_{t,k}[\text{return } t'] \| (M \triangleright \text{return}) \rangle_{t',k} \| P; \Sigma \rangle}{\langle \mathbb{T}_{t,k}[\text{fork } M] \| P; \Sigma \rangle \to \langle \mathbb{T}_{t,k}[\text{return } t'] \| (M \triangleright \text{return}) \rangle_{t',k} \| P; \Sigma \rangle} \quad (\text{FORKT}) \\
& \text{threads}(T_{t_1} \| \dots \| T_{t_n}) \triangleq \{t_1, \dots, t_n\} \\
& r \notin \text{dom}(\Sigma_\theta) \cup \text{dom}(\Sigma_\Delta) \quad \frac{\Sigma'_\theta = \Sigma_\theta[r \mapsto M]}{\langle \mathbb{P}_t[\text{newVar } M] \| P; \Sigma \rangle \to \langle \mathbb{P}_t[\text{return } r] \| P; \Sigma' \rangle} \quad (\text{NEWP}) \\
& r \notin \text{dom}(\Sigma_\theta) \cup \text{dom}(\Sigma_\Delta) \quad \frac{\Sigma'_\Delta = \Sigma_\Delta[r \mapsto (M, k)]}{\langle \mathbb{T}_{t,k}[\text{newVar } M] \| P; \Sigma \rangle \to \langle \mathbb{T}_{t,k}[\text{return } r] \| P; \Sigma' \rangle} \quad (\text{NEWT}) \\
& \frac{r \notin \text{dom}(\Sigma_\Delta) \quad \Sigma_\theta(r) = M}{\langle \mathbb{P}_t[\text{readVar } r] \| P; \Sigma \rangle \to \langle \mathbb{P}_t[\text{return } M] \| P; \Sigma \rangle} \quad (\text{READP}) \\
& \frac{r \notin \text{dom}(\Sigma_\Delta) \quad \Sigma_\theta(r) = M \quad \Sigma'_\Delta = \Sigma_\Delta[r \mapsto (M, k)]}{\langle \mathbb{T}_{t,k}[\text{readVar } r] \| P; \Sigma \rangle \to \langle \mathbb{T}_{t,k}[\text{return } M] \| P; \Sigma' \rangle} \quad (\text{READT}) \\
& \frac{M = \mathbb{E}[\text{readVar } r] \quad \Sigma_\Delta(r) = (M', k)}{\langle (M) \rangle_t \| P; \Sigma \rangle \to \langle (\mathbb{E}[\text{return } M'] \triangleright \lambda_{\cdot} M) \rangle_{t,k} \| P; \Sigma \rangle} \quad (\text{READJOIN}) \\
& \frac{\Sigma_\Delta(r) = (M, j) \quad \Sigma' = \Sigma[k \mapsto j]}{\langle \mathbb{T}_{t,k}[\text{readVar } r] \| P; \Sigma \rangle \to \langle \mathbb{T}_{t,j}[\text{return } M] \| P[k \mapsto j]; \Sigma' \rangle} \quad (\text{READMERGE}) \\
& \frac{r \notin \text{dom}(\Sigma_\Delta) \quad \Sigma_\theta(r) = N \quad \Sigma'_\theta = \Sigma_\theta[r \mapsto M]}{\langle \mathbb{P}_t[\text{writeVar } r M] \| P; \Sigma \rangle \to \langle \mathbb{P}_t[\text{return } ()] \| P; \Sigma' \rangle} \quad (\text{WRITEP}) \\
& \frac{r \notin \text{dom}(\Sigma_\Delta) \quad \Sigma_\theta(r) = N \quad \Sigma'_\Delta = \Sigma_\Delta[r \mapsto (M, k)]}{\langle \mathbb{T}_{t,k}[\text{writeVar } r M] \| P; \Sigma \rangle \to \langle \mathbb{T}_{t,k}[\text{return } ()] \| P; \Sigma' \rangle} \quad (\text{WRITET}) \\
& \frac{M = \mathbb{E}[\text{writeVar } r M'] \quad \Sigma_\Delta(r) = (M'', k) \quad \Sigma'_\Delta = \Sigma_\Delta[r \mapsto (M', k)]}{\langle (M) \rangle_t \| P; \Sigma \rangle \to \langle (\mathbb{E}[\text{return } ()] \triangleright \lambda_{\cdot} M) \rangle_{t,k} \| P; \Sigma' \rangle} \quad (\text{WRITEJOIN}) \\
& \frac{\Sigma_\Delta(r) = (N, j) \quad \Sigma' = \Sigma[k \mapsto j] \quad \Sigma'_\Delta = \Sigma_\Delta[k \mapsto (M, j)]}{\langle \mathbb{T}_{t,k}[\text{writeVar } r M] \| P; \Sigma \rangle \to \langle \mathbb{T}_{t,j}[\text{return } ()] \| P[k \mapsto j]; \Sigma' \rangle} \quad (\text{WRITEMERGE})
\end{align*}
$$

<caption>Fig. 4. OCTM semantics: rules for $\to$.</caption>

Derivation rules in Figure 4 characterize the execution of pure (effect-free) terms, forks and memory operations both inside, and outside of some transaction; Derivation rules in Figure 5 characterize auxiliary operations for transaction management (e.g. creation) and their coordination (e.g distributed commits). Note that there are no derivation rules for **retry**. In fact, the meaning of **retry** is to inform the machine that choices made by the scheduler led to a state from which the program cannot proceed. From an implementation perspective this translates in the transaction being re-executed from the beginning (or a suitable check-point) following a different scheduling of its operations.

Due to lack of space we shall describe only a representative subset of the derivation rules from Figure 4 and Figure 5.

Reading a location falls into four cases depending on the location being claimed (i.e. occurring in $\Delta$) and the reader being part of a transaction. The
$$
\begin{align*}
& \frac{k \notin \text{transactions}(P)}{\langle (\text{atomic } M \ N \ >>= N')_t \parallel P; \Sigma \rangle \xrightarrow{\text{new}_k} \langle (M \triangleright N; N')_{t,k} \parallel P; \Sigma \rangle} \quad \text{(ATOMIC)} \\
& \frac{\langle (M)_t; \Sigma \rangle \to^* \langle (\text{return } N)_t; \Sigma' \rangle}{\langle P_t[\text{isolated } M]; \Sigma \rangle \to \langle P_t[\text{return } N]; \Sigma' \rangle} \quad \text{(ISOLATEDP)} \\
& \frac{\text{op} \in \{\text{abort}, \text{return}\} \quad \langle (M \triangleright \text{return})_{t,k}; \Sigma \rangle \to^* \langle (\text{op } N \triangleright \text{return})_{t,k}; \Sigma' \rangle}{\langle \mathbb{T}_{t,k}[\text{isolated } M]; \Sigma \rangle \to \langle \mathbb{T}_{t,k}[\text{op } N]; \Sigma' \rangle} \quad \text{(ISOLATEDT)} \\
& \frac{\Sigma'_{\Delta} = \text{clean}(k, \Sigma_{\Delta})}{\langle (\text{abort } M \triangleright N; N')_{t,k}; \Sigma \rangle \xrightarrow{ab_k M} \langle (N(M) \ >>= N')_t; \Sigma' \rangle} \quad \text{(RAISEABORT1)} \\
& \frac{\Sigma'_{\Delta} = \text{clean}(k, \Sigma_{\Delta})}{\langle (\text{abort } M \triangleright N')_{t,k}; \Sigma \rangle \xrightarrow{ab_k M} \langle (N(M))_t; \Sigma' \rangle} \quad \text{(RAISEABORT2)} \\
& \frac{\Sigma'_{\Delta} = \text{clean}(k, \Sigma_{\Delta})}{\langle (M \triangleright N; N')_{t,k}; \Sigma \rangle \xrightarrow{\widehat{ab}_k M} \langle (N(M) \ >>= N')_t; \Sigma' \rangle} \quad \text{(SIGABORT1)} \\
& \frac{\Sigma'_{\Delta} = \text{clean}(k, \Sigma_{\Delta})}{\langle (M \triangleright N)_{t,k}; \Sigma \rangle \xrightarrow{\widehat{ab}_k M} \langle (N(M))_t; \Sigma' \rangle} \quad \text{(SIGABORT2)} \\
& \frac{\langle P; \Sigma \rangle \xrightarrow{ab_k M} \langle P'; \Sigma' \rangle \quad \langle Q; \Sigma \rangle \xrightarrow{ab_k M} \langle Q'; \Sigma' \rangle}{\langle P \parallel Q; \Sigma \rangle \xrightarrow{ab_k M} \langle P' \parallel Q'; \Sigma' \rangle} \quad \text{(ABBROADCAST)} \\
& \frac{\Sigma'_{\Theta} = \text{commit}(k, \Sigma_{\Theta}, \Sigma_{\Delta}) \quad \Sigma'_{\Delta} = \text{clean}(k, \Sigma_{\Delta})}{\langle (\text{return } M \triangleright N; N')_{t,k}; \Sigma \rangle \xrightarrow{co_k} \langle (\text{return } M \ >>= N')_t; \Sigma' \rangle} \quad \text{(COMMIT1)} \\
& \frac{\Sigma'_{\Theta} = \text{commit}(k, \Sigma_{\Theta}, \Sigma_{\Delta}) \quad \Sigma'_{\Delta} = \text{clean}(k, \Sigma_{\Delta})}{\langle (M \triangleright N)_{t,k}; \Sigma \rangle \xrightarrow{co_k} \langle (M)_t; \Sigma' \rangle} \quad \text{(COMMIT2)} \\
& \frac{\langle P; \Sigma \rangle \xrightarrow{co_k} \langle P'; \Sigma' \rangle \quad \langle Q; \Sigma \rangle \xrightarrow{co_k} \langle Q'; \Sigma' \rangle}{\langle P \parallel Q; \Sigma \rangle \xrightarrow{co_k} \langle P' \parallel Q'; \Sigma' \rangle} \quad \text{(COBROADCAST)} \\
& \frac{\langle P; \Sigma \rangle \xrightarrow{\beta} \langle P'; \Sigma' \rangle \quad \text{transactions}(\beta) \notin \text{transactions}(Q)}{\langle P \parallel Q; \Sigma \rangle \xrightarrow{\beta} \langle P' \parallel Q; \Sigma \rangle} \quad \text{(TRIGNORE)}
\end{align*}
$$

$$
\text{transactions}(T_{t_1} \parallel \cdots \parallel T_{t_n}) \triangleq \bigcup_{1 \le i \le n} \text{transactions}(T_{t_i}) \quad \text{clean}(k, \Delta)(r) \triangleq \begin{cases} \perp & \text{if } \Delta(r) = (M, k) \\ \Delta(r) & \text{otherwise} \end{cases}
$$

$$
\begin{align*}
\text{transactions}((M)_t) &\triangleq \emptyset \\
\text{transactions}((M \triangleright M'; N)_{t,k}) &\triangleq \{k\} \quad \text{commit}(k, \Theta, \Delta)(r) \triangleq \begin{cases} M & \text{if } \Delta(r) = (M, k) \\ \Theta(r) & \text{otherwise} \end{cases} \\
\text{transactions}((M \triangleright N)_{t,k}) &\triangleq \{k\}
\end{align*}
$$

<caption>Fig. 5. OCTM semantics: rules for $\xrightarrow{\beta}$.</caption>

rule (READP) characterize the reading of an unclaimed location from outside
any transaction; the read is performed as expected leaving it unclaimed. Rule
(READT) describes the reading of an unclaimed location *r* by a thread belonging
to some transaction *k*; the side effect of the reading is *r* being claimed for *k*. Rules
(READMERGE) and (READJOIN) cover the cases of readings against claimed lo-
cations. In the first scenario, the reading thread belongs to a transaction resulting
in the two being merged, which is expressed by renaming its transaction via a
substitution. In the remaining scenario, the reading thread does not belong to
any transaction and hence joins the transaction $k$ which claimed the location. The newly created participant does not have any continuation since the whole term is set to be executed inside $k$; any other choice for splitting the term sin-gling out a compensation would impose an artificial synchronization with the transaction commit. For a counter example, consider executing only the read operation inside the transaction and delaying everything after the commit; then concurrency will be clearly reduced. Because of the same reasoning, the whole term $M$ is taken as the compensation of the participant.

Atomic transactions are created by the rule (ATOMIC); threads participating in this transaction are non-deterministically interleaved with other threads. The stronger requirement of isolation is offered by (ISOLATEDP) and (ISOLATEDT); note that their premises forbid thread or transaction creation.

Committing or aborting a transaction require a synchronization of its participants. In particular, an abort can be read as a participant vetoing the outcome of the transaction; this corresponds to (RAISEABORT1) and (RAISEABORT2). The information is then propagated by (ABBROADCAST) and (TRIGNORE) to any other participant to the transaction being aborted; these participants abort performing a transition described by either (SIGABORT1) or (SIGABORT2).

## 3 TCCS<sup>m</sup>: CCS with open transactions

In order to assess the expressive power of OCTM, we have to compare it with a formal model for open transactions. To this end, in this section we recall TCCS<sup>m</sup> [10], a CCS-like calculus with open flat transactions: processes can synchronize even when belonging to different transactions, which in turn are joined into a distributed one. We refer to [10] for a detailed description of TCCS<sup>m</sup>.

The syntax of TCCS<sup>m</sup> is defined by the following grammar

$$ P ::= \sum_{i=1}^{n} \alpha_i.P_i \mid \prod_{i=0}^{m} P_i \mid P\backslash L \mid X \mid \mu X.P \mid \langle P_1 \triangleright P_2 \rangle \mid \langle P_1 \triangleright_k P_2 \rangle \mid \text{co}.P \quad (1) $$

where $\alpha_i ::= a | \bar{a} | \tau, a$ ranges over a given set of visible actions $A, L$ over subsets of $A$ and the bijection $\bar{\cdot}: A \to A$ maps every action to its coaction as usual. The calculus extends CCS with three constructs which represent inactive transactions, active transactions and commit actions respectively. Transactions such as $\langle P_1 \triangleright_k P_2 \rangle$ are formed by two processes with the former being executed atomically and the latter being executed whenever the transaction is aborted, i.e. as a compensation. Terms denoting active transactions expose also a name ($k$ in the previous example) which is used to track transaction fusions. For instance, consider the process denoted by $\langle P_1 \triangleright_j P_2 \rangle | \langle Q_1 \triangleright_k Q_2 \rangle$ where $P_1$ and $Q_1$ synchronize on some $a \in A$; the result of this synchronization is the fusion of the transactions $j$ and $k$ i.e. $\langle P'_1 \triangleright_l P_2 \rangle | \langle Q'_1 \triangleright_l Q_2 \rangle$. The fusion makes explicit the dependency between $j$ and $k$ introduced by the synchronization and ties them to agree on commits. In this sense, $P'_1$ and $Q'_1$ are participants of a distributed transaction [6].

As in [10] we restrict ourselves to well-formed terms. Intuitively, a term is well-formed if active transactions occur only at the top-level and commit actions occur only in a transaction (active or inactive). To this end we introduce a type system for TCCS<sup>m</sup>, whose rules are in Figure 6. Terms that cannot occur inside
<figure><img src="image_3.png" /><figcaption>Fig. 6. Simple types for TCCS<sup>m</sup>.</figcaption></figure>

a transaction have type `t`, terms that cannot occur outside a transaction have type `c`, and terms without such restrictions have type `p`; $\tau$ ranges over types.

**Definition 1 (Well-formed TCCS<sup>m</sup> terms).** A TCCS<sup>m</sup> term `P`, described by the grammar in (1), is said to be well-formed if, and only if, $\emptyset \vdash P : t$. Well-formed terms form the set Proc.

The operational semantics of well-formed TCCS<sup>m</sup> terms is given by the SOS in Figure 7 (further details can be found in [10]). The reduction semantics is given as a binary relation $\rightarrow$ defined by

$$P \rightarrow Q \stackrel{\Delta}{\rightleftharpoons} P \xrightarrow{\tau} Q \lor P \xrightarrow{\beta} Q \lor P \xrightarrow{k(\tau)} Q.$$

The first case is a synchronization between pure CCS processes. The second case corresponds to creation of new transactions and distributed commit or abort ($\beta \in \{\text{newk}, \text{cok}, \text{abk}\}$). The third case corresponds to synchronizations of processes inside a named (and possibly distributed) transaction. Notice that by (TSYNC) transaction fusion is driven by communication and that by (TSUM) any pure CCS process can join and interact with a transaction.

## 4 Encoding TCCS<sup>m</sup> in OCTM

In this section, we prove that OCTM is expressive enough to cover open transactions *a la* TCCS<sup>m</sup>. To this end, we provide an encoding of TCCS<sup>m</sup> in OCTM. Basically, we have to implement transactions and CCS-like synchronizations using shared transactional variables and the atomic and isolated operators. The encoding is proved to be correct, in the sense that a TCCS<sup>m</sup> process presents a reduction if and only if also its encoding has the corresponding reduction.

Synchronization is implemented by means of shared transactional variables, one for each channel, that take values of type `ChState` (cf. Figure 9); this type has four constructors: one for each of the three messages of the communication protocol below plus a “nothing” one providing the default value. Let $t_1$ and $t_2$ be the identifiers of two threads simulating `a.P` and `a.Q` respectively. The protocol is composed by the following four steps:

1. $t_1$ checks whether the channel is free and writes on the transactional variable modelling the channel *a* a nonce tagged with the constructor `M1`;

2. $t_2$ reads the variable for *a* and accepts the synchronization offered by the challenge (`M1 np`) adding a fresh nonce to it and writing back (`M2 np nq`);
<figure><img src="image_4.png" /><figcaption>Fig. 7. TCCS<sup>m</sup> operational semantics.</figcaption></figure>

3. $t_1$ reads the answer to its challenge and acknowledges the synchronization writing back the nonce it read tagged with the constructor M3;

4. $t_2$ reads the acknowledgement and frees the channel.

Each step has to be executed in isolation with respect to the interactions with the shared transactional variable *a*. Nonces are meant to correlate the steps only and hence can be easily implemented in *OCTM* by pairing thread identifiers with counter *a* la logical clock. If at any step a thread finds the channel in an unexpected state it means that the chosen scheduling has led to a state incoherent with respect to the above protocol; hence the thread executes a *retry*. This tells the scheduler to try another execution order; by fairness, we eventually find a scheduling such that the two processes do synchronize on *a* and these are the only executions leading to *P* | *Q*. The protocol is illustrated in Figure 8. If the synchronizing parties are involved in distinct transactions these are fused as a side effect of the interaction via the shared variable.

A choice like $\sum_{i=1}^{m} \alpha_i P_i$ can be seen as a race of threads $t_1, \dots, t_m$, each simulating a branch, to acquire a boolean transactional variable $l$ (private to the group). Each $t_i$ proceeds as follows. First, it checks $l$ and if it is set, it returns void and terminates (another thread has already acquired it); otherwise it tries to set it while carrying out $\alpha_i$, i.e. right before executing its last step of the
<figure><img src="image_5.png" /><figcaption>Fig. 8. Implementing TCCS<sup>m</sup> synchronization.</figcaption></figure>

communication protocol. If the variable is acquired by another thread while $t_i$ is finalizing $\alpha_i$ then $t_i$ issues a **retry** to retract any effect of $\alpha_i$. The OCTM code implementing this protocol is shown in Figure 9.

Encoding of TCCS<sup>m</sup> We can now define the encoding $\eta: \text{Proc} \to \text{State}$, mapping well-formed TCCS<sup>m</sup> terms to states of the OCTM abstract machine. Intuitively, a process $P \equiv \prod_{i=1}^m P_i$ is mapped into a state with a thread for each $P_i$ and a variable for each channel in $P$. Clearly, a state of this form can be easily generated by a single OCTM term which allocates all variables and forks the $m$ threads. We have preferred to map TCCS<sup>m</sup> terms to OCTM states for sake of simplicity.

The map $\eta$ is defined by recursion along the derivation of $\emptyset \vdash P : t$ and the number $m$ of parallel components in $P \equiv \prod_{i=1}^m P_i$. This is handled by the auxiliary encoding $\zeta: \text{Proc} \times \text{Heap} \to \text{State}$ (up to choice of fresh names) whose second argument is used to track memory allocations. The base case is given by $m = 0$ and yields a state with no threads i.e. $\langle 0, \Theta, \emptyset \rangle$. The recursive step is divided in three subcases depending on the structure and type of $P_1$ ($m > 0$).

1. If $\emptyset \vdash P_1 : c$ without top-level restrictions (i.e. $P_1 \not\equiv Q \setminus \{a_1, \dots, a_{n+1}\}$) then

$$ \zeta(\prod_{i=1}^{m+1} P_i, \Theta) \triangleq \langle [\varrho(P_1)]_{t_1} \mid \| S; \Sigma \rangle $$

where $\langle S; \Sigma \rangle = \zeta(\prod_{j=1}^{m-1} P_{j+1}, \Theta)$ is the translation of the rest of $P$ and $t_1$ is unique w.r.t. $S$ (i.e. $t_1 \notin \text{threads}(S)$). By hypothesis $P_1$ does not contain any top-level active transaction or parallel composition and hence can be translated directly into a OCTM-term by means of the encoding $\varrho$ (cf. Figure 10) – $\varrho(P)$ contain a free variable for each unrestricted channel occurring in $P$.

2. If $P_1$ has a top-level restriction (i.e. $P_1 \equiv Q \setminus \{a_1, \dots, a_{n+1}\}$) then

$$ \zeta(\prod_{i=1}^{m+1} P_i, \Theta) \triangleq \langle S_1[r_1/a_1, \dots, r_{n+1}/a_{n+1}] \mid \| S_2; \Theta_2[r_1, \dots, r_{n+1} \mapsto \text{MO}], \emptyset \rangle $$

where $\langle S_1; \Theta_1, \emptyset \rangle = \zeta(Q, \Theta)$ is the translation of the unrestricted process $Q$, $\langle S_2; \Theta_2, \emptyset \rangle = \zeta(\prod_{j=1}^{m-1} P_{j+1}, \Theta_1)$ is the translation of the rest of $P$, all threads have a unique identifier $\text{threads}(S_1) \cap \text{threads}(S_2) = \emptyset$, the heap is extended with $n$ channel variables fresh ($r_1, \dots, r_{n+1} \notin \text{dom}(\Theta_2)$) and known only to the translation of $Q$.
```pascal
data Channel = OTVar ChState
data ChState = M1 Nonce | M2 Nonce Nonce | M3 Nonce | M0

tau l P = isolated do
  case (readVar l) of
    False → return ()
    True → chooseThis l >> P

chooseThis l = writeVar l False

eqOrRetry x y
  | x == y = return ()
  | otherwise = retry

bang x = fork x >> bang x

recv c l P = do
  nq ← newNonce
  isolated do
    case (readVar l) of
      False → return ()
      True → do
        chooseThis l
        case (readVar c) of
          (M1 nx) → writeVar c (M2 nx nq)
            _ → retry
        isolated do
        case (readVar c) of
          (M3 ny) → eqOrRetry ny nq >> writeVar c M0 >> P
            _ → retry
        end
send c l P = do
  np ← newNonce
  isolated do
    case (readVar l) of
      False → return ()
      True → do
        chooseThis l
        case (readVar c) of
          M0 → writeVar c (M1 np)
            _ → retry
        isolated do
        case (readVar c) of
          (M2 nx ny) → eqOrRetry nx np >> writeVar c (M3 ny) >> P
            _ → retry
        end
```

<caption>Fig. 9. Encoding channels and communication</caption>
<figure><img src="image_6.png" /><figcaption>Fig. 10. Encoding TCCS<sup>m</sup> terms of type c</figcaption></figure>

3. If $P_1 \equiv \langle Q_1 \triangleright_k Q_2 \rangle$ is an active transaction then

$$
\begin{align*}
\varsigma(\prod_{i=1}^{m+1} P_i, \Theta) &\triangleq \langle S_{co} \parallel S_{ab} \parallel S_1[r_{co}/co] \parallel S_2; \Theta_2[r_l \mapsto \text{True}, r_{co} \mapsto \text{MO}], \emptyset \rangle \\
S_{co} &= (\text{recv } r_l \ r_{co} \triangleright \varrho(Q_1); \text{bang } (\text{recv } (\text{newVar True}) r_{co}))_{t_{co},k} \\
S_{ab} &= (\text{abort } () \triangleright \text{return})_{t_{ab},k}
\end{align*}
$$

where $\langle S_1; \Theta_1, \emptyset \rangle = \varsigma(Q_1, \Theta)$, $\langle S_2; \Theta_2, \emptyset \rangle = \varsigma(\prod_{j=1}^{m-1} P_{j+1}, \Theta_2)$ (like above),
the thread $S_{ab}$ is always ready to abort $k$ as in (TAB) and $S_{co}$ awaits on the
private channel $r_{co}$ a thread from $S_1$ to reach a commit and, after its commit,
collects all remaining synchronizations on $r_{co}$ to emulate the effect of $\Psi$
(cf. Figure 7). Finally, all threads have to be uniquely identified: $\text{threads}(S_1) \cap$
$\text{threads}(S_2) = \emptyset$ and $t_{co}, t_{ab} \notin \text{threads}(S_1) \cup \text{threads}(S_2)$

Remark 1. The third case of the definition above can be made more precise (at the cost of a longer definition) since the number of commits to be collected can be inferred from *Q* mimicking the definition of *Ψ*. This solution reduces the presence of dangling auxiliary processes and transaction fusions introduced by the cleaning process.

Like $\varrho$, $\varsigma(P, \Theta)$ contains a free variable for each unrestricted channel in $P$. Finally, the encoding $\eta$ is defined on each $P \in \text{Proc}$ as:

$$
\eta(P) \triangleq \langle S[r_1/a_1, \dots, r_n/a_n]; \Theta[r_1, \dots, r_n \mapsto \text{MO}], \emptyset \rangle
$$

where $\langle S; \Theta, \emptyset \rangle = \varsigma(P, \emptyset)$, $\{a_1, \dots, a_n\} \subseteq A$ is the set of channels occurring in $P$, and $\{r_1, \dots, r_n\} \subseteq \text{Loc}$.
**Adequacy of translation** In order to prove that the translation $\eta$ preserves the behaviour of $TCCS^m$ processes, we construct a simulation relation $S$ between well-formed $TCCS^m$ processes and states of $OCTM$. The basic idea is that a single step of $P$ is simulated by a sequence of reductions of $\eta(P)$, and $\eta(P)$ does not exhibit behaviours which are not exhibited by $P$. To this end we define an appropriate notion of star simulation, akin to [11]:

**Definition 2 (Star simulation).** A relation $S \subseteq \text{Proc} \times \text{State}$ is a star simulation if for all $(P, \langle S; \Sigma \rangle) \in S$:

1. for all $Q$ such that $P \xrightarrow{\tau} \sigma Q$ or $P \xrightarrow{k(\tau)} \sigma Q$, there exist $S'$, $\Sigma'$ such that $\langle S; \Sigma \rangle \to^* \langle S'; \Sigma' \rangle$ and $(Q, \langle S'; \Sigma' \rangle) \in S$;

2. for all $Q$ such that $P \xrightarrow{\beta} Q$, there exist $S'$, $\Sigma'$ such that $\langle S; \Sigma \rangle \xrightarrow{\beta^*} \langle S'; \Sigma' \rangle$ and $(Q, \langle S'; \Sigma' \rangle) \in S$.

3. for all $S'$, $\Sigma'$ such that $\langle S; \Sigma \rangle \to \langle S'; \Sigma' \rangle$, there exist $Q, S'', \Sigma''$ such that $(Q, \langle S''; \Sigma'' \rangle) \in S$ and one of the following holds:

- $P \xrightarrow{\tau} \sigma Q$ or $P \xrightarrow{k(\tau)} \sigma Q$, and $\langle S'; \Sigma' \rangle \to^* \langle S''; \Sigma'' \rangle$

- $P \xrightarrow{\beta} \epsilon Q$ and $\langle S'; \Sigma' \rangle \xrightarrow{\beta^*} \langle S''; \Sigma'' \rangle$.

where $\beta$-labels of the two transition relations are considered equivalent whenever they are both commits or both aborts for the same transaction name. We say that $P$ is star-simulated by $\langle S; \Sigma \rangle$ if there exists a star-simulation $S$ such that $(P, \langle S; \Sigma \rangle) \in S$. We denote by $\tilde{\approx}_t$ the largest star simulation.

Another technical issue is that two equivalent $TCCS^m$ processes can be translated to $OCTM$ states which differ only on non-observable aspects, like name renamings, terminated threads, etc. To this end, we need to consider $OCTM$ states up-to an equivalence relation $\cong_t \subseteq \text{State} \times \text{State}$, which we define next.

**Definition 3.** Two OCTM states are transaction-equivalent, written $\langle S_1; \Sigma_1 \rangle \cong_t \langle S_2; \Sigma_2 \rangle$, when they are equal up to:

- renaming of transaction and thread names;

- terminated threads, i.e. threads of one of the following forms: $((\text{return } M))_t$, $((\text{abort } M))_t$, $((\text{return} \triangleright \text{return})_{t,k})$, $((\text{abort} \triangleright \text{return})_{t,k})$, $((\text{psi})_t)$;

- threads blocked in synchronizations on co variables.

**Definition 4.** Let $P \in \text{Proc}$ be a well-formed process and $\langle S; \Sigma \rangle$ be a state. $P$ is star simulated by $\langle S; \Sigma \rangle$ up to $\cong_t$ if $(P, \langle S; \Sigma \rangle) \in \tilde{\approx}_t$.

We are now ready to state our main adequacy result, which is a direct consequence of the two next technical lemmata.

**Lemma 1.** For all $P, Q \in \text{Proc}$ the following hold true:

1. if $P \xrightarrow{\tau} \sigma Q$ or $P \xrightarrow{k(\tau)} \sigma Q$, there exist $S, \Sigma$ such that $\eta(P) \to^* \langle S; \Sigma \rangle$ and $\langle S; \Sigma \rangle \cong_t \eta(Q)$;

2. if $P \xrightarrow{\beta} Q$, there exist $S, \Sigma$ such that $\eta(P) \xrightarrow{\beta^*} \langle S; \Sigma \rangle$ and $\langle S; \Sigma \rangle \cong_t \eta(Q)$.

*Proof.* By induction on the syntax of $P$; see [15]. $\square$
**Lemma 2.** For $P \in \mathbf{Proc}$, for all $S, \Sigma$, if $\eta(P) \to \langle S; \Sigma \rangle$ then there exist $Q, S', \Sigma'$ such that $\langle S'; \Sigma' \rangle \cong_t \eta(Q)$ and one of the following holds:

- $P \xrightarrow{\tau} \sigma Q$ or $P \xrightarrow{k(\tau)} \sigma Q$, and $\langle S; \Sigma \rangle \to^* \langle S'; \Sigma' \rangle$;

- $P \xrightarrow{\beta} \epsilon Q$ and $\langle S; \Sigma \rangle \xrightarrow{\beta^*} \langle S'; \Sigma' \rangle$.

*Proof.* By induction on the semantics of $\eta(P)$; see [15]. □

**Theorem 1.** For all $P \in \mathbf{Proc}$, $P$ is star simulated by $\eta(P)$ up to $\cong_t$.

# 5 Conclusions and future work

In this paper we have introduced *OCTM*, a higher-order language extending the concurrency model of STM Haskell with composable *open (multi-thread)** transactions. In this language, processes can *join* transactions and transactions can *merge* at runtime. These interactions are driven only by access to shared transactional memory, and hence are implicit and loosely coupled. To this end, we have separated the isolation aspect from atomicity: the *atomic* construct ensures “all-or-nothing” execution but not isolation, while the new constructor *isolated* can be used to guarantee isolation when needed. In order to show the expressive power of *OCTM*, we have provided an adequate implementation in it of *TCCS<sup>m</sup>*; a recently introduced model of open transactions with CCS-like communication. As a side result, we have given a simple typing system for capturing *TCCS<sup>m</sup>* well-formed terms.

Several directions for future work stem from the present paper. First, we plan to implement *OCTM* along the line of STM Haskell, but clearly the basic ideas of *OCTM* are quite general and can be applied to other STM implementations, like C/C++ LibCMT and Java Multiverse. Then, we can use *TCCS<sup>m</sup>* as an *exogenous orchestration language* for *OCTM*: the *behaviour* of a transactional distributed system can be described as a *TCCS<sup>m</sup>* term, which can be translated into a *skeleton* in *OCTM* using the encoding provided in this paper; then, the programmer has only to “fill in the gaps”. Thus, *TCCS<sup>m</sup>* can be seen as a kind of “global behavioural type” for *OCTM*.

In fact, defining a proper behavioural typing system for transactional languages like *OCTM* is another interesting future work. Some preliminary experiments have shown that *TCCS<sup>m</sup>* is not enough expressive for modelling the dynamic creation of resources (locations, threads, etc.). We think that a good candidate could be a variant of *TCCS<sup>m</sup>* with local names and scope extrusions, i.e., a “transactional π-calculus”.

Being based on CCS, communication in *TCCS<sup>m</sup>* is synchronous; however, nowadays asynchronous models play an important rôle (see e.g. actors, event-driven programming, etc.). It may be interesting to generalize the discussion so as to consider also this case, e.g. by defining an actor-based calculus with open transactions. Such a calculus can be quite useful also for modelling speculative reasoning for cooperating systems [13, 14]. A local version of actor-based open transactions can be implemented in *OCTM* using lock-free data structures (e.g., message queues) in shared transactional memory.
*Acknowledgements* We thank the anonymous referees for useful remarks and suggestions on the preliminary version of this paper. This work is partially supported by MIUR PRIN project 2010LHT4KM, CINA.

References

1. M. Abadi, A. Birrell, T. Harris, and M. Isard. Semantics of transactional memory and automatic mutual exclusion. *ACM Trans. Program. Lang. Syst.*, 33(1):2, 2011.

2. R. Bruni, H. C. Melgratti, and U. Montanari. Nested commits for mobile calculi: Extending join. In J. Lévy, E. W. Mayr, and J. C. Mitchell, editors, *Proc. TCS*, volume 155 of *IFIP*, pages 563–576. Kluwer/Springer, 2004.

3. V. Danos and J. Krivine. Transactions in RCCS. In M. Abadi and L. de Alfaro, editors, *Proc. CONCUR*, volume 3653 of *Lecture Notes in Computer Science*, pages 398–412. Springer, 2005.

4. E. de Vries, V. Koutavas, and M. Hennessy. Communicating transactions (extended abstract). In P. Gastin and F. Laroussinie, editors, *Proc. CONCUR*, volume 6269 of *Lecture Notes in Computer Science*, pages 569–583. Springer, 2010.

5. E. de Vries, V. Koutavas, and M. Hennessy. Liveness of communicating transactions (extended abstract). In K. Ueda, editor, *Proc. APLAS*, volume 6461 of *Lecture Notes in Computer Science*, pages 392–407. Springer, 2010.

6. J. Gray and L. Lamport. Consensus on transaction commit. *ACM Transactions Database Systems*, 31(1):133–160, 2006.

7. T. Harris, S. Marlow, S. L. P. Jones, and M. Herlihy. Composable memory transactions. In *Proc. PPOPP*, pages 48–60, 2005.

8. M. Herlihy and J. E. B. Moss. Transactional memory: Architectural support for lock-free data structures. In A. J. Smith, editor, *Proceedings of the 20th Annual International Symposium on Computer Architecture*, pages 289–300. ACM, 1993.

9. M. Herlihy and N. Shavit. Transactional memory: beyond the first two decades. *SIGACT News*, 43(4):101–103, 2012.

10. V. Koutavas, C. Spaccasassi, and M. Hennessy. Bisimulations for communicating transactions - (extended abstract). In A. Muscholl, editor, *Proc. FOSSACS*, volume 8412 of *Lecture Notes in Computer Science*, pages 320–334. Springer, 2014.

11. X. Leroy. A formally verified compiler back-end. *Journal of Automated Reasoning*, 43(4):363–446, 2009.

12. M. Lesani and J. Palsberg. Communicating memory transactions. In C. Cascaval and P. Yew, editors, *Proc. PPOPP*, pages 157–168. ACM, 2011.

13. J. Ma, K. Broda, R. Goebel, H. Hosobe, A. Russo, and K. Satoh. Speculative abductive reasoning for hierarchical agent systems. In J. Dix, J. Leite, G. Governatori, and W. Jamroga, editors, *Proc. CLMAS*, volume 6245 of *Lecture Notes in Computer Science*, pages 49–64. Springer, 2010.

14. A. Mansutti, M. Miculan, and M. Peressotti. Multi-agent systems design and prototyping with bigraphical reactive systems. In K. Magoutis and P. Pietzuch, editors, *Proc. DAIS*, volume 8460 of *Lecture Notes in Computer Science*, pages 201–208. Springer, 2014.

15. M. Miculan, M. Peressotti, and A. Toneguzzo. Open transactions on shared memory. *CoRR*, abs/1503.09097, 2015.

16. R. Milner. *A Calculus of Communicating Systems*, volume 92 of *Lecture Notes in Computer Science*. Springer, 1980.

17. N. Shavit and D. Touitou. Software transactional memory. *Distributed Computing*, 10(2):99–116, 1997.