{-# LANGUAGE NamedFieldPuns #-}
module Control.Monad.IOSimPOR.Types
  ( -- * Effects
    Effect (..)
  , readEffects
  , writeEffects
  , forkEffect
  , throwToEffect
  , wakeupEffects
  , onlyReadEffect
  , racingEffects
  , ppEffect
    -- * Schedules
  , ScheduleControl (..)
  , isDefaultSchedule
  , ScheduleMod (..)
    -- * Steps
  , StepId
  , ppStepId
  , Step (..)
  , StepInfo (..)
    -- * Races
  , Races (..)
  , noRaces
  ) where

import qualified Data.List as List
import           Data.Set (Set)
import qualified Data.Set as Set

import           Control.Monad.IOSim.CommonTypes

--
-- Effects
--

-- | An `Effect` aggregates effects performed by a thread in a given
-- execution step.  Only used by *IOSimPOR*.
--
data Effect = Effect {
    Effect -> Set TVarId
effectReads  :: !(Set TVarId),
    Effect -> Set TVarId
effectWrites :: !(Set TVarId),
    Effect -> Set IOSimThreadId
effectForks  :: !(Set IOSimThreadId),
    Effect -> [IOSimThreadId]
effectThrows :: ![IOSimThreadId],
    Effect -> Set IOSimThreadId
effectWakeup :: !(Set IOSimThreadId)
  }
  deriving (Int -> Effect -> ShowS
[Effect] -> ShowS
Effect -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Effect] -> ShowS
$cshowList :: [Effect] -> ShowS
show :: Effect -> String
$cshow :: Effect -> String
showsPrec :: Int -> Effect -> ShowS
$cshowsPrec :: Int -> Effect -> ShowS
Show, Effect -> Effect -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Effect -> Effect -> Bool
$c/= :: Effect -> Effect -> Bool
== :: Effect -> Effect -> Bool
$c== :: Effect -> Effect -> Bool
Eq)

ppEffect :: Effect -> String
ppEffect :: Effect -> String
ppEffect Effect { Set TVarId
effectReads :: Set TVarId
effectReads :: Effect -> Set TVarId
effectReads, Set TVarId
effectWrites :: Set TVarId
effectWrites :: Effect -> Set TVarId
effectWrites, Set IOSimThreadId
effectForks :: Set IOSimThreadId
effectForks :: Effect -> Set IOSimThreadId
effectForks, [IOSimThreadId]
effectThrows :: [IOSimThreadId]
effectThrows :: Effect -> [IOSimThreadId]
effectThrows, Set IOSimThreadId
effectWakeup :: Set IOSimThreadId
effectWakeup :: Effect -> Set IOSimThreadId
effectWakeup } =
  String
"Effect { " forall a. [a] -> [a] -> [a]
++
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (forall a. a -> [a] -> [a]
List.intersperse String
", " forall a b. (a -> b) -> a -> b
$
           [ String
"reads = "  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set TVarId
effectReads  | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set TVarId
effectReads)  ]
        forall a. [a] -> [a] -> [a]
++ [ String
"writes = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Set TVarId
effectWrites | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set TVarId
effectWrites) ]
        forall a. [a] -> [a] -> [a]
++ [ String
"forks = "  forall a. [a] -> [a] -> [a]
++ forall a. (a -> String) -> [a] -> String
ppList IOSimThreadId -> String
ppIOSimThreadId (forall a. Set a -> [a]
Set.toList Set IOSimThreadId
effectForks)  | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set IOSimThreadId
effectForks)  ]
        forall a. [a] -> [a] -> [a]
++ [ String
"throws = " forall a. [a] -> [a] -> [a]
++ forall a. (a -> String) -> [a] -> String
ppList IOSimThreadId -> String
ppIOSimThreadId             [IOSimThreadId]
effectThrows  | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IOSimThreadId]
effectThrows) ]
        forall a. [a] -> [a] -> [a]
++ [ String
"wakeup = " forall a. [a] -> [a] -> [a]
++ forall a. (a -> String) -> [a] -> String
ppList IOSimThreadId -> String
ppIOSimThreadId (forall a. Set a -> [a]
Set.toList Set IOSimThreadId
effectWakeup) | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set IOSimThreadId
effectWakeup) ])
        forall a. [a] -> [a] -> [a]
++ String
" }"


instance Semigroup Effect where
  Effect Set TVarId
r Set TVarId
w Set IOSimThreadId
s [IOSimThreadId]
ts Set IOSimThreadId
wu <> :: Effect -> Effect -> Effect
<> Effect Set TVarId
r' Set TVarId
w' Set IOSimThreadId
s' [IOSimThreadId]
ts' Set IOSimThreadId
wu' =
    Set TVarId
