100 Prisoners

Date
Tags concurrency, dejafu, haskell, programming
Target Audience Mostly me.
Attention Conservation Notice There's a more polished version of this in my thesis, go read that instead.

There’s a pop­ular logic puzzle which goes some­thing like this:

There are 100 pris­oners in sol­itary cells. There’s a central living room with one light bulb; this bulb is ini­tially off. No pris­oner can see the light bulb from his or her own cell. Every­day, the warden picks a pris­oner equally at ran­dom, and that pris­oner visits the living room. While there, the pris­oner can toggle the bulb if he or she wishes. Also, the pris­oner has the op­tion of as­serting that all 100 pris­oners have been to the living room by now. If this as­ser­tion is false, all 100 pris­oners are shot. However, if it is in­deed true, all pris­oners are set free and in­ducted into MENSA, since the world could al­ways use more smart people. Thus, the as­ser­tion should only be made if the pris­oner is 100% cer­tain of its valid­ity. The pris­oners are al­lowed to get to­gether one night in the court­yard, to dis­cuss a plan. What plan should they agree on, so that even­tu­ally, someone will make a cor­rect as­ser­tion?

We can ex­press this as a con­cur­rency prob­lem: the warden is the sched­uler, each pris­oner is a thread, and when the pro­gram ter­min­ates every pris­oner should have vis­ited the living room.

Let’s set up some im­ports:

{-# LAN­GUAGE RankN­Types #-}

im­port qual­i­fied Con­trol.­Con­cur­rent.­Classy as C
im­port           Con­trol.­Monad             (forever, when)
im­port           Data.­Fold­able             (for_)
im­port           Data.List                 (gen­ericLength)
im­port           Data.Maybe                (map­Maybe)
im­port qual­i­fied Data.Set                  as S
im­port qual­i­fied Test.De­jaFu               as D
im­port qual­i­fied Test.De­jaFu.­Common        as D
im­port qual­i­fied Test.De­jaFu.SCT           as D

Cor­rect­ness

Be­fore we try to im­ple­ment a solu­tion, let’s think about how we can check if an ex­e­cu­tion cor­res­ponds to the pris­oners suc­ceeding an en­tering MENSA, or failing and being shot.

Pris­oners are threads, and the warden is the sched­uler. So if every thread (pris­oner) that is forked is sched­uled (taken to the room), then the pris­oners are suc­cess­ful:

-- | Check if an ex­e­cu­tion cor­res­ponds to a cor­rect guess.
isCor­rect :: D.Trace -> Bool
isCor­rect trc = S.from­List (threads trc) == S.from­List (visits trc)

-- | Get all threads cre­ated.
threads :: D.Trace -> [D.ThreadId]
threads trc = D.ini­tial­Thread : map­Maybe go trc where
  go (_, _, D.Fork tid) = Just tid
  go _ = Nothing

-- | Get all sched­uled threads
visits :: D.Trace -> [D.ThreadId]
visits = map­Maybe go where
  go (D.Start    tid, _, _) = Just tid
  go (D.SwitchTo tid, _, _) = Just tid
  go _ = Nothing

So now, given some way of set­ting up the game and run­ning it to com­ple­tion, we can test it and print some stat­ist­ics:

-- | Run the prison game and print stat­ist­ics.
run :: D.Way -> (forall m. C.Mon­ad­Conc m => m ()) -> IO ()
run way game = do
    traces <- map snd <$> D.runSCT way D.de­fault­Mem­Type game
    let suc­cesses = filter isCor­rect traces
    let fail­ures  = filter (not . isCor­rect) traces
    put­StrLn (show (length traces)    ++ " total at­tempts")
    put­StrLn (show (length suc­cesses) ++ " suc­cesses")
    put­StrLn (show (length fail­ures)  ++ " fail­ures")
    put­StrLn (show (avgvisits suc­cesses) ++ " av­erage number of room visits per suc­cess")
    put­StrLn (show (avgvisits fail­ures)  ++ " av­erage number of room visits per fail­ure")
    put­StrLn "Sample se­quences of vis­its:"
    for_ (take 5 traces) (print . visits)
  where
    avgvisits ts = sum (map (fro­mIn­tegral . num­visits) ts) / gen­ericLength ts
    num­visits = sum . map count where
      count (_, _, D.STM _ _) = 1
      count (_, _, D.BlockedSTM _) = 1
      count (_, _, D.Yield) = 1
      count _ = 0

I have de­cided to as­sume that a pris­oner will either yield (doing noth­ing) or per­form some STM trans­ac­tion while they’re in the room, to sim­plify things.

The Per­fect Solu­tion

A slow but simple strategy is for the pris­oners to nom­inate a leader. Only the leader can de­clare to the warden that everyone has vis­ited the room. Whenever a pris­oner other than the leader visits the room, if the light is on, they do noth­ing; oth­er­wise, if this is their first time in the room with the light off, they turn it on, oth­er­wise 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_­pris­oners times), they tell the warden that everyone has vis­ited.

