Skip to content

Commit

Permalink
io-sim-por: added exploreSimTraceST
Browse files Browse the repository at this point in the history
Unlike `exploreSimTrace` it allows to run `ST` action in the context of
each schedule, and thus allows to share state between schedules.  For
this reason it evaluates each schedule sequentially, while
`exploreSimTrace` evaluates each schedule in parallel.

This patch also makes the API more uniform by exposing:
* `exploreSimTrace` & `exploreSimTraceST`
* `controlSimTrace` & `controlSimTraceST`

Furthermore the tests are updated and they no longer use
`unsafePerformIO` as well.  The `traceCounter` property was removed as
it wasn't used and doesn't make much sense, since `IOSimPOR` is forcing
to evaluate each schedule only once by using a cache.
  • Loading branch information
coot committed Sep 25, 2023
1 parent 588c67e commit 5aec9e9
Show file tree
Hide file tree
Showing 4 changed files with 118 additions and 113 deletions.
1 change: 0 additions & 1 deletion io-sim/io-sim.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,6 @@ test-suite test
containers,
io-classes,
io-sim,
parallel,
QuickCheck,
si-timers,
strict-stm,
Expand Down
115 changes: 70 additions & 45 deletions io-sim/src/Control/Monad/IOSim.hs
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,9 @@ module Control.Monad.IOSim
-- ** Explore races using /IOSimPOR/
-- $iosimpor
, exploreSimTrace
, exploreSimTraceST
, controlSimTrace
, controlSimTraceST
, ScheduleMod (..)
, ScheduleControl (..)
-- *** Exploration options
Expand Down Expand Up @@ -173,6 +175,10 @@ selectTraceRaces = go
-- unsafe, of course, since that function may return different results
-- at different times.

-- | Detach discovered races. This is written in `ST` monad to support
-- simulations which do not terminate, in which case we will only detach races
-- up to the point we evaluated the simulation.
--
detachTraceRacesST :: forall a s. SimTrace a -> ST s (ST s [ScheduleControl], SimTrace a)
detachTraceRacesST trace0 = do
races <- newSTRef []
Expand All @@ -193,6 +199,15 @@ detachTraceRacesST trace0 = do
trace <- go trace0
return (readRaces, trace)


-- | Like `detachTraceRacesST`, but it doesn't expose discovered races.
--
detachTraceRaces :: forall a. SimTrace a -> SimTrace a
detachTraceRaces = Trace.filter (\a -> case a of
SimPOREvent { seType = EventRaces {} } -> False
SimRacesFound {} -> False
_ -> True)

-- | Select all the traced values matching the expected type. This relies on
-- the sim's dynamic trace facility.
--
Expand Down Expand Up @@ -491,6 +506,8 @@ runSimTrace mainAction = runST (runSimTraceST mainAction)
-- On property failure it will show the failing schedule (`ScheduleControl`)
-- which can be plugged to `controlSimTrace`.
--
-- Note: `exploreSimTrace` evaluates each schedule in parallel (using `par`).
--
exploreSimTrace
:: forall a test. Testable test
=> (ExplorationOptions -> ExplorationOptions)
Expand All @@ -501,34 +518,64 @@ exploreSimTrace
-- ^ a callback which receives the previous trace (e.g. before reverting
-- a race condition) and current trace
-> Property
exploreSimTrace optsf mainAction k =
case explorationReplay opts of
Nothing ->
case runST (do cacheRef <- createCacheST
prop <- explore cacheRef (explorationScheduleBound opts) (explorationBranching opts) ControlDefault Nothing
size <- cacheSizeST cacheRef
return (prop, size)
) of
(prop, !size) -> tabulate "Modified schedules explored" [bucket size] prop

Just control ->
replaySimTrace opts mainAction control (k Nothing)
exploreSimTrace optsf main k =
runST (unsafeExploreSimTraceST True optsf main (\a b -> pure (k a b)))


-- | An 'ST' version of 'exploreSimTrace'. The callback also receives
-- 'ScheduleControl'. This is mostly useful for testing /IOSimPOR/ itself.
--
-- Note: `exploreSimTraceST` evaluates each schedule sequentially.
--
exploreSimTraceST
:: forall s a test. Testable test
=> (ExplorationOptions -> ExplorationOptions)
-> (forall s. IOSim s a)
-> (Maybe (SimTrace a) -> SimTrace a -> ST s test)
-> ST s Property
exploreSimTraceST = unsafeExploreSimTraceST False


