-- |
-- 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 = Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
forall (n :: * -> *) a pty.
MonadDejaFu n =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings (Settings n a
 -> Program pty n a -> n [(Either Condition a, Trace)])
-> (MemType -> Settings n a)
-> MemType
-> Program pty n a
-> n [(Either Condition a, Trace)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings n a
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 = Settings n a -> Program pty n a -> n (Set (Either Condition a))
forall (n :: * -> *) a pty.
(MonadDejaFu n, Ord a) =>
Settings n a -> Program pty n a -> n (Set (Either Condition a))
resultsSetWithSettings (Settings n a -> Program pty n a -> n (Set (Either Condition a)))
-> (MemType -> Settings n a)
-> MemType
-> Program pty n a
-> n (Set (Either Condition a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings n a
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 = Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
forall (n :: * -> *) a pty.
(MonadDejaFu n, NFData a) =>
Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
runSCTWithSettings' (Settings n a
 -> Program pty n a -> n [(Either Condition a, Trace)])
-> (MemType -> Settings n a)
-> MemType
-> Program pty n a
-> n [(Either Condition a, Trace)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings n a
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 = Settings n a -> Program pty n a -> n (Set (Either Condition a))
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 -> Program pty n a -> n (Set (Either Condition a)))
-> (MemType -> Settings n a)
-> MemType
-> Program pty n a
-> n (Set (Either Condition a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Way -> MemType -> Settings n a
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 Settings n a -> Way
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
            (Bool
-> IncrementalBoundFunc
     ((Int, Maybe ThreadId), Map ThreadId Int, Int)
-> Scheduler
     (DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int))
forall k.
HasCallStack =>
Bool -> IncrementalBoundFunc k -> Scheduler (DPORSchedState k)
dporSched (Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
settings) (Maybe LengthBound
-> Bounds
-> IncrementalBoundFunc
     ((Int, Maybe ThreadId), Map ThreadId Int, Int)
cBound (Settings n a -> Maybe LengthBound
forall (n :: * -> *) a. Settings n a -> Maybe LengthBound
_lengthBound Settings n a
settings) Bounds
cb0))
            (Map ThreadId ThreadAction
-> [ThreadId] -> ConcurrencyState -> DPORSchedState k
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 (Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
settings) (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) (Bounds -> BacktrackFunc
cBacktrack Bounds
cb0) (DPORSchedState k -> Bool
forall k. DPORSchedState k -> Bool
schedBoundKill DPORSchedState k
s) ConcurrencyState
cstate0 (DPORSchedState k -> Seq ([(ThreadId, Lookahead)], [ThreadId])
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
Bool
-> MemType -> Bool -> Trace -> ConcurrencyState -> DPOR -> DPOR
incorporateTrace (Settings n a -> Bool
forall (n :: * -> *) a. Settings n a -> Bool
_safeIO Settings n a
settings) (Settings n a -> MemType
forall (n :: * -> *) a. Settings n a -> MemType
_memtype Settings n a
settings) Bool
conservative Trace
trace ConcurrencyState
cstate0 DPOR
dp

          (DPOR, Maybe (a, Trace)) -> m (DPOR, Maybe (a, Trace))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((DPOR, Maybe (a, Trace)) -> m (DPOR, Maybe (a, Trace)))
-> (DPOR, Maybe (a, Trace)) -> m (DPOR, Maybe (a, Trace))
forall a b. (a -> b) -> a -> b
$ if DPORSchedState k -> Bool
forall k. DPORSchedState k -> Bool
schedIgnore DPORSchedState k
s
                 then (DPOR -> DPOR
forall a. NFData a => a -> a
force DPOR
newDPOR, Maybe (a, Trace)
forall a. Maybe a
Nothing)
                 else (DPOR -> DPOR
forall a. NFData a => a -> a
force (HasCallStack => [BacktrackStep] -> DPOR -> DPOR
[BacktrackStep] -> DPOR -> DPOR
incorporateBacktrackSteps [BacktrackStep]
bpoints DPOR
newDPOR), (a, Trace) -> Maybe (a, Trace)
forall a. a -> Maybe a
Just (a
res, Trace
trace))
    in Settings n a
-> ([ThreadId] -> DPOR)
-> (DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction))
-> (ConcurrencyState
    -> (Scheduler
          (DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int))
        -> DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int)
        -> n (Either Condition a,
              DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int),
              Trace))
    -> DPOR
    -> ([ThreadId], Bool, Map ThreadId ThreadAction)
    -> n (DPOR, Maybe (Either Condition a, Trace)))
-> Program pty n a
-> n [(Either Condition a, Trace)]
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 ConcurrencyState
-> (Scheduler
      (DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int))
    -> DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int)
    -> n (Either Condition a,
          DPORSchedState ((Int, Maybe ThreadId), Map ThreadId Int, Int),
          Trace))
