-- |
-- Module      : Test.DejaFu.SCT
-- Copyright   : (c) 2015--2019 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : portable
--
-- Systematic testing for concurrent computations.
module Test.DejaFu.SCT
  ( -- * Running Concurrent Programs
    runSCT
  , runSCT'
  , resultsSet
  , resultsSet'

  -- ** Configuration
  , 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

-------------------------------------------------------------------------------
-- Running Concurrent Programs

-- | Explore possible executions of a concurrent program according to
-- the given 'Way'.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases.
--
-- @since 2.1.0.0
runSCT :: MonadDejaFu n
  => Way
  -- ^ How to run the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> Program pty n a
  -- ^ The computation to run many times.
  -> n [(Either Condition a, Trace)]
runSCT :: forall (n :: * -> *) pty a.
MonadDejaFu n =>
Way
-> MemType -> Program pty n a -> n [(Either Condition a, Trace)]
runSCT Way
way = forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | Return the set of results of a concurrent program.
--
-- @since 2.1.0.0
resultsSet :: (MonadDejaFu n, Ord a)
  => Way
  -- ^ How to run the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> Program pty n a
  -- ^ The computation to run many times.
  -> n (Set (Either Condition a))
resultsSet :: forall (n :: * -> *) a pty.
(MonadDejaFu n, Ord a) =>
Way -> MemType -> Program pty n a -> n (Set (Either Condition a))
resultsSet Way
way = forall (n :: * -> *) a pty.
(MonadDejaFu n, Ord a) =>
Settings n a -> Program pty n a -> n (Set (Either Condition a))
resultsSetWithSettings forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | A strict variant of 'runSCT'.
--
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases.
--
-- @since 2.1.0.0
runSCT' :: (MonadDejaFu n, NFData a)
  => Way
  -- ^ How to run the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> Program pty n a
  -- ^ The computation to run many times.
  -> n [(Either Condition a, Trace)]
runSCT' :: forall (n :: * -> *) a pty.
(MonadDejaFu n, NFData a) =>
Way
-> MemType -> Program pty n a -> n [(Either Condition a, Trace)]
runSCT' Way
way = forall (n :: * -> *) a pty.
(MonadDejaFu n, NFData a) =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-- | A strict variant of 'resultsSet'.
--
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- @since 2.1.0.0
resultsSet' :: (MonadDejaFu n, Ord a, NFData a)
  => Way
  -- ^ How to run the concurrent program.
  -> MemType
  -- ^ The memory model to use for non-synchronised @IORef@ operations.
  -> Program pty n a
  -- ^ The computation to run many times.
  -> n (Set (Either Condition a))
resultsSet' :: forall (n :: * -> *) a pty.
(MonadDejaFu n, Ord a, NFData a) =>
Way -> MemType -> Program pty n a -> n (Set (Either Condition a))
resultsSet' Way
way = forall (n :: * -> *) a pty.
(MonadDejaFu n, Ord a, NFData a) =>
Settings n a -> Program pty n a -> n (Set (Either Condition a))
resultsSetWithSettings' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: * -> *) a.
Applicative n =>
Way -> MemType -> Settings n a
fromWayAndMemType Way
way

-------------------------------------------------------------------------------
-- Configuration

-- | A variant of 'runSCT' which takes a 'Settings' record.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases.
--
-- @since 2.1.0.0
runSCTWithSettings :: MonadDejaFu n
  => Settings n a
  -- ^ The SCT settings.
  -> Program pty n a
  -- ^ The computation to run many times.
  -> n [(Either Condition a, Trace)]
runSCTWithSettings :: forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings Settings n a
settings Program pty n a
conc = case forall (n :: * -> *) a. Settings n a -> Way
_way Settings n a
settings of
  Systematic Bounds
cb0 ->
    let initial :: [ThreadId] -> DPOR
initial = [ThreadId] -> DPOR
initialState

        check :: DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
check = DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
findSchedulePrefix

        step :: ConcurrencyState
-> (Scheduler
      (DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int))
    -> DPORSchedState k -> m (a, DPORSchedState k, Trace))
