Introduction
Haskell has this library called stm
which implements Software Transactional Memory (STM). In a nutshell, STM allows you to group different variable-changing statements into atomic blocks. For an in-depth explanation I recommend the STM chapter of Parallel and Concurrent Haskell by Simon Marlow.
For our Haskell meetup, I tried to come up with a demo, so here’s a solution for the Dining Philosophers problem using STM.

Five silent philosophers sit at a round table with bowls of spaghetti. Forks are placed between each pair of adjacent philosophers.
Each philosopher must alternately think and eat. However, a philosopher can only eat spaghetti when they have both left and right forks. Each fork can be held by only one philosopher and so a philosopher can use the fork only if it is not being used by another philosopher. After an individual philosopher finishes eating, they need to put down both forks so that the forks become available to others. A philosopher can only take the fork on their right or the one on their left as they become available and they cannot start eating before getting both forks.
(from Wikipedia)
This blog post is a literal Haskell file, so let’s start with the imports.
{-# OPTIONS_GHC -threaded #-}
module Main where
import Control.Concurrent
import Control.Concurrent.STM.TMVar
import Control.Concurrent.STM.TVar
import Control.Concurrent.STM.TChan
import Control.Monad (forever, replicateM)
import Control.Monad.STM
import System.Random (randomRIO)
import GHC.Conc (unsafeIOToSTM) -- only for instructive purposes
The solution to this problem is an algorithm that each philosopher can execute concurrently and that makes sure that every philosopher eats regularly. The usual solution (e.g. in a distributed systems lecture) is a resource hierarchy. But I claim we don’t even have to think about any specific solution. With STM we just write the philosophers’ actions naively down and let STM handle the synchronization.
The general outline of our program is this:
dinnerParty :: Int -> IO ()
dinnerParty n = do
-- Ignore for now, explanation later
output <- setupLogOutput
-- create n forks
forks <- replicateM n createFork
-- create n philosophers
philosophers <- mapM (forkIO . philosopher output forks) [0..n-1]
-- let's keep the party alive for 10 seconds
threadDelay (10 * 1000 * 1000)
mapM_ killThread philosophers
Forks
Every fork can only be used by one philosopher at a time, therefore we wrap the fork into a TMVar
, stm
’s version of an MVar
. If you don’t know what an MVar
(Hoogle) is: Basically, an MVar a
is container that is either empty or contains one value of type a
. One can read the MVar and either
- if a value is present, get the contained value immediately
- if no value is present, the thread is suspended
Therefore, an MVar ()
is just a Mutex.
But to avoid confusion, we use Fork
instead of ()
.
Philosophers
philosopher :: TChan String -> [TMVar Fork] -> Int -> IO ()
philosopher output forks i = forever go
where
go = do
-- think
randomSleep
-- grab the forks
atomically $ do
takeTMVar leftFork
takeTMVar rightFork
log "is eating"
randomSleep
-- put the forks back
atomically $ do
putTMVar leftFork Fork
putTMVar rightFork Fork
leftFork = forks !! i
rightFork = forks !! ((i + 1) `mod` length forks)
log s = atomically $ writeTChan output $ "P " ++ show i ++ " " ++ s
randomSleep = randomRIO (10*1000,100*1000) >>= threadDelay
Main
When we execute the main function:
we will see something similar to this:
> runghc --ghc-arg="-package stm" stm.lhs
P 2 is eating
P 3 is eating
P 1 is eating
P 0 is eating
P 0 is eating
P 4 is eating
P 2 is eating
P 1 is eating
P 3 is eating
P 4 is eating
P 4 is eating
P 0 is eating
...
We can quickly check that all philosophers eat once in a while by counting unique occurences.
runghc --ghc-arg="-package stm" stm.lhs | sort | uniq -c
24 P 0 is eating
28 P 1 is eating
34 P 2 is eating
35 P 3 is eating
32 P 4 is eating
Mission accomplished.
Caveats
STM does not ensure fairness. This is in contrast to plain
MVar
s which store the sleeping threads in a FIFO queue.In an early version of this post I used
which lead to deadlocks. Obviously, using a function prefixed with ‘unsafe’ is a bad idea, but I thought I could get away with it because it seemed side-effect free. It turns out, it wasn’t. Handles like stdout
are protected with a lock to prevent garbled output.
STM sometimes has to abort a transaction and restart it later. If the IO code (e.g. putStrLn
) inside the transaction just aquired the lock right before getting aborted, the lock cannot be released anymore). That’s why we need to create a channel and a dedicated thread that writes from the channel to stdout like this:
setupLogOutput :: IO (TChan String)
setupLogOutput = do
output <- newTChanIO
forkIO $ forever $ atomically (readTChan output) >>= putStrLn
return output
Edit:
- (2020-04-08) Thanks to ‘u/bbdbdd’ for pointing out an improvement that makes the implementation more faithful to the original statement. The first published version performed the whole take-forks-eat-put-forks in one big STM transaction. So, from inside the STM block it looked like no blocking ever happens which is not really what the problem statement is about. Also, it had that little ugliness that de facto the “is eating” might have been performed more often than necessary. But of course that was not observable from outside STM (e.g. in the log output).