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.

Atomic Counters in Idris

Stateful Goroutines in Idris

Learn X By Example

Title here

Mutexes in Idris