-> DPOR
-> ([ThreadId], Bool, Map ThreadId ThreadAction)
-> m (DPOR, Maybe (a, Trace))
step ConcurrencyState
cstate0 Scheduler
  (DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int))
-> DPORSchedState k -> m (a, DPORSchedState k, Trace)
run DPOR
dp ([ThreadId]
prefix, Bool
conservative, Map ThreadId ThreadAction
sleep) = do
          (a
res, DPORSchedState k
s, Trace
trace) <- Scheduler
  (DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int))
-> DPORSchedState k -> m (a, DPORSchedState k, Trace)
run
            (forall k.
HasCallStack =>
Bool -> IncrementalBoundFunc k -> Scheduler (DPORSchedState k)
dporSched (forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
settings) (Maybe LengthBound
-> Bounds
-> IncrementalBoundFunc
     ((Int, Maybe ThreadId), Map ThreadId Int, Int)
cBound (forall (n :: * -> *) a. Settings n a -> Maybe LengthBound
_lengthBound Settings n a
settings) Bounds
cb0))
            (forall k.
Map ThreadId ThreadAction
-> [ThreadId] -> ConcurrencyState -> DPORSchedState k
initialDPORSchedState Map ThreadId ThreadAction
sleep [ThreadId]
prefix ConcurrencyState
cstate0)

          let bpoints :: [BacktrackStep]
bpoints = Bool
-> MemType
-> BacktrackFunc
-> Bool
-> ConcurrencyState
-> Seq ([(ThreadId, Lookahead)], [ThreadId])
-> Trace
-> [BacktrackStep]
findBacktrackSteps (forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
settings) (forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) (Bounds -> BacktrackFunc
cBacktrack Bounds
cb0) (forall k. DPORSchedState k -> Bool
schedBoundKill DPORSchedState k
s) ConcurrencyState
cstate0 (forall k.
DPORSchedState k -> Seq ([(ThreadId, Lookahead)], [ThreadId])
schedBPoints DPORSchedState k
s) Trace
trace
          let newDPOR :: DPOR
newDPOR = HasCallStack =>
Bool
-> MemType -> Bool -> Trace -> ConcurrencyState -> DPOR -> DPOR
incorporateTrace (forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
settings) (forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) Bool
conservative Trace
trace ConcurrencyState
cstate0 DPOR
dp

          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ if forall k. DPORSchedState k -> Bool
schedIgnore DPORSchedState k
s
                 then (forall a. NFData a => a -> a
force DPOR
newDPOR, forall a. Maybe a
Nothing)
                 else (forall a. NFData a => a -> a
force (HasCallStack => [BacktrackStep] -> DPOR -> DPOR
incorporateBacktrackSteps [BacktrackStep]
bpoints DPOR
newDPOR), forall a. a -> Maybe a
Just (a
res, Trace
trace))
    in forall (n :: * -> *) a s t g pty.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ([ThreadId] -> s)
-> (s -> Maybe t)
-> (ConcurrencyState
    -> (Scheduler g -> g -> n (Either Condition a, g, Trace))
    -> s
    -> t
    -> n (s, Maybe (Either Condition a, Trace)))
-> Program pty n a
-> n [(Either Condition a, Trace)]
sct Settings n a
settings [ThreadId] -> DPOR
initial DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
check forall {m :: * -> *} {k} {a} {k}.
Monad m =>
ConcurrencyState
-> (Scheduler
      (DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int))
    -> DPORSchedState k -> m (a, DPORSchedState k, Trace))
-> DPOR
-> ([ThreadId], Bool, Map ThreadId ThreadAction)
-> m (DPOR, Maybe (a, Trace))
step Program pty n a
conc

  Randomly g -> (Int, g)
gen g
g0 Int
lim0 ->
    let initial :: p -> (g, Int)