-> DPOR
-> ([ThreadId], Bool, Map ThreadId ThreadAction)
-> n (DPOR, Maybe (Either Condition a, Trace))
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, Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 Int
lim0)

        check :: (a, a) -> Maybe (a, a)
check (a
_, a
0) = Maybe (a, a)
forall a. Maybe a
Nothing
        check (a, a)
s = (a, a) -> Maybe (a, a)
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
            ((g -> (Int, g)) -> Scheduler (RandSchedState g)
forall g.
RandomGen g =>
(g -> (Int, g)) -> Scheduler (RandSchedState g)
randSched g -> (Int, g)
gen)
            (Maybe LengthBound -> g -> RandSchedState g
forall g. Maybe LengthBound -> g -> RandSchedState g
initialRandSchedState (Settings n a -> Maybe LengthBound
forall (n :: * -> *) a. Settings n a -> Maybe LengthBound
_lengthBound Settings n a
settings) g
g)
          ((a, b), Maybe (a, b)) -> m ((a, b), Maybe (a, b))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((RandSchedState a -> a
forall g. RandSchedState g -> g
schedGen RandSchedState a
s, b
nb -> b -> b
forall a. Num a => a -> a -> a
-b
1), (a, b) -> Maybe (a, b)
forall a. a -> Maybe a
Just (a
res, b
trace))
    in Settings n a
-> ([ThreadId] -> (g, Int))
-> ((g, Int) -> Maybe (g, Int))
-> (ConcurrencyState
    -> (Scheduler (RandSchedState g)
        -> RandSchedState g
        -> n (Either Condition a, RandSchedState g, Trace))
    -> (g, Int)
    -> (g, Int)
    -> n ((g, Int), Maybe (Either Condition a, Trace)))
-> Program pty n a
-> n [(Either Condition a, Trace)]
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] -> (g, Int)
forall {p}. p -> (g, Int)
initial (g, Int) -> Maybe (g, Int)
forall {a} {a}. (Eq a, Num a) => (a, a) -> Maybe (a, a)
check ConcurrencyState
-> (Scheduler (RandSchedState g)
    -> RandSchedState g
    -> n (Either Condition a, RandSchedState g, Trace))
-> (g, Int)
-> (g, Int)
-> n ((g, Int), Maybe (Either Condition a, Trace))
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 = Just $ \Either Condition a
efa -> (Either Condition a -> Maybe Discard)
-> Maybe (Either Condition a -> Maybe Discard)
-> Either Condition a
-> Maybe Discard
forall a. a -> Maybe a -> a
fromMaybe (Maybe Discard -> Either Condition a -> Maybe Discard
forall a b. a -> b -> a
const Maybe Discard
forall a. Maybe a
Nothing) (Settings n a -> Maybe (Either Condition a -> Maybe Discard)
forall (n :: * -> *) a.
Settings n a -> Maybe (Either Condition a -> Maybe Discard)
_discard Settings n a
settings) Either Condition a
efa Maybe Discard -> Maybe Discard -> Maybe Discard
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Discard -> Maybe Discard
forall a. a -> Maybe a
Just Discard
DiscardTrace }
  in [Either Condition a] -> Set (Either Condition a)
