So our approach is to use Haskell as a kind of “
laboratory” in which to study the ideas of transactional memory
in a setting with a very expressive type system. As we go, we
will mention primitives from the STM library, whose interface is summarized in Figure 1. In this paper, we focus on
examples of how STM can be used in building simple concurrency abstractions. Our original paper9 formally defines
the details of the design via an operational semantics
which we developed alongside our implementations; we
found this invaluable in highlighting interactions between
the constructs—for example, what happens if an exception is raised deep inside an atomic block, nested within
catch handlers and orElse? For the moment we return to
simpler examples.
figure 1: the stm interface.
-- The STM monad itself
data STM a
instance Monad STM
-- Monads support “do” notation and sequencing
-- Exceptions
throw :: Exception -> STM a
catch :: STM a -> (Exception->STM a) -> STM a
-- Running STM computations
atomic :: STM a -> IO a
retry :: STM a
orElse :: STM a -> STM a -> STM a
-- Transactional variables
data TVar a
newTVar :: a -> STM (TVar a)
readTVar :: TVar a -> STM a
writeTVar :: TVar a -> a -> STM ()
3. 1. transactional variables and atomicity
Suppose we wish to implement a resource manager, which
holds an integer-valued resource. The call (getR r n) should
acquire n units of resource r, blocking if r holds insufficient resource; the call (putR r n) should return n units of resource
to r.
Here is how we might program putR in STM-Haskell:
type Resource = TVar Int
putR :: Resource -> Int -> STM ()
putR r i = do { v <- readTVar r
; writeTVar r (v + i)}
The currently available resource is held in a transactional
variable of type TVar Int. The type declaration simply
gives a name to this type. The function putR reads the value
v of the resource from its cell, and writes back (v + i) into
the same cell. (We discuss getR next, in Section 3. 2.)
The read TVar and write TVar operations both return
STM actions (Figure 1), but Haskell allows us to use the same
do {. . .} syntax to compose STM actions as we did for I/O actions. These STM actions remain tentative during their execution: to expose an STM action to the rest of the system, it
can be passed to a new function atomic, with type:
atomic :: STM a -> IO a
It takes a memory transaction, of type STM a, and delivers
an I/O action that, when performed, runs the transaction
atomically with respect to all other memory transactions.
One might say:
main = do {...; atomic (putR r 3); ...}
The underlying transactional memory deals with maintaining a per-thread transaction log to record the tentative accesses made to TVars. When atomic is invoked, the STM checks
that the logged accesses are valid—i.e., no concurrent transaction has committed conflicting updates to those TVars. If
the log is valid then the STM commits it atomically to the heap,
thereby exposing its effects to other transactions. Otherwise
the memory transaction is rerun with a fresh log.
Splitting the world into STM actions and I/O actions provides two valuable properties, both statically checked by the
type system:
• There is no way to perform general I/O within a transaction, because there is no operation that takes an IO
computation and performs it in the STM monad. Hence
only STM actions and pure computation can be performed inside a memory transaction. This is precisely
the guarantee we sought in Section 2. 1. It statically prevents the programmer from calling launchMissiles
inside a transaction, because launching missiles is an
I/O action with type IO (), and cannot be composed
with STM actions.
• No STM actions can be performed outside a transaction, so the programmer cannot accidentally read or
write a TVar without the protection of atomic. Of
course, one can always say atomic (read TVar v) to
read a TVar in a trivial transaction, but the call to
atomic cannot be omitted.
3. 2. Blocking memory transactions
Any concurrency mechanism must provide a way for a
thread to await an event or events caused by other threads.
In lock-based programming, this is typically done using condition variables; message-based systems offer a
construct to wait for messages on a number of channels;
POSIX provides select; Win32 provides WaitForMul-tipleObjects; and STM systems to date allow the programmer to guard the atomic block with a Boolean condition (see Section 2. 1).
The Haskell setting led us to a remarkably simple new
mechanism for blocking. Furthermore, as we show in Sections 3. 3 and 3. 4, it supports composition in ways that are
not possible with lock-based programming.