initial p
_ = (g
g0, forall a. Ord a => a -> a -> a
max Int
0 Int
lim0)

        check :: (a, a) -> Maybe (a, a)
check (a
_, a
0) = forall a. Maybe a
Nothing
        check (a, a)
s = forall a. a -> Maybe a
Just (a, a)
s

        step :: p
-> (Scheduler (RandSchedState g)
    -> RandSchedState g -> m (a, RandSchedState a, b))
-> p
-> (g, b)
-> m ((a, b), Maybe (a, b))
step p
_ Scheduler (RandSchedState g)
-> RandSchedState g -> m (a, RandSchedState a, b)
run p
_ (g
g, b
n) = do
          (a
res, RandSchedState a
s, b
trace) <- Scheduler (RandSchedState g)
-> RandSchedState g -> m (a, RandSchedState a, b)
run
            (forall g.
RandomGen g =>
(g -> (Int, g)) -> Scheduler (RandSchedState g)
randSched g -> (Int, g)
gen)
            (forall g. Maybe LengthBound -> g -> RandSchedState g
initialRandSchedState (forall (n :: * -> *) a. Settings n a -> Maybe LengthBound
_lengthBound Settings n a
settings) g
g)
          forall (f :: * -> *) a. Applicative f => a -> f a
pure ((forall g. RandSchedState g -> g
schedGen RandSchedState a
s, b
nforall a. Num a => a -> a -> a
-b
1), forall a. a -> Maybe a
Just (a
res, b
trace))
    in forall (n :: * -> *) a s t g pty.
(MonadDejaFu n, HasCallStack) =>
Settings n a
-> ([ThreadId] -> s)
-> (s -> Maybe t)
-> (ConcurrencyState
    -> (Scheduler g -> g -> n (Either Condition a, g, Trace))
    -> s
    -> t
    -> n (s, Maybe (Either Condition a, Trace)))
-> Program pty n a
-> n [(Either Condition a, Trace)]
sct Settings n a
settings forall {p}. p -> (g, Int)
initial forall {a} {a}. (Eq a, Num a) => (a, a) -> Maybe (a, a)
check forall {m :: * -> *} {b} {p} {g} {a} {a} {b} {p}.
(Monad m, Num b) =>
p
-> (Scheduler (RandSchedState g)
    -> RandSchedState g -> m (a, RandSchedState a, b))
-> p
-> (g, b)
-> m ((a, b), Maybe (a, b))
step Program pty n a
conc

-- | A variant of 'resultsSet' which takes a 'Settings' record.
--
-- @since 2.1.0.0
resultsSetWithSettings :: (MonadDejaFu n, Ord a)
  => Settings n a
  -- ^ The SCT settings.
  -> Program pty n a
  -- ^ The computation to run many times.
  -> n (Set (Either Condition a))
resultsSetWithSettings :: forall (n :: * -> *) a pty.
(MonadDejaFu n, Ord a) =>
Settings n a -> Program pty n a -> n (Set (Either Condition a))
resultsSetWithSettings Settings n a
settings Program pty n a
conc =
  let settings' :: Settings n a
settings' = Settings n a
settings { _discard :: Maybe (Either Condition a -> Maybe Discard)
_discard = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ \Either Condition a
efa -> forall a. a -> Maybe a -> a
fromMaybe (forall a b. a -> b -> a
const forall a. Maybe a
Nothing) (forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Maybe Discard)
_discard Settings n a
settings) Either Condition a
efa forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. a -> Maybe a
Just Discard
DiscardTrace }
  in forall a. Ord a => [a] -> Set a
S.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings Settings n a
settings' Program pty n a
conc

-- | A strict variant of 'runSCTWithSettings'.
--
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- The exact executions tried, and the order in which results are
-- found, is unspecified and may change between releases.
--
-- @since 2.1.0.0
runSCTWithSettings' :: (MonadDejaFu n, NFData a)
  => Settings n a
  -- ^ The SCT settings.
  -> Program pty n a
  -- ^ The computation to run many times.
  -> n [(Either Condition a, Trace)]
