mirror of
https://github.com/barrucadu/dejafu.git
synced 2024-11-05 06:45:08 +03:00
Split Test.DejaFu.SCT.Internal up
This commit is contained in:
Michael Walker
parent
4a4baec1d9
commit
d3419845d3
@ -17,7 +17,7 @@ import qualified Test.DejaFu.Types as D
|
||||
import qualified Test.DejaFu.Internal as D
|
||||
import qualified Test.DejaFu.Conc.Internal.Common as D
|
||||
import qualified Test.DejaFu.Conc.Internal.Memory as Mem
|
||||
import qualified Test.DejaFu.SCT.Internal as SCT
|
||||
import qualified Test.DejaFu.SCT.Internal.DPOR as SCT
|
||||
import Test.Framework (Test)
|
||||
import Test.LeanCheck (Listable(..), (\/), (><), (==>), cons0, cons1, cons2, cons3, mapT)
|
||||
|
||||
|
||||
@ -81,20 +81,21 @@ module Test.DejaFu.SCT
|
||||
, sctWeightedRandomDiscard
|
||||
) where
|
||||
|
||||
import Control.Applicative ((<|>))
|
||||
import Control.DeepSeq (NFData(..), force)
|
||||
import Control.Monad.Conc.Class (MonadConc)
|
||||
import Control.Monad.Ref (MonadRef)
|
||||
import Data.List (foldl')
|
||||
import qualified Data.Map.Strict as M
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Set (Set)
|
||||
import qualified Data.Set as S
|
||||
import System.Random (RandomGen, randomR)
|
||||
import Control.Applicative ((<|>))
|
||||
import Control.DeepSeq (NFData(..), force)
|
||||
import Control.Monad.Conc.Class (MonadConc)
|
||||
import Control.Monad.Ref (MonadRef)
|
||||
import Data.List (foldl')
|
||||
import qualified Data.Map.Strict as M
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Set (Set)
|
||||
import qualified Data.Set as S
|
||||
import System.Random (RandomGen, randomR)
|
||||
|
||||
import Test.DejaFu.Conc
|
||||
import Test.DejaFu.Internal
|
||||
import Test.DejaFu.SCT.Internal
|
||||
import Test.DejaFu.SCT.Internal.DPOR
|
||||
import Test.DejaFu.SCT.Internal.Weighted
|
||||
import Test.DejaFu.Types
|
||||
import Test.DejaFu.Utils
|
||||
|
||||
|
||||
@ -1,17 +1,15 @@
|
||||
{-# LANGUAGE TupleSections #-}
|
||||
|
||||
-- |
|
||||
-- Module : Test.DejaFu.SCT.Internal
|
||||
-- Module : Test.DejaFu.SCT.Internal.DPOR
|
||||
-- Copyright : (c) 2015--2017 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : experimental
|
||||
-- Portability : TupleSections
|
||||
-- Portability : portable
|
||||
--
|
||||
-- Internal types and functions for dynamic partial-order
|
||||
-- reduction. This module is NOT considered to form part of the public
|
||||
-- interface of this library.
|
||||
module Test.DejaFu.SCT.Internal where
|
||||
-- Internal types and functions for SCT via dynamic partial-order
|
||||
-- reduction. This module is NOT considered to form part of the
|
||||
-- public interface of this library.
|
||||
module Test.DejaFu.SCT.Internal.DPOR where
|
||||
|
||||
import Control.Applicative ((<|>))
|
||||
import Control.DeepSeq (NFData(..))
|
||||
@ -22,13 +20,11 @@ import Data.List (nubBy, partition, sortOn)
|
||||
import Data.List.NonEmpty (toList)
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as M
|
||||
import Data.Maybe (fromMaybe, isJust, isNothing,
|
||||
listToMaybe)
|
||||
import Data.Maybe (isJust, isNothing, listToMaybe)
|
||||
import Data.Sequence (Seq, (|>))
|
||||
import qualified Data.Sequence as Sq
|
||||
import Data.Set (Set)
|
||||
import qualified Data.Set as S
|
||||
import System.Random (RandomGen, randomR)
|
||||
|
||||
import Test.DejaFu.Internal
|
||||
import Test.DejaFu.Schedule (Scheduler(..))
|
||||
@ -531,51 +527,7 @@ dporSched boundf = Scheduler $ \prior threads s ->
|
||||
(Nothing, (nextState []) { schedIgnore = signore', schedBoundKill = sbkill', schedBState = Nothing })
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- Weighted random scheduler
|
||||
|
||||
-- | The scheduler state
|
||||
data RandSchedState g = RandSchedState
|
||||
{ schedWeights :: Map ThreadId Int
|
||||
-- ^ The thread weights: used in determining which to run.
|
||||
, schedGen :: g
|
||||
-- ^ The random number generator.
|
||||
} deriving (Eq, Show)
|
||||
|
||||
instance NFData g => NFData (RandSchedState g) where
|
||||
rnf s = rnf ( schedWeights s
|
||||
, schedGen s
|
||||
)
|
||||
|
||||
-- | Initial weighted random scheduler state.
|
||||
initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g
|
||||
initialRandSchedState = RandSchedState . fromMaybe M.empty
|
||||
|
||||
-- | Weighted random scheduler: assigns to each new thread a weight,
|
||||
-- and makes a weighted random choice out of the runnable threads at
|
||||
-- every step.
|
||||
randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g)
|
||||
randSched weightf = Scheduler $ \_ threads s ->
|
||||
let
|
||||
-- Select a thread
|
||||
pick idx ((x, f):xs)
|
||||
| idx < f = Just x
|
||||
| otherwise = pick (idx - f) xs
|
||||
pick _ [] = Nothing
|
||||
(choice, g'') = randomR (0, sum (map snd enabled) - 1) g'
|
||||
enabled = M.toList $ M.filterWithKey (\tid _ -> tid `elem` tids) weights'
|
||||
|
||||
-- The weights, with any new threads added.
|
||||
(weights', g') = foldr assignWeight (M.empty, schedGen s) tids
|
||||
assignWeight tid ~(ws, g0) =
|
||||
let (w, g) = maybe (weightf g0) (,g0) (M.lookup tid (schedWeights s))
|
||||
in (M.insert tid w ws, g)
|
||||
|
||||
-- The runnable threads.
|
||||
tids = map fst (toList threads)
|
||||
in (pick choice enabled, RandSchedState weights' g'')
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- Dependency function
|
||||
-- * Dependency function
|
||||
|
||||
-- | Check if an action is dependent on another.
|
||||
--
|
||||
@ -697,7 +649,7 @@ dependentActions ds a1 a2 = case (a1, a2) of
|
||||
in if f1 == f2 then f1 else Nothing
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- Dependency function state
|
||||
-- ** Dependency function state
|
||||
|
||||
data DepState = DepState
|
||||
{ depCRState :: Map CRefId Bool
|
||||
66
dejafu/Test/DejaFu/SCT/Internal/Weighted.hs
Normal file
66
dejafu/Test/DejaFu/SCT/Internal/Weighted.hs
Normal file
@ -0,0 +1,66 @@
|
||||
-- |
|
||||
-- Module : Test.DejaFu.SCT.Internal.Weighted
|
||||
-- Copyright : (c) 2015--2017 Michael Walker
|
||||
-- License : MIT
|
||||
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
|
||||
-- Stability : experimental
|
||||
-- Portability : portable
|
||||
--
|
||||
-- Internal types and functions for SCT via weighted random
|
||||
-- scheduling. This module is NOT considered to form part of the
|
||||
-- public interface of this library.
|
||||
module Test.DejaFu.SCT.Internal.Weighted where
|
||||
|
||||
import Control.DeepSeq (NFData(..))
|
||||
import Data.List.NonEmpty (toList)
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as M
|
||||
import Data.Maybe (fromMaybe)
|
||||
import System.Random (RandomGen, randomR)
|
||||
|
||||
import Test.DejaFu.Schedule (Scheduler(..))
|
||||
import Test.DejaFu.Types
|
||||
|
||||
-------------------------------------------------------------------------------
|
||||
-- * Weighted random scheduler
|
||||
|
||||
-- | The scheduler state
|
||||
data RandSchedState g = RandSchedState
|
||||
{ schedWeights :: Map ThreadId Int
|
||||
-- ^ The thread weights: used in determining which to run.
|
||||
, schedGen :: g
|
||||
-- ^ The random number generator.
|
||||
} deriving (Eq, Show)
|
||||
|
||||
instance NFData g => NFData (RandSchedState g) where
|
||||
rnf s = rnf ( schedWeights s
|
||||
, schedGen s
|
||||
)
|
||||
|
||||
-- | Initial weighted random scheduler state.
|
||||
initialRandSchedState :: Maybe (Map ThreadId Int) -> g -> RandSchedState g
|
||||
initialRandSchedState = RandSchedState . fromMaybe M.empty
|
||||
|
||||
-- | Weighted random scheduler: assigns to each new thread a weight,
|
||||
-- and makes a weighted random choice out of the runnable threads at
|
||||
-- every step.
|
||||
randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g)
|
||||
randSched weightf = Scheduler $ \_ threads s ->
|
||||
let
|
||||
-- Select a thread
|
||||
pick idx ((x, f):xs)
|
||||
| idx < f = Just x
|
||||
| otherwise = pick (idx - f) xs
|
||||
pick _ [] = Nothing
|
||||
(choice, g'') = randomR (0, sum (map snd enabled) - 1) g'
|
||||
enabled = M.toList $ M.filterWithKey (\tid _ -> tid `elem` tids) weights'
|
||||
|
||||
-- The weights, with any new threads added.
|
||||
(weights', g') = foldr assignWeight (M.empty, schedGen s) tids
|
||||
assignWeight tid ~(ws, g0) =
|
||||
let (w, g) = maybe (weightf g0) (\w0 -> (w0, g0)) (M.lookup tid (schedWeights s))
|
||||
in (M.insert tid w ws, g)
|
||||
|
||||
-- The runnable threads.
|
||||
tids = map fst (toList threads)
|
||||
in (pick choice enabled, RandSchedState weights' g'')
|
||||
@ -51,7 +51,8 @@ library
|
||||
, Test.DejaFu.Conc.Internal.STM
|
||||
, Test.DejaFu.Conc.Internal.Threading
|
||||
, Test.DejaFu.Internal
|
||||
, Test.DejaFu.SCT.Internal
|
||||
, Test.DejaFu.SCT.Internal.DPOR
|
||||
, Test.DejaFu.SCT.Internal.Weighted
|
||||
|
||||
-- other-modules:
|
||||
-- other-extensions:
|
||||
|
||||
Loading…
Reference in New Issue
Block a user