-> Set TVarId
-> Set IOSimThreadId
-> [IOSimThreadId]
-> Set IOSimThreadId
-> Effect
Effect (Set TVarId
r forall a. Semigroup a => a -> a -> a
<> Set TVarId
r') (Set TVarId
w forall a. Semigroup a => a -> a -> a
<> Set TVarId
w') (Set IOSimThreadId
s forall a. Semigroup a => a -> a -> a
<> Set IOSimThreadId
s') ([IOSimThreadId]
ts forall a. [a] -> [a] -> [a]
++ [IOSimThreadId]
ts') (Set IOSimThreadId
wu forall a. Semigroup a => a -> a -> a
<> Set IOSimThreadId
wu')

instance Monoid Effect where
  mempty :: Effect
mempty = Set TVarId
-> Set TVarId
-> Set IOSimThreadId
-> [IOSimThreadId]
-> Set IOSimThreadId
-> Effect
Effect forall a. Set a
Set.empty forall a. Set a
Set.empty forall a. Set a
Set.empty [] forall a. Set a
Set.empty

--
-- Effect smart constructors
--

-- readEffect :: SomeTVar s -> Effect
-- readEffect r = mempty{effectReads = Set.singleton $ someTvarId r }

readEffects :: [SomeTVar s] -> Effect
readEffects :: forall s. [SomeTVar s] -> Effect
readEffects [SomeTVar s]
rs = forall a. Monoid a => a
mempty{effectReads :: Set TVarId
effectReads = forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall s. SomeTVar s -> TVarId
someTvarId [SomeTVar s]
rs)}

-- writeEffect :: SomeTVar s -> Effect
-- writeEffect r = mempty{effectWrites = Set.singleton $ someTvarId r }

writeEffects :: [SomeTVar s] -> Effect
writeEffects :: forall s. [SomeTVar s] -> Effect
writeEffects [SomeTVar s]
rs = forall a. Monoid a => a
mempty{effectWrites :: Set TVarId
effectWrites = forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall s. SomeTVar s -> TVarId
someTvarId [SomeTVar s]
rs)}

forkEffect :: IOSimThreadId -> Effect
forkEffect :: IOSimThreadId -> Effect
forkEffect IOSimThreadId
tid = forall a. Monoid a => a
mempty{effectForks :: Set IOSimThreadId
effectForks = forall a. a -> Set a
Set.singleton IOSimThreadId
tid}

throwToEffect :: IOSimThreadId -> Effect
throwToEffect :: IOSimThreadId -> Effect
throwToEffect IOSimThreadId
tid = forall a. Monoid a => a
mempty{ effectThrows :: [IOSimThreadId]
effectThrows = [IOSimThreadId
tid] }

wakeupEffects :: [IOSimThreadId] -> Effect
wakeupEffects :: [IOSimThreadId] -> Effect
wakeupEffects [IOSimThreadId]
tids = forall a. Monoid a => a
mempty{effectWakeup :: Set IOSimThreadId
effectWakeup = forall a. Ord a => [a] -> Set a
Set.fromList [IOSimThreadId]
tids}

--
-- Utils
--

someTvarId :: SomeTVar s -> TVarId
someTvarId :: forall s. SomeTVar s -> TVarId
someTvarId (SomeTVar TVar s a
r) = forall s a. TVar s a -> TVarId
tvarId TVar s a
r

onlyReadEffect :: Effect -> Bool
onlyReadEffect :: Effect -> Bool
onlyReadEffect Effect
e = Effect
e { effectReads :: Set TVarId
effectReads = Effect -> Set TVarId
effectReads forall a. Monoid a => a
mempty } forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty

-- | Check if two effects race.  The two effects are assumed to come from
-- different threads, from steps which do not wake one another, see
-- `racingSteps`.
--
racingEffects :: Effect -> Effect -> Bool
racingEffects :: Effect -> Effect -> Bool
racingEffects Effect
e Effect
e' =

       -- both effects throw to the same threads
       Effect -> [IOSimThreadId]
effectThrows Effect
e forall a. Eq a => [a] -> [a] -> Bool
`intersectsL` Effect -> [IOSimThreadId]
effectThrows Effect
e'

       -- concurrent reads & writes of the same TVars
    Bool -> Bool -> Bool
|| Effect -> Set TVarId
effectReads  Effect
e forall a. Ord a => Set a -> Set a -> Bool
`intersects`  Effect -> Set TVarId
effectWrites Effect
e'
    Bool -> Bool -> Bool
|| Effect -> Set TVarId
effectWrites Effect
e forall a. Ord a => Set a -> Set a -> Bool
`intersects`  Effect -> Set TVarId
effectReads  Effect
e'

       -- concurrent writes to the same TVars
    Bool -> Bool -> Bool
