module Test.DejaFu.SCT
(
BacktrackStep(..)
, sctBounded
, sctBoundedIO
, Bounds(..)
, defaultBounds
, noBounds
, sctBound
, sctBoundIO
, PreemptionBound(..)
, defaultPreemptionBound
, sctPreBound
, sctPreBoundIO
, pBacktrack
, pBound
, FairBound(..)
, defaultFairBound
, sctFairBound
, sctFairBoundIO
, fBacktrack
, fBound
, LengthBound(..)
, defaultLengthBound
, sctLengthBound
, sctLengthBoundIO
) where
import Data.Functor.Identity (Identity(..), runIdentity)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as M
import Data.Maybe (isJust, fromJust)
import Test.DPOR ( DPOR(..), dpor
, BacktrackStep(..), backtrackAt
, BoundFunc, (&+&), trueBound
, PreemptionBound(..), defaultPreemptionBound, preempBacktrack
, FairBound(..), defaultFairBound, fairBound, fairBacktrack
, LengthBound(..), defaultLengthBound, lenBound, lenBacktrack
)
import Test.DejaFu.Deterministic (ConcIO, ConcST, runConcIO, runConcST)
import Test.DejaFu.Deterministic.Internal
data Bounds = Bounds
{ boundPreemp :: Maybe PreemptionBound
, boundFair :: Maybe FairBound
, boundLength :: Maybe LengthBound
}
defaultBounds :: Bounds
defaultBounds = Bounds
{ boundPreemp = Just defaultPreemptionBound
, boundFair = Just defaultFairBound
, boundLength = Just defaultLengthBound
}
noBounds :: Bounds
noBounds = Bounds
{ boundPreemp = Nothing
, boundFair = Nothing
, boundLength = Nothing
}
sctBound :: MemType
-> Bounds
-> (forall t. ConcST t a)
-> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctBound memtype cb = sctBounded memtype (cBound cb) (cBacktrack cb)
sctBoundIO :: MemType
-> Bounds
-> ConcIO a
-> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctBoundIO memtype cb = sctBoundedIO memtype (cBound cb) (cBacktrack cb)
cBound :: Bounds -> BoundFunc ThreadId ThreadAction Lookahead
cBound (Bounds pb fb lb) = maybe trueBound pBound pb &+& maybe trueBound fBound fb &+& maybe trueBound lenBound lb
cBacktrack :: Bounds
-> [BacktrackStep ThreadId ThreadAction Lookahead s]
-> Int
-> ThreadId
-> [BacktrackStep ThreadId ThreadAction Lookahead s]
cBacktrack (Bounds Nothing Nothing Nothing) bs i t = backtrackAt (const False) False bs i t
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
fBack backs = if isJust fb then fBacktrack backs i t else backs
lBack backs = if isJust lb then lenBacktrack backs i t else backs
sctPreBound :: MemType
-> PreemptionBound
-> (forall t. ConcST t a)
-> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctPreBound memtype pb = sctBounded memtype (pBound pb) pBacktrack
sctPreBoundIO :: MemType
-> PreemptionBound
-> ConcIO a
-> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctPreBoundIO memtype pb = sctBoundedIO memtype (pBound pb) pBacktrack
pBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s]
-> Int
-> ThreadId
-> [BacktrackStep ThreadId ThreadAction Lookahead s]
pBacktrack = preempBacktrack isCommitRef
pBound :: PreemptionBound -> BoundFunc ThreadId ThreadAction Lookahead
pBound (PreemptionBound pb) ts dl = preEmpCount ts dl <= pb
sctFairBound :: MemType
-> FairBound
-> (forall t. ConcST t a)
-> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctFairBound memtype fb = sctBounded memtype (fBound fb) fBacktrack
sctFairBoundIO :: MemType
-> FairBound
-> ConcIO a
-> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctFairBoundIO memtype fb = sctBoundedIO memtype (fBound fb) fBacktrack
fBound :: FairBound -> BoundFunc ThreadId ThreadAction Lookahead
fBound = fairBound didYield willYield (\act -> case act of Fork t -> [t]; _ -> [])
fBacktrack :: [BacktrackStep ThreadId ThreadAction Lookahead s]
-> Int
-> ThreadId
-> [BacktrackStep ThreadId ThreadAction Lookahead s]
fBacktrack = fairBacktrack willRelease
sctLengthBound :: MemType
-> LengthBound
-> (forall t. ConcST t a)
-> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctLengthBound memtype lb = sctBounded memtype (lenBound lb) lenBacktrack
sctLengthBoundIO :: MemType
-> LengthBound
-> ConcIO a
-> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctLengthBoundIO memtype lb = sctBoundedIO memtype (lenBound lb) lenBacktrack
sctBounded :: MemType
-> BoundFunc ThreadId ThreadAction Lookahead
-> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])
-> (forall t. ConcST t a) -> [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctBounded memtype bf backtrack c = runIdentity $ sctBoundedM memtype bf backtrack run where
run memty sched s = Identity $ runConcST sched memty s c
sctBoundedIO :: MemType
-> BoundFunc ThreadId ThreadAction Lookahead
-> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])
-> ConcIO a -> IO [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctBoundedIO memtype bf backtrack c = sctBoundedM memtype bf backtrack run where
run memty sched s = runConcIO sched memty s c
sctBoundedM :: Monad m
=> MemType
-> ([(Decision ThreadId, ThreadAction)] -> (Decision ThreadId, Lookahead) -> Bool)
-> ([BacktrackStep ThreadId ThreadAction Lookahead CRState] -> Int -> ThreadId -> [BacktrackStep ThreadId ThreadAction Lookahead CRState])
-> (forall s. MemType -> Scheduler ThreadId ThreadAction Lookahead s -> s -> m (Either Failure a, s, Trace ThreadId ThreadAction Lookahead))
-> m [(Either Failure a, Trace ThreadId ThreadAction Lookahead)]
sctBoundedM memtype bf backtrack run =
dpor didYield
willYield
initialCRState
updateCRState
(dependent memtype)
(dependent' memtype)
initialThread
(>=initialThread)
bf
backtrack
pruneCommits
(run memtype)
pruneCommits :: DPOR ThreadId ThreadAction -> DPOR ThreadId ThreadAction
pruneCommits bpor
| not onlycommits || not alldonesync = go bpor
| otherwise = go bpor { dporTodo = M.empty }
where
go b = b { dporDone = pruneCommits <$> dporDone bpor }
onlycommits = all (<initialThread) . M.keys $ dporTodo bpor
alldonesync = all barrier . M.elems $ dporDone bpor
barrier = isBarrier . simplify . fromJust . dporAction
dependent :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, ThreadAction) -> Bool
dependent _ _ (_, Lift) (_, Lift) = True
dependent _ _ (_, ThrowTo t) (t2, Stop) | t == t2 = False
dependent _ _ (t2, Stop) (_, ThrowTo t) | t == t2 = False
dependent _ _ (_, ThrowTo t) (t2, _) = t == t2
dependent _ _ (t2, _) (_, ThrowTo t) = t == t2
dependent _ _ (_, STM _ _) (_, STM _ _) = True
dependent _ _ (_, GetNumCapabilities a) (_, SetNumCapabilities b) = a /= b
dependent _ _ (_, SetNumCapabilities a) (_, GetNumCapabilities b) = a /= b
dependent _ _ (_, SetNumCapabilities a) (_, SetNumCapabilities b) = a /= b
dependent memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify d2)
dependent' :: MemType -> CRState -> (ThreadId, ThreadAction) -> (ThreadId, Lookahead) -> Bool
dependent' _ _ (_, Lift) (_, WillLift) = True
dependent' _ _ (_, ThrowTo t) (t2, WillStop) | t == t2 = False
dependent' _ _ (t2, Stop) (_, WillThrowTo t) | t == t2 = False
dependent' _ _ (_, ThrowTo t) (t2, _) = t == t2
dependent' _ _ (t2, _) (_, WillThrowTo t) = t == t2
dependent' _ _ (_, STM _ _) (_, WillSTM) = True
dependent' _ _ (_, GetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b
dependent' _ _ (_, SetNumCapabilities _) (_, WillGetNumCapabilities) = True
dependent' _ _ (_, SetNumCapabilities a) (_, WillSetNumCapabilities b) = a /= b
dependent' _ _ (_, a1) (_, a2) | isBlock a1 && isBarrier (simplify' a2) = False
dependent' memtype buf (_, d1) (_, d2) = dependentActions memtype buf (simplify d1) (simplify' d2)
dependentActions :: MemType -> CRState -> ActionType -> ActionType -> Bool
dependentActions memtype buf a1 a2 = case (a1, a2) of
(UnsynchronisedRead r1, UnsynchronisedWrite r2) -> r1 == r2
(UnsynchronisedWrite r1, UnsynchronisedRead r2) -> r1 == r2
(UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2
(UnsynchronisedWrite r1, _) | same crefOf && isCommit a2 r1 && isBuffered buf r1 -> False
(_, UnsynchronisedWrite r2) | same crefOf && isCommit a1 r2 && isBuffered buf r2 -> False
(UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency
(_, UnsynchronisedRead r2) | isBarrier a1 -> isBuffered buf r2 && memtype /= SequentialConsistency
(_, _)
| same crefOf && (synchronises a1 (fromJust $ crefOf a1) || synchronises a2 (fromJust $ crefOf a2)) -> True
| same cvarOf -> True
_ -> False
where
same f = isJust (f a1) && f a1 == f a2
type CRState = Map CRefId Bool
initialCRState :: CRState
initialCRState = M.empty
updateCRState :: CRState -> ThreadAction -> CRState
updateCRState crstate (CommitRef _ r) = M.delete r crstate
updateCRState crstate (WriteRef r) = M.insert r True crstate
updateCRState crstate ta
| isBarrier $ simplify ta = initialCRState
| otherwise = crstate
isBuffered :: CRState -> CRefId -> Bool
isBuffered crstate r = M.findWithDefault False r crstate
isCommitRef :: ThreadAction -> Bool
isCommitRef (CommitRef _ _) = True
isCommitRef _ = False
didYield :: ThreadAction -> Bool
didYield Yield = True
didYield _ = False
willYield :: Lookahead -> Bool
willYield WillYield = True
willYield _ = False