haskell
, QuickCheck
, some monads, salt / pepper to taste.MVar a
is a link that either contains a value of type a or is empty.putMVar ref x
puts the reference ref value x.takeMVar ref
reads the contents of the link, leaving it empty after that.()
Is a type having a single value, which is denoted in the same way as the type itself - ()
.MVar ()
.()
. import System.Random import Control.Monad import Control.Concurrent import Control.Monad.Cont import Control.Monad.Trans import Data.IORef import Test.QuickCheck import Test.QuickCheck.Gen import Test.QuickCheck.Monadic -- sleep ( 0 0.3) sleep :: IO () sleep = randomRIO (0, 300000) >>= threadDelay phil :: Int -- . -> MVar () -- . -> MVar () -- . -> IO () phil n leftFork rightFork = forever $ do putStrLn $ show n ++ " is awaiting" sleep takeMVar leftFork putStrLn $ show n ++ " took left fork" -- sleep takeMVar rightFork putStrLn $ show n ++ " took right fork" sleep putMVar leftFork () putMVar rightFork () putStrLn $ show n ++ " put forks" sleep runPhil :: Int -> IO () runPhil n = do -- , . forks <- replicateM n $ newMVar () -- 5 , phil. forM_ [1..n] $ \i -> forkIO $ phil i (forks !! (i - 1)) (forks !! (i `mod` n)) main = do runPhil 5 -- , , . forever (threadDelay 1000000000)
sleep
and wait a bit.runPhil
definition of the functions sleep
, phil
and runPhil
, so that they work for other monads. sleep :: MonadIO m => m () sleep = do r <- liftIO $ randomRIO (0, 100) r `times` liftIO (threadDelay 300) where times :: Monad m => Int -> m () -> m () times ra = mapM_ (\_ -> a) [1..r]
sleep
function can work with any monad that supports IO operations. In the MonadIO
class, only one liftIO
function is liftIO
that allows this.liftIO
are performed atomically. Accordingly, the time at which we fall asleep does not affect anything, it only matters how many times we do it.MVar
is useless for us, and we will later define our type of links, assuming that the phil
function can work with MVar
and other types of links.MonadConcurrent
, in which there will be operations for creating, reading and writing by reference, as well as for creating threads. class Monad m => MonadConcurrent m where type CVar m :: * -> * newCVar :: a -> m (CVar ma) takeCVar :: CVar ma -> ma putCVar :: CVar ma -> a -> m () fork :: m () -> m ()
{-# LANGUAGE TypeFamilies, ExistentialQuantification, GeneralizedNewtypeDeriving #-}
instance
this class for the monad IO.MVar
. instance MonadConcurrent IO where type CVar IO = MVar newCVar = newMVar takeCVar = takeMVar putCVar = putMVar fork m = forkIO m >> return ()
runPhil
functions phil
and runPhil
. phil :: (MonadIO m, MonadConcurrent m) => Int -> CVar m () -> CVar m () -> m () phil n leftFork rightFork = forever $ do liftIO $ putStrLn $ show n ++ " is awaiting" sleep takeCVar leftFork liftIO $ putStrLn $ show n ++ " took left fork" takeCVar rightFork liftIO $ putStrLn $ show n ++ " took right fork" sleep putCVar leftFork () putCVar rightFork () liftIO $ putStrLn $ show n ++ " put forks" sleep runPhil :: (MonadIO m, MonadConcurrent m) => Int -> m () runPhil n = do forks <- replicateM n $ newCVar () forM_ [1..n] $ \i -> fork $ phil i (forks !! (i - 1)) (forks !! (i `mod` n))
Cont
). Also I would venture to suggest that Cont
is one of the most complex and most powerful monads at the same time.Action
type) and perform them later, perhaps in a different order. data Action = Atom (IO Action) | forall a. ReadRef (MaybeRef a) (a -> Action) | forall a. WriteRef (MaybeRef a) a Action | Fork Action Action | Stop
Stop
action means that the calculation is complete.Fork
action means that the calculations are branching, that is, now we have two threads that can be executed simultaneously.Atom
action performs an atomically IO operation, which returns us a new Action
, which contains the action, which should be performed in the next step.getSum
function sets an action that reads two numbers from the keyboard, prints their sum and ends. getSum :: Action getSum = Atom $ do x <- readLn -- return $ Atom $ do -- y <- readLn -- return $ Atom $ do -- print (x + y) -- return Stop --
WriteRef ref val act
writes the value val
by reference ref
, in act
is the continuation.ReadRef ref act
reads the value by reference ref
, act
takes this value and returns a continuation.Action
, we use another extension of the language - existential quantification.MaybeRef
type represents the type of links that we will use instead of MVar
, and it is defined as a link to Maybe
. newtype MaybeRef a = MaybeRef (IORef (Maybe a))
Cont
. newtype Concurrent a = Concurrent (Cont Action a) deriving Monad
Cont Action
organized as follows.a
, it takes an extension of the type (a -> Action)
, passes the value to this function, and returns the result.Cont Action a = (a -> Action) -> Action
.(a -> Action) -> Action
to Cont Action a
and back. cont :: ((a -> Action) -> Action) -> Cont Action a. runCont :: Cont Action a -> (a -> Action) -> Action
MonadIO
and MonadConcurrent
. instance MonadIO Concurrent where liftIO m = Concurrent $ cont $ \c -> Atom $ do a <- m return (ca)
liftIO
takes an IO operation and wraps it into an atomic action. Namely: we in cont
transfer to a function that accepts continuation (that is, c is of type a -> Action
) and returns an atomic action that performs an IO operation m
.Atom
so that an atomic operation must return an Action
that is a continuation.m
, we call c
, which returns the necessary continuation.instance MonadConcurrent
.newCVar
using the liftIO
function liftIO
just defined.takeCVar
and putCVar
return the corresponding action, and we continue the continuation inside this structure.fork
function, the other comes from a continuation. instance MonadConcurrent Concurrent where type CVar Concurrent = MaybeRef newCVar a = liftIO $ liftM MaybeRef $ newIORef (Just a) takeCVar v = Concurrent $ cont (ReadRef v) putCVar va = Concurrent $ cont $ \c -> WriteRef va $ c () fork (Concurrent m) = Concurrent $ cont $ \c -> Fork (runCont m $ \_ -> Stop) $ c ()
Action
. It takes a list of actions, each element in which is a separate thread. runAction :: [Action] -> IO () -- , . runAction [] = return () -- , , , . runAction (Atom m : as) = do a' <- m runAction $ as ++ [a'] -- . runAction (Fork a1 a2 : as) = runAction $ as ++ [a1,a2] -- . runAction (Stop : as) = runAction as runAction (ReadRef (MaybeRef ref) c : as) = do -- . ma <- readIORef ref case ma of -- -, Just a -> do -- . writeIORef ref Nothing -- . runAction (as ++ [ca]) -- , , . Nothing -> runAction (as ++ [ReadRef (MaybeRef ref) c]) -- , . runAction (WriteRef (MaybeRef ref) val a : as) = do writeIORef ref (Just val) runAction (as ++ [a])
putMVar
works slightly differently than our implementation of WriteRef
.putMVar
freeze the stream until the variable is released. In this case, overwrite the value.putMVar
in this situation, so as not to over-complicate the code.Concurrent
, and override the main
. runConcurrent :: Concurrent () -> IO () runConcurrent (Concurrent c) = runAction [runCont c $ \_ -> Stop] main = runConcurrent (runPhil 5)
threadDelay
stops all work, the speed has slowed down a bit.QuickCheck
library, which generates random input data for tests. Since we want to run our threads in different orders, the input to our tests is the order in which we select the next thread from the list.Int -> Int
, which take the number n
and return a number from the interval [0,n-1]
. newtype Route = Route [Int -> Int]
Arbitrary
class provided by the QuickCheck
library is designed to describe types that allow you to generate elements at random.shrink
and arbitrary
.shrink
has a default implementation, so we will not override it.arbitrary
function, we will generate a list of random functions, where each function returns a number from the interval [0,n-1]
. instance Arbitrary Route where arbitrary = fmap Route (listOf arbitraryFun) where arbitraryFun = MkGen $ \qsn -> unGen (choose (0, n - 1)) qs
instance Show
for Route
, as this is required by QuickCheck
.show
. Moreover, this function will not be used, so we leave it undefined. instance Show Route where show = undefined
runAction
.skipAtoms
, skipAtoms
write an auxiliary function, skipAtoms
, which performs atomic actions: the function accepts the list of actions, executes Atom
, Fork
and Stop
, the rest returns as a result. skipAtoms :: [Action] -> IO [Action] skipAtoms [] = return [] skipAtoms (Atom m : as) = do a <- m skipAtoms (as ++ [a]) skipAtoms (Fork a1 a2 : as) = skipAtoms (as ++ [a1,a2]) skipAtoms (Stop : as) = skipAtoms as skipAtoms (a : as) = fmap (a:) (skipAtoms as)
runAction
from the previous one is that we track the receipt of deadlock.Route
type argument used to select the stream number to be executed in the current step. runAction :: Route -> [Action] -> [Action] -> IO () runAction _ [] [] = return () runAction _ [] _ = fail "Deadlock" runAction (Route []) _ _ = return () runAction (Route (r:rs)) as bs = do as <- skipAtoms as let n = length as case splitAt (rn) as of (as1, ReadRef (MaybeRef ref) c : as2) -> do ma <- readIORef ref case ma of Just a -> do writeIORef ref Nothing runAction (Route rs) (as1 ++ [ca] ++ as2) bs Nothing -> runAction (Route rs) (as1 ++ as2) (bs ++ [ReadRef (MaybeRef ref) c]) (as1, WriteRef (MaybeRef ref) xc : as2) -> do writeIORef ref (Just x) runAction (Route rs) (as1 ++ [c] ++ as2 ++ bs) []
runConcurrent
function runConcurrent
hardly changed. runConcurrent :: Route -> Concurrent () -> IO () runConcurrent r (Concurrent c) = runAction r [runCont c $ \_ -> Stop] []
round_robin
as the first argument. This is a simple execution strategy, similar to how the runAction
function worked before. Here we simply generate an infinite list and for each element we take the remainder modulo the number of threads. round_robin :: Route round_robin = Route $ map rem [0..]
main = quickCheck $ monadicIO $ do r <- pick arbitrary run $ runConcurrent r (runPhil 5)
Route
type using the arbitrary
function that we implemented earlier. Then we run our calculation on this input.QuickCheck
will take care of the QuickCheck
, namely: run our test 100 times, each time increasing the size of the input data. ... 3 took left fork 4 put forks 4 is awaiting 5 took left fork 4 took left fork 1 took right fork 1 put forks 1 is awaiting 1 took left fork 2 took left fork *** Failed! Exception: 'user error (Deadlock)' (after 36 tests):
Cont
monad, type families, existential quantification, and the QuickCheck
library.Source: https://habr.com/ru/post/224075/
All Articles