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

1. if a value is present, get the contained value immediately
2. 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 ().

data Fork = Fork

createFork :: IO (TMVar Fork)
createFork = newTMVarIO Fork

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:

main :: IO ()
main = dinnerParty 5

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 MVars which store the sleeping threads in a FIFO queue.

• In an early version of this post I used

badLogSTM :: String -> STM ()
badLogSTM = unsafeIOToSTM . putStrln

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).