Add a "safe IO" flag

This is only sound to enable when all lifted IO is thread-safe.

dejafu/CHANGELOG.rst

@@ -7,6 +7,17 @@ standard Haskell versioning scheme.
 .. _PVP: https://pvp.haskell.org/
 
 
+unreleased
+----------
+
+Added
+~~~~~
+
+* (:issue:`224`) The ``Test.DejaFu.Settings.lsafeIO`` option, for when
+  all lifted IO is thread-safe (such as exclusively managing
+  thread-local state).
+
+
 1.10.0.0 (2018-06-17)
 ---------------------
 

dejafu/Test/DejaFu/Internal.hs

@@ -45,6 +45,7 @@ data Settings n a = Settings
   , _earlyExit :: Maybe (Either Failure a -> Bool)
   , _equality :: Maybe (a -> a -> Bool)
   , _simplify  :: Bool
+  , _safeIO :: Bool
   }
 
 -- | How to explore the possible executions of a concurrent program.

dejafu/Test/DejaFu/Settings.hs

@@ -188,6 +188,20 @@ module Test.DejaFu.Settings
 
   , lsimplify
 
+  -- ** Safe IO
+
+  -- | Normally, dejafu has to assume any IO action can influence any
+  -- other IO action, as there is no way to peek inside them.
+  -- However, this adds considerable overhead to systematic testing.
+  -- A perfectly legitimate use of IO is in managing thread-local
+  -- state, such as a PRNG; in this case, there is no point in
+  -- exploring interleavings of IO actions from other threads.
+  --
+  -- __Warning:__ Enabling this option is /unsound/ if your IO is not
+  -- thread safe!
+
+  , lsafeIO
+
   -- ** Debug output
 
   -- | You can opt to receive debugging messages by setting debugging
@@ -241,6 +255,7 @@ fromWayAndMemType way memtype = Settings
   , _earlyExit = Nothing
   , _equality = Nothing
   , _simplify = False
+  , _safeIO = False
   }
 
 -------------------------------------------------------------------------------
@@ -409,6 +424,15 @@ lequality afb s = (\b -> s {_equality = b}) <$> afb (_equality s)
 lsimplify :: Lens' (Settings n a) Bool
 lsimplify afb s = (\b -> s {_simplify = b}) <$> afb (_simplify s)
 
+-------------------------------------------------------------------------------
+-- Safe IO
+
+-- | A lens into the safe IO flag.
+--
+-- @since unreleased
+lsafeIO :: Lens' (Settings n a) Bool
+lsafeIO afb s = (\b -> s {_safeIO = b}) <$> afb (_safeIO s)
+
 -------------------------------------------------------------------------------
 -- Debug output
 

doc/advanced.rst

@@ -38,6 +38,9 @@ The available settings are:
 * **Trace simplification**, rewriting execution traces into a simpler
   form (particularly effective with the random testing).
 
+* **Safe IO**, pruning needless schedules when your IO is only used to
+  manage thread-local state.
+
 See the ``Test.DejaFu.Settings`` module for more information.