Mutexes in Idris
In the previous example, we saw how to manage simple counter state using atomic operations. For more complex state, we can use a mutex to safely access data across multiple threads.
import Data.IORef
import System.Concurrency
-- Container holds a map of counters; since we want to
-- update it concurrently from multiple threads, we
-- add a MVar to synchronize access.
-- Note that MVars must not be copied, so if this
-- record is passed around, it should be done by
-- reference.
record Container where
constructor MkContainer
mu : MVar ()
counters : IORef (Map String Int)
-- Lock the MVar before accessing `counters`; unlock
-- it at the end of the function using a finally block.
inc : Container -> String -> IO ()
inc c name = do
takeMVar c.mu
finally (do
map <- readIORef c.counters
let updatedMap = insert name (1 + (Map.lookup name map |> fromMaybe 0)) map
writeIORef c.counters updatedMap)
(putMVar c.mu ())
-- Note that the initial value of an MVar is full, so no
-- initialization is required here.
main : IO ()
main = do
countersRef <- newIORef (fromList [("a", 0), ("b", 0)])
c <- MkContainer <$> newEmptyMVar <*> pure countersRef
-- This function increments a named counter
-- in a loop.
let doIncrement : String -> Int -> IO ()
doIncrement name n = replicateM_ n (inc c name)
-- Run several threads concurrently; note
-- that they all access the same Container,
-- and two of them access the same counter.
forkIO $ doIncrement "a" 10000
forkIO $ doIncrement "a" 10000
forkIO $ doIncrement "b" 10000
-- Wait for the threads to finish
-- (In a real application, you'd use a proper synchronization mechanism)
threadDelay 1000000 -- Wait for 1 second
finalCounters <- readIORef c.counters
putStrLn $ "Final counters: " ++ show finalCounters
Running the program shows that the counters updated as expected.
$ idris -p contrib mutexes.idr -o mutexes
$ ./mutexes
Final counters: fromList [("a", 20000), ("b", 10000)]
In this Idris version, we use MVar
for mutual exclusion, which is similar to a mutex. We also use IORef
for mutable references, as Idris doesn’t have mutable variables by default. The Container
is implemented as a record containing an MVar
for synchronization and an IORef
for the mutable map of counters.
The inc
function now takes and releases the MVar
explicitly, using a finally
block to ensure the MVar
is always released, even if an exception occurs.
In the main
function, we create threads using forkIO
instead of goroutines. Note that Idris doesn’t have a built-in way to wait for threads to complete, so we use a simple threadDelay
as a placeholder. In a real application, you’d want to use a proper synchronization mechanism.
This example demonstrates how to use mutexes (via MVar
) to safely access shared state across multiple threads in Idris.