forall a. Ord a => [a] -> Set a
S.fromList ([Either Condition a] -> Set (Either Condition a))
-> ([(Either Condition a, Trace)] -> [Either Condition a])
-> [(Either Condition a, Trace)]
-> Set (Either Condition a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Either Condition a, Trace) -> Either Condition a)
-> [(Either Condition a, Trace)] -> [Either Condition a]
forall a b. (a -> b) -> [a] -> [b]
map (Either Condition a, Trace) -> Either Condition a
forall a b. (a, b) -> a
fst ([(Either Condition a, Trace)] -> Set (Either Condition a))
-> n [(Either Condition a, Trace)] -> n (Set (Either Condition a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
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 <- Settings n a -> Program pty n a -> n [(Either Condition a, Trace)]
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
  [(Either Condition a, Trace)] -> ()
forall a. NFData a => a -> ()
rnf [(Either Condition a, Trace)]
res ()
-> n [(Either Condition a, Trace)]
-> n [(Either Condition a, Trace)]
forall a b. a -> b -> b
`seq` [(Either Condition a, Trace)] -> n [(Either Condition a, Trace)]
forall a. a -> n a
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 <- Settings n a -> Program pty n a -> n (Set (Either Condition a))
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
  Set (Either Condition a) -> ()
forall a. NFData a => a -> ()
rnf Set (Either Condition a)
res () -> n (Set (Either Condition a)) -> n (Set (Either Condition a))
forall a b. a -> b -> b
`seq` Set (Either Condition a) -> n (Set (Either Condition a))
forall a. a -> n a
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' = (Maybe (Int, Maybe ThreadId)
 -> Maybe (ThreadId, ThreadAction)
 -> (Decision, Lookahead)
 -> Maybe (Int, Maybe ThreadId))
-> (PreemptionBound
    -> Maybe (Int, Maybe ThreadId)
    -> Maybe (ThreadId, ThreadAction)
    -> (Decision, Lookahead)
    -> Maybe (Int, Maybe ThreadId))
-> Maybe PreemptionBound
-> Maybe (Int, Maybe ThreadId)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Maybe (Int, Maybe ThreadId)
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 ((Int, Maybe ThreadId) -> Maybe (Int, Maybe ThreadId)
forall a. a -> Maybe a
Just (Int, Maybe ThreadId)
k1) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lh
      k2' :: Maybe (Map ThreadId Int)
k2' = (Maybe (Map ThreadId Int)
 -> Maybe (ThreadId, ThreadAction)
 -> (Decision, Lookahead)
 -> Maybe (Map ThreadId Int))
-> (FairBound
    -> Maybe (Map ThreadId Int)
    -> Maybe (ThreadId, ThreadAction)
    -> (Decision, Lookahead)
    -> Maybe (Map ThreadId Int))
-> Maybe FairBound
-> Maybe (Map ThreadId Int)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Maybe (Map ThreadId Int)
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 (Map ThreadId Int -> Maybe (Map ThreadId Int)
forall a. a -> Maybe a
Just Map ThreadId Int
k2) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lh
      k3' :: Maybe Int
k3' = (Maybe Int
 -> Maybe (ThreadId, ThreadAction)
 -> (Decision, Lookahead)
 -> Maybe Int)
-> (LengthBound
    -> Maybe Int
    -> Maybe (ThreadId, ThreadAction)
    -> (Decision, Lookahead)
    -> Maybe Int)
-> Maybe LengthBound
-> Maybe Int
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Maybe Int
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 (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
k3) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lh
  in (,,) ((Int, Maybe ThreadId)
 -> Map ThreadId Int
 -> Int
 -> ((Int, Maybe ThreadId), Map ThreadId Int, Int))
