{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      : Test.DejaFu.SCT.Internal.DPOR
-- Copyright   : (c) 2015--2020 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : DeriveAnyClass, DeriveGeneric, FlexibleContexts, ViewPatterns
--
-- Internal types and functions for SCT via dynamic partial-order
-- reduction.  This module is NOT considered to form part of the
-- public interface of this library.
module Test.DejaFu.SCT.Internal.DPOR where

import           Control.Applicative  ((<|>))
import           Control.DeepSeq      (NFData)
import qualified Data.Foldable        as F
import           Data.Function        (on)
import           Data.List            (nubBy, partition, sortOn)
import           Data.List.NonEmpty   (toList)
import           Data.Map.Strict      (Map)
import qualified Data.Map.Strict      as M
import           Data.Maybe           (isJust, isNothing, listToMaybe,
                                       maybeToList)
import           Data.Sequence        (Seq, (|>))
import qualified Data.Sequence        as Sq
import           Data.Set             (Set)
import qualified Data.Set             as S
import           GHC.Generics         (Generic)
import           GHC.Stack            (HasCallStack)

import           Test.DejaFu.Internal
import           Test.DejaFu.Schedule (Scheduler(..))
import           Test.DejaFu.Types
import           Test.DejaFu.Utils    (decisionOf, tidOf)

-------------------------------------------------------------------------------
-- * Dynamic partial-order reduction

-- | DPOR execution is represented as a tree of states, characterised
-- by the decisions that lead to that state.
data DPOR = DPOR
  { DPOR -> Set ThreadId
dporRunnable :: Set ThreadId
  -- ^ What threads are runnable at this step.
  , DPOR -> Map ThreadId Bool
dporTodo     :: Map ThreadId Bool
  -- ^ Follow-on decisions still to make, and whether that decision
  -- was added conservatively due to the bound.
  , DPOR -> Maybe (ThreadId, DPOR)
dporNext     :: Maybe (ThreadId, DPOR)
  -- ^ The next decision made. Executions are explored in a
  -- depth-first fashion, so this changes as old subtrees are
  -- exhausted and new ones explored.
  , DPOR -> Set ThreadId
dporDone     :: Set ThreadId
  -- ^ All transitions which have been taken from this point,
  -- including conservatively-added ones.
  , DPOR -> Map ThreadId ThreadAction
dporSleep    :: Map ThreadId ThreadAction
  -- ^ Transitions to ignore (in this node and children) until a
  -- dependent transition happens.
  , DPOR -> Map ThreadId ThreadAction
dporTaken    :: Map ThreadId ThreadAction
  -- ^ Transitions which have been taken, excluding
  -- conservatively-added ones. This is used in implementing sleep
  -- sets.
  } deriving (DPOR -> DPOR -> Bool
(DPOR -> DPOR -> Bool) -> (DPOR -> DPOR -> Bool) -> Eq DPOR
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DPOR -> DPOR -> Bool
== :: DPOR -> DPOR -> Bool
$c/= :: DPOR -> DPOR -> Bool
/= :: DPOR -> DPOR -> Bool
Eq, Int -> DPOR -> ShowS
[DPOR] -> ShowS
DPOR -> String
(Int -> DPOR -> ShowS)
-> (DPOR -> String) -> ([DPOR] -> ShowS) -> Show DPOR
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DPOR -> ShowS
showsPrec :: Int -> DPOR -> ShowS
$cshow :: DPOR -> String
show :: DPOR -> String
$cshowList :: [DPOR] -> ShowS
showList :: [DPOR] -> ShowS
Show, (forall x. DPOR -> Rep DPOR x)
-> (forall x. Rep DPOR x -> DPOR) -> Generic DPOR
forall x. Rep DPOR x -> DPOR
forall x. DPOR -> Rep DPOR x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. DPOR -> Rep DPOR x
from :: forall x. DPOR -> Rep DPOR x
$cto :: forall x. Rep DPOR x -> DPOR
to :: forall x. Rep DPOR x -> DPOR
Generic, DPOR -> ()
(DPOR -> ()) -> NFData DPOR
forall a. (a -> ()) -> NFData a
$crnf :: DPOR -> ()
rnf :: DPOR -> ()
NFData)

-- | Check the DPOR data invariants and raise an error if any are
-- broken.
--
-- This is a reasonable thing to do, because if the state is corrupted
-- then nothing sensible can happen anyway.
validateDPOR :: HasCallStack => DPOR -> DPOR
validateDPOR :: HasCallStack => DPOR -> DPOR
validateDPOR DPOR
dpor
    | Bool -> Bool
not (Set ThreadId
todo Set ThreadId -> Set ThreadId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set ThreadId
runnable) = String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"thread exists in todo set but not runnable set"
    | Bool -> Bool
not (Set ThreadId
done Set ThreadId -> Set ThreadId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set ThreadId
runnable) = String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"thread exists in done set but not runnable set"
    | Bool -> Bool
not (Set ThreadId
taken Set ThreadId -> Set ThreadId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set ThreadId
done) = String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"thread exists in taken set but not done set"
    | Bool -> Bool
not (Set ThreadId
todo Set ThreadId -> Set ThreadId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`disjoint` Set ThreadId
done) = String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"thread exists in both todo set and done set"
    | Bool -> Bool
not (Bool -> (ThreadId -> Bool) -> Maybe ThreadId -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (ThreadId -> Set ThreadId -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set ThreadId
done) Maybe ThreadId
next) = String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"taken thread does not exist in done set"
    | Bool
otherwise = DPOR
dpor
  where
    done :: Set ThreadId
done = DPOR -> Set ThreadId
dporDone DPOR
dpor
    next :: Maybe ThreadId
next = (ThreadId, DPOR) -> ThreadId
forall a b. (a, b) -> a
fst ((ThreadId, DPOR) -> ThreadId)
-> Maybe (ThreadId, DPOR) -> Maybe ThreadId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DPOR -> Maybe (ThreadId, DPOR)
dporNext DPOR
dpor
    runnable :: Set ThreadId
runnable = DPOR -> Set ThreadId
dporRunnable DPOR
dpor
    taken :: Set ThreadId
taken = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList (Map ThreadId ThreadAction -> [ThreadId]
forall k a. Map k a -> [k]
M.keys (DPOR -> Map ThreadId ThreadAction
dporTaken DPOR
dpor))
    todo :: Set ThreadId
todo = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList (Map ThreadId Bool -> [ThreadId]
forall k a. Map k a -> [k]
M.keys (DPOR -> Map ThreadId Bool
dporTodo DPOR
dpor))

    disjoint :: Set a -> Set a -> Bool
disjoint Set a
s1 Set a
s2 = Set a -> Bool
forall a. Set a -> Bool
S.null (Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
S.intersection Set a
s1 Set a
s2)

-- | One step of the execution, including information for backtracking
-- purposes. This backtracking information is used to generate new
-- schedules.
data BacktrackStep = BacktrackStep
  { BacktrackStep -> ThreadId
bcktThreadid   :: ThreadId
  -- ^ The thread running at this step
  , BacktrackStep -> Decision
bcktDecision   :: Decision
  -- ^ What was decided at this step.
  , BacktrackStep -> ThreadAction
bcktAction     :: ThreadAction
  -- ^ What happened at this step.
  , BacktrackStep -> Map ThreadId Lookahead
bcktRunnable   :: Map ThreadId Lookahead
  -- ^ The threads runnable at this step
  , BacktrackStep -> Map ThreadId Bool
bcktBacktracks :: Map ThreadId Bool
  -- ^ The list of alternative threads to run, and whether those
  -- alternatives were added conservatively due to the bound.
  , BacktrackStep -> ConcurrencyState
bcktState      :: ConcurrencyState
  -- ^ Some domain-specific state at this point.
  } deriving (BacktrackStep -> BacktrackStep -> Bool
(BacktrackStep -> BacktrackStep -> Bool)
-> (BacktrackStep -> BacktrackStep -> Bool) -> Eq BacktrackStep
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BacktrackStep -> BacktrackStep -> Bool
== :: BacktrackStep -> BacktrackStep -> Bool
$c/= :: BacktrackStep -> BacktrackStep -> Bool
/= :: BacktrackStep -> BacktrackStep -> Bool
Eq, Int -> BacktrackStep -> ShowS
[BacktrackStep] -> ShowS
BacktrackStep -> String
(Int -> BacktrackStep -> ShowS)
-> (BacktrackStep -> String)
-> ([BacktrackStep] -> ShowS)
-> Show BacktrackStep
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BacktrackStep -> ShowS
showsPrec :: Int -> BacktrackStep -> ShowS
$cshow :: BacktrackStep -> String
show :: BacktrackStep -> String
$cshowList :: [BacktrackStep] -> ShowS
showList :: [BacktrackStep] -> ShowS
Show, (forall x. BacktrackStep -> Rep BacktrackStep x)
-> (forall x. Rep BacktrackStep x -> BacktrackStep)
-> Generic BacktrackStep
forall x. Rep BacktrackStep x -> BacktrackStep
forall x. BacktrackStep -> Rep BacktrackStep x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BacktrackStep -> Rep BacktrackStep x
from :: forall x. BacktrackStep -> Rep BacktrackStep x
$cto :: forall x. Rep BacktrackStep x -> BacktrackStep
to :: forall x. Rep BacktrackStep x -> BacktrackStep
Generic, BacktrackStep -> ()
(BacktrackStep -> ()) -> NFData BacktrackStep
forall a. (a -> ()) -> NFData a
$crnf :: BacktrackStep -> ()
rnf :: BacktrackStep -> ()
NFData)

-- | Initial DPOR state, given an initial thread ID. This initial
-- thread should exist and be runnable at the start of execution.
--
-- The main thread must be in the list of initially runnable threads.
initialState :: [ThreadId] -> DPOR
initialState :: [ThreadId] -> DPOR
initialState [ThreadId]
threads
  | ThreadId
initialThread ThreadId -> [ThreadId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ThreadId]
threads = DPOR
    { dporRunnable :: Set ThreadId
dporRunnable = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList [ThreadId]
threads
    , dporTodo :: Map ThreadId Bool
dporTodo     = ThreadId -> Bool -> Map ThreadId Bool
forall k a. k -> a -> Map k a
M.singleton ThreadId
initialThread Bool
False
    , dporNext :: Maybe (ThreadId, DPOR)
dporNext     = Maybe (ThreadId, DPOR)
forall a. Maybe a
Nothing
    , dporDone :: Set ThreadId
dporDone     = Set ThreadId
forall a. Set a
S.empty
    , dporSleep :: Map ThreadId ThreadAction
dporSleep    = Map ThreadId ThreadAction
forall k a. Map k a
M.empty
    , dporTaken :: Map ThreadId ThreadAction
dporTaken    = Map ThreadId ThreadAction
forall k a. Map k a
M.empty
    }
  | Bool
otherwise = String -> String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"initialState" String
"Initial thread is not in initially runnable set"

-- | Produce a new schedule prefix from a @DPOR@ tree. If there are no new
-- prefixes remaining, return 'Nothing'. Also returns whether the
-- decision was added conservatively, and the sleep set at the point
-- where divergence happens.
--
-- A schedule prefix is a possibly empty sequence of decisions that
-- have already been made, terminated by a single decision from the
-- to-do set. The intent is to put the system into a new state when
-- executed with this initial sequence of scheduling decisions.
findSchedulePrefix
  :: DPOR
  -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
findSchedulePrefix :: DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
findSchedulePrefix DPOR
dpor = case DPOR -> Maybe (ThreadId, DPOR)
dporNext DPOR
dpor of
    Just (ThreadId
tid, DPOR
child) -> ThreadId
-> DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
go ThreadId
tid DPOR
child Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
here
    Maybe (ThreadId, DPOR)
Nothing -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
here
  where
    go :: ThreadId
-> DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
go ThreadId
tid DPOR
child = (\([ThreadId]
ts,Bool
c,Map ThreadId ThreadAction
slp) -> (ThreadId
tidThreadId -> [ThreadId] -> [ThreadId]
forall a. a -> [a] -> [a]
:[ThreadId]
ts,Bool
c,Map ThreadId ThreadAction
slp)) (([ThreadId], Bool, Map ThreadId ThreadAction)
 -> ([ThreadId], Bool, Map ThreadId ThreadAction))
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DPOR -> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
findSchedulePrefix DPOR
child

    -- Prefix traces terminating with a to-do decision at this point.
    here :: Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
here =
      let todos :: [([ThreadId], Bool, Map ThreadId ThreadAction)]
todos = [([ThreadId
t], Bool
c, Map ThreadId ThreadAction
sleeps) | (ThreadId
t, Bool
c) <- Map ThreadId Bool -> [(ThreadId, Bool)]
forall k a. Map k a -> [(k, a)]
M.toList (Map ThreadId Bool -> [(ThreadId, Bool)])
-> Map ThreadId Bool -> [(ThreadId, Bool)]
forall a b. (a -> b) -> a -> b
$ DPOR -> Map ThreadId Bool
dporTodo DPOR
dpor]
          ([([ThreadId], Bool, Map ThreadId ThreadAction)]
best, [([ThreadId], Bool, Map ThreadId ThreadAction)]
worst) = (([ThreadId], Bool, Map ThreadId ThreadAction) -> Bool)
-> [([ThreadId], Bool, Map ThreadId ThreadAction)]
-> ([([ThreadId], Bool, Map ThreadId ThreadAction)],
    [([ThreadId], Bool, Map ThreadId ThreadAction)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\([ThreadId
t],Bool
_,Map ThreadId ThreadAction
_) -> ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Ord a => a -> a -> Bool
>= ThreadId
initialThread) [([ThreadId], Bool, Map ThreadId ThreadAction)]
todos
      in [([ThreadId], Bool, Map ThreadId ThreadAction)]
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
forall a. [a] -> Maybe a
listToMaybe [([ThreadId], Bool, Map ThreadId ThreadAction)]
best Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [([ThreadId], Bool, Map ThreadId ThreadAction)]
-> Maybe ([ThreadId], Bool, Map ThreadId ThreadAction)
forall a. [a] -> Maybe a
listToMaybe [([ThreadId], Bool, Map ThreadId ThreadAction)]
worst

    -- The new sleep set is the union of the sleep set of the node
    -- we're branching from, plus all the decisions we've already
    -- explored.
    sleeps :: Map ThreadId ThreadAction
sleeps = DPOR -> Map ThreadId ThreadAction
dporSleep DPOR
dpor Map ThreadId ThreadAction
-> Map ThreadId ThreadAction -> Map ThreadId ThreadAction
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` DPOR -> Map ThreadId ThreadAction
dporTaken DPOR
dpor

-- | Add a new trace to the stack.  This won't work if to-dos aren't explored depth-first.
incorporateTrace :: HasCallStack
  => Bool
  -- ^ True if all IO is thread-safe.
  -> MemType
  -> Bool
  -- ^ Whether the \"to-do\" point which was used to create this new
  -- execution was conservative or not.
  -> Trace
  -- ^ The execution trace: the decision made, the runnable threads,
  -- and the action performed.
  -> ConcurrencyState
  -- ^ The initial concurrency state
  -> DPOR
  -> DPOR
incorporateTrace :: HasCallStack =>
Bool
-> MemType -> Bool -> Trace -> ConcurrencyState -> DPOR -> DPOR
incorporateTrace Bool
safeIO MemType
memtype Bool
conservative = ThreadId -> Trace -> ConcurrencyState -> DPOR -> DPOR
forall {b}.
ThreadId
-> [(Decision, [(ThreadId, b)], ThreadAction)]
-> ConcurrencyState
-> DPOR
-> DPOR
grow ThreadId
initialThread where
  grow :: ThreadId
-> [(Decision, [(ThreadId, b)], ThreadAction)]
-> ConcurrencyState
-> DPOR
-> DPOR
grow ThreadId
tid trc :: [(Decision, [(ThreadId, b)], ThreadAction)]
trc@((Decision
d, [(ThreadId, b)]
_, ThreadAction
a):[(Decision, [(ThreadId, b)], ThreadAction)]
rest) ConcurrencyState
state DPOR
dpor =
    let tid' :: ThreadId
tid'   = ThreadId -> Decision -> ThreadId
tidOf ThreadId
tid Decision
d
        state' :: ConcurrencyState
state' = MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
state ThreadId
tid' ThreadAction
a
    in case DPOR -> Maybe (ThreadId, DPOR)
dporNext DPOR
dpor of
         Just (ThreadId
t, DPOR
child)
           | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid' ->
             HasCallStack => DPOR -> DPOR
DPOR -> DPOR
validateDPOR (DPOR -> DPOR) -> DPOR -> DPOR
forall a b. (a -> b) -> a -> b
$ DPOR
dpor { dporNext = Just (tid', grow tid' rest state' child) }
           | DPOR -> Bool
hasTodos DPOR
child -> String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"replacing child with todos!"
         Maybe (ThreadId, DPOR)
_ -> HasCallStack => DPOR -> DPOR
DPOR -> DPOR
validateDPOR (DPOR -> DPOR) -> DPOR -> DPOR
forall a b. (a -> b) -> a -> b
$
           let taken :: Map ThreadId ThreadAction
taken = ThreadId
-> ThreadAction
-> Map ThreadId ThreadAction
-> Map ThreadId ThreadAction
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ThreadId
tid' ThreadAction
a (DPOR -> Map ThreadId ThreadAction
dporTaken DPOR
dpor)
               sleep :: Map ThreadId ThreadAction
sleep = DPOR -> Map ThreadId ThreadAction
dporSleep DPOR
dpor Map ThreadId ThreadAction
-> Map ThreadId ThreadAction -> Map ThreadId ThreadAction
forall k a. Ord k => Map k a -> Map k a -> Map k a
`M.union` DPOR -> Map ThreadId ThreadAction
dporTaken DPOR
dpor
           in DPOR
dpor { dporTaken = if conservative then dporTaken dpor else taken
                   , dporTodo  = M.delete tid' (dporTodo dpor)
                   , dporNext  = Just (tid', subtree state' tid' sleep trc)
                   , dporDone  = S.insert tid' (dporDone dpor)
                   }
  grow ThreadId
_ [(Decision, [(ThreadId, b)], ThreadAction)]
_ ConcurrencyState
_ DPOR
_ = String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"trace exhausted without reading a to-do point!"

  -- check if there are to-do points in a tree
  hasTodos :: DPOR -> Bool
hasTodos DPOR
dpor = Bool -> Bool
not (Map ThreadId Bool -> Bool
forall k a. Map k a -> Bool
M.null (DPOR -> Map ThreadId Bool
dporTodo DPOR
dpor)) Bool -> Bool -> Bool
|| (case DPOR -> Maybe (ThreadId, DPOR)
dporNext DPOR
dpor of Just (ThreadId
_, DPOR
dpor') -> DPOR -> Bool
hasTodos DPOR
dpor'; Maybe (ThreadId, DPOR)
_ -> Bool
False)

  -- Construct a new subtree corresponding to a trace suffix.
  subtree :: ConcurrencyState
-> ThreadId
-> Map ThreadId ThreadAction
-> [(Decision, [(ThreadId, b)], ThreadAction)]
-> DPOR
subtree ConcurrencyState
state ThreadId
tid Map ThreadId ThreadAction
sleep ((Decision
_, [(ThreadId, b)]
_, ThreadAction
a):[(Decision, [(ThreadId, b)], ThreadAction)]
rest) = HasCallStack => DPOR -> DPOR
DPOR -> DPOR
validateDPOR (DPOR -> DPOR) -> DPOR -> DPOR
forall a b. (a -> b) -> a -> b
$
    let state' :: ConcurrencyState
state' = MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
state ThreadId
tid ThreadAction
a
        sleep' :: Map ThreadId ThreadAction
sleep' = (ThreadId -> ThreadAction -> Bool)
-> Map ThreadId ThreadAction -> Map ThreadId ThreadAction
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\ThreadId
t ThreadAction
a' -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
dependent Bool
safeIO ConcurrencyState
state' ThreadId
tid ThreadAction
a ThreadId
t ThreadAction
a') Map ThreadId ThreadAction
sleep
    in DPOR
        { dporRunnable :: Set ThreadId
dporRunnable = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList ([ThreadId] -> Set ThreadId) -> [ThreadId] -> Set ThreadId
forall a b. (a -> b) -> a -> b
$ case [(Decision, [(ThreadId, b)], ThreadAction)]
rest of
            ((Decision
d', [(ThreadId, b)]
runnable, ThreadAction
_):[(Decision, [(ThreadId, b)], ThreadAction)]
_) -> ThreadId -> Decision -> ThreadId
tidOf ThreadId
tid Decision
d' ThreadId -> [ThreadId] -> [ThreadId]
forall a. a -> [a] -> [a]
: ((ThreadId, b) -> ThreadId) -> [(ThreadId, b)] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (ThreadId, b) -> ThreadId
forall a b. (a, b) -> a
fst [(ThreadId, b)]
runnable
            [] -> []
        , dporTodo :: Map ThreadId Bool
dporTodo = Map ThreadId Bool
forall k a. Map k a
M.empty
        , dporNext :: Maybe (ThreadId, DPOR)
dporNext = case [(Decision, [(ThreadId, b)], ThreadAction)]
rest of
          ((Decision
d', [(ThreadId, b)]
_, ThreadAction
_):[(Decision, [(ThreadId, b)], ThreadAction)]
_) ->
            let tid' :: ThreadId
tid' = ThreadId -> Decision -> ThreadId
tidOf ThreadId
tid Decision
d'
            in  (ThreadId, DPOR) -> Maybe (ThreadId, DPOR)
forall a. a -> Maybe a
Just (ThreadId
tid', ConcurrencyState
-> ThreadId
-> Map ThreadId ThreadAction
-> [(Decision, [(ThreadId, b)], ThreadAction)]
-> DPOR
subtree ConcurrencyState
state' ThreadId
tid' Map ThreadId ThreadAction
sleep' [(Decision, [(ThreadId, b)], ThreadAction)]
rest)
          [] -> Maybe (ThreadId, DPOR)
forall a. Maybe a
Nothing
        , dporDone :: Set ThreadId
dporDone = case [(Decision, [(ThreadId, b)], ThreadAction)]
rest of
            ((Decision
d', [(ThreadId, b)]
_, ThreadAction
_):[(Decision, [(ThreadId, b)], ThreadAction)]
_) -> ThreadId -> Set ThreadId
forall a. a -> Set a
S.singleton (ThreadId -> Decision -> ThreadId
tidOf ThreadId
tid Decision
d')
            [] -> Set ThreadId
forall a. Set a
S.empty
        , dporSleep :: Map ThreadId ThreadAction
dporSleep = Map ThreadId ThreadAction
sleep'
        , dporTaken :: Map ThreadId ThreadAction
dporTaken = case [(Decision, [(ThreadId, b)], ThreadAction)]
rest of
          ((Decision
d', [(ThreadId, b)]
_, ThreadAction
a'):[(Decision, [(ThreadId, b)], ThreadAction)]
_) -> ThreadId -> ThreadAction -> Map ThreadId ThreadAction
forall k a. k -> a -> Map k a
M.singleton (ThreadId -> Decision -> ThreadId
tidOf ThreadId
tid Decision
d') ThreadAction
a'
          [] -> Map ThreadId ThreadAction
forall k a. Map k a
M.empty
        }
  subtree ConcurrencyState
_ ThreadId
_ Map ThreadId ThreadAction
_ [(Decision, [(ThreadId, b)], ThreadAction)]
_ = String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"subtree suffix empty!"

-- | Produce a list of new backtracking points from an execution
-- trace. These are then used to inform new \"to-do\" points in the
-- @DPOR@ tree.
--
-- Two traces are passed in to this function: the first is generated
-- from the special DPOR scheduler, the other from the execution of
-- the concurrent program.
--
-- If the trace ends with any threads other than the initial one still
-- runnable, a dependency is imposed between this final action and
-- everything else.
findBacktrackSteps
  :: Bool
  -- ^ True if all IO is thread-safe
  -> MemType
  -> BacktrackFunc
  -- ^ Backtracking function. Given a list of backtracking points, and
  -- a thread to backtrack to at a specific point in that list, add
  -- the new backtracking points. There will be at least one: this
  -- chosen one, but the function may add others.
  -> Bool
  -- ^ Whether the computation was aborted due to no decisions being
  -- in-bounds.
  -> ConcurrencyState
  -- ^ The initial concurrency state.
  -> Seq ([(ThreadId, Lookahead)], [ThreadId])
  -- ^ A sequence of threads at each step: the list of runnable
  -- in-bound threads (with lookahead values), and the list of threads
  -- still to try. The reason for the two separate lists is because
  -- the threads chosen to try will be dependent on the specific
  -- domain.
  -> Trace
  -- ^ The execution trace.
  -> [BacktrackStep]
findBacktrackSteps :: Bool
-> MemType
-> BacktrackFunc
-> Bool
-> ConcurrencyState
-> Seq ([(ThreadId, Lookahead)], [ThreadId])
-> Trace
-> [BacktrackStep]
findBacktrackSteps Bool
safeIO MemType
memtype BacktrackFunc
backtrack Bool
boundKill ConcurrencyState
state0 = ConcurrencyState
-> Set ThreadId
-> ThreadId
-> [BacktrackStep]
-> [([(ThreadId, Lookahead)], [ThreadId])]
-> Trace
-> [BacktrackStep]
forall {b}.
ConcurrencyState
-> Set ThreadId
-> ThreadId
-> [BacktrackStep]
-> [([(ThreadId, Lookahead)], [ThreadId])]
-> [(Decision, b, ThreadAction)]
-> [BacktrackStep]
go ConcurrencyState
state0 Set ThreadId
forall a. Set a
S.empty ThreadId
initialThread [] ([([(ThreadId, Lookahead)], [ThreadId])]
 -> Trace -> [BacktrackStep])
-> (Seq ([(ThreadId, Lookahead)], [ThreadId])
    -> [([(ThreadId, Lookahead)], [ThreadId])])
-> Seq ([(ThreadId, Lookahead)], [ThreadId])
-> Trace
-> [BacktrackStep]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq ([(ThreadId, Lookahead)], [ThreadId])
-> [([(ThreadId, Lookahead)], [ThreadId])]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList where
  -- Walk through the traces one step at a time, building up a list of
  -- new backtracking points.
  go :: ConcurrencyState
-> Set ThreadId
-> ThreadId
-> [BacktrackStep]
-> [([(ThreadId, Lookahead)], [ThreadId])]
-> [(Decision, b, ThreadAction)]
-> [BacktrackStep]
go ConcurrencyState
state Set ThreadId
allThreads ThreadId
tid [BacktrackStep]
bs (([(ThreadId, Lookahead)]
e,[ThreadId]
i):[([(ThreadId, Lookahead)], [ThreadId])]
is) ((Decision
d,b
_,ThreadAction
a):[(Decision, b, ThreadAction)]
ts) =
    let tid' :: ThreadId
tid' = ThreadId -> Decision -> ThreadId
tidOf ThreadId
tid Decision
d
        state' :: ConcurrencyState
state' = MemType
-> ConcurrencyState -> ThreadId -> ThreadAction -> ConcurrencyState
updateCState MemType
memtype ConcurrencyState
state ThreadId
tid' ThreadAction
a
        this :: BacktrackStep
this = BacktrackStep
          { bcktThreadid :: ThreadId
bcktThreadid   = ThreadId
tid'
          , bcktDecision :: Decision
bcktDecision   = Decision
d
          , bcktAction :: ThreadAction
bcktAction     = ThreadAction
a
          , bcktRunnable :: Map ThreadId Lookahead
bcktRunnable   = [(ThreadId, Lookahead)] -> Map ThreadId Lookahead
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(ThreadId, Lookahead)]
e
          , bcktBacktracks :: Map ThreadId Bool
bcktBacktracks = [(ThreadId, Bool)] -> Map ThreadId Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(ThreadId, Bool)] -> Map ThreadId Bool)
-> [(ThreadId, Bool)] -> Map ThreadId Bool
forall a b. (a -> b) -> a -> b
$ (ThreadId -> (ThreadId, Bool)) -> [ThreadId] -> [(ThreadId, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (\ThreadId
i' -> (ThreadId
i', Bool
False)) [ThreadId]
i
          , bcktState :: ConcurrencyState
bcktState      = ConcurrencyState
state
          }
        bs' :: [BacktrackStep]
bs' = Bool
-> Set ThreadId
-> [(ThreadId, Lookahead)]
-> [BacktrackStep]
-> [BacktrackStep]
doBacktrack Bool
killsEarly Set ThreadId
allThreads' [(ThreadId, Lookahead)]
e ([BacktrackStep]
bs[BacktrackStep] -> [BacktrackStep] -> [BacktrackStep]
forall a. [a] -> [a] -> [a]
++[BacktrackStep
this])
        runnable :: Set ThreadId
runnable = [ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList (Map ThreadId Lookahead -> [ThreadId]
forall k a. Map k a -> [k]
M.keys (Map ThreadId Lookahead -> [ThreadId])
-> Map ThreadId Lookahead -> [ThreadId]
forall a b. (a -> b) -> a -> b
$ BacktrackStep -> Map ThreadId Lookahead
bcktRunnable BacktrackStep
this)
        allThreads' :: Set ThreadId
allThreads' = Set ThreadId
allThreads Set ThreadId -> Set ThreadId -> Set ThreadId
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Set ThreadId
runnable
        killsEarly :: Bool
killsEarly = [(Decision, b, ThreadAction)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Decision, b, ThreadAction)]
ts Bool -> Bool -> Bool
&& Bool
boundKill
    in ConcurrencyState
-> Set ThreadId
-> ThreadId
-> [BacktrackStep]
-> [([(ThreadId, Lookahead)], [ThreadId])]
-> [(Decision, b, ThreadAction)]
-> [BacktrackStep]
go ConcurrencyState
state' Set ThreadId
allThreads' ThreadId
tid' [BacktrackStep]
bs' [([(ThreadId, Lookahead)], [ThreadId])]
is [(Decision, b, ThreadAction)]
ts
  go ConcurrencyState
_ Set ThreadId
_ ThreadId
_ [BacktrackStep]
bs [([(ThreadId, Lookahead)], [ThreadId])]
_ [(Decision, b, ThreadAction)]
_ = [BacktrackStep]
bs

  -- Find the prior actions dependent with this one and add
  -- backtracking points.
  doBacktrack :: Bool
-> Set ThreadId
-> [(ThreadId, Lookahead)]
-> [BacktrackStep]
-> [BacktrackStep]
doBacktrack Bool
killsEarly Set ThreadId
allThreads [(ThreadId, Lookahead)]
enabledThreads [BacktrackStep]
bs =
    let tagged :: [(Int, BacktrackStep)]
tagged = [(Int, BacktrackStep)] -> [(Int, BacktrackStep)]
forall a. [a] -> [a]
reverse ([(Int, BacktrackStep)] -> [(Int, BacktrackStep)])
-> [(Int, BacktrackStep)] -> [(Int, BacktrackStep)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [BacktrackStep] -> [(Int, BacktrackStep)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [BacktrackStep]
bs
        idxs :: [(Int, Bool, ThreadId)]
idxs   = [ (Int
i, Bool
False, ThreadId
u)
                 | (ThreadId
u, Lookahead
n) <- [(ThreadId, Lookahead)]
enabledThreads
                 , ThreadId
v <- Set ThreadId -> [ThreadId]
forall a. Set a -> [a]
S.toList Set ThreadId
allThreads
                 , ThreadId
u ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadId
v
                 , Int
i <- Maybe Int -> [Int]
forall a. Maybe a -> [a]
maybeToList (ThreadId
-> Lookahead -> ThreadId -> [(Int, BacktrackStep)] -> Maybe Int
forall {a}.
ThreadId
-> Lookahead -> ThreadId -> [(a, BacktrackStep)] -> Maybe a
findIndex ThreadId
u Lookahead
n ThreadId
v [(Int, BacktrackStep)]
tagged)]

        findIndex :: ThreadId
-> Lookahead -> ThreadId -> [(a, BacktrackStep)] -> Maybe a
findIndex ThreadId
u Lookahead
n ThreadId
v = [(a, BacktrackStep)] -> Maybe a
forall {a}. [(a, BacktrackStep)] -> Maybe a
go' where
          {-# INLINE go' #-}
          go' :: [(a, BacktrackStep)] -> Maybe a
go' ((a
i,BacktrackStep
b):[(a, BacktrackStep)]
rest)
            -- If this is the final action in the trace and the
            -- execution was killed due to nothing being within bounds
            -- (@killsEarly == True@) assume worst-case dependency.
            | BacktrackStep -> ThreadId
bcktThreadid BacktrackStep
b ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
v Bool -> Bool -> Bool
&& (Bool
killsEarly Bool -> Bool -> Bool
|| BacktrackStep -> Bool
isDependent BacktrackStep
b) = a -> Maybe a
forall a. a -> Maybe a
Just a
i
            | Bool
otherwise = [(a, BacktrackStep)] -> Maybe a
go' [(a, BacktrackStep)]
rest
          go' [] = Maybe a
forall a. Maybe a
Nothing

          {-# INLINE isDependent #-}
          isDependent :: BacktrackStep -> Bool
isDependent BacktrackStep
b
            -- Don't impose a dependency if the other thread will
            -- immediately block already. This is safe because a
            -- context switch will occur anyway so there's no point
            -- pre-empting the action UNLESS the pre-emption would
            -- possibly allow for a different relaxed memory stage.
            | ThreadAction -> Bool
isBlock (BacktrackStep -> ThreadAction
bcktAction BacktrackStep
b) Bool -> Bool -> Bool
&& ActionType -> Bool
isBarrier (Lookahead -> ActionType
simplifyLookahead Lookahead
n) = Bool
False
            | Bool
otherwise = Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> Lookahead
-> Bool
dependent' Bool
safeIO (BacktrackStep -> ConcurrencyState
bcktState BacktrackStep
b) (BacktrackStep -> ThreadId
bcktThreadid BacktrackStep
b) (BacktrackStep -> ThreadAction
bcktAction BacktrackStep
b) ThreadId
u Lookahead
n
    in BacktrackFunc
backtrack [BacktrackStep]
bs [(Int, Bool, ThreadId)]
idxs

-- | Add new backtracking points, if they have not already been
-- visited and aren't in the sleep set.
incorporateBacktrackSteps :: HasCallStack
  => [BacktrackStep] -> DPOR -> DPOR
incorporateBacktrackSteps :: HasCallStack => [BacktrackStep] -> DPOR -> DPOR
incorporateBacktrackSteps (BacktrackStep
b:[BacktrackStep]
bs) DPOR
dpor = HasCallStack => DPOR -> DPOR
DPOR -> DPOR
validateDPOR DPOR
dpor' where
  tid :: ThreadId
tid = BacktrackStep -> ThreadId
bcktThreadid BacktrackStep
b

  dpor' :: DPOR
dpor' = DPOR
dpor
    { dporTodo = dporTodo dpor `M.union` M.fromList todo
    , dporNext = Just (tid, child)
    }

  todo :: [(ThreadId, Bool)]
todo =
    [ (ThreadId, Bool)
x
    | x :: (ThreadId, Bool)
x@(ThreadId
t,Bool
c) <- Map ThreadId Bool -> [(ThreadId, Bool)]
forall k a. Map k a -> [(k, a)]
M.toList (Map ThreadId Bool -> [(ThreadId, Bool)])
-> Map ThreadId Bool -> [(ThreadId, Bool)]
forall a b. (a -> b) -> a -> b
$ BacktrackStep -> Map ThreadId Bool
bcktBacktracks BacktrackStep
b
    , ThreadId -> Maybe ThreadId
forall a. a -> Maybe a
Just ThreadId
t Maybe ThreadId -> Maybe ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= ((ThreadId, DPOR) -> ThreadId
forall a b. (a, b) -> a
fst ((ThreadId, DPOR) -> ThreadId)
-> Maybe (ThreadId, DPOR) -> Maybe ThreadId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DPOR -> Maybe (ThreadId, DPOR)
dporNext DPOR
dpor)
    , ThreadId -> Set ThreadId -> Bool
forall a. Ord a => a -> Set a -> Bool
S.notMember ThreadId
t (DPOR -> Set ThreadId
dporDone DPOR
dpor)
    , Bool
c Bool -> Bool -> Bool
|| ThreadId -> Map ThreadId ThreadAction -> Bool
forall k a. Ord k => k -> Map k a -> Bool
M.notMember ThreadId
t (DPOR -> Map ThreadId ThreadAction
dporSleep DPOR
dpor)
    ]

  child :: DPOR
child = case DPOR -> Maybe (ThreadId, DPOR)
dporNext DPOR
dpor of
    Just (ThreadId
t, DPOR
d)
      | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadId
tid -> String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"incorporating wrong trace!"
      | Bool
otherwise -> HasCallStack => [BacktrackStep] -> DPOR -> DPOR
[BacktrackStep] -> DPOR -> DPOR
incorporateBacktrackSteps [BacktrackStep]
bs DPOR
d
    Maybe (ThreadId, DPOR)
Nothing -> String -> DPOR
forall a. HasCallStack => String -> a
fatal String
"child is missing!"
incorporateBacktrackSteps [] DPOR
dpor = DPOR
dpor

-------------------------------------------------------------------------------
-- * DPOR scheduler

-- | The scheduler state
data DPORSchedState k = DPORSchedState
  { forall k. DPORSchedState k -> Map ThreadId ThreadAction
schedSleep     :: Map ThreadId ThreadAction
  -- ^ The sleep set: decisions not to make until something dependent
  -- with them happens.
  , forall k. DPORSchedState k -> [ThreadId]
schedPrefix    :: [ThreadId]
  -- ^ Decisions still to make
  , forall k.
DPORSchedState k -> Seq ([(ThreadId, Lookahead)], [ThreadId])
schedBPoints   :: Seq ([(ThreadId, Lookahead)], [ThreadId])
  -- ^ Which threads are runnable and in-bound at each step, and the
  -- alternative decisions still to make.
  , forall k. DPORSchedState k -> Bool
schedIgnore    :: Bool
  -- ^ Whether to ignore this execution or not: @True@ if the
  -- execution is aborted due to all possible decisions being in the
  -- sleep set, as then everything in this execution is covered by
  -- another.
  , forall k. DPORSchedState k -> Bool
schedBoundKill :: Bool
  -- ^ Whether the execution was terminated due to all decisions being
  -- out of bounds.
  , forall k. DPORSchedState k -> ConcurrencyState
schedCState    :: ConcurrencyState
  -- ^ State used by the dependency function to determine when to
  -- remove decisions from the sleep set.
  , forall k. DPORSchedState k -> Maybe k
schedBState    :: Maybe k
  -- ^ State used by the incremental bounding function.
  } deriving (DPORSchedState k -> DPORSchedState k -> Bool
(DPORSchedState k -> DPORSchedState k -> Bool)
-> (DPORSchedState k -> DPORSchedState k -> Bool)
-> Eq (DPORSchedState k)
forall k. Eq k => DPORSchedState k -> DPORSchedState k -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall k. Eq k => DPORSchedState k -> DPORSchedState k -> Bool
== :: DPORSchedState k -> DPORSchedState k -> Bool
$c/= :: forall k. Eq k => DPORSchedState k -> DPORSchedState k -> Bool
/= :: DPORSchedState k -> DPORSchedState k -> Bool
Eq, Int -> DPORSchedState k -> ShowS
[DPORSchedState k] -> ShowS
DPORSchedState k -> String
(Int -> DPORSchedState k -> ShowS)
-> (DPORSchedState k -> String)
-> ([DPORSchedState k] -> ShowS)
-> Show (DPORSchedState k)
forall k. Show k => Int -> DPORSchedState k -> ShowS
forall k. Show k => [DPORSchedState k] -> ShowS
forall k. Show k => DPORSchedState k -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall k. Show k => Int -> DPORSchedState k -> ShowS
showsPrec :: Int -> DPORSchedState k -> ShowS
$cshow :: forall k. Show k => DPORSchedState k -> String
show :: DPORSchedState k -> String
$cshowList :: forall k. Show k => [DPORSchedState k] -> ShowS
showList :: [DPORSchedState k] -> ShowS
Show, (forall x. DPORSchedState k -> Rep (DPORSchedState k) x)
-> (forall x. Rep (DPORSchedState k) x -> DPORSchedState k)
-> Generic (DPORSchedState k)
forall x. Rep (DPORSchedState k) x -> DPORSchedState k
forall x. DPORSchedState k -> Rep (DPORSchedState k) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k x. Rep (DPORSchedState k) x -> DPORSchedState k
forall k x. DPORSchedState k -> Rep (DPORSchedState k) x
$cfrom :: forall k x. DPORSchedState k -> Rep (DPORSchedState k) x
from :: forall x. DPORSchedState k -> Rep (DPORSchedState k) x
$cto :: forall k x. Rep (DPORSchedState k) x -> DPORSchedState k
to :: forall x. Rep (DPORSchedState k) x -> DPORSchedState k
Generic, DPORSchedState k -> ()
(DPORSchedState k -> ()) -> NFData (DPORSchedState k)
forall k. NFData k => DPORSchedState k -> ()
forall a. (a -> ()) -> NFData a
$crnf :: forall k. NFData k => DPORSchedState k -> ()
rnf :: DPORSchedState k -> ()
NFData)

-- | Initial DPOR scheduler state for a given prefix
initialDPORSchedState :: Map ThreadId ThreadAction
  -- ^ The initial sleep set.
  -> [ThreadId]
  -- ^ The schedule prefix.
  -> ConcurrencyState
  -- ^ The initial concurrency state.
  -> DPORSchedState k
initialDPORSchedState :: forall k.
Map ThreadId ThreadAction
-> [ThreadId] -> ConcurrencyState -> DPORSchedState k
initialDPORSchedState Map ThreadId ThreadAction
sleep [ThreadId]
prefix ConcurrencyState
state0 = DPORSchedState
  { schedSleep :: Map ThreadId ThreadAction
schedSleep     = Map ThreadId ThreadAction
sleep
  , schedPrefix :: [ThreadId]
schedPrefix    = [ThreadId]
prefix
  , schedBPoints :: Seq ([(ThreadId, Lookahead)], [ThreadId])
schedBPoints   = Seq ([(ThreadId, Lookahead)], [ThreadId])
forall a. Seq a
Sq.empty
  , schedIgnore :: Bool
schedIgnore    = Bool
False
  , schedBoundKill :: Bool
schedBoundKill = Bool
False
  , schedCState :: ConcurrencyState
schedCState    = ConcurrencyState
state0
  , schedBState :: Maybe k
schedBState    = Maybe k
forall a. Maybe a
Nothing
  }

-- | An incremental bounding function is a stateful function that
-- takes the last and next decisions, and returns a new state only if
-- the next decision is within the bound.
type IncrementalBoundFunc k
  = Maybe k -> Maybe (ThreadId, ThreadAction) -> (Decision, Lookahead) -> Maybe k

-- | A backtracking step is a point in the execution where another
-- decision needs to be made, in order to explore interesting new
-- schedules. A backtracking /function/ takes the steps identified so
-- far and a list of points and thread at that point to backtrack
-- to. More points be added to compensate for the effects of the
-- bounding function. For example, under pre-emption bounding a
-- conservative backtracking point is added at the prior context
-- switch. The bool is whether the point is conservative. Conservative
-- points are always explored, whereas non-conservative ones might be
-- skipped based on future information.
--
-- In general, a backtracking function should identify one or more
-- backtracking points, and then use @backtrackAt@ to do the actual
-- work.
type BacktrackFunc
  = [BacktrackStep] -> [(Int, Bool, ThreadId)] -> [BacktrackStep]

-- | Add a backtracking point. If the thread isn't runnable, add all
-- runnable threads. If the backtracking point is already present,
-- don't re-add it UNLESS this would make it conservative.
backtrackAt :: HasCallStack
  => (ThreadId -> BacktrackStep -> Bool)
  -- ^ If this returns @True@, backtrack to all runnable threads,
  -- rather than just the given thread.
  -> BacktrackFunc
backtrackAt :: HasCallStack =>
(ThreadId -> BacktrackStep -> Bool) -> BacktrackFunc
backtrackAt ThreadId -> BacktrackStep -> Bool
toAll [BacktrackStep]
bs0 = [(Int, Bool, ThreadId)] -> [BacktrackStep]
forall {t}.
(Eq t, Num t) =>
[(t, Bool, ThreadId)] -> [BacktrackStep]
backtrackAt' ([(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) -> Bool)
-> [(Int, Bool, ThreadId)] -> [(Int, Bool, ThreadId)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Int -> Int -> Bool)
-> ((Int, Bool, ThreadId) -> Int)
-> (Int, Bool, ThreadId)
-> (Int, Bool, ThreadId)
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, Bool, ThreadId) -> Int
forall {a} {b} {c}. (a, b, c) -> a
fst') ([(Int, Bool, ThreadId)] -> [(Int, Bool, ThreadId)])
-> ([(Int, Bool, ThreadId)] -> [(Int, Bool, ThreadId)])
-> [(Int, Bool, ThreadId)]
-> [(Int, Bool, ThreadId)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Bool, ThreadId) -> Int)
-> [(Int, Bool, ThreadId)] -> [(Int, Bool, ThreadId)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Int, Bool, ThreadId) -> Int
forall {a} {b} {c}. (a, b, c) -> a
fst' where
  fst' :: (a, b, c) -> a
fst' (a
x,b
_,c
_) = a
x

  backtrackAt' :: [(t, Bool, ThreadId)] -> [BacktrackStep]
backtrackAt' ((t
i,Bool
c,ThreadId
t):[(t, Bool, ThreadId)]
is) = t
-> [BacktrackStep]
-> t
-> Bool
-> ThreadId
-> [(t, Bool, ThreadId)]
-> [BacktrackStep]
forall {t}.
(Eq t, Num t) =>
t
-> [BacktrackStep]
-> t
-> Bool
-> ThreadId
-> [(t, Bool, ThreadId)]
-> [BacktrackStep]
go t
i [BacktrackStep]
bs0 t
i Bool
c ThreadId
t [(t, Bool, ThreadId)]
is
  backtrackAt' [] = [BacktrackStep]
bs0

  go :: t
-> [BacktrackStep]
-> t
-> Bool
-> ThreadId
-> [(t, Bool, ThreadId)]
-> [BacktrackStep]
go t
i0 (BacktrackStep
b:[BacktrackStep]
bs) t
0 Bool
c ThreadId
tid [(t, Bool, ThreadId)]
is
    -- If the backtracking point is already present, don't re-add it,
    -- UNLESS this would force it to backtrack (it's conservative)
    -- where before it might not.
    | Bool -> Bool
not (ThreadId -> BacktrackStep -> Bool
toAll ThreadId
tid BacktrackStep
b) Bool -> Bool -> Bool
&& ThreadId
tid ThreadId -> Map ThreadId Lookahead -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`M.member` BacktrackStep -> Map ThreadId Lookahead
bcktRunnable BacktrackStep
b =
      let val :: Maybe Bool
val = ThreadId -> Map ThreadId Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup ThreadId
tid (Map ThreadId Bool -> Maybe Bool)
-> Map ThreadId Bool -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ BacktrackStep -> Map ThreadId Bool
bcktBacktracks BacktrackStep
b
          b' :: BacktrackStep
b' = if Maybe Bool -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Bool
val Bool -> Bool -> Bool
|| (Maybe Bool
val Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False Bool -> Bool -> Bool
&& Bool
c)
            then BacktrackStep
b { bcktBacktracks = backtrackTo tid c b }
            else BacktrackStep
b
      in BacktrackStep
b' BacktrackStep -> [BacktrackStep] -> [BacktrackStep]
forall a. a -> [a] -> [a]
: case [(t, Bool, ThreadId)]
is of
        ((t
i',Bool
c',ThreadId
t'):[(t, Bool, ThreadId)]
is') -> t
-> [BacktrackStep]
-> t
-> Bool
-> ThreadId
-> [(t, Bool, ThreadId)]
-> [BacktrackStep]
go t
i' [BacktrackStep]
bs (t
i't -> t -> t
forall a. Num a => a -> a -> a
-t
i0t -> t -> t
forall a. Num a => a -> a -> a
-t
1) Bool
c' ThreadId
t' [(t, Bool, ThreadId)]
is'
        [] -> [BacktrackStep]
bs
    -- Otherwise just backtrack to everything runnable.
    | Bool
otherwise =
      let b' :: BacktrackStep
b' = BacktrackStep
b { bcktBacktracks = backtrackAll c b }
      in BacktrackStep
b' BacktrackStep -> [BacktrackStep] -> [BacktrackStep]
forall a. a -> [a] -> [a]
: case [(t, Bool, ThreadId)]
is of
        ((t
i',Bool
c',ThreadId
t'):[(t, Bool, ThreadId)]
is') -> t
-> [BacktrackStep]
-> t
-> Bool
-> ThreadId
-> [(t, Bool, ThreadId)]
-> [BacktrackStep]
go t
i' [BacktrackStep]
bs (t
i't -> t -> t
forall a. Num a => a -> a -> a
-t
i0t -> t -> t
forall a. Num a => a -> a -> a
-t
1) Bool
c' ThreadId
t' [(t, Bool, ThreadId)]
is'
        [] -> [BacktrackStep]
bs
  go t
i0 (BacktrackStep
b:[BacktrackStep]
bs) t
i Bool
c ThreadId
tid [(t, Bool, ThreadId)]
is = BacktrackStep
b BacktrackStep -> [BacktrackStep] -> [BacktrackStep]
forall a. a -> [a] -> [a]
: t
-> [BacktrackStep]
-> t
-> Bool
-> ThreadId
-> [(t, Bool, ThreadId)]
-> [BacktrackStep]
go t
i0 [BacktrackStep]
bs (t
it -> t -> t
forall a. Num a => a -> a -> a
-t
1) Bool
c ThreadId
tid [(t, Bool, ThreadId)]
is
  go t
_ [] t
_ Bool
_ ThreadId
_ [(t, Bool, ThreadId)]
_ = String -> [BacktrackStep]
forall a. HasCallStack => String -> a
fatal String
"ran out of schedule whilst backtracking!"

  -- Backtrack to a single thread
  backtrackTo :: ThreadId -> Bool -> BacktrackStep -> Map ThreadId Bool
backtrackTo ThreadId
tid Bool
c = ThreadId -> Bool -> Map ThreadId Bool -> Map ThreadId Bool
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert ThreadId
tid Bool
c (Map ThreadId Bool -> Map ThreadId Bool)
-> (BacktrackStep -> Map ThreadId Bool)
-> BacktrackStep
-> Map ThreadId Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BacktrackStep -> Map ThreadId Bool
bcktBacktracks

  -- Backtrack to all runnable threads
  backtrackAll :: b -> BacktrackStep -> Map ThreadId b
backtrackAll b
c = (Lookahead -> b) -> Map ThreadId Lookahead -> Map ThreadId b
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (b -> Lookahead -> b
forall a b. a -> b -> a
const b
c) (Map ThreadId Lookahead -> Map ThreadId b)
-> (BacktrackStep -> Map ThreadId Lookahead)
-> BacktrackStep
-> Map ThreadId b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BacktrackStep -> Map ThreadId Lookahead
bcktRunnable

-- | DPOR scheduler: takes a list of decisions, and maintains a trace
-- including the runnable threads, and the alternative choices allowed
-- by the bound-specific initialise function.
--
-- After the initial decisions are exhausted, this prefers choosing
-- the prior thread if it's (1) still runnable and (2) hasn't just
-- yielded. Furthermore, threads which /will/ yield are ignored in
-- preference of those which will not.
dporSched :: HasCallStack
  => Bool
  -- ^ True if all IO is thread safe.
  -> IncrementalBoundFunc k
  -- ^ Bound function: returns true if that schedule prefix terminated
  -- with the lookahead decision fits within the bound.
  -> Scheduler (DPORSchedState k)
dporSched :: forall k.
HasCallStack =>
Bool -> IncrementalBoundFunc k -> Scheduler (DPORSchedState k)
dporSched Bool
safeIO IncrementalBoundFunc k
boundf = (Maybe (ThreadId, ThreadAction)
 -> NonEmpty (ThreadId, Lookahead)
 -> ConcurrencyState
 -> DPORSchedState k
 -> (Maybe ThreadId, DPORSchedState k))
-> Scheduler (DPORSchedState k)
forall state.
(Maybe (ThreadId, ThreadAction)
 -> NonEmpty (ThreadId, Lookahead)
 -> ConcurrencyState
 -> state
 -> (Maybe ThreadId, state))
-> Scheduler state
Scheduler ((Maybe (ThreadId, ThreadAction)
  -> NonEmpty (ThreadId, Lookahead)
  -> ConcurrencyState
  -> DPORSchedState k
  -> (Maybe ThreadId, DPORSchedState k))
 -> Scheduler (DPORSchedState k))
-> (Maybe (ThreadId, ThreadAction)
    -> NonEmpty (ThreadId, Lookahead)
    -> ConcurrencyState
    -> DPORSchedState k
    -> (Maybe ThreadId, DPORSchedState k))
-> Scheduler (DPORSchedState k)
forall a b. (a -> b) -> a -> b
$ \Maybe (ThreadId, ThreadAction)
prior NonEmpty (ThreadId, Lookahead)
threads ConcurrencyState
cstate DPORSchedState k
s ->
  let
    -- The next scheduler state
    nextState :: [ThreadId] -> DPORSchedState k
nextState [ThreadId]
rest = DPORSchedState k
s
      { schedBPoints  = schedBPoints s |> (restrictToBound fst threads', rest)
      -- we only update this after using the current value; so in
      -- effect this field is the depstate *before* the action which
      -- just happened, we need this because we need to know if the
      -- prior action (in the state we did it from) is dependent with
      -- anything in the sleep set.
      , schedCState = cstate
      }

    -- Pick a new thread to run, not considering bounds. Choose the
    -- current thread if available and it hasn't just yielded,
    -- otherwise add all runnable threads.
    initialise :: [ThreadId]
initialise = [ThreadId] -> [ThreadId]
tryDaemons ([ThreadId] -> [ThreadId])
-> ([ThreadId] -> [ThreadId]) -> [ThreadId] -> [ThreadId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ThreadId] -> [ThreadId]
yieldsToEnd ([ThreadId] -> [ThreadId]) -> [ThreadId] -> [ThreadId]
forall a b. (a -> b) -> a -> b
$ case Maybe (ThreadId, ThreadAction)
prior of
      Just (ThreadId
tid, ThreadAction
act)
        | Bool -> Bool
not (ThreadAction -> Bool
didYield ThreadAction
act) Bool -> Bool -> Bool
&& ThreadId
tid ThreadId -> [ThreadId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [ThreadId]
tids Bool -> Bool -> Bool
&& ThreadId -> Bool
isInBound ThreadId
tid -> [ThreadId
tid]
      Maybe (ThreadId, ThreadAction)
_ -> [ThreadId]
tids

    -- If one of the chosen actions will kill the computation, and
    -- there are daemon threads, try them instead.
    --
    -- This is necessary if the killing action is NOT dependent with
    -- every other action, according to the dependency function. This
    -- is, strictly speaking, wrong; an action that kills another
    -- thread is definitely dependent with everything in that
    -- thread. HOWEVER, implementing it that way leads to an explosion
    -- of schedules tried. Really, all that needs to happen is for the
    -- thread-that-would-be-killed to be executed fully ONCE, and then
    -- the normal dependency mechanism will identify any other
    -- backtracking points that should be tried. This is achieved by
    -- adding every thread that would be killed to the to-do list.
    -- Furthermore, these threads MUST be ahead of the killing thread,
    -- or the killing thread will end up in the sleep set and so the
    -- killing action not performed. This is, again, because of the
    -- lack of the dependency messing things up in the name of
    -- performance.
    --
    -- See commits a056f54 and 8554ce9, and my 4th June comment in
    -- issue #52.
    tryDaemons :: [ThreadId] -> [ThreadId]
tryDaemons [ThreadId]
ts
      | (ThreadId -> Bool) -> [ThreadId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ThreadId -> Bool
doesKill [ThreadId]
ts = case (ThreadId -> Bool) -> [ThreadId] -> ([ThreadId], [ThreadId])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ThreadId -> Bool
doesKill [ThreadId]
tids of
          ([ThreadId]
kills, [ThreadId]
nokills) -> [ThreadId]
nokills [ThreadId] -> [ThreadId] -> [ThreadId]
forall a. [a] -> [a] -> [a]
++ [ThreadId]
kills
      | Bool
otherwise = [ThreadId]
ts
    doesKill :: ThreadId -> Bool
doesKill ThreadId
t = ThreadId -> Lookahead -> Bool
killsDaemons ThreadId
t (ThreadId -> Lookahead
action ThreadId
t)

    -- Restrict the possible decisions to those in the bound.
    restrictToBound :: (a -> ThreadId) -> [a] -> [a]
restrictToBound a -> ThreadId
f = (a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (ThreadId -> Bool
isInBound (ThreadId -> Bool) -> (a -> ThreadId) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ThreadId
f)
    isInBound :: ThreadId -> Bool
isInBound ThreadId
t = Maybe k -> Bool
forall a. Maybe a -> Bool
isJust (Maybe k -> Bool) -> Maybe k -> Bool
forall a b. (a -> b) -> a -> b
$ IncrementalBoundFunc k
boundf (DPORSchedState k -> Maybe k
forall k. DPORSchedState k -> Maybe k
schedBState DPORSchedState k
s) Maybe (ThreadId, ThreadAction)
prior (ThreadId -> Decision
decision ThreadId
t, ThreadId -> Lookahead
action ThreadId
t)

    -- Move the threads which will immediately yield to the end of the list
    yieldsToEnd :: [ThreadId] -> [ThreadId]
yieldsToEnd [ThreadId]
ts = case (ThreadId -> Bool) -> [ThreadId] -> ([ThreadId], [ThreadId])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Lookahead -> Bool
willYield (Lookahead -> Bool) -> (ThreadId -> Lookahead) -> ThreadId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ThreadId -> Lookahead
action) [ThreadId]
ts of
      ([ThreadId]
yields, [ThreadId]
noyields) -> [ThreadId]
noyields [ThreadId] -> [ThreadId] -> [ThreadId]
forall a. [a] -> [a] -> [a]
++ [ThreadId]
yields

    -- Get the decision that will lead to a thread being scheduled.
    decision :: ThreadId -> Decision
decision = Maybe ThreadId -> Set ThreadId -> ThreadId -> Decision
forall (f :: * -> *).
Foldable f =>
Maybe ThreadId -> f ThreadId -> ThreadId -> Decision
decisionOf ((ThreadId, ThreadAction) -> ThreadId
forall a b. (a, b) -> a
fst ((ThreadId, ThreadAction) -> ThreadId)
-> Maybe (ThreadId, ThreadAction) -> Maybe ThreadId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (ThreadId, ThreadAction)
prior) ([ThreadId] -> Set ThreadId
forall a. Ord a => [a] -> Set a
S.fromList [ThreadId]
tids)

    -- Get the action of a thread
    action :: ThreadId -> Lookahead
action ThreadId
t = Maybe Lookahead -> Lookahead
forall a. HasCallStack => Maybe a -> a
efromJust (ThreadId -> [(ThreadId, Lookahead)] -> Maybe Lookahead
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup ThreadId
t [(ThreadId, Lookahead)]
threads')

    -- The runnable thread IDs
    tids :: [ThreadId]
tids = ((ThreadId, Lookahead) -> ThreadId)
-> [(ThreadId, Lookahead)] -> [ThreadId]
forall a b. (a -> b) -> [a] -> [b]
map (ThreadId, Lookahead) -> ThreadId
forall a b. (a, b) -> a
fst [(ThreadId, Lookahead)]
threads'

    -- The runnable threads as a normal list.
    threads' :: [(ThreadId, Lookahead)]
threads' = NonEmpty (ThreadId, Lookahead) -> [(ThreadId, Lookahead)]
forall a. NonEmpty a -> [a]
toList NonEmpty (ThreadId, Lookahead)
threads
  in case DPORSchedState k -> [ThreadId]
forall k. DPORSchedState k -> [ThreadId]
schedPrefix DPORSchedState k
s of
    -- If there is a decision available, make it
    (ThreadId
t:[ThreadId]
ts) ->
      let bstate' :: Maybe k
bstate' = IncrementalBoundFunc k
boundf (DPORSchedState k -> Maybe k
forall k. DPORSchedState k -> Maybe k
schedBState DPORSchedState k
s) Maybe (ThreadId, ThreadAction)
prior (ThreadId -> Decision
decision ThreadId
t, ThreadId -> Lookahead
action ThreadId
t)
      in (ThreadId -> Maybe ThreadId
forall a. a -> Maybe a
Just ThreadId
t, ([ThreadId] -> DPORSchedState k
nextState []) { schedPrefix = ts, schedBState = bstate' })

    -- Otherwise query the initialise function for a list of possible
    -- choices, filter out anything in the sleep set, and make one of
    -- them arbitrarily (recording the others).
    [] ->
      let choices :: [ThreadId]
choices  = (ThreadId -> ThreadId) -> [ThreadId] -> [ThreadId]
forall {a}. (a -> ThreadId) -> [a] -> [a]
restrictToBound ThreadId -> ThreadId
forall a. a -> a
id [ThreadId]
initialise
          checkDep :: ThreadId -> ThreadAction -> Bool
checkDep ThreadId
t ThreadAction
a = case Maybe (ThreadId, ThreadAction)
prior of
            Just (ThreadId
tid, ThreadAction
act) -> Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
dependent Bool
safeIO (DPORSchedState k -> ConcurrencyState
forall k. DPORSchedState k -> ConcurrencyState
schedCState DPORSchedState k
s) ThreadId
tid ThreadAction
act ThreadId
t ThreadAction
a
            Maybe (ThreadId, ThreadAction)
Nothing -> Bool
False
          ssleep' :: Map ThreadId ThreadAction
ssleep'  = (ThreadId -> ThreadAction -> Bool)
-> Map ThreadId ThreadAction -> Map ThreadId ThreadAction
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey (\ThreadId
t ThreadAction
a -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ThreadId -> ThreadAction -> Bool
checkDep ThreadId
t ThreadAction
a) (Map ThreadId ThreadAction -> Map ThreadId ThreadAction)
-> Map ThreadId ThreadAction -> Map ThreadId ThreadAction
forall a b. (a -> b) -> a -> b
$ DPORSchedState k -> Map ThreadId ThreadAction
forall k. DPORSchedState k -> Map ThreadId ThreadAction
schedSleep DPORSchedState k
s
          choices' :: [ThreadId]
choices' = (ThreadId -> Bool) -> [ThreadId] -> [ThreadId]
forall a. (a -> Bool) -> [a] -> [a]
filter (ThreadId -> [ThreadId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Map ThreadId ThreadAction -> [ThreadId]
forall k a. Map k a -> [k]
M.keys Map ThreadId ThreadAction
ssleep') [ThreadId]
choices
          signore' :: Bool
signore' = Bool -> Bool
not ([ThreadId] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ThreadId]
choices) Bool -> Bool -> Bool
&& (ThreadId -> Bool) -> [ThreadId] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (ThreadId -> [ThreadId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map ThreadId ThreadAction -> [ThreadId]
forall k a. Map k a -> [k]
M.keys Map ThreadId ThreadAction
ssleep') [ThreadId]
choices
          sbkill' :: Bool
sbkill'  = Bool -> Bool
not ([ThreadId] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ThreadId]
initialise) Bool -> Bool -> Bool
&& [ThreadId] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ThreadId]
choices
      in case [ThreadId]
choices' of
        (ThreadId
nextTid:[ThreadId]
rest) ->
          let bstate' :: Maybe k
bstate' = IncrementalBoundFunc k
boundf (DPORSchedState k -> Maybe k
forall k. DPORSchedState k -> Maybe k
schedBState DPORSchedState k
s) Maybe (ThreadId, ThreadAction)
prior (ThreadId -> Decision
decision ThreadId
nextTid, ThreadId -> Lookahead
action ThreadId
nextTid)
          in (ThreadId -> Maybe ThreadId
forall a. a -> Maybe a
Just ThreadId
nextTid, ([ThreadId] -> DPORSchedState k
nextState [ThreadId]
rest) { schedSleep = ssleep', schedBState = bstate' })
        [] ->
          (Maybe ThreadId
forall a. Maybe a
Nothing, ([ThreadId] -> DPORSchedState k
nextState []) { schedIgnore = signore', schedBoundKill = sbkill', schedBState = Nothing })

-------------------------------------------------------------------------------
-- * Dependency function

-- | Check if two actions commute.
--
-- This implements a stronger check that @not (dependent ...)@, as it
-- handles some cases which 'dependent' doesn't need to care about.
independent :: Bool -> ConcurrencyState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
independent :: Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
independent Bool
safeIO ConcurrencyState
ds ThreadId
t1 ThreadAction
a1 ThreadId
t2 ThreadAction
a2
    | ThreadId
t1 ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
t2 = Bool
False
    | ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
forall {p}. p -> ThreadAction -> ThreadId -> ThreadAction -> Bool
check ThreadId
t1 ThreadAction
a1 ThreadId
t2 ThreadAction
a2 = Bool
False
    | ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
forall {p}. p -> ThreadAction -> ThreadId -> ThreadAction -> Bool
check ThreadId
t2 ThreadAction
a2 ThreadId
t1 ThreadAction
a1 = Bool
False
    | Bool
otherwise = Bool -> Bool
not (Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
dependent Bool
safeIO ConcurrencyState
ds ThreadId
t1 ThreadAction
a1 ThreadId
t2 ThreadAction
a2)
  where
    -- can't re-order any action of a thread with the fork which
    -- created it.
    check :: p -> ThreadAction -> ThreadId -> ThreadAction -> Bool
check p
_ (Fork ThreadId
t) ThreadId
tid ThreadAction
_ | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid = Bool
True
    check p
_ (ForkOS ThreadId
t) ThreadId
tid ThreadAction
_ | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid = Bool
True
    -- because we can't easily tell if this will terminate the other
    -- thread, we just can't re-order asynchronous exceptions at all
    -- :(
    --
    -- See #191 / #190
    check p
_ (ThrowTo ThreadId
t Maybe MaskingState
_) ThreadId
tid ThreadAction
_ | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid = Bool
True
    check p
_ (BlockedThrowTo ThreadId
t) ThreadId
tid ThreadAction
_ | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
tid = Bool
True
    -- can't re-order an unsynchronised write with something which synchronises that IORef.
    check p
_ (ThreadAction -> ActionType
simplifyAction -> UnsynchronisedWrite IORefId
r) ThreadId
_ (ThreadAction -> ActionType
simplifyAction -> ActionType
a) | ActionType -> IORefId -> Bool
synchronises ActionType
a IORefId
r = Bool
True
    check p
_ ThreadAction
_ ThreadId
_ ThreadAction
_ = Bool
False

-- | Check if an action is dependent on another.
--
-- This is basically the same as 'dependent'', but can make use of the
-- additional information in a 'ThreadAction' to make better decisions
-- in a few cases.
dependent :: Bool -> ConcurrencyState -> ThreadId -> ThreadAction -> ThreadId -> ThreadAction -> Bool
dependent :: Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> ThreadAction
-> Bool
dependent Bool
safeIO ConcurrencyState
ds ThreadId
t1 ThreadAction
a1 ThreadId
t2 ThreadAction
a2 = case (ThreadAction
a1, ThreadAction
a2) of
  -- When masked interruptible, a thread can only be interrupted when
  -- actually blocked. 'dependent'' has to assume that all
  -- potentially-blocking operations can block, and so is more
  -- pessimistic in this case.
  (ThrowTo ThreadId
t Maybe MaskingState
_, ThrowTo ThreadId
u Maybe MaskingState
_)
    | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
t2 Bool -> Bool -> Bool
&& ThreadId
u ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
t1 -> ConcurrencyState -> ThreadId -> ThreadAction -> Bool
canInterrupt ConcurrencyState
ds ThreadId
t1 ThreadAction
a1 Bool -> Bool -> Bool
|| ConcurrencyState -> ThreadId -> ThreadAction -> Bool
canInterrupt ConcurrencyState
ds ThreadId
t2 ThreadAction
a2
  (ThrowTo ThreadId
t Maybe MaskingState
_, ThreadAction
_) | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
t2 -> ConcurrencyState -> ThreadId -> ThreadAction -> Bool
canInterrupt ConcurrencyState
ds ThreadId
t2 ThreadAction
a2 Bool -> Bool -> Bool
&& ThreadAction
a2 ThreadAction -> ThreadAction -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadAction
Stop
  (ThreadAction
_, ThrowTo ThreadId
t Maybe MaskingState
_) | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
t1 -> ConcurrencyState -> ThreadId -> ThreadAction -> Bool
canInterrupt ConcurrencyState
ds ThreadId
t1 ThreadAction
a1 Bool -> Bool -> Bool
&& ThreadAction
a1 ThreadAction -> ThreadAction -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadAction
Stop

  -- Dependency of STM transactions can be /greatly/ improved here, as
  -- the 'Lookahead' does not know which @TVar@s will be touched, and
  -- so has to assume all transactions are dependent.
  (STM [TAction]
_ [ThreadId]
_, STM [TAction]
_ [ThreadId]
_)       -> Bool
checkSTM
  (STM [TAction]
_ [ThreadId]
_, BlockedSTM [TAction]
_)  -> Bool
checkSTM
  (STM [TAction]
_ [ThreadId]
_, ThrownSTM [TAction]
_ Maybe MaskingState
_) -> Bool
checkSTM
  (BlockedSTM [TAction]
_, STM [TAction]
_ [ThreadId]
_)       -> Bool
checkSTM
  (BlockedSTM [TAction]
_, BlockedSTM [TAction]
_)  -> Bool
checkSTM
  (BlockedSTM [TAction]
_, ThrownSTM [TAction]
_ Maybe MaskingState
_) -> Bool
checkSTM
  (ThrownSTM [TAction]
_ Maybe MaskingState
_, STM [TAction]
_ [ThreadId]
_)       -> Bool
checkSTM
  (ThrownSTM [TAction]
_ Maybe MaskingState
_, BlockedSTM [TAction]
_)  -> Bool
checkSTM
  (ThrownSTM [TAction]
_ Maybe MaskingState
_, ThrownSTM [TAction]
_ Maybe MaskingState
_) -> Bool
checkSTM

  (ThreadAction, ThreadAction)
_ -> Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> Lookahead
-> Bool
dependent' Bool
safeIO ConcurrencyState
ds ThreadId
t1 ThreadAction
a1 ThreadId
t2 (ThreadAction -> Lookahead
rewind ThreadAction
a2)
    Bool -> Bool -> Bool
&& Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> Lookahead
-> Bool
dependent' Bool
safeIO ConcurrencyState
ds ThreadId
t2 ThreadAction
a2 ThreadId
t1 (ThreadAction -> Lookahead
rewind ThreadAction
a1)

  where
    -- STM actions A and B are dependent if A wrote to anything B
    -- touched, or vice versa.
    checkSTM :: Bool
checkSTM = ThreadAction -> ThreadAction -> Bool
checkSTM' ThreadAction
a1 ThreadAction
a2 Bool -> Bool -> Bool
|| ThreadAction -> ThreadAction -> Bool
checkSTM' ThreadAction
a2 ThreadAction
a1
    checkSTM' :: ThreadAction -> ThreadAction -> Bool
checkSTM' ThreadAction
a ThreadAction
b = Bool -> Bool
not (Bool -> Bool) -> (Set TVarId -> Bool) -> Set TVarId -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TVarId -> Bool
forall a. Set a -> Bool
S.null (Set TVarId -> Bool) -> Set TVarId -> Bool
forall a b. (a -> b) -> a -> b
$ ThreadAction -> Set TVarId
tvarsWritten ThreadAction
a Set TVarId -> Set TVarId -> Set TVarId
forall a. Ord a => Set a -> Set a -> Set a
`S.intersection` ThreadAction -> Set TVarId
tvarsOf ThreadAction
b

-- | Variant of 'dependent' to handle 'Lookahead'.
--
-- Termination of the initial thread is handled specially in the DPOR
-- implementation.
dependent' :: Bool -> ConcurrencyState -> ThreadId -> ThreadAction -> ThreadId -> Lookahead -> Bool
dependent' :: Bool
-> ConcurrencyState
-> ThreadId
-> ThreadAction
-> ThreadId
-> Lookahead
-> Bool
dependent' Bool
safeIO ConcurrencyState
ds ThreadId
t1 ThreadAction
a1 ThreadId
t2 Lookahead
l2 = case (ThreadAction
a1, Lookahead
l2) of
  -- Worst-case assumption: all IO is dependent.
  (ThreadAction
LiftIO, Lookahead
WillLiftIO) -> Bool -> Bool
not Bool
safeIO

  -- Throwing an exception is only dependent with actions in that
  -- thread and if the actions can be interrupted. We can also
  -- slightly improve on that by not considering interrupting the
  -- normal termination of a thread: it doesn't make a difference.
  (ThrowTo ThreadId
t Maybe MaskingState
_, WillThrowTo ThreadId
u)
    | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
t2 Bool -> Bool -> Bool
&& ThreadId
u ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
t1 -> ConcurrencyState -> ThreadId -> ThreadAction -> Bool
canInterrupt ConcurrencyState
ds ThreadId
t1 ThreadAction
a1 Bool -> Bool -> Bool
|| ConcurrencyState -> ThreadId -> Lookahead -> Bool
canInterruptL ConcurrencyState
ds ThreadId
t2 Lookahead
l2
  (ThrowTo ThreadId
t Maybe MaskingState
_, Lookahead
_)   | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
t2 -> ConcurrencyState -> ThreadId -> Lookahead -> Bool
canInterruptL ConcurrencyState
ds ThreadId
t2 Lookahead
l2 Bool -> Bool -> Bool
&& Lookahead
l2 Lookahead -> Lookahead -> Bool
forall a. Eq a => a -> a -> Bool
/= Lookahead
WillStop
  (ThreadAction
_, WillThrowTo ThreadId
t) | ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
t1 -> ConcurrencyState -> ThreadId -> ThreadAction -> Bool
canInterrupt  ConcurrencyState
ds ThreadId
t1 ThreadAction
a1 Bool -> Bool -> Bool
&& ThreadAction
a1 ThreadAction -> ThreadAction -> Bool
forall a. Eq a => a -> a -> Bool
/= ThreadAction
Stop

  -- Another worst-case: assume all STM is dependent.
  (STM [TAction]
_ [ThreadId]
_, Lookahead
WillSTM) -> Bool
True
  (BlockedSTM [TAction]
_, Lookahead
WillSTM) -> Bool
True
  (ThrownSTM [TAction]
_ Maybe MaskingState
_, Lookahead
WillSTM) -> Bool
True

  -- the number of capabilities is essentially a global shared
  -- variable
  (GetNumCapabilities Int
_, WillSetNumCapabilities Int
_) -> Bool
True
  (SetNumCapabilities Int
_, Lookahead
WillGetNumCapabilities)   -> Bool
True
  (SetNumCapabilities Int
_, WillSetNumCapabilities Int
_) -> Bool
True

  (ThreadAction, Lookahead)
_ -> ConcurrencyState -> ActionType -> ActionType -> Bool
dependentActions ConcurrencyState
ds (ThreadAction -> ActionType
simplifyAction ThreadAction
a1) (Lookahead -> ActionType
simplifyLookahead Lookahead
l2)

-- | Check if two 'ActionType's are dependent. Note that this is not
-- sufficient to know if two 'ThreadAction's are dependent, without
-- being so great an over-approximation as to be useless!
dependentActions :: ConcurrencyState -> ActionType -> ActionType -> Bool
dependentActions :: ConcurrencyState -> ActionType -> ActionType -> Bool
dependentActions ConcurrencyState
ds ActionType
a1 ActionType
a2 = case (ActionType
a1, ActionType
a2) of
  (UnsynchronisedRead IORefId
_, UnsynchronisedRead IORefId
_) -> Bool
False

  -- Unsynchronised writes and synchronisation where the buffer is not
  -- empty.
  --
  -- See [RMMVerification], lemma 5.25.
  (UnsynchronisedWrite IORefId
r1, PartiallySynchronisedCommit IORefId
r2) | IORefId
r1 IORefId -> IORefId -> Bool
forall a. Eq a => a -> a -> Bool
== IORefId
r2 Bool -> Bool -> Bool
&& ConcurrencyState -> IORefId -> Bool
isBuffered ConcurrencyState
ds IORefId
r1 -> Bool
False
  (PartiallySynchronisedCommit IORefId
r1, UnsynchronisedWrite IORefId
r2) | IORefId
r1 IORefId -> IORefId -> Bool
forall a. Eq a => a -> a -> Bool
== IORefId
r2 Bool -> Bool -> Bool
&& ConcurrencyState -> IORefId -> Bool
isBuffered ConcurrencyState
ds IORefId
r1 -> Bool
False

  -- Unsynchronised reads where a memory barrier would flush a
  -- buffered write
  (UnsynchronisedRead IORefId
r1, ActionType
_) | ActionType -> Bool
isBarrier ActionType
a2 Bool -> Bool -> Bool
&& ConcurrencyState -> IORefId -> Bool
isBuffered ConcurrencyState
ds IORefId
r1 -> Bool
True
  (ActionType
_, UnsynchronisedRead IORefId
r2) | ActionType -> Bool
isBarrier ActionType
a1 Bool -> Bool -> Bool
&& ConcurrencyState -> IORefId -> Bool
isBuffered ConcurrencyState
ds IORefId
r2 -> Bool
True

  -- Commits and memory barriers must be dependent, as memory barriers
  -- (currently) flush in a consistent order.  Alternative orders need
  -- to be explored as well.  Perhaps a better implementation of
  -- memory barriers would just block every non-commit thread while
  -- any buffer is nonempty.
  (PartiallySynchronisedCommit IORefId
r1, ActionType
_) | ActionType -> IORefId -> Bool
synchronises ActionType
a2 IORefId
r1 -> Bool
True
  (ActionType
_, PartiallySynchronisedCommit IORefId
r2) | ActionType -> IORefId -> Bool
synchronises ActionType
a1 IORefId
r2 -> Bool
True

  -- Two @MVar@ puts are dependent if they're to the same empty
  -- @MVar@, and two takes are dependent if they're to the same full
  -- @MVar@.
  (SynchronisedWrite MVarId
v1, SynchronisedWrite MVarId
v2) | MVarId
v1 MVarId -> MVarId -> Bool
forall a. Eq a => a -> a -> Bool
== MVarId
v2 -> Bool -> Bool
not (ConcurrencyState -> MVarId -> Bool
isFull ConcurrencyState
ds MVarId
v1)
  (SynchronisedRead  MVarId
v1, SynchronisedRead  MVarId
v2) | MVarId
v1 MVarId -> MVarId -> Bool
forall a. Eq a => a -> a -> Bool
== MVarId
v2 -> ConcurrencyState -> MVarId -> Bool
isFull ConcurrencyState
ds MVarId
v1
  (SynchronisedWrite MVarId
v1, SynchronisedRead  MVarId
v2) | MVarId
v1 MVarId -> MVarId -> Bool
forall a. Eq a => a -> a -> Bool
== MVarId
v2 -> Bool
True
  (SynchronisedRead  MVarId
v1, SynchronisedWrite MVarId
v2) | MVarId
v1 MVarId -> MVarId -> Bool
forall a. Eq a => a -> a -> Bool
== MVarId
v2 -> Bool
True

  (ActionType
_, ActionType
_) -> Bool -> (IORefId -> Bool) -> Maybe IORefId -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (\IORefId
r -> IORefId -> Maybe IORefId
forall a. a -> Maybe a
Just IORefId
r Maybe IORefId -> Maybe IORefId -> Bool
forall a. Eq a => a -> a -> Bool
== ActionType -> Maybe IORefId
iorefOf ActionType
a2) (ActionType -> Maybe IORefId
iorefOf ActionType
a1)

-------------------------------------------------------------------------------
-- * Utilities

-- | Check if a thread yielded.
didYield :: ThreadAction -> Bool
didYield :: ThreadAction -> Bool
didYield ThreadAction
Yield = Bool
True
didYield (ThreadDelay Int
_) = Bool
True
didYield ThreadAction
_ = Bool
False

-- | Check if a thread will yield.
willYield :: Lookahead -> Bool
willYield :: Lookahead -> Bool
willYield Lookahead
WillYield = Bool
True
willYield (WillThreadDelay Int
_) = Bool
True
willYield Lookahead
_ = Bool
False

-- | Check if an action will kill daemon threads.
killsDaemons :: ThreadId -> Lookahead -> Bool
killsDaemons :: ThreadId -> Lookahead -> Bool
killsDaemons ThreadId
t Lookahead
WillStop = ThreadId
t ThreadId -> ThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== ThreadId
initialThread
killsDaemons ThreadId
_ Lookahead
_ = Bool
False