# 100 Prisoners

There’s a popular logic puzzle which goes something like this:

There are 100 prisoners in solitary cells. There’s a central living room with one light bulb; this bulb is initially off. No prisoner can see the light bulb from his or her own cell. Everyday, the warden picks a prisoner equally at random, and that prisoner visits the living room. While there, the prisoner can toggle the bulb if he or she wishes. Also, the prisoner has the option of asserting that all 100 prisoners have been to the living room by now. If this assertion is false, all 100 prisoners are shot. However, if it is indeed true, all prisoners are set free and inducted into MENSA, since the world could always use more smart people. Thus, the assertion should only be made if the prisoner is 100% certain of its validity. The prisoners are allowed to get together one night in the courtyard, to discuss a plan. What plan should they agree on, so that eventually, someone will make a correct assertion?

We can express this as a concurrency problem: the warden is the scheduler, each prisoner is a thread, and when the program terminates every prisoner should have visited the living room.

Let’s set up some imports:

{-# LANGUAGE RankNTypes #-}

import qualified Control.Concurrent.Classy as C
import           Data.Foldable             (for_)
import           Data.List                 (genericLength)
import           Data.Maybe                (mapMaybe)
import qualified Data.Set                  as S
import qualified Test.DejaFu               as D
import qualified Test.DejaFu.Common        as D
import qualified Test.DejaFu.SCT           as D


## Correctness

Before we try to implement a solution, let’s think about how we can check if an execution corresponds to the prisoners succeeding an entering MENSA, or failing and being shot.

Prisoners are threads, and the warden is the scheduler. So if every thread (prisoner) that is forked is scheduled (taken to the room), then the prisoners are successful:

-- | Check if an execution corresponds to a correct guess.
isCorrect :: D.Trace -> Bool
isCorrect trc = S.fromList (threads trc) == S.fromList (visits trc)

-- | Get all threads created.
go (_, _, D.Fork tid) = Just tid
go _ = Nothing

-- | Get all scheduled threads
visits = mapMaybe go where
go (D.Start    tid, _, _) = Just tid
go (D.SwitchTo tid, _, _) = Just tid
go _ = Nothing


So now, given some way of setting up the game and running it to completion, we can test it and print some statistics:

-- | Run the prison game and print statistics.
run :: D.Way -> (forall m. C.MonadConc m => m ()) -> IO ()
run way game = do
traces <- map snd <$> D.runSCT way D.defaultMemType game let successes = filter isCorrect traces let failures = filter (not . isCorrect) traces putStrLn (show (length traces) ++ " total attempts") putStrLn (show (length successes) ++ " successes") putStrLn (show (length failures) ++ " failures") putStrLn (show (avgvisits successes) ++ " average number of room visits per success") putStrLn (show (avgvisits failures) ++ " average number of room visits per failure") putStrLn "Sample sequences of visits:" for_ (take 5 traces) (print . visits) where avgvisits ts = sum (map (fromIntegral . numvisits) ts) / genericLength ts numvisits = sum . map count where count (_, _, D.STM _ _) = 1 count (_, _, D.BlockedSTM _) = 1 count (_, _, D.Yield) = 1 count _ = 0  I have decided to assume that a prisoner will either yield (doing nothing) or perform some STM transaction while they’re in the room, to simplify things. ## The Perfect Solution A slow but simple strategy is for the prisoners to nominate a leader. Only the leader can declare to the warden that everyone has visited the room. Whenever a prisoner other than the leader visits the room, if the light is on, they do nothing; otherwise, if this is their first time in the room with the light off, they turn it on, otherwise they leave it. Whenever the leader enters the room, they turn the light off. When the leader has turned the light off 99 times (or 1 - num_prisoners times), they tell the warden that everyone has visited. Let’s set up those algorithms: -- | The state of the light bulb. data Light = IsOn | IsOff -- | Count how many prisoners have toggled the light and terminate -- when everyone has. leader :: C.MonadConc m => Int -> C.TVar (C.STM m) Light -> m () leader prisoners light = go 0 where go counter = do counter' <- C.atomically$ do
case state of
IsOn -> do
C.writeTVar light IsOff
pure (counter + 1)
IsOff -> C.retry
when (counter' < prisoners - 1)
(go counter')

-- | Turn the light on once then do nothing.
notLeader :: C.MonadConc m => C.TVar (C.STM m) Light -> m ()
C.atomically $do state <- C.readTVar light case state of IsOn -> C.retry IsOff -> C.writeTVar light IsOn forever C.yield  So now we just need to create a program where the leader is the main thread and everyone else is a separate thread: -- | Most popular English male and female names, according to -- Wikipedia. name :: Int -> String name i = ns !! (i mod length ns) where ns = ["Oliver", "Olivia", "George", "Amelia", "Harry", "Emily"] -- | Set up the prison game. The number of prisoners should be at -- least 1. prison :: C.MonadConc m => Int -> m () prison prisoners = do light <- C.atomically (C.newTVar IsOff) for_ [1..prisoners-1] (\i -> C.forkN (name i) (notLeader light)) leader prisoners light  Because these are people, not just threads, I’ve given them names. The leader is just called “main” though, how unfortunate for them. ### Testing Now we can try out our system and see if it works: λ> let runS = run$ D.systematically (D.defaultBounds { D.boundPreemp = Nothing })
λ> runS 1
1 total attempts
1 successes
0 failures
2.0 average number of room visits per success
NaN average number of room visits per failure
Sample sequences of visits:
[main]

λ> runS 2
5 total attempts
5 successes
0 failures
7.0 average number of room visits per success
NaN average number of room visits per failure
Sample sequences of visits:
[main,Olivia,main,Olivia,main]
[main,Olivia,main,Olivia,main]
[main,Olivia,main,Olivia,main]
[main,Olivia,main,Olivia,main]
[main,Olivia,main]

λ> runS 3
2035 total attempts
2035 successes
0 failures
133.39066339066338 average number of room visits per success
NaN average number of room visits per failure
Sample sequences of visits:
(big lists omitted)

This doesn’t scale well. It’s actually a really bad case for concurrency testing: every thread is messing with the same shared state, so dejafu has to try all the orderings. Not good.

Taking another look at our prisoners, we can see two things which a human would use to decide whether some schedules are redundant or not:

2. When a non-leader has completed their task, they will always yield. So we should never schedule a prisoner who will yield.

Unfortunately dejafu can’t really make use of (1). It could be inferred if dejafu was able to compare values inside TVars, rather than just seeing that there had been a write. But Haskell doesn’t let us do that without slapping an Eq constraint on writeTVar, which I definitely don’t want to do (although maybe having a separate eqwriteTVar, eqputMVar, and so on would be a nice addition).

Fortunately, dejafu can do something with (2). It already bounds the maximum number of times a thread can yield, so that we can test constructs like spinlocks. This is called fair bounding. The default bound is 5, but if we set it to 0 dejafu will just never schedule a thread which is going to yield. Here we go:

λ> let runS = run $D.systematically (D.defaultBounds { D.boundPreemp = Nothing, D.boundFair = Just 0 }) λ> runS 1 1 total attempts 1 successes 0 failures 2.0 average number of room visits per success NaN average number of room visits per failure Sample sequences of visits: [main] λ> runS 2 1 total attempts 1 successes 0 failures 4.0 average number of room visits per success NaN average number of room visits per failure Sample sequences of visits: [main,Olivia,main] λ> runS 3 4 total attempts 4 successes 0 failures 7.5 average number of room visits per success NaN average number of room visits per failure Sample sequences of visits: [main,Olivia,main,George,main] [main,Olivia,George,main,George,main] [main,George,main,Olivia,main] [main,George,Olivia,main,Olivia,main] Much better! Although it still doesn’t scale as nicely as we’d like λ> runS 4 48 total attempts 48 successes 0 failures 11.5 average number of room visits per success NaN average number of room visits per failure Sample sequences of visits: [main,Olivia,main,George,main,Amelia,main] [main,Olivia,main,George,Amelia,main,Amelia,main] [main,Olivia,main,Amelia,main,George,main] [main,Olivia,main,Amelia,George,main,George,main] [main,Olivia,George,main,George,main,Amelia,main] λ> runS 5 1536 total attempts 1536 successes 0 failures 16.0 average number of room visits per success NaN average number of room visits per failure Sample sequences of visits: [main,Olivia,main,George,main,Amelia,main,Harry,main] [main,Olivia,main,George,main,Amelia,Harry,main,Harry,main] [main,Olivia,main,George,main,Harry,main,Amelia,main] [main,Olivia,main,George,main,Harry,Amelia,main,Amelia,main] [main,Olivia,main,George,Amelia,main,Amelia,main,Harry,main] λ> runS 6 122880 total attempts 122880 successes 0 failures 21.0 average number of room visits per success NaN average number of room visits per failure Sample sequences of visits: [main,Olivia,main,George,main,Amelia,main,Harry,main,Emily,main] [main,Olivia,main,George,main,Amelia,main,Harry,Emily,main,Emily,main] [main,Olivia,main,George,main,Amelia,main,Emily,main,Harry,main] [main,Olivia,main,George,main,Amelia,main,Emily,Harry,main,Harry,main] [main,Olivia,main,George,main,Amelia,Harry,main,Harry,main,Emily,main] The prisoners are stepping on each other’s toes and causing needless work. This is probably as good as we can do without adding some extra primitives to dejafu to optimise the case where we have an Eq instance available, unfortunately. ### A Silver Lining In concurrency testing terms, six threads is actually quite a lot. Empirical studies have found that many concurrency bugs can be exhibited with only two or three threads! Furthermore, most real-world concurrent programs don’t have every single thread operating on the same bit of shared state. ## The “Good-Enough” Solution There’s another school of thought which says to just wait for three years, because by then it’s very unlikely that any single prisoner had never visited the room. In fact, we would expect each prisoner to have been to the room ten times by then, assuming the warden is fair. By keeping track of how many days have passed, we can try this out as well: leader :: C.MonadConc m => Int -> C.TVar (C.STM m) Int -> m () leader prisoners days = C.atomically$ do
C.check (numDays >= (prisoners - 1) * 10)

notLeader :: C.MonadConc m => C.TVar (C.STM m) Int -> m ()
notLeader days = forever . C.atomically $C.modifyTVar days (+1) prison :: C.MonadConc m => Int -> m () prison prisoners = do days <- C.atomically (C.newTVar 0) for_ [1..prisoners-1] (\i -> C.forkN (name i) (notLeader days)) leader prisoners days  Now let’s see how these brave prisoners do (sample visit sequences omitted because they’re pretty long): λ> let runR = run$ D.uniformly (R.mkStdGen 0) 100
λ> runR 1
100 total attempts
100 successes
0 failures
2.0 average number of room visits per success
NaN average number of room visits per failure

λ> runR 2
100 total attempts
100 successes
0 failures
18.35 average number of room visits per success
NaN average number of room visits per failure

λ> runR 3
100 total attempts
100 successes
0 failures
31.92 average number of room visits per success
NaN average number of room visits per failure

λ> runR 4
100 total attempts
100 successes
0 failures
43.52 average number of room visits per success
NaN average number of room visits per failure

λ> runR 5
100 total attempts
100 successes
0 failures
55.88 average number of room visits per success
NaN average number of room visits per failure

λ> runR 6
100 total attempts
100 successes
0 failures
67.37 average number of room visits per success
NaN average number of room visits per failure

λ> runR 7
100 total attempts
100 successes
0 failures
77.05 average number of room visits per success
NaN average number of room visits per failure

λ> runR 8
100 total attempts
99 successes
1 failures
90.4040404040404 average number of room visits per success
81.0 average number of room visits per failure

λ> runR 9
100 total attempts
100 successes
0 failures
101.64 average number of room visits per success
NaN average number of room visits per failure

λ> runR 10
100 total attempts
100 successes
0 failures
114.89 average number of room visits per success
NaN average number of room visits per failure

Not bad at all! Although my puny VPS still can’t manage all 100.