{-# LANGUAGE NamedFieldPuns #-}
module Control.Monad.IOSimPOR.Types
(
Effect (..)
, readEffects
, writeEffects
, forkEffect
, throwToEffect
, wakeupEffects
, onlyReadEffect
, racingEffects
, ppEffect
, ScheduleControl (..)
, isDefaultSchedule
, ScheduleMod (..)
, StepId
, ppStepId
, Step (..)
, StepInfo (..)
, Races (..)
, noRaces
) where
import Data.List qualified as List
import Data.Set (Set)
import Data.Set qualified as Set
import Control.Monad.IOSim.CommonTypes
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
(Int -> Effect -> ShowS)
-> (Effect -> String) -> ([Effect] -> ShowS) -> Show Effect
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Effect -> ShowS
showsPrec :: Int -> Effect -> ShowS
$cshow :: Effect -> String
show :: Effect -> String
$cshowList :: [Effect] -> ShowS
showList :: [Effect] -> ShowS
Show, Effect -> Effect -> Bool
(Effect -> Effect -> Bool)
-> (Effect -> Effect -> Bool) -> Eq Effect
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Effect -> Effect -> Bool
== :: Effect -> Effect -> Bool
$c/= :: Effect -> Effect -> Bool
/= :: Effect -> Effect -> Bool
Eq)
ppEffect :: Effect -> String
ppEffect :: Effect -> String
ppEffect Effect { Set TVarId
effectReads :: Effect -> Set TVarId
effectReads :: Set TVarId
effectReads, Set TVarId
effectWrites :: Effect -> Set TVarId
effectWrites :: Set TVarId
effectWrites, Set IOSimThreadId
effectForks :: Effect -> Set IOSimThreadId
effectForks :: Set IOSimThreadId
effectForks, [IOSimThreadId]
effectThrows :: Effect -> [IOSimThreadId]
effectThrows :: [IOSimThreadId]
effectThrows, Set IOSimThreadId
effectWakeup :: Effect -> Set IOSimThreadId
effectWakeup :: Set IOSimThreadId
effectWakeup } =
String
"Effect { " String -> ShowS
forall a. [a] -> [a] -> [a]
++
[String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
List.intersperse String
", " ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$
[ String
"reads = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set TVarId -> String
forall a. Show a => a -> String
show Set TVarId
effectReads | Bool -> Bool
not (Set TVarId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set TVarId
effectReads) ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"writes = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Set TVarId -> String
forall a. Show a => a -> String
show Set TVarId
effectWrites | Bool -> Bool
not (Set TVarId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set TVarId
effectWrites) ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"forks = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (IOSimThreadId -> String) -> [IOSimThreadId] -> String
forall a. (a -> String) -> [a] -> String
ppList IOSimThreadId -> String
ppIOSimThreadId (Set IOSimThreadId -> [IOSimThreadId]
forall a. Set a -> [a]
Set.toList Set IOSimThreadId
effectForks) | Bool -> Bool
not (Set IOSimThreadId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set IOSimThreadId
effectForks) ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"throws = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (IOSimThreadId -> String) -> [IOSimThreadId] -> String
forall a. (a -> String) -> [a] -> String
ppList IOSimThreadId -> String
ppIOSimThreadId [IOSimThreadId]
effectThrows | Bool -> Bool
not ([IOSimThreadId] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [IOSimThreadId]
effectThrows) ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"wakeup = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (IOSimThreadId -> String) -> [IOSimThreadId] -> String
forall a. (a -> String) -> [a] -> String
ppList IOSimThreadId -> String
ppIOSimThreadId (Set IOSimThreadId -> [IOSimThreadId]
forall a. Set a -> [a]
Set.toList Set IOSimThreadId
effectWakeup) | Bool -> Bool
not (Set IOSimThreadId -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set IOSimThreadId
effectWakeup) ])
String -> ShowS
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 Set TVarId -> Set TVarId -> Set TVarId
forall a. Semigroup a => a -> a -> a
<> Set TVarId
r') (Set TVarId
w Set TVarId -> Set TVarId -> Set TVarId
forall a. Semigroup a => a -> a -> a
<> Set TVarId
w') (Set IOSimThreadId
s Set IOSimThreadId -> Set IOSimThreadId -> Set IOSimThreadId
forall a. Semigroup a => a -> a -> a
<> Set IOSimThreadId
s') ([IOSimThreadId]
ts [IOSimThreadId] -> [IOSimThreadId] -> [IOSimThreadId]
forall a. [a] -> [a] -> [a]
++ [IOSimThreadId]
ts') (Set IOSimThreadId
wu Set IOSimThreadId -> Set IOSimThreadId -> Set IOSimThreadId
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 Set TVarId
forall a. Set a
Set.empty Set TVarId
forall a. Set a
Set.empty Set IOSimThreadId
forall a. Set a
Set.empty [] Set IOSimThreadId
forall a. Set a
Set.empty
readEffects :: [SomeTVar s] -> Effect
readEffects :: forall s. [SomeTVar s] -> Effect
readEffects [SomeTVar s]
rs = Effect
forall a. Monoid a => a
mempty{effectReads = Set.fromList (map someTvarId rs)}
writeEffects :: [SomeTVar s] -> Effect
writeEffects :: forall s. [SomeTVar s] -> Effect
writeEffects [SomeTVar s]
rs = Effect
forall a. Monoid a => a
mempty{effectWrites = Set.fromList (map someTvarId rs)}
forkEffect :: IOSimThreadId -> Effect
forkEffect :: IOSimThreadId -> Effect
forkEffect IOSimThreadId
tid = Effect
forall a. Monoid a => a
mempty{effectForks = Set.singleton tid}
throwToEffect :: IOSimThreadId -> Effect
throwToEffect :: IOSimThreadId -> Effect
throwToEffect IOSimThreadId
tid = Effect
forall a. Monoid a => a
mempty{ effectThrows = [tid] }
wakeupEffects :: [IOSimThreadId] -> Effect
wakeupEffects :: [IOSimThreadId] -> Effect
wakeupEffects [IOSimThreadId]
tids = Effect
forall a. Monoid a => a
mempty{effectWakeup = Set.fromList tids}
someTvarId :: SomeTVar s -> TVarId
someTvarId :: forall s. SomeTVar s -> TVarId
someTvarId (SomeTVar TVar s a
r) = TVar s a -> TVarId
forall s a. TVar s a -> TVarId
tvarId TVar s a
r
onlyReadEffect :: Effect -> Bool
onlyReadEffect :: Effect -> Bool
onlyReadEffect Effect
e = Effect
e { effectReads = effectReads mempty } Effect -> Effect -> Bool
forall a. Eq a => a -> a -> Bool
== Effect
forall a. Monoid a => a
mempty
racingEffects :: Effect -> Effect -> Bool
racingEffects :: Effect -> Effect -> Bool
racingEffects Effect
e Effect
e' =
Effect -> [IOSimThreadId]
effectThrows Effect
e [IOSimThreadId] -> [IOSimThreadId] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`intersectsL` Effect -> [IOSimThreadId]
effectThrows Effect
e'
Bool -> Bool -> Bool
|| Effect -> Set TVarId
effectReads Effect
e Set TVarId -> Set TVarId -> Bool
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 Set TVarId -> Set TVarId -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`intersects` Effect -> Set TVarId
effectReads Effect
e'
Bool -> Bool -> Bool
|| Effect -> Set TVarId
effectWrites Effect
e Set TVarId -> Set TVarId -> Bool
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set a
a Set a -> Set a -> Bool
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 (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([a] -> Bool) -> [a] -> Bool
forall a b. (a -> b) -> a -> b
$ [a]
a [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
`List.intersect` [a]
b
data ScheduleControl = ControlDefault
| ControlAwait [ScheduleMod]
| ControlFollow [StepId] [ScheduleMod]
deriving (ScheduleControl -> ScheduleControl -> Bool
(ScheduleControl -> ScheduleControl -> Bool)
-> (ScheduleControl -> ScheduleControl -> Bool)
-> Eq ScheduleControl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ScheduleControl -> ScheduleControl -> Bool
== :: ScheduleControl -> ScheduleControl -> Bool
$c/= :: ScheduleControl -> ScheduleControl -> Bool
/= :: ScheduleControl -> ScheduleControl -> Bool
Eq, Eq ScheduleControl
Eq ScheduleControl =>
(ScheduleControl -> ScheduleControl -> Ordering)
-> (ScheduleControl -> ScheduleControl -> Bool)
-> (ScheduleControl -> ScheduleControl -> Bool)
-> (ScheduleControl -> ScheduleControl -> Bool)
-> (ScheduleControl -> ScheduleControl -> Bool)
-> (ScheduleControl -> ScheduleControl -> ScheduleControl)
-> (ScheduleControl -> ScheduleControl -> ScheduleControl)
-> Ord 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
$ccompare :: ScheduleControl -> ScheduleControl -> Ordering
compare :: ScheduleControl -> ScheduleControl -> Ordering
$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
>= :: ScheduleControl -> ScheduleControl -> Bool
$cmax :: ScheduleControl -> ScheduleControl -> ScheduleControl
max :: ScheduleControl -> ScheduleControl -> ScheduleControl
$cmin :: ScheduleControl -> ScheduleControl -> ScheduleControl
min :: ScheduleControl -> ScheduleControl -> ScheduleControl
Ord, Int -> ScheduleControl -> ShowS
[ScheduleControl] -> ShowS
ScheduleControl -> String
(Int -> ScheduleControl -> ShowS)
-> (ScheduleControl -> String)
-> ([ScheduleControl] -> ShowS)
-> Show ScheduleControl
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ScheduleControl -> ShowS
showsPrec :: Int -> ScheduleControl -> ShowS
$cshow :: ScheduleControl -> String
show :: ScheduleControl -> String
$cshowList :: [ScheduleControl] -> ShowS
showList :: [ScheduleControl] -> ShowS
Show)
isDefaultSchedule :: ScheduleControl -> Bool
isDefaultSchedule :: ScheduleControl -> Bool
isDefaultSchedule ScheduleControl
ControlDefault = Bool
True
isDefaultSchedule (ControlFollow [] []) = Bool
True
isDefaultSchedule ScheduleControl
_ = Bool
False
data ScheduleMod = ScheduleMod{
ScheduleMod -> StepId
scheduleModTarget :: StepId,
ScheduleMod -> ScheduleControl
scheduleModControl :: ScheduleControl,
ScheduleMod -> [StepId]
scheduleModInsertion :: [StepId]
}
deriving (ScheduleMod -> ScheduleMod -> Bool
(ScheduleMod -> ScheduleMod -> Bool)
-> (ScheduleMod -> ScheduleMod -> Bool) -> Eq ScheduleMod
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ScheduleMod -> ScheduleMod -> Bool
== :: ScheduleMod -> ScheduleMod -> Bool
$c/= :: ScheduleMod -> ScheduleMod -> Bool
/= :: ScheduleMod -> ScheduleMod -> Bool
Eq, Eq ScheduleMod
Eq ScheduleMod =>
(ScheduleMod -> ScheduleMod -> Ordering)
-> (ScheduleMod -> ScheduleMod -> Bool)
-> (ScheduleMod -> ScheduleMod -> Bool)
-> (ScheduleMod -> ScheduleMod -> Bool)
-> (ScheduleMod -> ScheduleMod -> Bool)
-> (ScheduleMod -> ScheduleMod -> ScheduleMod)
-> (ScheduleMod -> ScheduleMod -> ScheduleMod)
-> Ord 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
$ccompare :: ScheduleMod -> ScheduleMod -> Ordering
compare :: ScheduleMod -> ScheduleMod -> Ordering
$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
>= :: ScheduleMod -> ScheduleMod -> Bool
$cmax :: ScheduleMod -> ScheduleMod -> ScheduleMod
max :: ScheduleMod -> ScheduleMod -> ScheduleMod
$cmin :: ScheduleMod -> ScheduleMod -> ScheduleMod
min :: ScheduleMod -> ScheduleMod -> ScheduleMod
Ord)
instance Show ScheduleMod where
showsPrec :: Int -> ScheduleMod -> ShowS
showsPrec Int
d (ScheduleMod StepId
tgt ScheduleControl
ctrl [StepId]
insertion) =
Bool -> ShowS -> ShowS
showParen (Int
dInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
String -> ShowS
showString String
"ScheduleMod " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> StepId -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 StepId
tgt ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> ScheduleControl -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 ScheduleControl
ctrl ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
String -> ShowS
showString String
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
Int -> [StepId] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 [StepId]
insertion
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
(Int -> Step -> ShowS)
-> (Step -> String) -> ([Step] -> ShowS) -> Show Step
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Step -> ShowS
showsPrec :: Int -> Step -> ShowS
$cshow :: Step -> String
show :: Step -> String
$cshowList :: [Step] -> ShowS
showList :: [Step] -> ShowS
Show
data StepInfo = StepInfo {
StepInfo -> Step
stepInfoStep :: !Step,
StepInfo -> ScheduleControl
stepInfoControl :: !ScheduleControl,
StepInfo -> Set IOSimThreadId
stepInfoConcurrent :: !(Set IOSimThreadId),
StepInfo -> [Step]
stepInfoNonDep :: ![Step],
StepInfo -> [Step]
stepInfoRaces :: ![Step]
}
deriving Int -> StepInfo -> ShowS
[StepInfo] -> ShowS
StepInfo -> String
(Int -> StepInfo -> ShowS)
-> (StepInfo -> String) -> ([StepInfo] -> ShowS) -> Show StepInfo
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StepInfo -> ShowS
showsPrec :: Int -> StepInfo -> ShowS
$cshow :: StepInfo -> String
show :: StepInfo -> String
$cshowList :: [StepInfo] -> ShowS
showList :: [StepInfo] -> ShowS
Show
data Races = Races {
Races -> [StepInfo]
activeRaces :: ![StepInfo],
Races -> [StepInfo]
completeRaces :: ![StepInfo]
}
deriving Int -> Races -> ShowS
[Races] -> ShowS
Races -> String
(Int -> Races -> ShowS)
-> (Races -> String) -> ([Races] -> ShowS) -> Show Races
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Races -> ShowS
showsPrec :: Int -> Races -> ShowS
$cshow :: Races -> String
show :: Races -> String
$cshowList :: [Races] -> ShowS
showList :: [Races] -> ShowS
Show
noRaces :: Races
noRaces :: Races
noRaces = [StepInfo] -> [StepInfo] -> Races
Races [] []