|| Effect -> Set TVarId
effectWrites Effect
e forall a. Ord a => Set a -> Set a -> Bool
`intersects`  Effect -> Set TVarId
effectWrites Effect
e'

  where
    intersects :: Ord a => Set a -> Set a -> Bool
    intersects :: forall a. Ord a => Set a -> Set a -> Bool
intersects Set a
a Set a
b = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Set a
a forall a. Ord a => Set a -> Set a -> Bool
`Set.disjoint` Set a
b

    intersectsL :: Eq a => [a] -> [a] -> Bool
    intersectsL :: forall a. Eq a => [a] -> [a] -> Bool
intersectsL [a]
a [a]
b = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ [a]
a forall a. Eq a => [a] -> [a] -> [a]
`List.intersect` [a]
b


---
--- Schedules
---

-- | Modified execution schedule.
--
data ScheduleControl = ControlDefault
                     -- ^ default scheduling mode
                     | ControlAwait [ScheduleMod]
                     -- ^ if the current control is 'ControlAwait', the normal
                     -- scheduling will proceed, until the thread found in the
                     -- first 'ScheduleMod' reaches the given step.  At this
                     -- point the thread is put to sleep, until after all the
                     -- steps are followed.
                     | ControlFollow [StepId] [ScheduleMod]
                     -- ^ follow the steps then continue with schedule
                     -- modifications.  This control is set by 'followControl'
                     -- when 'controlTargets' returns true.
  deriving (ScheduleControl -> ScheduleControl -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScheduleControl -> ScheduleControl -> Bool
$c/= :: ScheduleControl -> ScheduleControl -> Bool
== :: ScheduleControl -> ScheduleControl -> Bool
$c== :: ScheduleControl -> ScheduleControl -> Bool
Eq, Eq ScheduleControl
ScheduleControl -> ScheduleControl -> Bool
ScheduleControl -> ScheduleControl -> Ordering
ScheduleControl -> ScheduleControl -> ScheduleControl
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ScheduleControl -> ScheduleControl -> ScheduleControl
$cmin :: ScheduleControl -> ScheduleControl -> ScheduleControl
max :: ScheduleControl -> ScheduleControl -> ScheduleControl
$cmax :: ScheduleControl -> ScheduleControl -> ScheduleControl
>= :: ScheduleControl -> ScheduleControl -> Bool
$c>= :: ScheduleControl -> ScheduleControl -> Bool
> :: ScheduleControl -> ScheduleControl -> Bool
$c> :: ScheduleControl -> ScheduleControl -> Bool
<= :: ScheduleControl -> ScheduleControl -> Bool
$c<= :: ScheduleControl -> ScheduleControl -> Bool
< :: ScheduleControl -> ScheduleControl -> Bool
$c< :: ScheduleControl -> ScheduleControl -> Bool
compare :: ScheduleControl -> ScheduleControl -> Ordering
$ccompare :: ScheduleControl -> ScheduleControl -> Ordering
Ord, Int -> ScheduleControl -> ShowS
[ScheduleControl] -> ShowS
ScheduleControl -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ScheduleControl] -> ShowS
$cshowList :: [ScheduleControl] -> ShowS
show :: ScheduleControl -> String
$cshow :: ScheduleControl -> String
showsPrec :: Int -> ScheduleControl -> ShowS
$cshowsPrec :: Int -> ScheduleControl -> ShowS
Show)


isDefaultSchedule :: ScheduleControl -> Bool
isDefaultSchedule :: ScheduleControl -> Bool
isDefaultSchedule ScheduleControl
ControlDefault        = Bool
True
isDefaultSchedule (ControlFollow [] []) = Bool
True
isDefaultSchedule ScheduleControl
_                     = Bool
False