-> Maybe (Int, Maybe ThreadId)
-> Maybe
     (Map ThreadId Int
      -> Int -> ((Int, Maybe ThreadId), Map ThreadId Int, Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Int, Maybe ThreadId)
k1' Maybe
  (Map ThreadId Int
   -> Int -> ((Int, Maybe ThreadId), Map ThreadId Int, Int))
-> Maybe (Map ThreadId Int)
-> Maybe (Int -> ((Int, Maybe ThreadId), Map ThreadId Int, Int))
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (Map ThreadId Int)
k2' Maybe (Int -> ((Int, Maybe ThreadId), Map ThreadId Int, Int))
-> Maybe Int
-> Maybe ((Int, Maybe ThreadId), Map ThreadId Int, Int)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
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)
_ = ((Int, Maybe ThreadId), Map ThreadId Int, Int)
-> Maybe ((Int, Maybe ThreadId), Map ThreadId Int, Int)
forall a. a -> Maybe a
Just ((Int
0, Maybe ThreadId
forall a. Maybe a
Nothing), Map ThreadId Int
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
(ThreadId -> BacktrackStep -> Bool) -> BacktrackFunc
backtrackAt (\ThreadId
_ BacktrackStep
_ -> Bool
False) [BacktrackStep]
bs ([(Int, Bool, ThreadId)] -> [BacktrackStep])
-> ([(Int, Bool, ThreadId)] -> [(Int, Bool, ThreadId)])
-> [(Int, Bool, ThreadId)]
-> [BacktrackStep]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Bool, ThreadId) -> [(Int, Bool, ThreadId)])
-> [(Int, Bool, ThreadId)] -> [(Int, Bool, ThreadId)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int, Bool, ThreadId) -> [(Int, Bool, ThreadId)]
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 (Int, Bool, c) -> [(Int, Bool, c)] -> [(Int, Bool, c)]
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 = [BacktrackStep] -> Int -> Maybe Int
forall {t}. (Eq t, Num t) => [BacktrackStep] -> t -> Maybe t
go ([BacktrackStep] -> [BacktrackStep]
forall a. [a] -> [a]
reverse (Int -> [BacktrackStep] -> [BacktrackStep]
forall a. Int -> [a] -> [a]
take (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [BacktrackStep]
bs)) (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) where
      go :: [BacktrackStep] -> t -> Maybe t
go [BacktrackStep]
_ (-1) = Maybe t
forall a. Maybe a
Nothing
      go (BacktrackStep
b1:rest :: [BacktrackStep]
rest@(BacktrackStep
b2:[BacktrackStep]
_)) t
j
        | BacktrackStep -> ThreadId
bcktThreadid BacktrackStep
b1 ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= BacktrackStep -> ThreadId
bcktThreadid BacktrackStep
b2
          Bool -> Bool -> Bool
&& Bool -> Bool
not (ThreadAction -> Bool
isCommitRef (ThreadAction -> Bool) -> ThreadAction -> Bool
forall a b. (a -> b) -> a -> b
$ BacktrackStep -> ThreadAction
bcktAction BacktrackStep
b1)
          Bool -> Bool -> Bool
&& Bool -> Bool
not (ThreadAction -> Bool
isCommitRef (ThreadAction -> Bool) -> ThreadAction -> Bool
forall a b. (a -> b) -> a -> b
$ BacktrackStep -> ThreadAction
bcktAction BacktrackStep
b2) = t -> Maybe t
forall a. a -> Maybe a
Just t
j
        | Bool
otherwise = [BacktrackStep] -> t -> Maybe t
go [BacktrackStep]
rest (t
jt -> t -> t
forall a. Num a => a -> a -> a
-t
1)
      go [BacktrackStep]
_ t
_ = Maybe t
forall a. Maybe a
Nothing
cBacktrack Bounds
_ [BacktrackStep]
bs = HasCallStack =>
(ThreadId -> BacktrackStep -> Bool) -> BacktrackFunc
(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
_) = (Int, Maybe ThreadId)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> (Int, Maybe ThreadId)
forall a.
(Int, Maybe ThreadId)
-> Maybe (ThreadId, ThreadAction)
-> (Decision, a)
-> (Int, Maybe ThreadId)
preEmpCountInc ((Int, Maybe ThreadId)
-> Maybe (Int, Maybe ThreadId) -> (Int, Maybe ThreadId)
forall a. a -> Maybe a -> a
fromMaybe (Int
0, Maybe ThreadId
forall a. Maybe a
Nothing) Maybe (Int, Maybe ThreadId)
k) Maybe (ThreadId, ThreadAction)
prior (Decision, Lookahead)
lhead
  in if Int
pcount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
pb then (Int, Maybe ThreadId) -> Maybe (Int, Maybe ThreadId)
forall a. a -> Maybe a
Just (Int, Maybe ThreadId)
k' else Maybe (Int, Maybe ThreadId)
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' = Map ThreadId Int
-> Maybe (ThreadId, ThreadAction)
-> (Decision, Lookahead)
-> Map ThreadId Int
forall a.
Map ThreadId Int
-> Maybe (ThreadId, a) -> (Decision, Lookahead) -> Map ThreadId Int
yieldCountInc (Map ThreadId Int -> Maybe (Map ThreadId Int) -> Map ThreadId Int
forall a. a -> Maybe a -> a
fromMaybe Map ThreadId Int
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 ((Decision, Lookahead) -> Lookahead
forall a b. (a, b) -> b
snd (Decision, Lookahead)
lhead)) Bool -> Bool -> Bool
|| [Int] -> Int
maxDiff (Map ThreadId Int -> [Int]
forall k a. Map k a -> [a]
M.elems Map ThreadId Int
k') Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
fb
     then Map ThreadId Int -> Maybe (Map ThreadId Int)
forall a. a -> Maybe a
Just Map ThreadId Int
k'
     else Maybe (Map ThreadId Int)
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' = Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Maybe Int
len
  in if Int
len' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
lb then Int -> Maybe Int
forall a. a -> Maybe a
Just Int
len' else Maybe Int
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 ThreadId -> Maybe ThreadId
forall a. a -> Maybe a
Just ThreadId
tid)
      | ThreadId -> Bool
isCommitThread ThreadId
tid   = (if Maybe ThreadId
lastnoncommit Maybe ThreadId -> Maybe ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId -> Maybe ThreadId
forall a. a -> Maybe a
Just ThreadId
tnext then Int
sofar else Int
sofar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Maybe ThreadId
forall a. Maybe a
Nothing)
      | Bool
otherwise = (if Bool
isPreemptive then Int
sofar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 else Int
sofar, Maybe ThreadId
forall a. Maybe a
Nothing)

    isCommitThread :: ThreadId -> Bool
isCommitThread = (ThreadId -> ThreadId -> Bool
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 = (Maybe Int -> Maybe Int)
-> ThreadId -> Map ThreadId Int -> Map ThreadId Int
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
M.alter (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Maybe Int -> Int) -> Maybe Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> (Int -> Int) -> Maybe Int -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
1 (Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)) ThreadId
tnext Map ThreadId Int
sofar
      | Bool
otherwise       = (Maybe Int -> Maybe Int)
-> ThreadId -> Map ThreadId Int -> Map ThreadId Int
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
M.alter (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> (Maybe Int -> Int) -> Maybe Int -> Maybe Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe Int -> Int
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 = Int -> [Int] -> Int
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 t -> t -> t
forall a. Ord a => a -> a -> a
`max` (t -> t -> t) -> t -> [t] -> t
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (t -> t -> t -> t
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 a -> a -> a
forall a. Ord a => a -> a -> a
`max` a -> a
forall a. Num a => a -> a
abs (a
x0 a -> a -> a
forall a. Num a => a -> a -> a
- a
x)