runSCTWithSettings' :: forall (n :: * -> *) a pty.
(MonadDejaFu n, NFData a) =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings' Settings n a
settings Program pty n a
conc = do
  [(Either Condition a, Trace)]
res <- forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings Settings n a
settings Program pty n a
conc
  forall a. NFData a => a -> ()
rnf [(Either Condition a, Trace)]
res seq :: forall a b. a -> b -> b
`seq` forall (f :: * -> *) a. Applicative f => a -> f a
pure [(Either Condition a, Trace)]
res

-- | A strict variant of 'resultsSetWithSettings'.
--
-- Demanding the result of this will force it to normal form, which
-- may be more efficient in some situations.
--
-- @since 2.1.0.0
resultsSetWithSettings' :: (MonadDejaFu n, Ord a, NFData a)
  => Settings n a
  -- ^ The SCT settings.
  -> Program pty n a
  -- ^ The computation to run many times.
  -> n (Set (Either Condition a))
resultsSetWithSettings' :: forall (n :: * -> *) a pty.
(MonadDejaFu n, Ord a, NFData a) =>
Settings n a -> Program pty n a -> n (Set (Either Condition a))
resultsSetWithSettings' Settings n a
settings Program pty n a
conc = do
  Set (Either Condition a)
res <- forall (n :: * -> *) a pty.
(MonadDejaFu n, Ord a) =>
Settings n a -> Program pty n a -> n (Set (Either Condition a))
resultsSetWithSettings Settings n a
settings Program pty n a
conc
  forall a. NFData a => a -> ()
rnf Set (Either Condition a)
res seq :: forall a b. a -> b -> b
`seq` forall (f :: * -> *) a. Applicative f => a -> f a
pure Set (Either Condition a)
res

-------------------------------------------------------------------------------
-- Combined Bounds

-- | Combination bound function
cBound :: Maybe LengthBound -> Bounds -> IncrementalBoundFunc ((Int, Maybe ThreadId), M.Map ThreadId Int, Int)
cBound :: Maybe LengthBound
-> Bounds
-> IncrementalBoundFunc
     ((Int, Maybe ThreadId), Map ThreadId Int, Int)
cBound Maybe LengthBound
lb (Bounds Maybe PreemptionBound
pb Maybe FairBound
fb) (Just ((Int, Maybe ThreadId)
k1, Map ThreadId Int
k2, Int
k3)) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lh =
  let k1' :: Maybe (Int, Maybe ThreadId)
k1' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (\Maybe (Int, Maybe ThreadId)
k Maybe (ThreadId, ThreadAction)
_ (Decision, Lookahead)
_ -> Maybe (Int, Maybe ThreadId)
k) PreemptionBound
-> Maybe (Int, Maybe ThreadId)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Maybe (Int, Maybe ThreadId)
pBound Maybe PreemptionBound
pb (forall a. a -> Maybe a
Just (Int, Maybe ThreadId)
k1) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lh
      k2' :: Maybe (Map ThreadId Int)
k2' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (\Maybe (Map ThreadId Int)
k Maybe (ThreadId, ThreadAction)
_ (Decision, Lookahead)
_ -> Maybe (Map ThreadId Int)
k) FairBound
-> Maybe (Map ThreadId Int)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Maybe (Map ThreadId Int)
fBound Maybe FairBound
fb (forall a. a -> Maybe a
Just Map ThreadId Int
k2) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lh
      k3' :: Maybe Int
k3' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (\Maybe Int
k Maybe (ThreadId, ThreadAction)
_ (Decision, Lookahead)
_ -> Maybe Int
k) LengthBound
-> Maybe Int
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Maybe Int
lBound Maybe LengthBound
lb (forall a. a -> Maybe a
Just Int
k3) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lh
  in (,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Int, Maybe ThreadId)