unsafeExploreSimTraceST
:: forall s a test. Testable test
=> Bool -- ^ use parallel evaluation of each shedule. This is unsafe if
-- there's a shared `STRef` involved.
-> (ExplorationOptions -> ExplorationOptions)
-> (forall s. IOSim s a)
-> (Maybe (SimTrace a) -> SimTrace a -> ST s test)
-> ST s Property
unsafeExploreSimTraceST par optsf main k =
case explorationReplay opts of
Just control -> do
trace <- controlSimTraceST (explorationStepTimelimit opts) control main
counterexample ("Shedule control: " ++ show control)
<$> k Nothing trace
Nothing -> do
cacheRef <- createCacheST
prop <- go cacheRef (explorationScheduleBound opts)
(explorationBranching opts)
ControlDefault Nothing
!size <- cacheSizeST cacheRef
return $ tabulate "Modified schedules explored" [bucket size] prop
where
conjoinST = if par then conjoinParST else conjoinSeqST

opts = optsf stdExplorationOptions

explore :: forall s.
STRef s (Set ScheduleControl)
-> Int -- schedule bound
-> Int -- branching factor
-> ScheduleControl -> Maybe (SimTrace a) -> ST s Property
explore cacheRef n m control passingTrace = do
traceWithRaces <- IOSimPOR.controlSimTraceST (explorationStepTimelimit opts) control mainAction
go :: STRef s (Set ScheduleControl)
-> Int -- schedule bound
-> Int -- branching factor
-> ScheduleControl
-> Maybe (SimTrace a)
-> ST s Property
go cacheRef n m control passingTrace = do
traceWithRaces <- IOSimPOR.controlSimTraceST (explorationStepTimelimit opts) control main
(readRaces, trace0) <- detachTraceRacesST traceWithRaces
(readSleeperST, trace) <- compareTracesST passingTrace trace0
conjoinNoCatchST
[ do sleeper <- readSleeperST
() <- traceDebugLog (explorationDebugLevel opts) traceWithRaces
prop <- k passingTrace trace
return $ counterexample ("Schedule control: " ++ show control)
$ counterexample
(case sleeper of
Expand All @@ -540,7 +587,7 @@ exploreSimTrace optsf mainAction k =
"\n until after:\n" ++
unlines (map ((" "++).showThread) $ Set.toList racing)
)
$ k passingTrace trace
prop
, do let limit = (n+m-1) `div` m
-- To ensure the set of schedules explored is deterministic, we
-- filter out cached ones *after* selecting the children of this
Expand All @@ -552,8 +599,8 @@ exploreSimTrace optsf mainAction k =
-- tabulate "Races explored" (map show races) $
tabulate "Branching factor" [bucket branching]
. tabulate "Race reversals per schedule" [bucket (raceReversals control)]
<$> conjoinParST
[ explore cacheRef n' ((m-1) `max` 1) r (Just trace0)
<$> conjoinST
[ go cacheRef n' ((m-1) `max` 1) r (Just trace0)
| (r,n') <- zip races (divide (n-branching) branching) ]
]

Expand Down Expand Up @@ -611,28 +658,6 @@ traceDebugLog _ trace = Debug.traceM $ "Simulation trace with discovered schedul
++ Trace.ppTrace show (ppSimEvent 0 0 0) (void `first` trace)



-- | A specialised version of `controlSimTrace'.
--
-- An internal function.
--
replaySimTrace :: forall a test. (Testable test)
=> ExplorationOptions
-- ^ race exploration options
-> (forall s. IOSim s a)
-> ScheduleControl
-- ^ a schedule control to reproduce
-> (SimTrace a -> test)
-- ^ a callback which receives the simulation trace. The trace
-- will not contain any race events
-> Property
replaySimTrace opts mainAction control k =
let trace = runST $ do
(_readRaces, trace) <- IOSimPOR.controlSimTraceST (explorationStepTimelimit opts) control mainAction
>>= detachTraceRacesST
return (ignoreRaces trace)
in property (k trace)

-- | Run a simulation using a given schedule. This is useful to reproduce
-- failing cases without exploring the races.
--
Expand All @@ -652,7 +677,7 @@ controlSimTrace limit control main =

controlSimTraceST :: Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
controlSimTraceST limit control main =
ignoreRaces <$> IOSimPOR.controlSimTraceST limit control main
detachTraceRaces <$> IOSimPOR.controlSimTraceST limit control main


--
Expand Down
15 changes: 9 additions & 6 deletions io-sim/src/Control/Monad/IOSimPOR/QuickCheckUtils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -10,13 +10,16 @@ import Control.Monad.ST.Lazy.Unsafe (unsafeInterleaveST)
import Test.QuickCheck.Gen
import Test.QuickCheck.Property

-- note: this only evaluates `prop` in parallel, not `ST` actions
conjoinSeqST :: Testable prop => [ST s prop] -> ST s Property
conjoinSeqST sts = conjoin <$> sequence sts

-- | Evaluate each `ST s prop` in parallel using `pseq`.
--
conjoinParST :: TestableNoCatch prop => [ST s prop] -> ST s Property
conjoinParST sts = do
-- ps <- sequence sts
-- TODO: this could increase parallelism
ps <- sequence (unsafeInterleaveST <$> sts)
return $ conjoinPar ps
conjoinParST sts =
-- `unsafeInterleaveST` is needed to turn each `ST` computation into an
-- independent thunk which can be evaluated in parallel.
conjoinPar <$> sequence (unsafeInterleaveST <$> sts)

-- Take the conjunction of several properties, in parallel This is a
-- modification of code from Test.QuickCheck.Property, to run non-IO
Expand Down
100 changes: 39 additions & 61 deletions io-sim/test/Test/Control/Monad/IOSimPOR.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,19 +14,18 @@ module Test.Control.Monad.IOSimPOR (tests) where
import Data.Fixed (Micro)
import Data.Foldable (foldl', traverse_)
import Data.Functor (($>))
import Data.IORef
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map as Map
import Data.STRef.Lazy

import System.Exit
import System.IO.Error (ioeGetErrorString, isUserError)
import System.IO.Unsafe

import Control.Exception (ArithException (..), AsyncException)
import Control.Monad
import Control.Monad.Fix
import Control.Parallel
import Control.Monad.ST.Lazy (ST, runST)

import Control.Concurrent.Class.MonadSTM
import Control.Monad.Class.MonadAsync
Expand Down Expand Up @@ -343,22 +342,26 @@ propSimulates cmp (Shrink2 (Tasks tasks)) =
Left x -> counterexample (ppTrace trace)
$ counterexample (show x) True

-- NOTE: This property needs to be executed sequentially, otherwise it fails
-- undeterministically, which `exploreSimTraceST` does.
--
propExploration :: Compare -> (Shrink2 Tasks) -> Property
propExploration cmp (Shrink2 ts@(Tasks tasks)) =
any (not . null . (\(Task steps)->steps)) tasks ==>
runST $
traceNoDuplicates $ \addTrace ->
--traceCounter $ \addTrace ->
exploreSimTrace (\a -> a { explorationDebugLevel = 0 })
(say (show ts) >> runTasks cmp tasks) $ \_ trace ->
addTrace trace $
exploreSimTraceST (\a -> a { explorationDebugLevel = 0 })
(say (show ts) >> runTasks cmp tasks)
$ \_ trace -> do
addTrace trace
-- TODO: for now @coot is leaving `Trace.ppTrace`, but once we change all
-- assertions into `FailureInternal`, we can use `ppTrace` instead
counterexample (noExceptions $ Trace.ppTrace show (ppSimEvent 0 0 0) trace) $
case traceResult False trace of
Right (m,a) -> property (m >= a)
Left (FailureInternal msg)
-> counterexample msg False
Left _ -> property True
return $ counterexample (Trace.ppTrace show (ppSimEvent 0 0 0) trace) $
case traceResult False trace of
Right (m,a) -> property (m >= a)
Left (FailureInternal msg)
-> counterexample msg False
Left _ -> property True


-- | This is a counterexample for a fix included in the commit: "io-sim-por:
Expand Down Expand Up @@ -387,14 +390,6 @@ unit_issue113_racy =
Task [ThrowTo 1,WhenSet 0 0],
Task [ThrowTo 1]]

prop :: Property
prop = shrinking shrink (Shrink2 tasks) (propExploration AreNotEqual)
where
tasks = Tasks [Task [WhenSet 1 0,ThrowTo 1],
Task [],
Task [ThrowTo 1,WhenSet 0 0],
Task [ThrowTo 1]]


-- | This test checks that we don't build a schedule which execute a non
-- dependent step that depends on something that wasn't added to
Expand All @@ -416,12 +411,12 @@ unit_issue113_nonDep =
-- Test manually, and supply a small value of n.
propPermutations :: Int -> Property
propPermutations n =
runST $
traceNoDuplicates $ \addTrace ->
exploreSimTrace (withScheduleBound 10000) (doit n) $ \_ trace ->
addTrace trace $
let Right result = traceResult False trace in
tabulate "Result" [noExceptions $ show $ result] $
True
exploreSimTraceST (withScheduleBound 10000) (doit n) $ \_ trace -> do
addTrace trace
let Right result = traceResult False trace
return $ tabulate "Result" [show $ result] $ True

doit :: Int -> IOSim s [Int]
doit n = do
Expand All @@ -431,55 +426,38 @@ doit n = do
threadDelay 1
atomically $ readTVar r

ordered :: Ord a => [a] -> Bool
ordered xs = and (zipWith (<) xs (drop 1 xs))

noExceptions :: [Char] -> [Char]
noExceptions xs = unsafePerformIO $ try (evaluate xs) >>= \case
Right [] -> return []
Right (x:ys) -> return (x:noExceptions ys)
Left e -> return ("\n"++show (e :: SomeException))
traceNoDuplicates :: forall s a prop. (Show a, Testable prop)
=> ((a -> ST s ()) -> ST s prop)
-> ST s Property
traceNoDuplicates k = do
v <- newSTRef Map.empty :: ST s (STRef s (Map String Int))
prop <- k (\a -> modifySTRef v (Map.insertWith (+) (show a) 1))
m <- readSTRef v
return $ prop .&&. counterexample (show (Map.keys $ Map.filter (> 1) m)) (maximum m === 1)

traceCounter :: (Testable prop1, Show a1) => ((a1 -> a2 -> a2) -> prop1) -> Property
traceCounter k = r `pseq` (k addTrace .&&.
tabulate "Trace repetitions" (map show $ traceCounts ()) True)
where
r = unsafePerformIO $ newIORef (Map.empty :: Map String Int)
addTrace t x = unsafePerformIO $ do
atomicModifyIORef r (\m->(Map.insertWith (+) (show t) 1 m,()))
return x
traceCounts () = unsafePerformIO $ Map.elems <$> readIORef r

traceNoDuplicates :: (Testable prop1, Show a1) => ((a1 -> a2 -> a2) -> prop1) -> Property
traceNoDuplicates k = r `pseq` (k addTrace .&&. maximum (traceCounts ()) == 1)
where
r = unsafePerformIO $ newIORef (Map.empty :: Map String Int)
addTrace t x = unsafePerformIO $ do
atomicModifyIORef r (\m->(Map.insertWith (+) (show t) 1 m,()))
return x
traceCounts () = unsafePerformIO $ Map.elems <$> readIORef r

--
-- IOSim reused properties
--


--
-- Read/Write graph
--

prop_stm_graph_sim :: TestThreadGraph -> Property
prop_stm_graph_sim g =
runST $
traceNoDuplicates $ \addTrace ->
exploreSimTrace id (prop_stm_graph g) $ \_ trace ->
addTrace trace $
counterexample (noExceptions $ Trace.ppTrace show show trace) $
case traceResult False trace of
Right () -> property True
Left e -> counterexample (show e) False
-- TODO: Note that we do not use runSimStrictShutdown here to check
-- that all other threads finished, but perhaps we should and structure
-- the graph tests so that's the case.
exploreSimTraceST id (prop_stm_graph g) $ \_ trace -> do
addTrace trace
return $ counterexample (Trace.ppTrace show show trace) $
case traceResult False trace of
Right () -> property True
Left e -> counterexample (show e) False
-- TODO: Note that we do not use runSimStrictShutdown here to check
-- that all other threads finished, but perhaps we should and structure
-- the graph tests so that's the case.

prop_timers_ST :: TestMicro -> Property
prop_timers_ST (TestMicro xs) =
Expand Down

0 comments on commit 5aec9e9

Please sign in to comment.