-- | A schedule modification inserted at given execution step.
--
data ScheduleMod = ScheduleMod{
    -- | Step at which the 'ScheduleMod' is activated.
    ScheduleMod -> StepId
scheduleModTarget    :: StepId,
    -- | 'ScheduleControl' at the activation step.  It is needed by
    -- 'extendScheduleControl' when combining the discovered schedule with the
    -- initial one.
    ScheduleMod -> ScheduleControl
scheduleModControl   :: ScheduleControl,
    -- | Series of steps which are executed at the target step.  This *includes*
    -- the target step, not necessarily as the last step.
    ScheduleMod -> [StepId]
scheduleModInsertion :: [StepId]
  }
  deriving (ScheduleMod -> ScheduleMod -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScheduleMod -> ScheduleMod -> Bool
$c/= :: ScheduleMod -> ScheduleMod -> Bool
== :: ScheduleMod -> ScheduleMod -> Bool
$c== :: ScheduleMod -> ScheduleMod -> Bool
Eq, Eq ScheduleMod
ScheduleMod -> ScheduleMod -> Bool
ScheduleMod -> ScheduleMod -> Ordering
ScheduleMod -> ScheduleMod -> ScheduleMod
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ScheduleMod -> ScheduleMod -> ScheduleMod
$cmin :: ScheduleMod -> ScheduleMod -> ScheduleMod
max :: ScheduleMod -> ScheduleMod -> ScheduleMod
$cmax :: ScheduleMod -> ScheduleMod -> ScheduleMod
>= :: ScheduleMod -> ScheduleMod -> Bool
$c>= :: ScheduleMod -> ScheduleMod -> Bool
> :: ScheduleMod -> ScheduleMod -> Bool
$c> :: ScheduleMod -> ScheduleMod -> Bool
<= :: ScheduleMod -> ScheduleMod -> Bool
$c<= :: ScheduleMod -> ScheduleMod -> Bool
< :: ScheduleMod -> ScheduleMod -> Bool
$c< :: ScheduleMod -> ScheduleMod -> Bool
compare :: ScheduleMod -> ScheduleMod -> Ordering
$ccompare :: ScheduleMod -> ScheduleMod -> Ordering
Ord)


instance Show ScheduleMod where
  showsPrec :: Int -> ScheduleMod -> ShowS
showsPrec Int
d (ScheduleMod StepId
tgt ScheduleControl
ctrl [StepId]
insertion) =
    Bool -> ShowS -> ShowS
showParen (Int
dforall a. Ord a => a -> a -> Bool
>Int
10) forall a b. (a -> b) -> a -> b
$
      String -> ShowS
showString String
"ScheduleMod " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 StepId
tgt forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 ScheduleControl
ctrl forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      String -> ShowS
showString String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 [StepId]
insertion

--
-- Steps
--

data Step = Step {
    Step -> IOSimThreadId
stepThreadId :: !IOSimThreadId,
    Step -> Int
stepStep     :: !Int,
    Step -> Effect
stepEffect   :: !Effect,
    Step -> VectorClock
stepVClock   :: !VectorClock
  }
  deriving Int -> Step -> ShowS
[Step] -> ShowS
Step -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Step] -> ShowS
$cshowList :: [Step] -> ShowS
show :: Step -> String
$cshow :: Step -> String
showsPrec :: Int -> Step -> ShowS
$cshowsPrec :: Int -> Step -> ShowS
Show


--
-- StepInfo
--

-- | As we execute a simulation, we collect information about each step.  This
-- information is updated as the simulation evolves by
-- `Control.Monad.IOSimPOR.Types.updateRaces`.
--
data StepInfo = StepInfo {
    -- | Step that we want to reschedule to run after a step in `stepInfoRaces`
    -- (there will be one schedule modification per step in
    -- `stepInfoRaces`).
    StepInfo -> Step
stepInfoStep       :: !Step,

    -- | Control information when we reached this step.
    StepInfo -> ScheduleControl
stepInfoControl    :: !ScheduleControl,

    -- | Threads that are still concurrent with this step.
    StepInfo -> Set IOSimThreadId
stepInfoConcurrent :: !(Set IOSimThreadId),

    -- | Steps following this one that did not happen after it
    -- (in reverse order).
    StepInfo -> [Step]
stepInfoNonDep     :: ![Step],

    -- | Later steps that race with `stepInfoStep`.
    StepInfo -> [Step]
stepInfoRaces      :: ![Step]
  }
  deriving Int -> StepInfo -> ShowS
[StepInfo] -> ShowS
StepInfo -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [StepInfo] -> ShowS
$cshowList :: [StepInfo] -> ShowS
show :: StepInfo -> String
$cshow :: StepInfo -> String
showsPrec :: Int -> StepInfo -> ShowS
$cshowsPrec :: Int -> StepInfo -> ShowS
Show

--
-- Races
--

data Races = Races { -- These steps may still race with future steps
                     Races -> [StepInfo]
activeRaces   :: ![StepInfo],
                     -- These steps cannot be concurrent with future steps
                     Races -> [StepInfo]
completeRaces :: ![StepInfo]
                   }
  deriving Int -> Races -> ShowS
[Races] -> ShowS
Races -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Races] -> ShowS
$cshowList :: [Races] -> ShowS
show :: Races -> String
$cshow :: Races -> String
showsPrec :: Int -> Races -> ShowS
$cshowsPrec :: Int -> Races -> ShowS
Show

noRaces :: Races
noRaces :: Races
noRaces = [StepInfo] -> [StepInfo] -> Races
Races [] []