k1' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (Map ThreadId Int)
k2' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe Int
k3'
cBound Maybe LengthBound
_ Bounds
_ Maybe ((Int, Maybe ThreadId), Map ThreadId Int, Int)
Nothing Maybe (ThreadId, ThreadAction)
_ (Decision, Lookahead)
_ = forall a. a -> Maybe a
Just ((Int
0, forall a. Maybe a
Nothing), forall k a. Map k a
M.empty, Int
1)

-- | Backtracks to the given point.
--
-- If pre-emption bounding is enabled, also conservatively adds a
-- backtracking point 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.
cBacktrack :: Bounds -> BacktrackFunc
cBacktrack :: Bounds -> BacktrackFunc
cBacktrack (Bounds (Just PreemptionBound
_) Maybe FairBound
_) [BacktrackStep]
bs =
    HasCallStack =>
(ThreadId -> BacktrackStep -> Bool) -> BacktrackFunc
backtrackAt (\ThreadId
_ BacktrackStep
_ -> Bool
False) [BacktrackStep]
bs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {c}. (Int, Bool, c) -> [(Int, Bool, c)]
addConservative
  where
    addConservative :: (Int, Bool, c) -> [(Int, Bool, c)]
addConservative o :: (Int, Bool, c)
o@(Int
i, Bool
_, c
tid) = (Int, Bool, c)
o forall a. a -> [a] -> [a]
: case Int -> Maybe Int
conservative Int
i of
      Just Int
j  -> [(Int
j, Bool
True, c
tid)]
      Maybe Int
Nothing -> []

    -- index of conservative point
    conservative :: Int -> Maybe Int
conservative Int
i = forall {t}. (Eq t, Num t) => [BacktrackStep] -> t -> Maybe t
go (forall a. [a] -> [a]
reverse (forall a. Int -> [a] -> [a]
take (Int
iforall a. Num a => a -> a -> a
-Int
1) [BacktrackStep]
bs)) (Int
iforall a. Num a => a -> a -> a
-Int
1) where
      go :: [BacktrackStep] -> t -> Maybe t
go [BacktrackStep]
_ (-1) = forall a. Maybe a
Nothing
      go (BacktrackStep
b1:rest :: [BacktrackStep]
rest@(BacktrackStep
b2:[BacktrackStep]
_)) t
j
        | BacktrackStep -> ThreadId
bcktThreadid BacktrackStep
b1 forall a. Eq a => a -> a -> Bool
/= BacktrackStep -> ThreadId
bcktThreadid BacktrackStep
b2
          Bool -> Bool -> Bool
&& Bool -> Bool
not (ThreadAction -> Bool
isCommitRef forall a b. (a -> b) -> a -> b
$ BacktrackStep -> ThreadAction
bcktAction BacktrackStep
b1)
          Bool -> Bool -> Bool
&& Bool -> Bool
not (ThreadAction -> Bool
isCommitRef forall a b. (a -> b) -> a -> b
$ BacktrackStep -> ThreadAction
bcktAction BacktrackStep
b2) = forall a. a -> Maybe a
Just t
j
        | Bool
otherwise = [BacktrackStep] -> t -> Maybe t
go [BacktrackStep]
rest (t
jforall a. Num a => a -> a -> a
-t
1)
      go [BacktrackStep]
_ t
_ = forall a. Maybe a
Nothing
cBacktrack Bounds
_ [BacktrackStep]
bs = HasCallStack =>
(ThreadId -> BacktrackStep -> Bool) -> BacktrackFunc
backtrackAt (\ThreadId
_ BacktrackStep
_ -> Bool
False) [BacktrackStep]
bs

-------------------------------------------------------------------------------
-- Pre-emption bounding

-- | Pre-emption bound function. This does not count pre-emptive
-- context switches to a commit thread.
pBound :: PreemptionBound -> IncrementalBoundFunc (Int, Maybe ThreadId)
pBound :: PreemptionBound
-> Maybe (Int, Maybe ThreadId)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Maybe (Int, Maybe ThreadId)
pBound (PreemptionBound Int
pb) Maybe (Int, Maybe ThreadId)
k Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lhead =
  let k' :: (Int, Maybe ThreadId)
