barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-11-27 13:39:16 +03:00
Code Issues Projects Releases Wiki Activity

Implement uniform random scheduling

Browse Source 
Adds a new `uniformly` smart constructor and `sctUniformRandom`
function.

Also renames `sctRandom` to `sctWeightedRandom`.
This commit is contained in:
Michael Walker 2017-05-28 04:02:59 +01:00
parent 1146ce9b38
commit 6b1fd17024
9 changed files with 86 additions and 29 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
dejafu-tests/Utils.hs
View File

@ -13,7 +13,7 @@ import Test.DejaFu.Conc (ConcST)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (hUnitTestToTests)
import Test.HUnit (test)
import Test.HUnit.DejaFu (Bounds, defaultBounds, defaultMemType, randomly, swarmy, systematically, testDejafuWay)
import Test.HUnit.DejaFu (Bounds, defaultBounds, defaultMemType, uniformly, randomly, swarmy, systematically, testDejafuWay)
-- | Wrap up a test
data T where
@ -23,9 +23,10 @@ data T where
-- | Run a test group with different execution ways.
tg :: String -> [T] -> Test
tg name ts = testGroup name
[ testGroup "Systematic" . hUnitTestToTests . test . useWay $ systematically
, testGroup "Random" . hUnitTestToTests . test . useWay . const $ randomly (mkStdGen 0) 100
, testGroup "Swarm (10)" . hUnitTestToTests . test . useWay . const $ swarmy (mkStdGen 0) 100 10
[ testGroup "Systematic" . hUnitTestToTests . test . useWay $ systematically
, testGroup "Uniform" . hUnitTestToTests . test . useWay . const $ uniformly (mkStdGen 0) 100
, testGroup "Weighted" . hUnitTestToTests . test . useWay . const $ randomly (mkStdGen 0) 100
, testGroup "Swarm (10)" . hUnitTestToTests . test . useWay . const $ swarmy (mkStdGen 0) 100 10
]
where
useWay wayf = map (go wayf) ts

5
dejafu/CHANGELOG.markdown
View File

@ -32,9 +32,12 @@ unreleased
- The `Way` type is now abstract and exposes smart constructor functions:
- `systematically`, corresponding to the old `Systematically`.
- `randomly`, corresponding to the old `Randomly`,
- `uniformly`, a new uniform random (as opposed to weighted random) scheduler.
- `swarmy`, corresponding to the old `Randomly` and specifying how many executions to use the
same weights for.
- The `sctRandom` function can now re-use the same weights for multiple executions.
- A new `sctUniformRandom` function to do uniform (non-weighted) scheduling.
- The `sctRandom` function is now called `sctWeightedRandom` and can now re-use the same weights for
multiple executions.
### Fixed

1
dejafu/Test/DejaFu.hs
View File

@ -97,6 +97,7 @@ module Test.DejaFu
, defaultWay
, systematically
, randomly
, uniformly
, swarmy
, autocheckWay

87
dejafu/Test/DejaFu/SCT.hs
View File

@ -15,6 +15,7 @@ module Test.DejaFu.SCT
Way
, systematically
, randomly
, uniformly
, swarmy
, runSCT
, runSCT'
@ -91,7 +92,8 @@ module Test.DejaFu.SCT
-- because a random scheduler is more chaotic than the real
-- scheduler.
, sctRandom
, sctUniformRandom
, sctWeightedRandom
) where
import Control.DeepSeq (NFData(..))
@ -100,7 +102,7 @@ import Data.List (foldl')
import qualified Data.Map.Strict as M
import Data.Set (Set)
import qualified Data.Set as S
import System.Random (RandomGen)
import System.Random (RandomGen, randomR)
import Test.DejaFu.Common
import Test.DejaFu.Conc
@ -113,12 +115,14 @@ import Test.DejaFu.SCT.Internal
--
-- @since unreleased
data Way where
Systematically :: Bounds -> Way
Randomly :: RandomGen g => g -> Int -> Int -> Way
Systematic :: Bounds -> Way
Weighted :: RandomGen g => g -> Int -> Int -> Way
Uniform :: RandomGen g => g -> Int -> Way
instance Show Way where
show (Systematically bs) = "Systematically (" ++ show bs ++ ")"
show (Randomly _ n t) = "Randomly <gen> " ++ show (n, t)
show (Systematic bs) = "Systematic (" ++ show bs ++ ")"
show (Weighted _ n t) = "Weighted <gen> " ++ show (n, t)
show (Uniform _ n) = "Uniform <gen> " ++ show n
-- | Systematically execute a program, trying all distinct executions
-- within the bounds.
@ -130,7 +134,7 @@ systematically
:: Bounds
-- ^ The bounds to constrain the exploration.
-> Way
systematically bs = Systematically Bounds
systematically bs = Systematic Bounds
{ boundPreemp = max 0 <$> boundPreemp bs
, boundFair = max 0 <$> boundFair bs
, boundLength = max 0 <$> boundLength bs
@ -142,9 +146,9 @@ systematically bs = Systematically Bounds
-- Threads are scheduled by a weighted random selection, where weights
-- are assigned randomly on thread creation.
--
-- This corresponds to 'sctRandom' with weight re-use disabled, and is
-- not guaranteed to find all distinct results (unlike
-- 'systematically' / 'sctBound').
-- This corresponds to 'sctWeightedRandom' with weight re-use
-- disabled, and is not guaranteed to find all distinct results
-- (unlike 'systematically' / 'sctBound').
--
-- @since unreleased
randomly :: RandomGen g
@ -155,14 +159,31 @@ randomly :: RandomGen g
-> Way
randomly g lim = swarmy g lim 1
-- | Randomly execute a program, exploring a fixed number of
-- executions.
--
-- Threads are scheduled by a uniform random selection.
--
-- This corresponds to 'sctUniformRandom', and is not guaranteed to
-- find all distinct results (unlike 'systematically' / 'sctBound').
--
-- @since unreleased
uniformly :: RandomGen g
=> g
-- ^ The random generator to drive the scheduling.
-> Int
-- ^ The number of executions to try.
-> Way
uniformly g lim = Uniform g (max 0 lim)
-- | Randomly execute a program, exploring a fixed number of
-- executions.
--
-- Threads are scheduled by a weighted random selection, where weights
-- are assigned randomly on thread creation.
--
-- This corresponds to 'sctRandom', and is not guaranteed to find all
-- distinct results (unlike 'systematically' / 'sctBound').
-- This corresponds to 'sctWeightedRandom', and is not guaranteed to
-- find all distinct results (unlike 'systematically' / 'sctBound').
--
-- @since unreleased
swarmy :: RandomGen g
@ -173,7 +194,7 @@ swarmy :: RandomGen g
-> Int
-- ^ The number of executions to use the thread weights for.
-> Way
swarmy g lim use = Randomly g (max 0 lim) (max 1 use)
swarmy g lim use = Weighted g (max 0 lim) (max 1 use)
-- | Explore possible executions of a concurrent program according to
-- the given 'Way'.
@ -187,8 +208,9 @@ runSCT :: MonadRef r n
-> ConcT r n a
-- ^ The computation to run many times.
-> n [(Either Failure a, Trace)]
runSCT (Systematically cb) memtype = sctBound memtype cb
runSCT (Randomly g lim use) memtype = sctRandom memtype g lim use
runSCT (Systematic cb) memtype = sctBound memtype cb
runSCT (Weighted g lim use) memtype = sctWeightedRandom memtype g lim use
runSCT (Uniform g lim) memtype = sctUniformRandom memtype g lim
-- | A strict variant of 'runSCT'.
--
@ -452,7 +474,7 @@ sctBound memtype cb conc = go initialState where
-- Incorporate the new backtracking steps into the DPOR tree.
addBacktracks = incorporateBacktrackSteps (cBound cb)
-- | SCT via random scheduling.
-- | SCT via uniform random scheduling.
--
-- Schedules are generated by assigning to each new thread a random
-- weight. Threads are then scheduled by a weighted random selection.
@ -460,7 +482,34 @@ sctBound memtype cb conc = go initialState where
-- This is not guaranteed to find all distinct results.
--
-- @since unreleased
sctRandom :: (MonadRef r n, RandomGen g)
sctUniformRandom :: (MonadRef r n, RandomGen g)
=> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> g
-- ^ The random number generator.
-> Int
-- ^ The number of executions to perform.
-> ConcT r n a
-- ^ The computation to run many times.
-> n [(Either Failure a, Trace)]
sctUniformRandom memtype g0 lim0 conc = go g0 lim0 where
go _ 0 = pure []
go g n = do
(res, s, trace) <- runConcurrent (randSched $ \g' -> (1, g'))
memtype
(initialRandSchedState Nothing g)
conc
((res, trace):) <$> go (schedGen s) (n-1)
-- | SCT via weighted random scheduling.
--
-- Schedules are generated by assigning to each new thread a random
-- weight. Threads are then scheduled by a weighted random selection.
--
-- This is not guaranteed to find all distinct results.
--
-- @since unreleased
sctWeightedRandom :: (MonadRef r n, RandomGen g)
=> MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations.
-> g
@ -472,11 +521,11 @@ sctRandom :: (MonadRef r n, RandomGen g)
-> ConcT r n a
-- ^ The computation to run many times.
-> n [(Either Failure a, Trace)]
sctRandom memtype g0 lim0 use0 conc = go g0 lim0 (max 1 use0) M.empty where
sctWeightedRandom memtype g0 lim0 use0 conc = go g0 lim0 (max 1 use0) M.empty where
go _ 0 _ _ = pure []
go g n 0 _ = go g n (max 1 use0) M.empty
go g n use ws = do
(res, s, trace) <- runConcurrent randSched
(res, s, trace) <- runConcurrent (randSched $ randomR (1, 50))
memtype
(initialRandSchedState (Just ws) g)
conc

9
dejafu/Test/DejaFu/SCT/Internal.hs
View File

@ -13,10 +13,9 @@ module Test.DejaFu.SCT.Internal where
import Control.DeepSeq (NFData(..))
import Control.Exception (MaskingState(..))
import Data.Char (ord)
import qualified Data.Foldable as F
import Data.Function (on)
import Data.List (intercalate, nubBy, partition, sortOn)
import Data.List (nubBy, partition, sortOn)
import Data.List.NonEmpty (NonEmpty(..), toList)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
@ -537,8 +536,8 @@ 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 => Scheduler (RandSchedState g)
randSched _ _ threads s = (pick choice enabled, RandSchedState weights' g'') where
randSched :: RandomGen g => (g -> (Int, g)) -> Scheduler (RandSchedState g)
randSched weightf _ _ threads s = (pick choice enabled, RandSchedState weights' g'') where
-- Select a thread
pick idx ((x, f):xs)
| idx < f = Just x
@ -551,7 +550,7 @@ randSched _ _ threads s = (pick choice enabled, RandSchedState weights' g'') whe
weights' = schedWeights s `M.union` M.fromList newWeights
(newWeights, g') = foldr assignWeight ([], schedGen s) $ filter (`M.notMember` schedWeights s) tids
assignWeight tid ~(ws, g0) =
let (w, g) = randomR (1, 50) g0
let (w, g) = weightf g0
in ((tid, w):ws, g)
-- The runnable threads.

1
hunit-dejafu/CHANGELOG.markdown
View File

@ -17,6 +17,7 @@ unreleased
- Due to changes in dejafu, the `Way` type is now abstract and exposes smart constructor functions:
- `systematically`, corresponding to the old `Systematically`.
- `randomly`, corresponding to the old `Randomly`.
- `uniformly`, a new uniform random (as opposed to weighted random) scheduler.
- `swarmy`, corresponding to the old `Randomly` and specifying how many executions to use the
same weights for.
- The `defaultWay`, `defaultMemType`, and `defaultBounds` values are all now re-exported.

1
hunit-dejafu/Test/HUnit/DejaFu.hs
View File

@ -59,6 +59,7 @@ module Test.HUnit.DejaFu
, defaultWay
, systematically
, randomly
, uniformly
, swarmy
, Bounds(..)
, defaultBounds

1
tasty-dejafu/CHANGELOG.markdown
View File

@ -17,6 +17,7 @@ unreleased
- Due to changes in dejafu, the `Way` type is now abstract and exposes smart constructor functions:
- `systematically`, corresponding to the old `Systematically`.
- `randomly`, corresponding to the old `Randomly`.
- `uniformly`, a new uniform random (as opposed to weighted random) scheduler.
- `swarmy`, corresponding to the old `Randomly` and specifying how many executions to use the
same weights for.
- The `defaultWay`, `defaultMemType`, and `defaultBounds` values are all now re-exported.

1
tasty-dejafu/Test/Tasty/DejaFu.hs
View File

@ -56,6 +56,7 @@ module Test.Tasty.DejaFu
, defaultWay
, systematically
, randomly
, uniformly
, swarmy
, Bounds(..)
, defaultBounds