Let’s set up those al­gorithms:

-- | The state of the light bulb.
data Light = IsOn | IsOff

-- | Count how many pris­oners have toggled the light and ter­minate
-- when everyone has.
leader :: C.Mon­ad­Conc m => Int -> C.TVar (C.STM m) Light -> m ()
leader pris­oners light = go 0 where
  go counter = do
    coun­ter' <- C.atom­ic­ally $ do
      state <- C.readTVar light
      case state of
        IsOn -> do
          C.writeTVar light IsOff
          pure (counter + 1)
        IsOff -> C.retry
    when (coun­ter' < pris­oners - 1)
      (go coun­ter')

-- | Turn the light on once then do noth­ing.
notLeader :: C.Mon­ad­Conc m => C.TVar (C.STM m) Light -> m ()
notLeader light = do
  C.atom­ic­ally $ 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 pro­gram where the leader is the main thread and everyone else is a sep­arate thread:

-- | Most pop­ular Eng­lish male and fe­male names, ac­cording to
-- Wiki­pe­dia.
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 pris­oners should be at
-- least 1.
prison :: C.Mon­ad­Conc m => Int -> m ()
prison pris­oners = do
  light <- C.atom­ic­ally (C.newTVar IsOff)
  for_ [1..pris­oners-1] (\i -> C.forkN (name i) (notLeader light))
  leader pris­oners light

Be­cause these are people, not just threads, I’ve given them names. The leader is just called “main” though, how un­for­tu­nate for them.

Testing

Now we can try out our system and see if it works:

λ> let runS = run $ D.sys­tem­at­ic­ally (D.de­fault­Bounds { D.bound­Preemp = Nothing })
λ> runS 1
1 total at­tempts
1 suc­cesses
0 fail­ures
2.0 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure
Sample se­quences of vis­its:
[main]

λ> runS 2
5 total at­tempts
5 suc­cesses
0 fail­ures
7.0 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure
Sample se­quences of vis­its:
[main,Olivi­a,­main,Olivi­a,­main]
[main,Olivi­a,­main,Olivi­a,­main]
[main,Olivi­a,­main,Olivi­a,­main]
[main,Olivi­a,­main,Olivi­a,­main]
[main,Olivi­a,­main]

λ> runS 3
2035 total at­tempts
2035 suc­cesses
0 fail­ures
133.39066339066338 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure
Sample se­quences of vis­its:
(big lists omit­ted)

This doesn’t scale well. It’s ac­tu­ally a really bad case for con­cur­rency test­ing: every thread is messing with the same shared state, so de­jafu has to try all the or­der­ings. Not good.

Taking an­other look at our pris­on­ers, we can see two things which a human would use to de­cide whether some sched­ules are re­dundant or not:

  1. If we adopt any schedule other than al­tern­ating leader / non-leader, threads will block without doing any­thing. So we should al­tern­ate.

  2. When a non-leader has com­pleted their task, they will al­ways yield. So we should never schedule a pris­oner who will yield.

Un­for­tu­nately de­jafu can’t really make use of (1). It could be in­ferred if de­jafu was able to com­pare values in­side TVars, rather than just seeing that there had been a write. But Haskell doesn’t let us do that without slap­ping an Eq con­straint on writeTVar, which I def­in­itely don’t want to do (al­though maybe having a sep­arate eqwriteTVar, eqput­MVar, and so on would be a nice ad­di­tion).

For­tu­nately, de­jafu can do some­thing with (2). It already bounds the max­imum number of times a thread can yield, so that we can test con­structs like spin­locks. This is called fair bounding. The de­fault bound is 5, but if we set it to 0 de­jafu will just never schedule a thread which is going to yield. Here we go:

λ> let runS = run $ D.sys­tem­at­ic­ally (D.de­fault­Bounds { D.bound­Preemp = Noth­ing, D.bound­Fair = Just 0 })
λ> runS 1
1 total at­tempts
1 suc­cesses
0 fail­ures
2.0 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure
Sample se­quences of vis­its:
[main]

λ> runS 2
1 total at­tempts
1 suc­cesses
0 fail­ures
4.0 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure
Sample se­quences of vis­its:
[main,Olivi­a,­main]

λ> runS 3
4 total at­tempts
4 suc­cesses
0 fail­ures
7.5 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure
Sample se­quences of vis­its:
[main,Olivi­a,­main,George,­main]
[main,Olivi­a,George,­main,George,­main]
[main,George,­main,Olivi­a,­main]
[main,George,Olivi­a,­main,Olivi­a,­main]

Much bet­ter! Al­though it still doesn’t scale as nicely as we’d like

λ> runS 4
48 total at­tempts
48 suc­cesses
0 fail­ures
11.5 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure
Sample se­quences of vis­its:
[main,Olivi­a,­main,George,­main,Ameli­a,­main]
[main,Olivi­a,­main,George,Ameli­a,­main,Ameli­a,­main]
[main,Olivi­a,­main,Ameli­a,­main,George,­main]
[main,Olivi­a,­main,Ameli­a,George,­main,George,­main]
[main,Olivi­a,George,­main,George,­main,Ameli­a,­main]

λ> runS 5
1536 total at­tempts
1536 suc­cesses
0 fail­ures
16.0 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure
Sample se­quences of vis­its:
[main,Olivi­a,­main,George,­main,Ameli­a,­main,Harry­,­main]
[main,Olivi­a,­main,George,­main,Ameli­a,Harry­,­main,Harry­,­main]
[main,Olivi­a,­main,George,­main,Harry­,­main,Ameli­a,­main]
[main,Olivi­a,­main,George,­main,Harry­,Ameli­a,­main,Ameli­a,­main]
[main,Olivi­a,­main,George,Ameli­a,­main,Ameli­a,­main,Harry­,­main]

λ> runS 6
122880 total at­tempts
122880 suc­cesses
0 fail­ures
21.0 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure
Sample se­quences of vis­its:
[main,Olivi­a,­main,George,­main,Ameli­a,­main,Harry­,­main,Emily,­main]
[main,Olivi­a,­main,George,­main,Ameli­a,­main,Harry­,Emily,­main,Emily,­main]
[main,Olivi­a,­main,George,­main,Ameli­a,­main,Emily,­main,Harry­,­main]
[main,Olivi­a,­main,George,­main,Ameli­a,­main,Emily,Harry­,­main,Harry­,­main]
[main,Olivi­a,­main,George,­main,Ameli­a,Harry­,­main,Harry­,­main,Emily,­main]

The pris­oners are step­ping on each oth­er’s toes and causing need­less work. This is prob­ably as good as we can do without adding some extra prim­it­ives to de­jafu to op­timise the case where we have an Eq in­stance avail­able, un­for­tu­nately.

A Silver Lining

In con­cur­rency testing terms, six threads is ac­tu­ally quite a lot.

Em­pir­ical studies have found that many con­cur­rency bugs can be ex­hib­ited with only two or three threads! Fur­ther­more, most real-­world con­cur­rent pro­grams don’t have every single thread op­er­ating on the same bit of shared state.

The “Good-Enough” Solu­tion

There’s an­other school of thought which says to just wait for three years, be­cause by then it’s very un­likely that any single pris­oner had never vis­ited the room. In fact, we would ex­pect each pris­oner to have been to the room ten times by then, as­suming the warden is fair.

By keeping track of how many days have passed, we can try this out as well:

leader :: C.Mon­ad­Conc m => Int -> C.TVar (C.STM m) Int -> m ()
leader pris­oners days = C.atom­ic­ally $ do
  num­Days <- C.readTVar days
  C.check (num­Days >= (pris­oners - 1) * 10)

notLeader :: C.Mon­ad­Conc m => C.TVar (C.STM m) Int -> m ()
notLeader days = forever . C.atom­ic­ally $ C.modi­fyTVar days (+1)

prison :: C.Mon­ad­Conc m => Int -> m ()
prison pris­oners = do
  days <- C.atom­ic­ally (C.newTVar 0)
  for_ [1..pris­oners-1] (\i -> C.forkN (name i) (notLeader days))
  leader pris­oners days

Now let’s see how these brave pris­oners do (sample visit se­quences omitted be­cause they’re pretty long):

λ> let runR = run $ D.uni­formly (R.mk­StdGen 0) 100
λ> runR 1
100 total at­tempts
100 suc­cesses
0 fail­ures
2.0 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure

λ> runR 2
100 total at­tempts
100 suc­cesses
0 fail­ures
18.35 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure

λ> runR 3
100 total at­tempts
100 suc­cesses
0 fail­ures
31.92 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure

λ> runR 4
100 total at­tempts
100 suc­cesses
0 fail­ures
43.52 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure

λ> runR 5
100 total at­tempts
100 suc­cesses
0 fail­ures
55.88 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure

λ> runR 6
100 total at­tempts
100 suc­cesses
0 fail­ures
67.37 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure

λ> runR 7
100 total at­tempts
100 suc­cesses
0 fail­ures
77.05 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure

λ> runR 8
100 total at­tempts
99 suc­cesses
1 fail­ures
90.4040404040404 av­erage number of room visits per suc­cess
81.0 av­erage number of room visits per failure

λ> runR 9
100 total at­tempts
100 suc­cesses
0 fail­ures
101.64 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure

λ> runR 10
100 total at­tempts
100 suc­cesses
0 fail­ures
114.89 av­erage number of room visits per suc­cess
NaN av­erage number of room visits per failure

Not bad at all! Al­though my puny VPS still can’t manage all 100.