k'@(Int
pcount, Maybe ThreadId
_) = forall a.
(Int, Maybe ThreadId)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, a)
-> (Int, Maybe ThreadId)
preEmpCountInc (forall a. a -> Maybe a -> a
fromMaybe (Int
0, forall a. Maybe a
Nothing) Maybe (Int, Maybe ThreadId)
k) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lhead
  in if Int
pcount forall a. Ord a => a -> a -> Bool
<= Int
pb then forall a. a -> Maybe a
Just (Int, Maybe ThreadId)
k' else forall a. Maybe a
Nothing

-------------------------------------------------------------------------------
-- Fair bounding

-- | Fair bound function
fBound :: FairBound -> IncrementalBoundFunc (M.Map ThreadId Int)
fBound :: FairBound
-> Maybe (Map ThreadId Int)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Maybe (Map ThreadId Int)
fBound (FairBound Int
fb) Maybe (Map ThreadId Int)
k Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lhead =
  let k' :: Map ThreadId Int
k' = forall a.
Map ThreadId Int
-> Maybe (ThreadId, a) -> (Decision, Lookahead) -> Map ThreadId Int
yieldCountInc (forall a. a -> Maybe a -> a
fromMaybe forall k a. Map k a
M.empty Maybe (Map ThreadId Int)
k) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lhead
  in if Bool -> Bool
not (Lookahead -> Bool
willYield (forall a b. (a, b) -> b
snd (Decision, Lookahead)
lhead)) Bool -> Bool -> Bool
|| [Int] -> Int
maxDiff (forall k a. Map k a -> [a]
M.elems Map ThreadId Int
k') forall a. Ord a => a -> a -> Bool
<= Int
fb
     then forall a. a -> Maybe a
Just Map ThreadId Int
k'
     else forall a. Maybe a
Nothing

-------------------------------------------------------------------------------
-- Length bounding

-- | Length bound function
lBound :: LengthBound -> IncrementalBoundFunc Int
lBound :: LengthBound
-> Maybe Int
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Maybe Int
lBound (LengthBound Int
lb) Maybe Int
len Maybe (ThreadId, ThreadAction)
_ (Decision, Lookahead)
_ =
  let len' :: Int
len' = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 (forall a. Num a => a -> a -> a
+Int
1) Maybe Int
len
  in if Int
len' forall a. Ord a => a -> a -> Bool
< Int
lb then forall a. a -> Maybe a
Just Int
len' else forall a. Maybe a
Nothing

-------------------------------------------------------------------------------
-- Utilities

-- | An incremental version of 'preEmpCount', going one step at a time.
preEmpCountInc
  :: (Int, Maybe ThreadId)
  -- ^ The number of preemptions so far and, if currently executing a
  -- commit thread, what the prior thread was.
  -> Maybe (ThreadId, ThreadAction)
  -- ^ What just happened.
  -> (Decision, a)
  -- ^ What's coming up.
  -> (Int, Maybe ThreadId)
preEmpCountInc :: forall a.
(Int, Maybe ThreadId)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, a)
-> (Int, Maybe ThreadId)
preEmpCountInc (Int
sofar, Maybe ThreadId
lastnoncommit) Maybe (ThreadId, ThreadAction)
prior (Decision
d, a
_) = case (Maybe (ThreadId, ThreadAction)
prior, Decision
d) of
    (Just (ThreadId
tid, ThreadAction
_),   Start    ThreadId
tnext) -> ThreadId -> ThreadId -> Bool -> (Int, Maybe ThreadId)
cswitch ThreadId
tid ThreadId
tnext Bool
False
    (Just (ThreadId
tid, ThreadAction
act), SwitchTo ThreadId
tnext) -> ThreadId -> ThreadId -> Bool -> (Int, Maybe ThreadId)
cswitch ThreadId
tid ThreadId
tnext (Bool -> Bool
not (ThreadAction -> Bool
didYield ThreadAction
act))
    (Maybe (ThreadId, ThreadAction)
_, Decision
Continue) -> (Int
sofar, Maybe ThreadId
lastnoncommit)
    (Maybe (ThreadId, ThreadAction)
Nothing, Decision
_)  -> (Int
sofar, Maybe ThreadId
lastnoncommit)
  where
    cswitch :: ThreadId -> ThreadId -> Bool -> (Int, Maybe ThreadId)
