Software Transactional memory (STM) is an emerging abstraction for concurrent programming alternative to lock-based synchronizations. Most STM models admit only isolated transactions, which are not adequate in multithreaded programming where transactions need to interact via shared data before committing. To overcome this limitation, in this paper we present Atomic Transactional Memory (ATM), a programming abstraction supporting safe, data-driven interactions between composable memory transactions. This is achieved by relaxing isolation between transactions, still ensuring atomicity. 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.
Modern multicore architectures have emphasized the importance of abstractions
supporting correct and scalable multi-threaded programming. In this model,
threads can collaborate by interacting on shared data structures, such as tables,
message queues, buffers, etc., whose access must be regulated to avoid
inconsistencies. Traditional lock-based mechanisms (like semaphores and monitors)
are notoriously difficult and error-prone, as they easily lead to deadlocks, race
conditions and priority inversions; moreover, they are not composable and hinder
parallelism, thus reducing efficiency and scalability. Transactional memory (TM)
has emerged as a promising abstraction to replace locks [
However, in multi-threaded programming transactions may need to interact and exchange data before committing. In this situation, transaction isolation is a severe shortcoming. A simple example is a request-response interaction between two transactions via a shared buffer. We could try to synchronize the threads accessing the buffer b by means of two semaphores c1, c2 as follows: // Party1 (Master) atomically { <put request in b> up(c1); <some other code; may abort> down(c2); // wait for answer <get answer from b; may abort> } // Party2 (Worker) atomically { down(c1); // wait for data <get request from b> <compute answer; may abort> <put answer in b> up(c2); } Unfortunately, this solution does not work: any admissible execution requires an interleaved scheduling between the two transactions, thus violating isolation; hence, the transactions deadlock as none of them can progress. It is important to notice that this deadlock arises because interaction occurs between threads of different transactions; in fact, the solution above is perfectly fine for threads outside transactions or within the same transaction.
To overcome this limitation, in this paper we propose a programming model for safe, data-driven interactions between memory transactions. The key observation is that atomicity and isolation are two disjoint computational aspects: – an atomic non-isolated block is executed “all-or-nothing”, but its execution can overlap others’ and uncontrolled access to shared data is allowed; – a non-atomic isolated block is executed “as if it were the only one” (i.e., in mutual exclusion with others), but no rollback on errors is provided. Thus, a “normal” block of code is neither atomic nor isolated; a mutex block (like Java synchronized methods) is isolated but not atomic; and a usual STM transaction is a block which is both atomic and isolated.
Our claim is that atomic non-isolated blocks can be fruitfully used for
implementing safe composable interacting memory transactions. In this model, which
we call Atomic Transactional Memory (ATM), a transaction is composed by
several threads, called participants, which can cooperate on shared data. A
transaction commits when all its participants commit, and aborts if any thread aborts.
Threads participating to different transactions can access to shared data, but
when this happens the transactions are transparently merged into a single one.
For instance, the two transactions of the synchronization example above would
automatically merge becoming the same transaction, so that the two threads can
synchronize and proceed. Thus, this model relaxes the isolation requirement still
guaranteeing atomicity and consistency; moreover, it allows for loosely-coupled
interactions since transaction merging is driven only by run-time accesses to shared
data, without any explicit coordination among the participants beforehand.
Related work. Many authors have proposed mechanisms to allow transactions
to interact. Perhaps the work closest to ours are transaction communicators
(TC) [
Other authors have proposed events- and message passing -based mechanisms;
we mention transactional events (TE) [
In this section we give a brief overview of the interface for atomic transactions for Haskell. In fact, ATM can be implemented in any programming language, provided we have some means to forbid irreversible effects inside transactions; we have chosen Haskell because its typing system allows us to implement this restriction quite easily. Namely, we define two monads ATM and ITM (see Figure 1), representing the computational aspects of atomic multi-threaded atomic, nonisolated transactions and atomic single-threaded isolated transactions, respectively. Transactional memory locations are values of type ATVar and can be manipulated by isolated transactional actions only.
Using the construct atomic, programs in the ATM monad are executed “all-ornothing” but without isolation; hence these transactions can merge at runtime. -- Types for transactional actions -----------------------------------------data ITM a -- isolated atomic transactional action, return a value of type a data ATM a -- non-isolated atomic transaction, return a value of type a -- Sequencing, do notation. Here t is a placeholder for ITM or ATM ---------(>>=) :: t a -> (a -> t b) -> t b return :: a -> t a -- Running isolated and atomic actions -------------------------------------atomic :: ATM a -> IO a -- deliver the IO action for an atomic one isolated :: ITM a -> ATM a -- deliver the atomic action for an isolated one retry :: ITM a -- retry the current transaction orElse :: ITM a -> ITM a -> ITM a -- fall back on the second action when -- the first action issues a retry -- Exceptions --------------------------------------------------------------throw :: Exception e => e -> t a catch :: Exception e => t a -> (e -> t a) -> t a -- Threading ---------------------------------------------------------------fork :: ATM () -> ATM ThreadId -- Transactional shared memory ---------------------------------------------data ATVar a -- sharable memory location holding values of type a newATVar :: a -> ITM (ATVar a) readATVar :: ATVar a -> ITM a writeATVar :: ATVar a -> a -> ITM ()
When needed, actions inside transactions can be executed in isolation by using the
construct isolated. Both ATM and ITM transactions are composable; we exploit
Haskell type system to prevent irreversible effects inside these monads. ATM is
a conservative extension of STM [
ATM as ATVars holding a counter and operation up and down as atomic and isolated actions. The first increments the counter held by the semaphore and the second decrements it when the counter is positive or retries the transaction otherwise thus blocking the thread. tu type Semaphore = ATVar Int up :: Semaphore -> ITM () up s = modifyATVar s (1+) down :: Semaphore -> ITM () down s = do assertATVar s (> 0) modifyATVar s (-1+) Example 2.2. A Petri net is readily implemented in ATM by representing each transition by a thread and each place by a semaphore. Putting and taking a token from a place correspond to increasing (up) or decreasing (down) its semaphore— the latter blocks if no tokens are available. Each thread repeatedly simulates the firing of the transition it represents, by taking tokens from its input places and putting tokens in its output places. These semaphore operations must be performed atomically but not in isolation: isolation would prevent transitions sharing a place to fire concurrently. Using ATM, all this is achieved in few lines: type Place = Semaphore transition :: [Place] -> [Place] -> IO ThreadId transition inputs outputs = forkIO (forever fire) where fire = atomic $ do mapM_ (isolated . down) inputs mapM_ (isolated . up) outputs Observe that, since firing is atomic but not isolated, this is an implementation of true concurrent Petri nets, which is usually more difficult to achieve than interleaving semantics. Here is a simple Petri net and its implementation: main = do p1 p2 p1 <- atomically (newPlace 1)
p2 <- atomically (newPlace 0) t1 t2 p3 <- atomically (newPlace 0) p4 <- atomically (newPlace 0) transition [p1] [p3, p4] p3 p4 transition [p1, p2] [p4] When t1 or t2 race to take the token in p1, if t2 takes it first the transaction will eventually retry since there is no token in p2. tu
In this section we provide the formal semantics of ATM. Following [
The language syntax is given by the following grammar: Values V ::= r j \x -> M j return M j M >>= N j throw M j catch M N j putChar c j getChar j fork M j atomic M j isolated M j retry j M ‘orElse‘ N j newATVar M j readATVar r j writeATVar r M
Terms M ::= x j V j M N where the meta-variables x and r range over a given countable set of variables Var and of location names Loc, respectively. We assume Haskell typing conventions and denote the set of all well-typed terms by Term.
Terms are evaluated by an abstract state machine whose states are pairs hP ; i formed by: (a) a thread family (or process) P = Tt1 k k Ttn where ti are unique thread identifiers; (b) a memory = h ; ; i, where : Loc * Term is the heap and : Loc * Term TrName is the working memory ; TrName is a set of names used to identify active transactions; is a forest of threads identifiers keeping track of how threads have been forked. Threads are the smaller unit of execution the machine scheduler operates on; they evaluate ATM terms and do not have any private transactional memory. A thread Tt has two forms: ([M ])t for threads evaluating a term M outside a transaction and ([M ; N ])t;k for threads evaluating M inside transaction k with continuation N (the term to evaluate after that k has committed).
As for traditional closed (ACID) transactions (e.g., [
Semantics The machine dynamics is defined by the two transition relations induced by the rules in Figures 3 to 6; auxiliary definitions are in Figure 7.
The first relation M ! N is defined on terms only, and models pure computations (Figure 3). In particular, rule Eval allows a term M that is not a value to be evaluated by means of an auxiliary (partial) function V[M ] yielding the value V ; the other rules define the semantics of the monadic bind and exception handling in a standard way. It is interesting to notice the symmetry between
Eval return M >>= N ! N M r 2 fretry; return N g CatchVal r ‘catch‘ M ! r
BindVal e 2 fretry; throw N g BindEx
e >>= M ! e throw M ‘catch‘ N ! N M
CatchEx h([atomic M >>= N ])t; i newhk!i h([M ; N ])t;k; i 0 = commit(k; )
0 = cleanup(k; ) 0 = leak(k; ) h([return M ; N ])t;k; i cohk!i h([return M >>= N ])t; 0i 0 = cleanup(k; ) 0 = remove(r; ) r = root(t; New
Commit h([throw M ; N ])t;k; i abhk;t;M!i h([throw M >>= N ])t; 0i hP ; i bind and catch and how retry is treated as an exception by rule BindEx and as a result value by rule CatchVal.
Relation ! is used to define the labelled transition relation hP ; i ! hP 0; 0i over states. This relation is non deterministic, to model the fact that the scheduler can choose among various threads to execute next; therefore, several rules can apply to a given state according to different evaluation contexts:
E ::=[ ] j E >>= M Transaction: Tt;k ::=([E; M ])t;k k P Plain process: Pt ::=([E])t k P Any process: At ::=Pt j Tt;k
::=
j newhki j cohki j abhk; t; M i j abhk; t; M i j ?c j !c where k 2 TrName; M 2 Term as usual.
Transitions labelled by represent internal steps of transactions, i.e., which do not need any coordination: reduction of pure terms, memory operations and
k Ttn ) , ft1; : : : tng transaction( ) , k for
2 fnewhki; cohki; abhk; t; M i; abhk; t; M ig ( [k 7! j])(r) , ( (r)
if (r) = (M; l); l 6= k (M; j) if (r) = (M; k) 8>transactions(P1) [ transactions(P2) if P = P1 k P2 transactions(P ) , <fkg if P = ([M ; N ])t;k >:; otherwise P [k 7! j] , 8>P1[k 7! j] k P2[k 7! j] if P = P1 k P2 <([M ; N ])t;j if P = ([M ; N ])t;k >:P otherwise [r 7! M ](s) , if r = s then M else (s) [r 7! (M; k)](s) , if r = s then (M; k) else (s) cleanup(k; )(r) , if commit(k; )(r) , if (r) = (M; k) then ? else (r) = (M; k) then M else (r) (r) leak(k; )(r) , M if (r) = M or (r) = ? and (r) = (M; k) thread creation (see rules in Figure 5). Reading a location falls into two cases: rule Read1 models the reading of an unclaimed location and its effect is to record the claim in , while rule Read2 models the reading of a claimed location and its effect is to merge the transactions of the current thread with that claiming the location. Writes behave similarly. Rules Or1 and Or2 describe the semantics of alternative sub-transactions: if the first one retry-es the second is executed discarding any effect of the first. Rule ForkT spawns a new thread for the current transaction; a term fork M can appear inside atomic, thus allowing multi-threaded atomic transactions, but its use inside isolated is prevented by the type system and by the shape of rule Isolated as well.
The remaining labels describe state transitions concerning the life-cycle of transactions: creation, commit, abort, and restart (see rules in Figure 6). These operations require a coordination among threads; for instance, an abort from a thread has to be propagated to every thread participating to the same transaction. This is captured in the semantics by labelling the transition with the operation and the name of the transaction involved; this information is used to force synchronisation of all participants of that transaction. To illustrate this mechanism, we describe the commit of a transaction k, namely hP ; i cohk!i hP 0; 0i. First, by means of rule MCastGroup we split P into two subprocesses, one of which contains all threads participating in k (those not in k cannot do a transition whose label contains k). Secondly, using recursively rule MCastCo we single out every thread in k. Finally, we apply rule Commit provided that every thread is ready to commit, i.e., it is of the form ([return M ; N ])t;k.
Aborting a transaction works similarly, but it based on vetoes instead of an
unanimous vote. Aborts are triggered by unhandled exceptions raised by some
thread, but threads react to this situation in different ways:
– threads forked within the transaction, in the same tree of the thread raising
the exception: these threads are killed (and the root thread aborted) because
their creation must be discarded, as for any transactional side-effect;
– threads from different trees which joined the transaction after it was created,
due to a merging: these threads just retry their transaction, since aborting
would require them to handle exceptions raised by “foreign” threads.
Like Haskell STM [
Note that there are no derivation rules for retry: its meaning is to inform the scheduler that we have reached a state where the execution is stuck; hence the machine has to re-execute the transaction from the beginning (or backtracking from a suitable check-point), possibly following a different execution order. 4
In this section we validate the formal semantics of ATM by proving it satisfies the
opacity correctness criterion for transactional memory [
In order to formally capture these intuitive requirements let us recall some
notions from [
We can now recall Guerraoui-Kapałka’s definition3 of opacity [3, Def. 1]. Definition 4.1 (Opacity). A history H is said to be opaque if there exists a sequential history S equivalent to some history in complete(H) such that S preserves the happens-before order of H. 3 The original definition requires the history H to be “legal”, but this notion is relevant only in presence of non-transactional operations which ATM prevents by design.
As shown in [
2. k reads something written by k0; 3. k0 reads some location written by k and k0 k; 4. k0 is neither running nor aborted and there are a location r and a transaction k00 such that k0 k00, k0 writes to r, and k00 reads r from k.
The edge is red if the second case applies, otherwise it is black. The graph is said to be well-formed if all edges from red nodes in OP G(H; ) are also red.
Let H be a history and let k be a transaction appearing in it. A read operation by k is said to be local (to k) whenever the previous operation by k on the same location was a write. A write operation by k is said to be local (to k) whenever the next operation by k on the same location is a write. We denote by nonlocal (H) the longest sub-history of H without any local operations. A history H is said locally-consistent if every local read is preceded by a write operation that writes the read value; it is said consistent if, additionally, whenever some k reads v from r in nonlocal (H) then some k0 writes v to r in nonlocal (H).
Theorem 4.1 ([3, Thm. 2]). A history H is opaque if and only if (a) H is consistent and (b) there exists a total order on the set of transactions in H such that OP G(nonlocal (H); ) is well-formed and acyclic.
In [
Proof. By inspection of the rules it is easy to see that (a) transactions may access only locations they claimed; (b) claimed locations are released only on commits, aborts and retries; (c) transactions have to merge with any transaction holding a location they need. Therefore, at any given time there is at most one running transaction issuing operations on a given location, hence reads and writes do not create edges. Thus edges are created only during the execution of merges and, by inspecting the above implementation, it easy to see that (d) any transaction can issue at most one merge; (e) a transaction issuing a merge is a red node; (f ) the edge created by a merge is red. Therefore, transactions form a forest made of red edges where any non-root node is red. tu
Since a forest formed by red edges whose sources are always red is always acyclic and well-formed, we can conclude our correctness result: Corollary 4.1 (Opacity). ATM meets the opacity criterion. 5
In this paper we have presented ATM, a programming model supporting interactions between composable memory transactions. This model separates isolated transactions from non-isolated ones, still guaranteeing atomicity; the latter can interact by accessing to shared variables. Consistency is ensured by transparently merging interacting transactions at runtime. We have given a formal semantics for ATM, and proved that this model satisfies the important opacity criterion.
As future work, it would be interesting to add some heuristics to better
handle retry events. Currently, a retry restarts all threads participating to the
transaction; a more efficient implementation would keep track of the working
set of each thread, and at a retry we need to restart only the threads whose
working sets have non-empty intersection with that being restarted. Another
optimization is to implement transactions and ATVars directly in the runtime,
akin the implementation of STM in the Glasgow Haskell Compiler [
We have presented ATM within Haskell (especially to leverage its type system), but this model is general and can be applied to other languages. A possible future work is to port this model to an imperative object oriented language, such as Java or C++; however, like other TM implementations, we expect that this extension will require some changes in the compiler and/or the runtime.
This work builds on the calculus with shared memory and atomic transactions
described in [