1
1
mirror of https://github.com/barrucadu/dejafu.git synced 2024-12-23 05:22:25 +03:00
dejafu/dejafu-tests/Examples/Philosophers.hs
2016-04-03 06:45:11 +01:00

47 lines
1.6 KiB
Haskell
Executable File

-- An implementation of the Dining Philosophers. This is interesting
-- as it show-cases testing a non-terminating program.
module Examples.Philosophers where
import Control.Monad (replicateM, forever)
import Control.Monad.Conc.Class
import Data.Functor (void)
import Test.DejaFu
import Test.Framework (Test)
import Test.Framework.Providers.HUnit (hUnitTestToTests)
import Test.HUnit (test)
import Test.HUnit.DejaFu
tests :: [Test]
tests = hUnitTestToTests $ test
[ testDejafu' defaultMemType bound (philosophers 3) "deadlocks" deadlocksSometimes
, testDejafu' defaultMemType bound (philosophers 3) "loops" abortsSometimes
]
-- | Shorter execution length bound
bound :: Bounds
bound = defaultBounds { boundLength = Just 30 }
--------------------------------------------------------------------------------
-- | Run the Dining Philosophers. Result is irrelevant, we just care
-- about deadlocks.
philosophers :: MonadConc m => Int -> m ()
philosophers n = do
forks <- replicateM n newEmptyMVar
let phils = map (\(i,p) -> p i forks) $ zip [0..] $ replicate n philosopher
cvars <- mapM spawn phils
mapM_ takeMVar cvars
where
philosopher ident forks = forever $ do
let leftId = ident
let rightId = (ident + 1) `mod` length forks
putMVar (forks !! leftId) ()
putMVar (forks !! rightId) ()
-- In the traditional approach, we'd wait for a random time
-- here, but we want the only source of (important)
-- nondeterminism to come from the scheduler, which it does, as
-- pre-emption is effectively a delay.
takeMVar $ forks !! leftId
takeMVar $ forks !! rightId