cswitch ThreadId
tid ThreadId
tnext Bool
isPreemptive
      | ThreadId -> Bool
isCommitThread ThreadId
tnext = (Int
sofar, if ThreadId -> Bool
isCommitThread ThreadId
tid then Maybe ThreadId
lastnoncommit else forall a. a -> Maybe a
Just ThreadId
tid)
      | ThreadId -> Bool
isCommitThread ThreadId
tid   = (if Maybe ThreadId
lastnoncommit forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just ThreadId
tnext then Int
sofar else Int
sofar forall a. Num a => a -> a -> a
+ Int
1, forall a. Maybe a
Nothing)
      | Bool
otherwise = (if Bool
isPreemptive then Int
sofar forall a. Num a => a -> a -> a
+ Int
1 else Int
sofar, forall a. Maybe a
Nothing)

    isCommitThread :: ThreadId -> Bool
isCommitThread = (forall a. Ord a => a -> a -> Bool
< ThreadId
initialThread)

-- | An incremental count of yields, going one step at a time.
yieldCountInc
  :: M.Map ThreadId Int
  -- ^ The number of yields of each thread so far
  -> Maybe (ThreadId, a)
  -- ^ What just happened.
  -> (Decision, Lookahead)
  -- ^ What's coming up.
  -> M.Map ThreadId Int
yieldCountInc :: forall a.
Map ThreadId Int
-> Maybe (ThreadId, a) -> (Decision, Lookahead) -> Map ThreadId Int
yieldCountInc Map ThreadId Int
sofar Maybe (ThreadId, a)
prior (Decision
d, Lookahead
lnext) = case Maybe (ThreadId, a)
prior of
    Just (ThreadId
tid, a
_) -> ThreadId -> Map ThreadId Int
ycount (ThreadId -> Decision -> ThreadId
tidOf ThreadId
tid Decision
d)
    Maybe (ThreadId, a)
Nothing       -> ThreadId -> Map ThreadId Int
ycount ThreadId
initialThread
  where
    ycount :: ThreadId -> Map ThreadId Int
ycount ThreadId
tnext
      | Lookahead -> Bool
willYield Lookahead
lnext = forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
M.alter (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 (forall a. Num a => a -> a -> a
+Int
1)) ThreadId
tnext Map ThreadId Int
sofar
      | Bool
otherwise       = forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
M.alter (forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe Int
0) ThreadId
tnext Map ThreadId Int
sofar

-- | Determine if an action is a commit or not.
isCommitRef :: ThreadAction -> Bool
isCommitRef :: ThreadAction -> Bool
isCommitRef (CommitIORef ThreadId
_ IORefId
_) = Bool
True
isCommitRef ThreadAction
_ = Bool
False

-- | Get the maximum difference between two ints in a list.
maxDiff :: [Int] -> Int
maxDiff :: [Int] -> Int
maxDiff = forall {t}. (Ord t, Num t) => t -> [t] -> t
go Int
0 where
  go :: t -> [t] -> t
go t
m (t
x:[t]
xs) =
    let m' :: t
m' = t
m forall a. Ord a => a -> a -> a
`max` forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall {a}. (Ord a, Num a) => a -> a -> a -> a
go' t
x) t
0 [t]
xs
    in t -> [t] -> t
go t
m' [t]
xs
  go t
m [] = t
m
  go' :: a -> a -> a -> a
go' a
x0 a
m a
x = a
m forall a. Ord a => a -> a -> a
`max` forall a. Num a => a -> a
abs (a
x0 forall a. Num a => a -> a -> a
- a
x)