module Test.DejaFu.SCT
(
runSCT
, runSCT'
, resultsSet
, resultsSet'
, runSCTWithSettings
, runSCTWithSettings'
, resultsSetWithSettings
, resultsSetWithSettings'
, module Test.DejaFu.Settings
) where
import Control.Applicative ((<|>))
import Control.DeepSeq (NFData(..), force)
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 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.Settings
import Test.DejaFu.Types
import Test.DejaFu.Utils
runSCT :: MonadDejaFu n
=> Way
-> MemType
-> Program pty n a
-> n [(Either Condition a, Trace)]
runSCT way = runSCTWithSettings . fromWayAndMemType way
resultsSet :: (MonadDejaFu n, Ord a)
=> Way
-> MemType
-> Program pty n a
-> n (Set (Either Condition a))
resultsSet way = resultsSetWithSettings . fromWayAndMemType way
runSCT' :: (MonadDejaFu n, NFData a)
=> Way
-> MemType
-> Program pty n a
-> n [(Either Condition a, Trace)]
runSCT' way = runSCTWithSettings' . fromWayAndMemType way
resultsSet' :: (MonadDejaFu n, Ord a, NFData a)
=> Way
-> MemType
-> Program pty n a
-> n (Set (Either Condition a))
resultsSet' way = resultsSetWithSettings' . fromWayAndMemType way
runSCTWithSettings :: MonadDejaFu n
=> Settings n a
-> Program pty n a
-> n [(Either Condition a, Trace)]
runSCTWithSettings settings conc = case _way settings of
Systematic cb0 ->
let initial = initialState
check = findSchedulePrefix
step cstate0 run dp (prefix, conservative, sleep) = do
(res, s, trace) <- run
(dporSched (_safeIO settings) (cBound (_lengthBound settings) cb0))
(initialDPORSchedState sleep prefix cstate0)
let bpoints = findBacktrackSteps (_safeIO settings) (_memtype settings) (cBacktrack cb0) (schedBoundKill s) cstate0 (schedBPoints s) trace
let newDPOR = incorporateTrace (_safeIO settings) (_memtype settings) conservative trace cstate0 dp
pure $ if schedIgnore s
then (force newDPOR, Nothing)
else (force (incorporateBacktrackSteps bpoints newDPOR), Just (res, trace))
in sct settings initial check step conc
Randomly gen g0 lim0 ->
let initial _ = (g0, max 0 lim0)
check (_, 0) = Nothing
check s = Just s
step _ run _ (g, n) = do
(res, s, trace) <- run
(randSched gen)
(initialRandSchedState (_lengthBound settings) g)
pure ((schedGen s, n-1), Just (res, trace))
in sct settings initial check step conc
resultsSetWithSettings :: (MonadDejaFu n, Ord a)
=> Settings n a
-> Program pty n a
-> n (Set (Either Condition a))
resultsSetWithSettings settings conc =
let settings' = settings { _discard = Just $ \efa -> fromMaybe (const Nothing) (_discard settings) efa <|> Just DiscardTrace }
in S.fromList . map fst <$> runSCTWithSettings settings' conc
runSCTWithSettings' :: (MonadDejaFu n, NFData a)
=> Settings n a
-> Program pty n a
-> n [(Either Condition a, Trace)]
runSCTWithSettings' settings conc = do
res <- runSCTWithSettings settings conc
rnf res `seq` pure res
resultsSetWithSettings' :: (MonadDejaFu n, Ord a, NFData a)
=> Settings n a
-> Program pty n a
-> n (Set (Either Condition a))
resultsSetWithSettings' settings conc = do
res <- resultsSetWithSettings settings conc
rnf res `seq` pure res
cBound :: Maybe LengthBound -> Bounds -> IncrementalBoundFunc ((Int, Maybe ThreadId), M.Map ThreadId Int, Int)
cBound lb (Bounds pb fb) (Just (k1, k2, k3)) prior lh =
let k1' = maybe (\k _ _ -> k) pBound pb (Just k1) prior lh
k2' = maybe (\k _ _ -> k) fBound fb (Just k2) prior lh
k3' = maybe (\k _ _ -> k) lBound lb (Just k3) prior lh
in (,,) <$> k1' <*> k2' <*> k3'
cBound _ _ Nothing _ _ = Just ((0, Nothing), M.empty, 1)
cBacktrack :: Bounds -> BacktrackFunc
cBacktrack (Bounds (Just _) _) bs =
backtrackAt (\_ _ -> False) bs . concatMap addConservative
where
addConservative o@(i, _, tid) = o : case conservative i of
Just j -> [(j, True, tid)]
Nothing -> []
conservative i = go (reverse (take (i-1) bs)) (i-1) where
go _ (-1) = Nothing
go (b1:rest@(b2:_)) j
| bcktThreadid b1 /= bcktThreadid b2
&& not (isCommitRef $ bcktAction b1)
&& not (isCommitRef $ bcktAction b2) = Just j
| otherwise = go rest (j-1)
go _ _ = Nothing
cBacktrack _ bs = backtrackAt (\_ _ -> False) bs
pBound :: PreemptionBound -> IncrementalBoundFunc (Int, Maybe ThreadId)
pBound (PreemptionBound pb) k prior lhead =
let k'@(pcount, _) = preEmpCountInc (fromMaybe (0, Nothing) k) prior lhead
in if pcount <= pb then Just k' else Nothing
fBound :: FairBound -> IncrementalBoundFunc (M.Map ThreadId Int)
fBound (FairBound fb) k prior lhead =
let k' = yieldCountInc (fromMaybe M.empty k) prior lhead
in if not (willYield (snd lhead)) || maxDiff (M.elems k') <= fb
then Just k'
else Nothing
lBound :: LengthBound -> IncrementalBoundFunc Int
lBound (LengthBound lb) len _ _ =
let len' = maybe 1 (+1) len
in if len' < lb then Just len' else Nothing
preEmpCountInc
:: (Int, Maybe ThreadId)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, a)
-> (Int, Maybe ThreadId)
preEmpCountInc (sofar, lastnoncommit) prior (d, _) = case (prior, d) of
(Just (tid, _), Start tnext) -> cswitch tid tnext False
(Just (tid, act), SwitchTo tnext) -> cswitch tid tnext (not (didYield act))
(_, Continue) -> (sofar, lastnoncommit)
(Nothing, _) -> (sofar, lastnoncommit)
where
cswitch tid tnext isPreemptive
| isCommitThread tnext = (sofar, if isCommitThread tid then lastnoncommit else Just tid)
| isCommitThread tid = (if lastnoncommit == Just tnext then sofar else sofar + 1, Nothing)
| otherwise = (if isPreemptive then sofar + 1 else sofar, Nothing)
isCommitThread = (< initialThread)
yieldCountInc
:: M.Map ThreadId Int
-> Maybe (ThreadId, a)
-> (Decision, Lookahead)
-> M.Map ThreadId Int
yieldCountInc sofar prior (d, lnext) = case prior of
Just (tid, _) -> ycount (tidOf tid d)
Nothing -> ycount initialThread
where
ycount tnext
| willYield lnext = M.alter (Just . maybe 1 (+1)) tnext sofar
| otherwise = M.alter (Just . fromMaybe 0) tnext sofar
isCommitRef :: ThreadAction -> Bool
isCommitRef (CommitIORef _ _) = True
isCommitRef _ = False
maxDiff :: [Int] -> Int
maxDiff = go 0 where
go m (x:xs) =
let m' = m `max` foldl' (go' x) 0 xs
in go m' xs
go m [] = m
go' x0 m x = m `max` abs (x0 - x)