1
1
{-# LANGUAGE BangPatterns #-}
2
+ {-# LANGUAGE LambdaCase #-}
2
3
{-# LANGUAGE ExplicitNamespaces #-}
3
4
{-# LANGUAGE NamedFieldPuns #-}
4
5
{-# LANGUAGE RankNTypes #-}
@@ -89,14 +90,17 @@ module Control.Monad.IOSim
89
90
import Prelude
90
91
91
92
import Data.Bifoldable
93
+ import Data.Bifunctor (first )
92
94
import Data.Dynamic (fromDynamic )
95
+ import Data.Functor (void )
93
96
import Data.List (intercalate )
94
97
import Data.Maybe (catMaybes )
95
98
import Data.Set (Set )
96
99
import qualified Data.Set as Set
97
100
import Data.Typeable (Typeable )
98
101
99
102
import Data.List.Trace (Trace (.. ))
103
+ import qualified Data.List.Trace as Trace
100
104
101
105
import Control.Exception (throw )
102
106
@@ -107,13 +111,13 @@ import Control.Monad.Class.MonadThrow as MonadThrow
107
111
108
112
import Control.Monad.IOSim.Internal (runSimTraceST )
109
113
import Control.Monad.IOSim.Types
110
- import Control.Monad.IOSimPOR.Internal (controlSimTraceST )
114
+ import qualified Control.Monad.IOSimPOR.Internal as IOSimPOR (controlSimTraceST )
111
115
import Control.Monad.IOSimPOR.QuickCheckUtils
112
116
113
117
import Test.QuickCheck
114
118
115
-
116
119
import System.IO.Unsafe
120
+ import qualified Debug.Trace as Debug
117
121
118
122
119
123
selectTraceEvents
@@ -497,11 +501,12 @@ exploreSimTrace optsf mainAction k =
497
501
-> Int -- branching factor
498
502
-> ScheduleControl -> Maybe (SimTrace a ) -> ST s Property
499
503
explore cacheRef n m control passingTrace = do
500
- traceWithRaces <- controlSimTraceST (explorationStepTimelimit opts) control mainAction
504
+ traceWithRaces <- IOSimPOR. controlSimTraceST (explorationStepTimelimit opts) control mainAction
501
505
(readRaces, trace0) <- detachTraceRacesST traceWithRaces
502
506
(readSleeperST, trace) <- compareTracesST passingTrace trace0
503
507
conjoinNoCatchST
504
508
[ do sleeper <- readSleeperST
509
+ () <- traceDebugLog (explorationDebugLevel opts) traceWithRaces
505
510
return $ counterexample (" Schedule control: " ++ show control)
506
511
$ counterexample
507
512
(case sleeper of
@@ -520,15 +525,13 @@ exploreSimTrace optsf mainAction k =
520
525
-- node.
521
526
races <- catMaybes
522
527
<$> (readRaces >>= traverse (cachedST cacheRef) . take limit)
528
+ () <- traceDebugLog (explorationDebugLevel opts) traceWithRaces
523
529
let branching = length races
524
530
-- tabulate "Races explored" (map show races) $
525
531
tabulate " Branching factor" [bucket branching]
526
532
. tabulate " Race reversals per schedule" [bucket (raceReversals control)]
527
533
<$> conjoinParST
528
- [ -- Debug.trace "New schedule:" $
529
- -- Debug.trace (" "++show r) $
530
- -- counterexample ("Schedule control: " ++ show r) $
531
- explore cacheRef n' ((m- 1 ) `max` 1 ) r (Just trace0)
534
+ [ explore cacheRef n' ((m- 1 ) `max` 1 ) r (Just trace0)
532
535
| (r,n') <- zip races (divide (n- branching) branching) ]
533
536
]
534
537
@@ -546,8 +549,8 @@ exploreSimTrace optsf mainAction k =
546
549
547
550
showThread :: (ThreadId ,Maybe ThreadLabel ) -> String
548
551
showThread (tid,lab) =
549
- show tid ++ (case lab of Nothing -> " "
550
- Just l -> " (" ++ l++ " )" )
552
+ ppIOSimThreadId tid ++ (case lab of Nothing -> " "
553
+ Just l -> " (" ++ l++ " )" )
551
554
552
555
-- insert a schedule into the cache
553
556
cachedST :: STRef s (Set ScheduleControl ) -> ScheduleControl -> ST s (Maybe ScheduleControl )
@@ -562,8 +565,6 @@ exploreSimTrace optsf mainAction k =
562
565
-- Caching in ST monad
563
566
--
564
567
565
- -- TODO: Use STRef!
566
-
567
568
-- It is possible for the same control to be generated several times.
568
569
-- To avoid exploring them twice, we keep a cache of explored schedules.
569
570
createCacheST :: ST s (STRef s (Set ScheduleControl ))
@@ -578,6 +579,17 @@ exploreSimTrace optsf mainAction k =
578
579
cacheSizeST = fmap Set. size . readSTRef
579
580
580
581
582
+ -- | Trace `SimTrace` to `stderr`.
583
+ --
584
+ traceDebugLog :: Int -> SimTrace a -> ST s ()
585
+ traceDebugLog logLevel _trace | logLevel <= 0 = pure ()
586
+ traceDebugLog 1 trace = Debug. traceM $ " Simulation trace with discovered schedules:\n "
587
+ ++ Trace. ppTrace show (ppSimEvent 0 0 0 ) (ignoreRaces $ void `first` trace)
588
+ traceDebugLog _ trace = Debug. traceM $ " Simulation trace with discovered schedules:\n "
589
+ ++ Trace. ppTrace show (ppSimEvent 0 0 0 ) (void `first` trace)
590
+
591
+
592
+
581
593
-- | A specialised version of `controlSimTrace'.
582
594
--
583
595
-- An internal function.
@@ -593,8 +605,10 @@ replaySimTrace :: forall a test. (Testable test)
593
605
-- will not contain any race events
594
606
-> Property
595
607
replaySimTrace opts mainAction control k =
596
- let trace = runST $ fmap snd $ detachTraceRacesST =<<
597
- controlSimTraceST (explorationStepTimelimit opts) control mainAction
608
+ let trace = runST $ do
609
+ (_readRaces, trace) <- IOSimPOR. controlSimTraceST (explorationStepTimelimit opts) control mainAction
610
+ >>= detachTraceRacesST
611
+ return (ignoreRaces trace)
598
612
in property (k trace)
599
613
600
614
-- | Run a simulation using a given schedule. This is useful to reproduce
@@ -611,8 +625,22 @@ controlSimTrace :: forall a.
611
625
-> (forall s . IOSim s a )
612
626
-- ^ a simulation to run
613
627
-> SimTrace a
614
- controlSimTrace limit control mainAction =
615
- runST (controlSimTraceST limit control mainAction)
628
+ controlSimTrace limit control main =
629
+ runST (controlSimTraceST limit control main)
630
+
631
+ controlSimTraceST :: Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a )
632
+ controlSimTraceST limit control main =
633
+ ignoreRaces <$> IOSimPOR. controlSimTraceST limit control main
634
+
635
+
636
+ --
637
+ -- Utils
638
+ --
639
+
640
+ ignoreRaces :: SimTrace a -> SimTrace a
641
+ ignoreRaces = Trace. filter (\ a -> case a of
642
+ SimPOREvent { seType = EventRaces {} } -> False
643
+ _ -> True )
616
644
617
645
raceReversals :: ScheduleControl -> Int
618
646
raceReversals ControlDefault = 0
@@ -629,6 +657,7 @@ raceReversals ControlFollow{} = error "Impossible: raceReversals ControlFoll
629
657
-- this far, then we collect its identity only if it is reached using
630
658
-- unsafePerformIO.
631
659
660
+ -- TODO: return StepId
632
661
compareTracesST :: forall a b s .
633
662
Maybe (SimTrace a ) -- ^ passing
634
663
-> SimTrace b -- ^ failing
0 commit comments