module Control.Concurrent.CHP.Traces.Base where
import Control.Concurrent.STM
import Control.Monad (liftM)
import Data.IORef
import Data.List
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Unique
import Control.Concurrent.CHP.Event
import Control.Concurrent.CHP.ProcessId
type RecordedEvent u = (RecordedEventType, u)
data RecordedIndivEvent u =
ChannelWrite u Integer String
| ChannelRead u Integer String
| BarrierSyncIndiv u Integer String
| ClockSyncIndiv u Integer String
deriving (Eq, Ord, Read, Show)
recordedIndivEventLabel :: RecordedIndivEvent u -> u
recordedIndivEventLabel (ChannelWrite x _ _) = x
recordedIndivEventLabel (ChannelRead x _ _) = x
recordedIndivEventLabel (BarrierSyncIndiv x _ _) = x
recordedIndivEventLabel (ClockSyncIndiv x _ _) = x
recordedIndivEventSeq :: RecordedIndivEvent u -> Integer
recordedIndivEventSeq (ChannelWrite _ n _) = n
recordedIndivEventSeq (ChannelRead _ n _) = n
recordedIndivEventSeq (BarrierSyncIndiv _ n _) = n
recordedIndivEventSeq (ClockSyncIndiv _ n _) = n
indivRec :: (u -> Integer -> String -> RecordedIndivEvent u)
-> u -> (u -> Integer) -> String -> (RecordedIndivEvent u)
indivRec r u f = r u (f u)
indivRecJust :: (u -> Integer -> String -> RecordedIndivEvent u)
-> u -> (u -> Integer) -> String -> [RecordedIndivEvent u]
indivRecJust r u f x = [indivRec r u f x]
type RecEvents = ([RecordedEvent Unique], [RecordedIndivEvent Unique])
data LabelM u a = LabelM { runLabelM :: ChannelLabels u -> (a, ChannelLabels u) }
labelWith :: LabelM u a -> ChannelLabels u -> a
labelWith = (fst .) . runLabelM
instance Monad (LabelM u) where
return = LabelM . (,)
m >>= k = LabelM $ \s -> let (a, s') = runLabelM m s in runLabelM (k a) s'
getName :: Ord u => String -> u -> LabelM u String
getName prefix u = LabelM $ \m ->
case Map.lookup u m of
Just x -> (x, m)
Nothing -> let x = prefix ++ show (Map.size m) in (x, Map.insert u x m)
nameEvent :: Ord u => RecordedEvent u -> LabelM u String
nameEvent (t, c) = liftM (++ suffix) $ getName prefix c
where
(prefix, suffix) = case t of
ChannelComm x -> ("_c", if null x then "" else '.' : x)
BarrierSync x -> ("_b", if null x then "" else '.' : x)
ClockSync st -> ("_t", ':' : st)
nameEvent' :: Ord u => RecordedEvent u -> LabelM u (RecordedEvent String)
nameEvent' (t, c) = do c' <- getName prefix c
return (t, c' ++ suffix)
where
(prefix, suffix) = case t of
ChannelComm _ -> ("_c", "")
BarrierSync _ -> ("_b", "")
ClockSync st -> ("_t", ':' : st)
nameIndivEvent :: Ord u => RecordedIndivEvent u -> LabelM u String
nameIndivEvent (ChannelWrite c n _) = do c' <- getName "_c" c
return $ c' ++ "![" ++ show n ++ "]"
nameIndivEvent (ChannelRead c n _) = do c' <- getName "_c" c
return $ c' ++ "?[" ++ show n ++ "]"
nameIndivEvent (BarrierSyncIndiv c n _) = do c' <- getName "_b" c
return $ c' ++ "[" ++ show n ++ "]"
nameIndivEvent (ClockSyncIndiv c n t) = do c' <- getName "_t" c
return $ c' ++ ":" ++ t
++ "[" ++ show n ++ "]"
nameIndivEvent' :: Ord u => RecordedIndivEvent u -> LabelM u (RecordedIndivEvent String)
nameIndivEvent' (ChannelWrite c n x) = do c' <- getName "_c" c
return $ ChannelWrite c' n x
nameIndivEvent' (ChannelRead c n x) = do c' <- getName "_c" c
return $ ChannelRead c' n x
nameIndivEvent' (BarrierSyncIndiv c n x) = do c' <- getName "_b" c
return $ BarrierSyncIndiv c' n x
nameIndivEvent' (ClockSyncIndiv c n t) = do c' <- getName "_t" c
return $ ClockSyncIndiv c' n t
data TraceStore =
NoTrace ProcessId
| Trace (ProcessId, TVar (ChannelLabels Unique), SubTraceStore)
mapSubTrace :: Monad m => (SubTraceStore -> m ()) -> TraceStore -> m ()
mapSubTrace _ (NoTrace {}) = return ()
mapSubTrace f (Trace (_pid, _tv, s)) = f s
type ChannelLabels u = Map.Map u String
data SubTraceStore =
Hierarchy (IORef (Structured (RecordedIndivEvent Unique)))
| CSPTraceRev (TVar [(Int, [RecordedEvent Unique])])
| VCRTraceRev (TVar [Set.Set (Set.Set ProcessId, RecordedEvent Unique)])
data Ord a => Structured a =
StrEvent a
| Par [Structured a]
| RevSeq [(Int, [Structured a])]
deriving (Eq, Ord)
recordEventLast :: [(RecordedEvent Unique, Set.Set ProcessId)] -> TraceStore -> STM ()
recordEventLast news y
= case y of
Trace (_,_,CSPTraceRev tv) ->
do t <- readTVar tv
writeTVar tv $! foldl (flip addRLE) t (map fst news)
Trace (pid, _, VCRTraceRev tv) -> do
t <- readTVar tv
let news' = map (\(a,b) -> (b,a)) news
pidSet = (foldl Set.union (Set.singleton pid) $ map fst news')
t' = prependVCR t pidSet news'
writeTVar tv $! t'
_ -> return ()
prependVCR :: Ord u =>
[Set.Set (Set.Set ProcessId, RecordedEvent u)]
-> Set.Set ProcessId
-> [(Set.Set ProcessId, RecordedEvent u)]
-> [Set.Set (Set.Set ProcessId, RecordedEvent u)]
prependVCR t pidSet news'
= case t of
[] -> [Set.fromList news']
(z:zs) | shouldMakeNewSetVCR pidSet z
-> Set.fromList news' : t
| otherwise
-> foldl (flip Set.insert) z news' : zs
recordEvent :: [RecordedIndivEvent Unique] -> TraceStore -> IO ()
recordEvent e = mapSubTrace recH
where
recH (Hierarchy es) = modifyIORef es (addParEventsH (map StrEvent e))
recH _ = return ()
mergeSubProcessTraces :: [TraceStore] -> TraceStore -> IO ()
mergeSubProcessTraces ts
= mapSubTrace merge
where
ts' = mapM readIORef [t | Trace (_,_,Hierarchy t) <- ts]
merge (Hierarchy es) = ts' >>= modifyIORef es . addParEventsH
merge _ = return ()
shouldMakeNewSetVCR :: Ord u => Set.Set ProcessId -> Set.Set (Set.Set ProcessId, RecordedEvent u)
-> Bool
shouldMakeNewSetVCR newpids existingSet
= exists existingSet $ \(bigP,_) -> exists bigP $ \p -> exists newpids $ \q ->
p `pidLessThanOrEqual` q
where
exists :: Ord a => Set.Set a -> (a -> Bool) -> Bool
exists s f = not . Set.null $ Set.filter f s
compress :: (Eq a, Ord a) => Structured a -> Structured a
compress (RevSeq ((1,s):(n,s'):ss))
| n == 1 && (s `isPrefixOf` s') = compress $ RevSeq $ (2,s):(1,drop (length s) s'):ss
| s == s' = compress $ RevSeq $ (n+1,s'):ss
compress x = x
addParEventsH :: (Eq a, Ord a) => [Structured a] -> Structured a -> Structured a
addParEventsH es t = let n = es in case t of
StrEvent _ -> RevSeq [(1, [Par n, t])]
Par _ -> RevSeq [(1, [Par n, t])]
RevSeq ((1,s):ss) -> compress $ RevSeq $ (1,Par n : s) : ss
RevSeq ss -> compress $ RevSeq $ (1, [Par n]):ss
addSeqEventH :: (Eq a, Ord a) => a -> Structured a -> Structured a
addSeqEventH e (StrEvent e') = RevSeq [(1,[StrEvent e, StrEvent e'])]
addSeqEventH e (Par p) = RevSeq [(1,[StrEvent e, Par p])]
addSeqEventH e (RevSeq ((1,s):ss))
| (StrEvent e) `notElem` s = compress $ RevSeq $ (1,StrEvent e:s):ss
addSeqEventH e (RevSeq ss) = compress $ RevSeq $ (1,[StrEvent e]):ss
addRLE :: Eq a => a -> [(Int,[a])] -> [(Int,[a])]
addRLE x ((n,[e]):nes)
| x == e = (n+1,[e]):nes
addRLE x allEs@[(1,es)]
| x == head es = [(2, [x]), (1, tail es)]
| x `elem` es = (1,[x]):allEs
| otherwise = [(1,x:es)]
addRLE x allEs@((1,es):(n,es'):nes)
| x == head es' && es == tail es' = (n+1,es'):nes
| x `elem` es = (1,[x]):allEs
| otherwise = (1,x:es):(n,es'):nes
addRLE x nes = (1,[x]):nes
labelEvent :: TraceStore -> Event -> String -> IO ()
labelEvent t e = labelUnique t (getEventUnique e)
labelUnique :: TraceStore -> Unique -> String -> IO ()
labelUnique t u l
= case t of
NoTrace {} -> return ()
Trace (_,tvls,_) -> add tvls
where
add :: TVar (Map.Map Unique String) -> IO ()
add tv = atomically $ do
m <- readTVar tv
writeTVar tv $ Map.insert u l m
newIds :: Int -> ProcessId -> [ProcessId]
newIds n pid = let ProcessId parts = pid in
[ProcessId $ parts ++ [ParSeq i 0] | i <- [0 .. (n 1)]]
blankTraces :: TraceStore -> Int -> IO [TraceStore]
blankTraces (NoTrace pid) n = return $ map NoTrace $ newIds n pid
blankTraces (Trace (pid, tvls, subT)) n =
sequence [liftM (\s -> Trace (newId, tvls, s)) newSubT | newId <- newIds n pid]
where
newSubT :: IO SubTraceStore
newSubT = case subT of
Hierarchy {} -> liftM Hierarchy $ newIORef $ RevSeq []
_ -> return subT
chp_permutations :: [b] -> [[b]]
chp_permutations xs0 = xs0 : perms xs0 []
where
perms [] _ = []
perms (t:ts) is = foldr interleave (perms ts (t:is)) (chp_permutations is)
where
interleave xs r = let (_,zs) = interleave' id xs r in zs
interleave' _ [] r = (ts, r)
interleave' f (y:ys) r = let (us,zs) = interleave' (f . (y:)) ys r
in (y:us, f (t:y:us) : zs)
bagsEq :: Eq a => [a] -> [a] -> Bool
bagsEq a b = or [a' == b' | a' <- chp_permutations a, b' <- chp_permutations b]