barrucadu/dejafu
1
1
Fork 0
mirror of https://github.com/barrucadu/dejafu.git synced 2024-12-20 03:51:39 +03:00
Code Issues Projects Releases Wiki Activity

Merge 'Test.DPOR' with 'Test.DejaFu.SCT'.

Browse Source
This commit is contained in:
Michael Walker 2016-12-04 19:21:06 +00:00
parent 0418f28507
commit db5d5cda17
6 changed files with 186 additions and 523 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

465
dejafu/Test/DPOR.hs
View File

@ -1,465 +0,0 @@
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-- |
-- Module : Test.DPOR
-- Copyright : (c) 2016 Michael Walker
-- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental
-- Portability : GeneralizedNewtypeDeriving
--
-- Systematic testing of concurrent computations through dynamic
-- partial-order reduction and schedule bounding.
module Test.DPOR
( -- * Bounded dynamic partial-order reduction
-- | We can characterise the state of a concurrent computation by
-- considering the ordering of dependent events. This is a partial
-- order: independent events can be performed in any order without
-- affecting the result, and so are /not/ ordered.
--
-- Partial-order reduction is a technique for computing these
-- partial orders, and only testing one total order for each partial
-- order. This cuts down the amount of work to be done
-- significantly. /Bounded/ partial-order reduction is a further
-- optimisation, which only considers schedules within some bound.
--
-- This module provides a generic function for DPOR, parameterised
-- by the actual (domain-specific) dependency function to use.
--
-- See /Bounded partial-order reduction/, K. Coons, M. Musuvathi,
-- K. McKinley for more details.
dpor
, simpleDPOR
, DPOR(..)
-- ** Backtracking
, BacktrackFunc
, BacktrackStep(..)
, backtrackAt
-- ** Bounding
, BoundFunc
, (&+&)
, trueBound
-- *** Preemption
-- | DPOR with preemption bounding. This adds conservative
-- backtracking points at the prior context switch whenever a
-- non-conervative backtracking point is added, as alternative
-- decisions can influence the reachability of different states.
--
-- See the BPOR paper for more details.
, PreemptionBound(..)
, defaultPreemptionBound
, preempBound
, preempBacktrack
, preempCount
-- *** Fair
-- | DPOR using fair bounding. This bounds the maximum difference
-- between the number of yield operations different threads have
-- performed.
--
-- See the DPOR paper for more details.
, FairBound(..)
, defaultFairBound
, fairBound
, fairBacktrack
, yieldCount
, maxYieldCountDiff
-- *** Length
-- | BPOR using length bounding. This bounds the maximum length (in
-- terms of primitive actions) of an execution.
, LengthBound(..)
, defaultLengthBound
, lenBound
, lenBacktrack
-- * Scheduling & execution traces
-- | The partial-order reduction is driven by incorporating
-- information gained from trial executions of the concurrent
-- program.
, DPORScheduler
, SchedState
, Trace
, module Test.DPOR.Schedule
) where
import Control.DeepSeq (NFData)
import Data.List (nub)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.Map.Strict as M
import Test.DPOR.Internal
import Test.DPOR.Schedule
-------------------------------------------------------------------------------
-- Bounded dynamic partial-order reduction
-- | Dynamic partial-order reduction.
--
-- This takes a lot of functional parameters because it's so generic,
-- but most are fairly simple.
--
-- Some state may be maintained when determining backtracking points,
-- which can then inform the dependency functions. This state is not
-- preserved between different schedules, and built up from scratch
-- each time.
--
-- The dependency functions must be consistent: if we can convert
-- between @action@ and @lookahead@, and supply some sensible default
-- state, then (1) == true implies that (2) is. In practice, (1) is
-- the most specific and (2) will be more pessimistic (due to,
-- typically, less information being available when merely looking
-- ahead).
--
-- The daemon-termination predicate returns @True@ if the action being
-- looked at will cause the entire computation to terminate,
-- regardless of the other runnable threads (which are passed in the
-- 'NonEmpty' list). Such actions will then be put off for as long as
-- possible. This allows supporting concurrency models with daemon
-- threads without doing something as drastic as imposing a dependency
-- between the program-terminating action and /everything/ else.
dpor :: ( Ord tid
, NFData tid
, NFData action
, NFData lookahead
, NFData s
, Monad m
)
=> (action -> Bool)
-- ^ Determine if a thread yielded.
-> (lookahead -> Bool)
-- ^ Determine if a thread will yield.
-> s
-- ^ The initial state for backtracking.
-> (s -> (tid, action) -> s)
-- ^ The backtracking state step function.
-> (s -> (tid, action) -> (tid, action) -> Bool)
-- ^ The dependency (1) function.
-> (s -> (tid, action) -> (tid, lookahead) -> Bool)
-- ^ The dependency (2) function.
-> (s -> (tid, lookahead) -> NonEmpty tid -> Bool)
-- ^ The daemon-termination predicate.
-> tid
-- ^ The initial thread.
-> (tid -> Bool)
-- ^ The thread partitioning function: when choosing what to
-- execute, prefer threads which return true.
-> BoundFunc tid action lookahead
-- ^ The bounding function.
-> BacktrackFunc tid action lookahead s
-- ^ The backtracking function. Note that, for some bounding
-- functions, this will need to add conservative backtracking
-- points.
-> (DPOR tid action -> DPOR tid action)
-- ^ Some post-processing to do after adding the new to-do points.
-> (DPORScheduler tid action lookahead s
-> SchedState tid action lookahead s
-> m (a, SchedState tid action lookahead s, Trace tid action lookahead))
-- ^ The runner: given the scheduler and state, execute the
-- computation under that scheduler.
-> m [(a, Trace tid action lookahead)]
dpor didYield
willYield
stinit
ststep
dependency1
dependency2
killsDaemons
initialTid
predicate
inBound
backtrack
transform
run
= go (initialState initialTid)
where
-- Repeatedly run the computation gathering all the results and
-- traces into a list until there are no schedules remaining to
-- try.
go dp = case nextPrefix dp of
Just (prefix, conservative, sleep, ()) -> do
(res, s, trace) <- run scheduler
(initialSchedState stinit sleep prefix)
let bpoints = findBacktracks (schedBoundKill s) (schedBPoints s) trace
let newDPOR = addTrace conservative trace dp
if schedIgnore s
then go newDPOR
else ((res, trace):) <$> go (transform $ addBacktracks bpoints newDPOR)
Nothing -> pure []
-- Find the next schedule prefix.
nextPrefix = findSchedulePrefix predicate (const (0, ()))
-- The DPOR scheduler.
scheduler = dporSched didYield willYield dependency1 killsDaemons ststep inBound
-- Find the new backtracking steps.
findBacktracks = findBacktrackSteps stinit ststep dependency2 backtrack
-- Incorporate a trace into the DPOR tree.
addTrace = incorporateTrace stinit ststep dependency1
-- Incorporate the new backtracking steps into the DPOR tree.
addBacktracks = incorporateBacktrackSteps inBound
-- | A much simplified DPOR function: no state, no preference between
-- threads, and no post-processing between iterations.
simpleDPOR :: ( Ord tid
, NFData tid
, NFData action
, NFData lookahead
, Monad m
)
=> (action -> Bool)
-- ^ Determine if a thread yielded.
-> (lookahead -> Bool)
-- ^ Determine if a thread will yield.
-> ((tid, action) -> (tid, action) -> Bool)
-- ^ The dependency (1) function.
-> ((tid, action) -> (tid, lookahead) -> Bool)
-- ^ The dependency (2) function.
-> ((tid, lookahead) -> NonEmpty tid -> Bool)
-- ^ The daemon-termination predicate.
-> tid
-- ^ The initial thread.
-> BoundFunc tid action lookahead
-- ^ The bounding function.
-> BacktrackFunc tid action lookahead ()
-- ^ The backtracking function. Note that, for some bounding
-- functions, this will need to add conservative backtracking
-- points.
-> (DPORScheduler tid action lookahead ()
-> SchedState tid action lookahead ()
-> m (a, SchedState tid action lookahead (), Trace tid action lookahead))
-- ^ The runner: given the scheduler and state, execute the
-- computation under that scheduler.
-> m [(a, Trace tid action lookahead)]
simpleDPOR didYield
willYield
dependency1
dependency2
killsDaemons
initialTid
inBound
backtrack
= dpor didYield
willYield
()
(\_ _ -> ())
(const dependency1)
(const dependency2)
(const killsDaemons)
initialTid
(const True)
inBound
backtrack
id
-------------------------------------------------------------------------------
-- Bounds
-- | Combine two bounds into a larger bound, where both must be
-- satisfied.
(&+&) :: BoundFunc tid action lookahead
-> BoundFunc tid action lookahead
-> BoundFunc tid action lookahead
(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl
-------------------------------------------------------------------------------
-- Preemption bounding
newtype PreemptionBound = PreemptionBound Int
deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | A sensible default preemption bound: 2.
--
-- See /Concurrency Testing Using Schedule Bounding: an Empirical Study/,
-- P. Thomson, A. F. Donaldson, A. Betts for justification.
defaultPreemptionBound :: PreemptionBound
defaultPreemptionBound = 2
-- | Preemption bound function
preempBound :: (action -> Bool)
-- ^ Determine if a thread yielded.
-> PreemptionBound
-> BoundFunc tid action lookahead
preempBound didYield (PreemptionBound pb) ts dl =
preempCount didYield ts dl <= pb
-- | Add a backtrack point, and also conservatively add one prior to
-- the most recent transition before that point. This may result in
-- the same state being reached multiple times, but is needed because
-- of the artificial dependency imposed by the bound.
preempBacktrack :: Ord tid
=> (action -> Bool)
-- ^ If this is true of the action at a preemptive context switch,
-- do NOT use that point for the conservative point, try earlier.
-> BacktrackFunc tid action lookahead s
preempBacktrack ignore bs i tid =
maybe id (\j' b -> backtrack True b j' tid) j $ backtrack False bs i tid
where
-- Index of the conservative point
j = goJ . reverse . pairs $ zip [0..i-1] bs where
goJ (((_,b1), (j',b2)):rest)
| bcktThreadid b1 /= bcktThreadid b2
&& not (ignore . snd $ bcktDecision b1)
&& not (ignore . snd $ bcktDecision b2) = Just j'
| otherwise = goJ rest
goJ [] = Nothing
-- List of adjacent pairs
{-# INLINE pairs #-}
pairs = zip <*> tail
-- Add a backtracking point.
backtrack = backtrackAt $ const False
-- | Count the number of preemptions in a schedule prefix.
preempCount :: (action -> Bool)
-- ^ Determine if a thread yielded.
-> [(Decision tid, action)]
-- ^ The schedule prefix.
-> (Decision tid, lookahead)
-- ^ The to-do point.
-> Int
preempCount didYield ts (d, _) = go Nothing ts where
go p ((d', a):rest) = preempC p d' + go (Just a) rest
go p [] = preempC p d
preempC (Just act) (SwitchTo _) | didYield act = 0
preempC _ (SwitchTo _) = 1
preempC _ _ = 0
-------------------------------------------------------------------------------
-- Fair bounding
newtype FairBound = FairBound Int
deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | A sensible default fair bound: 5.
--
-- This comes from playing around myself, but there is probably a
-- better default.
defaultFairBound :: FairBound
defaultFairBound = 5
-- | Fair bound function
fairBound :: Eq tid
=> (action -> Bool)
-- ^ Determine if a thread yielded.
-> (lookahead -> Bool)
-- ^ Determine if a thread will yield.
-> (action -> [tid])
-- ^ The new threads an action causes to come into existence.
-> FairBound -> BoundFunc tid action lookahead
fairBound didYield willYield forkTids (FairBound fb) ts dl =
maxYieldCountDiff didYield willYield forkTids ts dl <= fb
-- | Add a backtrack point. If the thread isn't runnable, or performs
-- a release operation, add all runnable threads.
fairBacktrack :: Ord tid
=> (lookahead -> Bool)
-- ^ Determine if an action is a release operation: if it could
-- cause other threads to become runnable.
-> BacktrackFunc tid action lookahead s
fairBacktrack willRelease bs i t = backtrackAt check False bs i t where
-- True if a release operation is performed.
check b = Just True == (willRelease <$> M.lookup t (bcktRunnable b))
-- | Count the number of yields by a thread in a schedule prefix.
yieldCount :: Eq tid
=> (action -> Bool)
-- ^ Determine if a thread yielded.
-> (lookahead -> Bool)
-- ^ Determine if a thread will yield.
-> tid
-- ^ The thread to count yields for.
-> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int
yieldCount didYield willYield tid ts (ld, l) = go initialThread ts where
go t ((Start t', act):rest) = go' t t' act rest
go t ((SwitchTo t', act):rest) = go' t t' act rest
go t ((Continue, act):rest) = go' t t act rest
go t []
| t == tid && willYield l = 1
| otherwise = 0
go' t t' act rest
| t == tid && didYield act = 1 + go t' rest
| otherwise = go t' rest
-- The initial thread ID
initialThread = case (ts, ld) of
((Start t, _):_, _) -> t
([], Start t) -> t
_ -> error "yieldCount: unknown initial thread."
-- | Get the maximum difference between the yield counts of all
-- threads in this schedule prefix.
maxYieldCountDiff :: Eq tid
=> (action -> Bool)
-- ^ Determine if a thread yielded.
-> (lookahead -> Bool)
-- ^ Determine if a thread will yield.
-> (action -> [tid])
-- ^ The new threads an action causes to come into existence.
-> [(Decision tid, action)] -> (Decision tid, lookahead) -> Int
maxYieldCountDiff didYield willYield forkTids ts dl = maximum yieldCountDiffs
where
yieldsBy tid = yieldCount didYield willYield tid ts dl
yieldCounts = [yieldsBy tid | tid <- nub $ allTids ts]
yieldCountDiffs = [y1 - y2 | y1 <- yieldCounts, y2 <- yieldCounts]
-- All the threads created during the lifetime of the system.
allTids ((_, act):rest) =
let tids' = forkTids act
in if null tids' then allTids rest else tids' ++ allTids rest
allTids [] = [initialThread]
-- The initial thread ID
initialThread = case (ts, dl) of
((Start t, _):_, _) -> t
([], (Start t, _)) -> t
_ -> error "maxYieldCountDiff: unknown initial thread."
-------------------------------------------------------------------------------
-- Length bounding
newtype LengthBound = LengthBound Int
deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | A sensible default length bound: 250.
--
-- Based on the assumption that anything which executes for much
-- longer (or even this long) will take ages to test.
defaultLengthBound :: LengthBound
defaultLengthBound = 250
-- | Length bound function
lenBound :: LengthBound -> BoundFunc tid action lookahead
lenBound (LengthBound lb) ts _ = length ts < lb
-- | Add a backtrack point. If the thread isn't runnable, add all
-- runnable threads.
lenBacktrack :: Ord tid => BacktrackFunc tid action lookahead s
lenBacktrack = backtrackAt (const False) False

4
dejafu/Test/DPOR/Internal.hs
View File

@ -406,10 +406,6 @@ initialSchedState s sleep prefix = SchedState
type BoundFunc tid action lookahead type BoundFunc tid action lookahead
= [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool = [(Decision tid, action)] -> (Decision tid, lookahead) -> Bool
-- | The \"true\" bound, which allows everything.
trueBound :: BoundFunc tid action lookahead
trueBound _ _ = True
-- | A backtracking step is a point in the execution where another -- | A backtracking step is a point in the execution where another
-- decision needs to be made, in order to explore interesting new -- decision needs to be made, in order to explore interesting new
-- schedules. A backtracking /function/ takes the steps identified so -- schedules. A backtracking /function/ takes the steps identified so

3
dejafu/Test/DejaFu/Common.hs
View File

@ -67,7 +67,8 @@ import Data.List (sort, nub, intercalate)
import Data.Maybe (fromMaybe, mapMaybe) import Data.Maybe (fromMaybe, mapMaybe)
import Data.Set (Set) import Data.Set (Set)
import qualified Data.Set as S import qualified Data.Set as S
import Test.DPOR (Decision(..), Trace) import Test.DPOR.Schedule (Decision(..))
import Test.DPOR.Internal (Trace)
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
-- Identifiers -- Identifiers

2
dejafu/Test/DejaFu/Conc/Internal.hs
View File

@ -22,7 +22,7 @@ import Data.List (sort)
import Data.List.NonEmpty (NonEmpty(..), fromList) import Data.List.NonEmpty (NonEmpty(..), fromList)
import qualified Data.Map.Strict as M import qualified Data.Map.Strict as M
import Data.Maybe (fromJust, isJust, isNothing, listToMaybe) import Data.Maybe (fromJust, isJust, isNothing, listToMaybe)
import Test.DPOR (Scheduler) import Test.DPOR.Schedule (Scheduler)
import Test.DejaFu.Common import Test.DejaFu.Common
import Test.DejaFu.Conc.Internal.Common import Test.DejaFu.Conc.Internal.Common

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

@ -1,10 +1,12 @@
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-- | -- |
-- Module : Test.DejaFu.SCT -- Module : Test.DejaFu.SCT
-- Copyright : (c) 2016 Michael Walker -- Copyright : (c) 2016 Michael Walker
-- License : MIT -- License : MIT
-- Maintainer : Michael Walker <mike@barrucadu.co.uk> -- Maintainer : Michael Walker <mike@barrucadu.co.uk>
-- Stability : experimental -- Stability : experimental
-- Portability : portable -- Portability : GeneralizedNewtypeDeriving
-- --
-- Systematic testing for concurrent computations. -- Systematic testing for concurrent computations.
module Test.DejaFu.SCT module Test.DejaFu.SCT
@ -62,8 +64,8 @@ module Test.DejaFu.SCT
, PreemptionBound(..) , PreemptionBound(..)
, defaultPreemptionBound , defaultPreemptionBound
, sctPreBound , sctPreBound
, pBacktrack
, pBound , pBound
, pBacktrack
-- ** Fair Bounding -- ** Fair Bounding
@ -76,8 +78,8 @@ module Test.DejaFu.SCT
, FairBound(..) , FairBound(..)
, defaultFairBound , defaultFairBound
, sctFairBound , sctFairBound
, fBacktrack
, fBound , fBound
, fBacktrack
-- ** Length Bounding -- ** Length Bounding
@ -87,26 +89,23 @@ module Test.DejaFu.SCT
, LengthBound(..) , LengthBound(..)
, defaultLengthBound , defaultLengthBound
, sctLengthBound , sctLengthBound
, lBound
, lBacktrack
-- * Backtracking -- * Backtracking
, BacktrackStep(..) , I.BacktrackStep(..)
, BacktrackFunc , I.BacktrackFunc
) where ) where
import Control.DeepSeq (NFData(..)) import Control.DeepSeq (NFData(..))
import Control.Monad.Ref (MonadRef) import Control.Monad.Ref (MonadRef)
import Data.List (nub)
import Data.Map.Strict (Map) import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M import qualified Data.Map.Strict as M
import Data.Maybe (isJust, fromJust) import Data.Maybe (isJust, fromJust)
import qualified Data.Set as S import qualified Data.Set as S
import Test.DPOR ( DPOR(..), dpor import qualified Test.DPOR.Internal as I
, BacktrackFunc, BacktrackStep(..), backtrackAt
, BoundFunc, (&+&), trueBound
, PreemptionBound(..), defaultPreemptionBound, preempBacktrack
, FairBound(..), defaultFairBound, fairBound, fairBacktrack
, LengthBound(..), defaultLengthBound, lenBound, lenBacktrack
)
import Test.DejaFu.Common import Test.DejaFu.Common
import Test.DejaFu.Conc import Test.DejaFu.Conc
@ -150,23 +149,36 @@ sctBound :: MonadRef r n
sctBound memtype cb = sctBounded memtype (cBound cb) (cBacktrack cb) sctBound memtype cb = sctBounded memtype (cBound cb) (cBacktrack cb)
-- | Combination bound function -- | Combination bound function
cBound :: Bounds -> BoundFunc ThreadId ThreadAction Lookahead cBound :: Bounds -> I.BoundFunc ThreadId ThreadAction Lookahead
cBound (Bounds pb fb lb) = maybe trueBound pBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lenBound lb cBound (Bounds pb fb lb) =
maybe trueBound pBound pb &+&
maybe trueBound fBound fb &+&
maybe trueBound lBound lb
-- | Combination backtracking function. Add all backtracking points -- | Combination backtracking function. Add all backtracking points
-- corresponding to enabled bound functions. -- corresponding to enabled bound functions.
-- --
-- If no bounds are enabled, just backtrack to the given point. -- If no bounds are enabled, just backtrack to the given point.
cBacktrack :: Bounds -> BacktrackFunc ThreadId ThreadAction Lookahead s cBacktrack :: Bounds -> I.BacktrackFunc ThreadId ThreadAction Lookahead s
cBacktrack (Bounds Nothing Nothing Nothing) bs i t = backtrackAt (const False) False bs i t cBacktrack (Bounds Nothing Nothing Nothing) bs i t = I.backtrackAt (const False) False bs i t
cBacktrack (Bounds pb fb lb) bs i t = lBack . fBack $ pBack bs where cBacktrack (Bounds pb fb lb) bs i t = lBack . fBack $ pBack bs where
pBack backs = if isJust pb then pBacktrack backs i t else backs pBack backs = if isJust pb then pBacktrack backs i t else backs
fBack backs = if isJust fb then fBacktrack backs i t else backs fBack backs = if isJust fb then fBacktrack backs i t else backs
lBack backs = if isJust lb then lenBacktrack backs i t else backs lBack backs = if isJust lb then lBacktrack backs i t else backs
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
-- Pre-emption bounding -- Pre-emption bounding
newtype PreemptionBound = PreemptionBound Int
deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | A sensible default preemption bound: 2.
--
-- See /Concurrency Testing Using Schedule Bounding: an Empirical Study/,
-- P. Thomson, A. F. Donaldson, A. Betts for justification.
defaultPreemptionBound :: PreemptionBound
defaultPreemptionBound = 2
-- | An SCT runner using a pre-emption bounding scheduler. -- | An SCT runner using a pre-emption bounding scheduler.
sctPreBound :: MonadRef r n sctPreBound :: MonadRef r n
=> MemType => MemType
@ -179,22 +191,49 @@ sctPreBound :: MonadRef r n
-> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctPreBound memtype pb = sctBounded memtype (pBound pb) pBacktrack sctPreBound memtype pb = sctBounded memtype (pBound pb) pBacktrack
-- | Pre-emption bound function. This does not count pre-emptive
-- context switches to a commit thread.
pBound :: PreemptionBound -> I.BoundFunc ThreadId ThreadAction Lookahead
pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb
-- | Add a backtrack point, and also conservatively add one prior to -- | Add a backtrack point, and also conservatively add one prior to
-- the most recent transition before that point. This may result in -- the most recent transition before that point. This may result in
-- the same state being reached multiple times, but is needed because -- the same state being reached multiple times, but is needed because
-- of the artificial dependency imposed by the bound. -- of the artificial dependency imposed by the bound.
pBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s pBacktrack :: I.BacktrackFunc ThreadId ThreadAction Lookahead s
pBacktrack = preempBacktrack isCommitRef pBacktrack bs i tid =
maybe id (\j' b -> backtrack True b j' tid) j $ backtrack False bs i tid
-- | Pre-emption bound function. This is different to @preempBound@ in where
-- that it does not count pre-emptive context switches to a commit -- Index of the conservative point
-- thread. j = goJ . reverse . pairs $ zip [0..i-1] bs where
pBound :: PreemptionBound -> BoundFunc ThreadId ThreadAction Lookahead goJ (((_,b1), (j',b2)):rest)
pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb | I.bcktThreadid b1 /= I.bcktThreadid b2
&& not (isCommitRef . snd $ I.bcktDecision b1)
&& not (isCommitRef . snd $ I.bcktDecision b2) = Just j'
| otherwise = goJ rest
goJ [] = Nothing
-- List of adjacent pairs
{-# INLINE pairs #-}
pairs = zip <*> tail
-- Add a backtracking point.
backtrack = I.backtrackAt $ const False
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
-- Fair bounding -- Fair bounding
newtype FairBound = FairBound Int
deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | A sensible default fair bound: 5.
--
-- This comes from playing around myself, but there is probably a
-- better default.
defaultFairBound :: FairBound
defaultFairBound = 5
-- | An SCT runner using a fair bounding scheduler. -- | An SCT runner using a fair bounding scheduler.
sctFairBound :: MonadRef r n sctFairBound :: MonadRef r n
=> MemType => MemType
@ -208,17 +247,29 @@ sctFairBound :: MonadRef r n
sctFairBound memtype fb = sctBounded memtype (fBound fb) fBacktrack sctFairBound memtype fb = sctBounded memtype (fBound fb) fBacktrack
-- | Fair bound function -- | Fair bound function
fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead fBound :: FairBound -> I.BoundFunc ThreadId ThreadAction Lookahead
fBound = fairBound didYield willYield (\act -> case act of Fork t -> [t]; _ -> []) fBound (FairBound fb) ts (_, l) = maxYieldCountDiff ts l <= fb
-- | Add a backtrack point. If the thread isn't runnable, or performs -- | Add a backtrack point. If the thread isn't runnable, or performs
-- a release operation, add all runnable threads. -- a release operation, add all runnable threads.
fBacktrack :: BacktrackFunc ThreadId ThreadAction Lookahead s fBacktrack :: I.BacktrackFunc ThreadId ThreadAction Lookahead s
fBacktrack = fairBacktrack willRelease fBacktrack bs i t = I.backtrackAt check False bs i t where
-- True if a release operation is performed.
check b = Just True == (willRelease <$> M.lookup t (I.bcktRunnable b))
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
-- Length bounding -- Length bounding
newtype LengthBound = LengthBound Int
deriving (NFData, Enum, Eq, Ord, Num, Real, Integral, Read, Show)
-- | A sensible default length bound: 250.
--
-- Based on the assumption that anything which executes for much
-- longer (or even this long) will take ages to test.
defaultLengthBound :: LengthBound
defaultLengthBound = 250
-- | An SCT runner using a length bounding scheduler. -- | An SCT runner using a length bounding scheduler.
sctLengthBound :: MonadRef r n sctLengthBound :: MonadRef r n
=> MemType => MemType
@ -229,7 +280,16 @@ sctLengthBound :: MonadRef r n
-> Conc n r a -> Conc n r a
-- ^ The computation to run many times -- ^ The computation to run many times
-> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctLengthBound memtype lb = sctBounded memtype (lenBound lb) lenBacktrack sctLengthBound memtype lb = sctBounded memtype (lBound lb) lBacktrack
-- | Length bound function
lBound :: LengthBound -> I.BoundFunc tid action lookahead
lBound (LengthBound lb) ts _ = length ts < lb
-- | Add a backtrack point. If the thread isn't runnable, add all
-- runnable threads.
lBacktrack :: Ord tid => I.BacktrackFunc tid action lookahead s
lBacktrack = I.backtrackAt (const False) False
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
-- DPOR -- DPOR
@ -249,29 +309,51 @@ sctLengthBound memtype lb = sctBounded memtype (lenBound lb) lenBacktrack
sctBounded :: MonadRef r n sctBounded :: MonadRef r n
=> MemType => MemType
-- ^ The memory model to use for non-synchronised @CRef@ operations. -- ^ The memory model to use for non-synchronised @CRef@ operations.
-> BoundFunc ThreadId ThreadAction Lookahead -> I.BoundFunc ThreadId ThreadAction Lookahead
-- ^ Check if a prefix trace is within the bound -- ^ Check if a prefix trace is within the bound
-> BacktrackFunc ThreadId ThreadAction Lookahead DepState -> I.BacktrackFunc ThreadId ThreadAction Lookahead DepState
-- ^ Add a new backtrack point, this takes the history of the -- ^ Add a new backtrack point, this takes the history of the
-- execution so far, the index to insert the backtracking point, and -- execution so far, the index to insert the backtracking point, and
-- the thread to backtrack to. This may insert more than one -- the thread to backtrack to. This may insert more than one
-- backtracking point. -- backtracking point.
-> Conc n r a -> Conc n r a
-> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)] -> n [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctBounded memtype bf backtrack conc = sctBounded memtype bf backtrack conc = go (I.initialState initialThread) where
dpor didYield -- Repeatedly run the computation gathering all the results and
willYield -- traces into a list until there are no schedules remaining to try.
initialDepState go dp = case nextPrefix dp of
updateDepState Just (prefix, conservative, sleep, ()) -> do
(dependent memtype) (res, s, trace) <- runConcurrent scheduler
(dependent' memtype) memtype
(\_ (t, l) _ -> t == initialThread && case l of WillStop -> True; _ -> False) (I.initialSchedState initialDepState sleep prefix)
initialThread conc
(>=initialThread)
bf let bpoints = findBacktracks (I.schedBoundKill s) (I.schedBPoints s) trace
backtrack let newDPOR = addTrace conservative trace dp
pruneCommits
(\sched s -> runConcurrent sched memtype s conc) if I.schedIgnore s
then go newDPOR
else ((res, trace):) <$> go (pruneCommits $ addBacktracks bpoints newDPOR)
Nothing -> pure []
-- Find the next schedule prefix.
nextPrefix = I.findSchedulePrefix (>=initialThread) (const (0, ()))
-- The DPOR scheduler.
scheduler = I.dporSched didYield willYield (dependent memtype) killsDaemons updateDepState bf
-- Find the new backtracking steps.
findBacktracks = I.findBacktrackSteps initialDepState updateDepState (dependent' memtype) backtrack
-- Incorporate a trace into the DPOR tree.
addTrace = I.incorporateTrace initialDepState updateDepState (dependent memtype)
-- Incorporate the new backtracking steps into the DPOR tree.
addBacktracks = I.incorporateBacktrackSteps bf
-- Check if an action kills daemon threads.
killsDaemons _ (t, l) _ = t == initialThread && case l of WillStop -> True; _ -> False
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
-- Post-processing -- Post-processing
@ -281,18 +363,18 @@ sctBounded memtype bf backtrack conc =
-- --
-- To get the benefit from this, do not execute commit actions from -- To get the benefit from this, do not execute commit actions from
-- the todo set until there are no other choises. -- the todo set until there are no other choises.
pruneCommits :: DPOR ThreadId ThreadAction -> DPOR ThreadId ThreadAction pruneCommits :: I.DPOR ThreadId ThreadAction -> I.DPOR ThreadId ThreadAction
pruneCommits bpor pruneCommits bpor
| not onlycommits || not alldonesync = go bpor | not onlycommits || not alldonesync = go bpor
| otherwise = go bpor { dporTodo = M.empty } | otherwise = go bpor { I.dporTodo = M.empty }
where where
go b = b { dporDone = pruneCommits <$> dporDone bpor } go b = b { I.dporDone = pruneCommits <$> I.dporDone bpor }
onlycommits = all (<initialThread) . M.keys $ dporTodo bpor onlycommits = all (<initialThread) . M.keys $ I.dporTodo bpor
alldonesync = all barrier . M.elems $ dporDone bpor alldonesync = all barrier . M.elems $ I.dporDone bpor
barrier = isBarrier . simplifyAction . fromJust . dporAction barrier = isBarrier . simplifyAction . fromJust . I.dporAction
------------------------------------------------------------------------------- -------------------------------------------------------------------------------
-- Dependency function -- Dependency function
@ -521,3 +603,53 @@ didYield _ = False
willYield :: Lookahead -> Bool willYield :: Lookahead -> Bool
willYield WillYield = True willYield WillYield = True
willYield _ = False willYield _ = False
-- | Extra threads created in a fork.
forkTids :: ThreadAction -> [ThreadId]
forkTids (Fork t) = [t]
forkTids _ = []
-- | Count the number of yields by a thread in a schedule prefix.
yieldCount :: ThreadId
-- ^ The thread to count yields for.
-> [(Decision ThreadId, ThreadAction)]
-> Lookahead
-> Int
yieldCount tid ts l = go initialThread ts where
go t ((Start t', act):rest) = go' t t' act rest
go t ((SwitchTo t', act):rest) = go' t t' act rest
go t ((Continue, act):rest) = go' t t act rest
go t []
| t == tid && willYield l = 1
| otherwise = 0
go' t t' act rest
| t == tid && didYield act = 1 + go t' rest
| otherwise = go t' rest
-- | Get the maximum difference between the yield counts of all
-- threads in this schedule prefix.
maxYieldCountDiff :: [(Decision ThreadId, ThreadAction)]
-> Lookahead
-> Int
maxYieldCountDiff ts l = maximum yieldCountDiffs where
yieldsBy tid = yieldCount tid ts l
yieldCounts = [yieldsBy tid | tid <- nub $ allTids ts]
yieldCountDiffs = [y1 - y2 | y1 <- yieldCounts, y2 <- yieldCounts]
-- All the threads created during the lifetime of the system.
allTids ((_, act):rest) =
let tids' = forkTids act
in if null tids' then allTids rest else tids' ++ allTids rest
allTids [] = [initialThread]
-- | The \"true\" bound, which allows everything.
trueBound :: I.BoundFunc tid action lookahead
trueBound _ _ = True
-- | Combine two bounds into a larger bound, where both must be
-- satisfied.
(&+&) :: I.BoundFunc tid action lookahead
-> I.BoundFunc tid action lookahead
-> I.BoundFunc tid action lookahead
(&+&) b1 b2 ts dl = b1 ts dl && b2 ts dl

1
dejafu/dejafu.cabal
View File

@ -83,7 +83,6 @@ library
, Test.DejaFu.SCT , Test.DejaFu.SCT
, Test.DejaFu.STM , Test.DejaFu.STM
, Test.DPOR
, Test.DPOR.Internal , Test.DPOR.Internal
, Test.DPOR.Schedule , Test.DPOR.Schedule