dejafu 1.10.1.0 → 1.11.0.0

raw patch · 15 files changed

+352/−346 lines, 15 filesdep ~concurrencyPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: concurrency

API changes (from Hackage documentation)

Files

• CHANGELOG.rst +15/−0
• Test/DejaFu.hs +10/−10
• Test/DejaFu/Conc.hs +14/−14
• Test/DejaFu/Conc/Internal.hs +52/−52
• Test/DejaFu/Conc/Internal/Common.hs +24/−24
• Test/DejaFu/Conc/Internal/Memory.hs +48/−48
• Test/DejaFu/Conc/Internal/STM.hs +9/−9
• Test/DejaFu/Internal.hs +52/−52
• Test/DejaFu/SCT.hs +11/−11
• Test/DejaFu/SCT/Internal.hs +27/−27
• Test/DejaFu/SCT/Internal/DPOR.hs +13/−13
• Test/DejaFu/Settings.hs +9/−9
• Test/DejaFu/Types.hs +63/−72
• Test/DejaFu/Utils.hs +2/−2
• dejafu.cabal +3/−3

@@ -7,6 +7,21 @@ .. _PVP: https://pvp.haskell.org/  +1.11.0.0 - IORefs (2018-07-01)+------------------------------++* Git: :tag:`dejafu-1.11.0.0`+* Hackage: :hackage:`dejafu-1.11.0.0`++Changed+~~~~~~~++* (:issue:`274`) ``CRef`` is now ``IORef``: all functions, data+  constructors, and types have been renamed.++* The lower bound on :hackage:`concurrency` is 1.6.++ 1.10.1.0 (2018-06-17) --------------------- 

@@ -102,7 +102,7 @@ The defaults should generally be good enough, but if not you have a few tricks available.  The main two are: the 'Way', which controls how schedules are explored; and the 'MemType', which controls how reads-and writes to @CRef@s behave; see "Test.DejaFu.Settings" for a+and writes to @IORef@s behave; see "Test.DejaFu.Settings" for a complete listing.  -}@@ -301,10 +301,10 @@  >>> :{ let relaxed = do-      r1 <- newCRef False-      r2 <- newCRef False-      x <- spawn $ writeCRef r1 True >> readCRef r2-      y <- spawn $ writeCRef r2 True >> readCRef r1+      r1 <- newIORef False+      r2 <- newIORef False+      x <- spawn $ writeIORef r1 True >> readIORef r2+      y <- spawn $ writeIORef r2 True >> readIORef r1       (,) <$> readMVar x <*> readMVar y :} @@ -363,7 +363,7 @@   => Way   -- ^ How to run the concurrent program.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ConcT n a   -- ^ The computation to test.   -> n Bool@@ -454,7 +454,7 @@   => Way   -- ^ How to run the concurrent program.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> String   -- ^ The name of the test.   -> ProPredicate a b@@ -505,7 +505,7 @@   -> Way   -- ^ How to run the concurrent program.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> String   -- ^ The name of the test.   -> ProPredicate a b@@ -555,7 +555,7 @@   => Way   -- ^ How to run the concurrent program.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> [(String, ProPredicate a b)]   -- ^ The list of predicates (with names) to check.   -> ConcT n a@@ -672,7 +672,7 @@   => Way   -- ^ How to run the concurrent program.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ProPredicate a b   -- ^ The predicate to check   -> ConcT n a

@@ -46,7 +46,7 @@   , ThreadAction(..)   , Lookahead(..)   , MVarId-  , CRefId+  , IORefId   , MaskingState(..)   , showTrace   , showFail@@ -124,7 +124,7 @@  instance Monad n => C.MonadConc (ConcT n) where   type MVar     (ConcT n) = ModelMVar n-  type CRef     (ConcT n) = ModelCRef n+  type IORef    (ConcT n) = ModelIORef n   type Ticket   (ConcT n) = ModelTicket   type STM      (ConcT n) = ModelSTM n   type ThreadId (ConcT n) = ThreadId@@ -153,18 +153,18 @@    -- ---------- -  newCRefN n a = toConc (ANewCRef n a)+  newIORefN n a = toConc (ANewIORef n a) -  readCRef   ref = toConc (AReadCRef    ref)-  readForCAS ref = toConc (AReadCRefCas ref)+  readIORef   ref = toConc (AReadIORef    ref)+  readForCAS ref = toConc (AReadIORefCas ref)    peekTicket' _ = ticketVal -  writeCRef ref      a = toConc (\c -> AWriteCRef ref a (c ()))-  casCRef   ref tick a = toConc (ACasCRef ref tick a)+  writeIORef ref      a = toConc (\c -> AWriteIORef ref a (c ()))+  casIORef   ref tick a = toConc (ACasIORef ref tick a) -  atomicModifyCRef ref f = toConc (AModCRef    ref f)-  modifyCRefCAS    ref f = toConc (AModCRefCas ref f)+  atomicModifyIORef ref f = toConc (AModIORef    ref f)+  modifyIORefCAS    ref f = toConc (AModIORefCas ref f)    -- ---------- @@ -218,7 +218,7 @@   -> n (Either Failure a, s, Trace) runConcurrent sched memtype s ma = do   res <- runConcurrency False sched memtype s initialIdSource 2 (unC ma)-  out <- efromJust <$> C.readCRef (finalRef res)+  out <- efromJust <$> C.readIORef (finalRef res)   pure ( out        , cSchedState (finalContext res)        , F.toList (finalTrace res)@@ -284,7 +284,7 @@ -- -- __Snapshotting @IO@:__ A snapshot captures entire state of your -- concurrent program: the state of every thread, the number of--- capabilities, the values of any @CRef@s, @MVar@s, and @TVar@s, and+-- capabilities, the values of any @IORef@s, @MVar@s, and @TVar@s, and -- records any @IO@ that you performed. -- -- When restoring a snapshot this @IO@ is replayed, in order.  But the@@ -311,7 +311,7 @@ -- To safely use @IO@ in a snapshotted computation, __the combined effect must be idempotent__. -- You should either use actions which set the state to the final -- value directly, rather than modifying it (eg, using a combination--- of @liftIO . readCRef@ and @liftIO . writeIORef@ here), or reset+-- of @liftIO . readIORef@ and @liftIO . writeIORef@ here), or reset -- the state to a known value.  Both of these approaches will work: -- -- @@@ -349,7 +349,7 @@   -> n (Maybe (Either Failure (DCSnapshot n a), Trace)) runForDCSnapshot ma = do   res <- runConcurrency True roundRobinSchedNP SequentialConsistency () initialIdSource 2 (unC ma)-  out <- C.readCRef (finalRef res)+  out <- C.readIORef (finalRef res)   pure $ case (finalRestore res, out) of     (Just _, Just (Left f)) -> Just (Left f, F.toList (finalTrace res))     (Just restore, _) -> Just (Right (DCSnapshot (finalContext res) restore (finalRef res)), F.toList (finalTrace res))@@ -374,7 +374,7 @@   let restore = dcsRestore snapshot   let ref = dcsRef snapshot   res <- runConcurrencyWithSnapshot sched memtype context restore ref-  out <- efromJust <$> C.readCRef (finalRef res)+  out <- efromJust <$> C.readIORef (finalRef res)   pure ( out        , cSchedState (finalContext res)        , F.toList (finalTrace res)

@@ -49,7 +49,7 @@ -- | The result of running a concurrent program. data CResult n g a = CResult   { finalContext :: Context n g-  , finalRef :: C.CRef n (Maybe (Either Failure a))+  , finalRef :: C.IORef n (Maybe (Either Failure a))   , finalRestore :: Maybe (Threads n -> n ())   -- ^ Meaningless if this result doesn't come from a snapshotting   -- execution.@@ -66,8 +66,8 @@   -- ^ The execution context.  The scheduler state is ignored when   -- restoring.   , dcsRestore :: Threads n -> n ()-  -- ^ Action to restore CRef, MVar, and TVar values.-  , dcsRef :: C.CRef n (Maybe (Either Failure a))+  -- ^ Action to restore IORef, MVar, and TVar values.+  , dcsRef :: C.IORef n (Maybe (Either Failure a))   -- ^ Reference where the result will be written.   } @@ -118,7 +118,7 @@   -> MemType   -> Context n g   -> (Threads n -> n ())-  -> C.CRef n (Maybe (Either Failure a))+  -> C.IORef n (Maybe (Either Failure a))   -> n (CResult n g a) runConcurrencyWithSnapshot sched memtype ctx restore ref = do   let boundThreads = M.filter (isJust . _bound) (cThreads ctx)@@ -151,13 +151,13 @@   => Bool   -> Scheduler g   -> MemType-  -> C.CRef n (Maybe (Either Failure a))+  -> C.IORef n (Maybe (Either Failure a))   -> Context n g   -> n (CResult n g a) runThreads forSnapshot sched memtype ref = schedule (const $ pure ()) Seq.empty Nothing where   -- signal failure & terminate   die reason finalR finalT finalD finalC = do-    C.writeCRef ref (Just $ Left reason)+    C.writeIORef ref (Just $ Left reason)     stop finalR finalT finalD finalC    -- just terminate; 'ref' must have been written to before calling@@ -367,11 +367,11 @@ -- create a new @MVar@, using the next 'MVarId'. stepThread _ _ _ _ tid (ANewMVar n c) = \ctx@Context{..} -> do   let (idSource', newmvid) = nextMVId n cIdSource-  ref <- C.newCRef Nothing+  ref <- C.newIORef Nothing   let mvar = ModelMVar newmvid ref   pure ( Succeeded ctx { cThreads = goto (c mvar) tid cThreads, cIdSource = idSource' }        , Single (NewMVar newmvid)-       , const (C.writeCRef ref Nothing)+       , const (C.writeIORef ref Nothing)        )  -- put a value into a @MVar@, blocking the thread until it's empty.@@ -424,85 +424,85 @@        , const effect        ) --- create a new @CRef@, using the next 'CRefId'.-stepThread _ _ _ _  tid (ANewCRef n a c) = \ctx@Context{..} -> do-  let (idSource', newcrid) = nextCRId n cIdSource+-- create a new @IORef@, using the next 'IORefId'.+stepThread _ _ _ _  tid (ANewIORef n a c) = \ctx@Context{..} -> do+  let (idSource', newiorid) = nextIORId n cIdSource   let val = (M.empty, 0, a)-  ref <- C.newCRef val-  let cref = ModelCRef newcrid ref-  pure ( Succeeded ctx { cThreads = goto (c cref) tid cThreads, cIdSource = idSource' }-       , Single (NewCRef newcrid)-       , const (C.writeCRef ref val)+  ioref <- C.newIORef val+  let ref = ModelIORef newiorid ioref+  pure ( Succeeded ctx { cThreads = goto (c ref) tid cThreads, cIdSource = idSource' }+       , Single (NewIORef newiorid)+       , const (C.writeIORef ioref val)        ) --- read from a @CRef@.-stepThread _ _ _ _  tid (AReadCRef cref@ModelCRef{..} c) = \ctx@Context{..} -> do-  val <- readCRef cref tid+-- read from a @IORef@.+stepThread _ _ _ _  tid (AReadIORef ref@ModelIORef{..} c) = \ctx@Context{..} -> do+  val <- readIORef ref tid   pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }-       , Single (ReadCRef crefId)+       , Single (ReadIORef iorefId)        , const (pure ())        ) --- read from a @CRef@ for future compare-and-swap operations.-stepThread _ _ _ _ tid (AReadCRefCas cref@ModelCRef{..} c) = \ctx@Context{..} -> do-  tick <- readForTicket cref tid+-- read from a @IORef@ for future compare-and-swap operations.+stepThread _ _ _ _ tid (AReadIORefCas ref@ModelIORef{..} c) = \ctx@Context{..} -> do+  tick <- readForTicket ref tid   pure ( Succeeded ctx { cThreads = goto (c tick) tid cThreads }-       , Single (ReadCRefCas crefId)+       , Single (ReadIORefCas iorefId)        , const (pure ())        ) --- modify a @CRef@.-stepThread _ _ _ _ tid (AModCRef cref@ModelCRef{..} f c) = synchronised $ \ctx@Context{..} -> do-  (new, val) <- f <$> readCRef cref tid-  effect <- writeImmediate cref new+-- modify a @IORef@.+stepThread _ _ _ _ tid (AModIORef ref@ModelIORef{..} f c) = synchronised $ \ctx@Context{..} -> do+  (new, val) <- f <$> readIORef ref tid+  effect <- writeImmediate ref new   pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }-       , Single (ModCRef crefId)+       , Single (ModIORef iorefId)        , const effect        ) --- modify a @CRef@ using a compare-and-swap.-stepThread _ _ _ _ tid (AModCRefCas cref@ModelCRef{..} f c) = synchronised $ \ctx@Context{..} -> do-  tick@(ModelTicket _ _ old) <- readForTicket cref tid+-- modify a @IORef@ using a compare-and-swap.+stepThread _ _ _ _ tid (AModIORefCas ref@ModelIORef{..} f c) = synchronised $ \ctx@Context{..} -> do+  tick@(ModelTicket _ _ old) <- readForTicket ref tid   let (new, val) = f old-  (_, _, effect) <- casCRef cref tid tick new+  (_, _, effect) <- casIORef ref tid tick new   pure ( Succeeded ctx { cThreads = goto (c val) tid cThreads }-       , Single (ModCRefCas crefId)+       , Single (ModIORefCas iorefId)        , const effect        ) --- write to a @CRef@ without synchronising.-stepThread _ _ _ memtype tid (AWriteCRef cref@ModelCRef{..} a c) = \ctx@Context{..} -> case memtype of+-- write to a @IORef@ without synchronising.+stepThread _ _ _ memtype tid (AWriteIORef ref@ModelIORef{..} a c) = \ctx@Context{..} -> case memtype of   -- write immediately.   SequentialConsistency -> do-    effect <- writeImmediate cref a+    effect <- writeImmediate ref a     pure ( Succeeded ctx { cThreads = goto c tid cThreads }-         , Single (WriteCRef crefId)+         , Single (WriteIORef iorefId)          , const effect          )   -- add to buffer using thread id.   TotalStoreOrder -> do-    wb' <- bufferWrite cWriteBuf (tid, Nothing) cref a+    wb' <- bufferWrite cWriteBuf (tid, Nothing) ref a     pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }-         , Single (WriteCRef crefId)+         , Single (WriteIORef iorefId)          , const (pure ())          )-  -- add to buffer using both thread id and cref id+  -- add to buffer using both thread id and IORef id   PartialStoreOrder -> do-    wb' <- bufferWrite cWriteBuf (tid, Just crefId) cref a+    wb' <- bufferWrite cWriteBuf (tid, Just iorefId) ref a     pure ( Succeeded ctx { cThreads = goto c tid cThreads, cWriteBuf = wb' }-         , Single (WriteCRef crefId)+         , Single (WriteIORef iorefId)          , const (pure ())          ) --- perform a compare-and-swap on a @CRef@.-stepThread _ _ _ _ tid (ACasCRef cref@ModelCRef{..} tick a c) = synchronised $ \ctx@Context{..} -> do-  (suc, tick', effect) <- casCRef cref tid tick a+-- perform a compare-and-swap on a @IORef@.+stepThread _ _ _ _ tid (ACasIORef ref@ModelIORef{..} tick a c) = synchronised $ \ctx@Context{..} -> do+  (suc, tick', effect) <- casIORef ref tid tick a   pure ( Succeeded ctx { cThreads = goto (c (suc, tick')) tid cThreads }-       , Single (CasCRef crefId suc)+       , Single (CasIORef iorefId suc)        , const effect        ) --- commit a @CRef@ write+-- commit a @IORef@ write stepThread _ _ _ memtype _ (ACommit t c) = \ctx@Context{..} -> do   wb' <- case memtype of     -- shouldn't ever get here@@ -511,11 +511,11 @@     -- commit using the thread id.     TotalStoreOrder ->       commitWrite cWriteBuf (t, Nothing)-    -- commit using the cref id.+    -- commit using the IORef id.     PartialStoreOrder ->       commitWrite cWriteBuf (t, Just c)   pure ( Succeeded ctx { cWriteBuf = wb' }-       , Single (CommitCRef t c)+       , Single (CommitIORef t c)        , const (pure ())        ) @@ -634,7 +634,7 @@      | M.size (cThreads ctx) > 1 -> pure (Failed IllegalSubconcurrency, Single Subconcurrency, const (pure ()))      | otherwise -> do          res <- runConcurrency False sched memtype (cSchedState ctx) (cIdSource ctx) (cCaps ctx) ma-         out <- efromJust <$> C.readCRef (finalRef res)+         out <- efromJust <$> C.readIORef (finalRef res)          pure ( Succeeded ctx                 { cThreads    = goto (AStopSub (c out)) tid (cThreads ctx)                 , cIdSource   = cIdSource (finalContext res)@@ -662,7 +662,7 @@          threads' <- kill tid (cThreads ctx)          let dcCtx = ctx { cThreads = threads', cSchedState = lb }          res <- runConcurrency' forSnapshot dcSched SequentialConsistency dcCtx ma-         out <- efromJust <$> C.readCRef (finalRef res)+         out <- efromJust <$> C.readIORef (finalRef res)          case out of            Right a -> do              let threads'' = launch' Unmasked tid (const (c a)) (cThreads (finalContext res))

@@ -56,22 +56,22 @@ -- @Maybe@ value. data ModelMVar n a = ModelMVar   { mvarId  :: MVarId-  , mvarRef :: C.CRef n (Maybe a)+  , mvarRef :: C.IORef n (Maybe a)   } --- | A @CRef@ is modelled as a unique ID and a reference holding+-- | A @IORef@ is modelled as a unique ID and a reference holding -- thread-local values, the number of commits, and the most recent -- committed value.-data ModelCRef n a = ModelCRef-  { crefId  :: CRefId-  , crefRef :: C.CRef n (Map ThreadId a, Integer, a)+data ModelIORef n a = ModelIORef+  { iorefId  :: IORefId+  , iorefRef :: C.IORef n (Map ThreadId a, Integer, a)   } --- | A @Ticket@ is modelled as the ID of the @ModelCRef@ it came from,--- the commits to the @ModelCRef@ at the time it was produced, and the+-- | A @Ticket@ is modelled as the ID of the @ModelIORef@ it came from,+-- the commits to the @ModelIORef@ at the time it was produced, and the -- value observed. data ModelTicket a = ModelTicket-  { ticketCRef   :: CRefId+  { ticketIORef  :: IORefId   , ticketWrites :: Integer   , ticketVal    :: a   }@@ -100,13 +100,13 @@   | forall a. ATakeMVar    (ModelMVar n a) (a -> Action n)   | forall a. ATryTakeMVar (ModelMVar n a) (Maybe a -> Action n) -  | forall a.   ANewCRef String a (ModelCRef n a -> Action n)-  | forall a.   AReadCRef    (ModelCRef n a) (a -> Action n)-  | forall a.   AReadCRefCas (ModelCRef n a) (ModelTicket a -> Action n)-  | forall a b. AModCRef     (ModelCRef n a) (a -> (a, b)) (b -> Action n)-  | forall a b. AModCRefCas  (ModelCRef n a) (a -> (a, b)) (b -> Action n)-  | forall a.   AWriteCRef   (ModelCRef n a) a (Action n)-  | forall a.   ACasCRef     (ModelCRef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n)+  | forall a.   ANewIORef String a (ModelIORef n a -> Action n)+  | forall a.   AReadIORef    (ModelIORef n a) (a -> Action n)+  | forall a.   AReadIORefCas (ModelIORef n a) (ModelTicket a -> Action n)+  | forall a b. AModIORef     (ModelIORef n a) (a -> (a, b)) (b -> Action n)+  | forall a b. AModIORefCas  (ModelIORef n a) (a -> (a, b)) (b -> Action n)+  | forall a.   AWriteIORef   (ModelIORef n a) a (Action n)+  | forall a.   ACasIORef     (ModelIORef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n)    | forall e.   Exception e => AThrow e   | forall e.   Exception e => AThrowTo ThreadId e (Action n)@@ -120,7 +120,7 @@   | AYield  (Action n)   | ADelay Int (Action n)   | AReturn (Action n)-  | ACommit ThreadId CRefId+  | ACommit ThreadId IORefId   | AStop (n ())    | forall a. ASub (ModelConc n a) (Either Failure a -> Action n)@@ -145,14 +145,14 @@ lookahead (ATryReadMVar (ModelMVar m _) _) = WillTryReadMVar m lookahead (ATakeMVar (ModelMVar m _) _) = WillTakeMVar m lookahead (ATryTakeMVar (ModelMVar m _) _) = WillTryTakeMVar m-lookahead (ANewCRef _ _ _) = WillNewCRef-lookahead (AReadCRef (ModelCRef r _) _) = WillReadCRef r-lookahead (AReadCRefCas (ModelCRef r _) _) = WillReadCRefCas r-lookahead (AModCRef (ModelCRef r _) _ _) = WillModCRef r-lookahead (AModCRefCas (ModelCRef r _) _ _) = WillModCRefCas r-lookahead (AWriteCRef (ModelCRef r _) _ _) = WillWriteCRef r-lookahead (ACasCRef (ModelCRef r _) _ _ _) = WillCasCRef r-lookahead (ACommit t c) = WillCommitCRef t c+lookahead (ANewIORef _ _ _) = WillNewIORef+lookahead (AReadIORef (ModelIORef r _) _) = WillReadIORef r+lookahead (AReadIORefCas (ModelIORef r _) _) = WillReadIORefCas r+lookahead (AModIORef (ModelIORef r _) _ _) = WillModIORef r+lookahead (AModIORefCas (ModelIORef r _) _ _) = WillModIORefCas r+lookahead (AWriteIORef (ModelIORef r _) _ _) = WillWriteIORef r+lookahead (ACasIORef (ModelIORef r _) _ _ _) = WillCasIORef r+lookahead (ACommit t c) = WillCommitIORef t c lookahead (AAtom _ _) = WillSTM lookahead (AThrow _) = WillThrow lookahead (AThrowTo tid _ _) = WillThrowTo tid

@@ -12,14 +12,14 @@ -- Stability   : experimental -- Portability : BangPatterns, GADTs, FlexibleContexts, LambdaCase, RecordWildCards ----- Operations over @CRef@s and @MVar@s. This module is NOT considered+-- Operations over @IORef@s and @MVar@s. This module is NOT considered -- to form part of the public interface of this library. ----- Relaxed memory operations over @CRef@s are implemented with an+-- Relaxed memory operations over @IORef@s are implemented with an -- explicit write buffer: one per thread for TSO, and one per -- thread/variable combination for PSO. Unsynchronised writes append -- to this buffer, and periodically separate threads commit from these--- buffers to the \"actual\" @CRef@.+-- buffers to the \"actual\" @IORef@. -- -- This model comes from /Dynamic Partial Order Reduction for Relaxed -- Memory Models/, N. Zhang, M. Kusano, and C. Wang (2015).@@ -40,93 +40,93 @@ import           Test.DejaFu.Types  ----------------------------------------------------------------------------------- * Manipulating @CRef@s+-- * Manipulating @IORef@s  -- | In non-sequentially-consistent memory models, non-synchronised -- writes get buffered. ----- The @CRefId@ parameter is only used under PSO. Under TSO each+-- The @IORefId@ parameter is only used under PSO. Under TSO each -- thread has a single buffer. newtype WriteBuffer n = WriteBuffer-  { buffer :: Map (ThreadId, Maybe CRefId) (Seq (BufferedWrite n)) }+  { buffer :: Map (ThreadId, Maybe IORefId) (Seq (BufferedWrite n)) }  -- | A buffered write is a reference to the variable, and the value to -- write. Universally quantified over the value type so that the only -- thing which can be done with it is to write it to the reference. data BufferedWrite n where-  BufferedWrite :: ThreadId -> ModelCRef n a -> a -> BufferedWrite n+  BufferedWrite :: ThreadId -> ModelIORef n a -> a -> BufferedWrite n  -- | An empty write buffer. emptyBuffer :: WriteBuffer n emptyBuffer = WriteBuffer M.empty  -- | Add a new write to the end of a buffer.-bufferWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe CRefId) -> ModelCRef n a -> a -> n (WriteBuffer n)-bufferWrite (WriteBuffer wb) k@(tid, _) cref@ModelCRef{..} new = do+bufferWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> ModelIORef n a -> a -> n (WriteBuffer n)+bufferWrite (WriteBuffer wb) k@(tid, _) ref@ModelIORef{..} new = do   -- Construct the new write buffer-  let write = singleton $ BufferedWrite tid cref new+  let write = singleton $ BufferedWrite tid ref new   let buffer' = M.insertWith (flip (><)) k write wb -  -- Write the thread-local value to the @CRef@'s update map.-  (locals, count, def) <- C.readCRef crefRef-  C.writeCRef crefRef (M.insert tid new locals, count, def)+  -- Write the thread-local value to the @IORef@'s update map.+  (locals, count, def) <- C.readIORef iorefRef+  C.writeIORef iorefRef (M.insert tid new locals, count, def)    pure (WriteBuffer buffer')  -- | Commit the write at the head of a buffer.-commitWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe CRefId) -> n (WriteBuffer n)+commitWrite :: C.MonadConc n => WriteBuffer n -> (ThreadId, Maybe IORefId) -> n (WriteBuffer n) commitWrite w@(WriteBuffer wb) k = case maybe EmptyL viewl $ M.lookup k wb of-  BufferedWrite _ cref a :< rest -> do-    _ <- writeImmediate cref a+  BufferedWrite _ ref a :< rest -> do+    _ <- writeImmediate ref a     pure . WriteBuffer $ M.insert k rest wb   EmptyL -> pure w --- | Read from a @CRef@, returning a newer thread-local non-committed+-- | Read from a @IORef@, returning a newer thread-local non-committed -- write if there is one.-readCRef :: C.MonadConc n => ModelCRef n a -> ThreadId -> n a-readCRef cref tid = do-  (val, _) <- readCRefPrim cref tid+readIORef :: C.MonadConc n => ModelIORef n a -> ThreadId -> n a+readIORef ref tid = do+  (val, _) <- readIORefPrim ref tid   pure val --- | Read from a @CRef@, returning a @Ticket@ representing the current+-- | Read from a @IORef@, returning a @Ticket@ representing the current -- view of the thread.-readForTicket :: C.MonadConc n => ModelCRef n a -> ThreadId -> n (ModelTicket a)-readForTicket cref@ModelCRef{..} tid = do-  (val, count) <- readCRefPrim cref tid-  pure (ModelTicket crefId count val)+readForTicket :: C.MonadConc n => ModelIORef n a -> ThreadId -> n (ModelTicket a)+readForTicket ref@ModelIORef{..} tid = do+  (val, count) <- readIORefPrim ref tid+  pure (ModelTicket iorefId count val) --- | Perform a compare-and-swap on a @CRef@ if the ticket is still+-- | Perform a compare-and-swap on a @IORef@ if the ticket is still -- valid. This is strict in the \"new\" value argument.-casCRef :: C.MonadConc n => ModelCRef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())-casCRef cref tid (ModelTicket _ cc _) !new = do-  tick'@(ModelTicket _ cc' _) <- readForTicket cref tid+casIORef :: C.MonadConc n => ModelIORef n a -> ThreadId -> ModelTicket a -> a -> n (Bool, ModelTicket a, n ())+casIORef ref tid (ModelTicket _ cc _) !new = do+  tick'@(ModelTicket _ cc' _) <- readForTicket ref tid    if cc == cc'   then do-    effect <- writeImmediate cref new-    tick'' <- readForTicket cref tid+    effect <- writeImmediate ref new+    tick'' <- readForTicket ref tid     pure (True, tick'', effect)   else pure (False, tick', pure ()) --- | Read the local state of a @CRef@.-readCRefPrim :: C.MonadConc n => ModelCRef n a -> ThreadId -> n (a, Integer)-readCRefPrim ModelCRef{..} tid = do-  (vals, count, def) <- C.readCRef crefRef+-- | Read the local state of a @IORef@.+readIORefPrim :: C.MonadConc n => ModelIORef n a -> ThreadId -> n (a, Integer)+readIORefPrim ModelIORef{..} tid = do+  (vals, count, def) <- C.readIORef iorefRef   pure (M.findWithDefault def tid vals, count) --- | Write and commit to a @CRef@ immediately, clearing the update map+-- | Write and commit to a @IORef@ immediately, clearing the update map -- and incrementing the write count.-writeImmediate :: C.MonadConc n => ModelCRef n a -> a -> n (n ())-writeImmediate ModelCRef{..} a = do-  (_, count, _) <- C.readCRef crefRef-  let effect = C.writeCRef crefRef (M.empty, count + 1, a)+writeImmediate :: C.MonadConc n => ModelIORef n a -> a -> n (n ())+writeImmediate ModelIORef{..} a = do+  (_, count, _) <- C.readIORef iorefRef+  let effect = C.writeIORef iorefRef (M.empty, count + 1, a)   effect   pure effect  -- | Flush all writes in the buffer. writeBarrier :: C.MonadConc n => WriteBuffer n -> n () writeBarrier (WriteBuffer wb) = mapM_ flush $ M.elems wb where-  flush = mapM_ $ \(BufferedWrite _ cref a) -> writeImmediate cref a+  flush = mapM_ $ \(BufferedWrite _ ref a) -> writeImmediate ref a  -- | Add phantom threads to the thread list to commit pending writes. addCommitThreads :: WriteBuffer n -> Threads n -> Threads n@@ -135,13 +135,13 @@              | (k, b) <- M.toList wb              , c <- maybeToList (go $ viewl b)              ]-  go (BufferedWrite tid ModelCRef{..} _ :< _) = Just $ ACommit tid crefId+  go (BufferedWrite tid ModelIORef{..} _ :< _) = Just $ ACommit tid iorefId   go EmptyL = Nothing  -- | The ID of a commit thread.-commitThreadId :: ThreadId -> Maybe CRefId -> ThreadId+commitThreadId :: ThreadId -> Maybe IORefId -> ThreadId commitThreadId (ThreadId (Id _ t)) = ThreadId . Id Nothing . negate . go where-  go (Just (CRefId (Id _ c))) = t + 1 + c * 10000+  go (Just (IORefId (Id _ c))) = t + 1 + c * 10000   go Nothing = t + 1  -- | Remove phantom threads.@@ -220,7 +220,7 @@   -> ThreadId   -> Threads n   -> n (Bool, Threads n, [ThreadId], n ())-mutMVar blocking ModelMVar{..} a c threadid threads = C.readCRef mvarRef >>= \case+mutMVar blocking ModelMVar{..} a c threadid threads = C.readIORef mvarRef >>= \case   Just _ -> case blocking of     Blocking ->       let threads' = block (OnMVarEmpty mvarId) threadid threads@@ -228,7 +228,7 @@     NonBlocking ->       pure (False, goto (c False) threadid threads, [], pure ())   Nothing -> do-    let effect = C.writeCRef mvarRef $ Just a+    let effect = C.writeIORef mvarRef $ Just a     let (threads', woken) = wake (OnMVarFull mvarId) threads     effect     pure (True, goto (c True) threadid threads', woken, effect)@@ -243,10 +243,10 @@   -> ThreadId   -> Threads n   -> n (Bool, Threads n, [ThreadId], n ())-seeMVar emptying blocking ModelMVar{..} c threadid threads = C.readCRef mvarRef >>= \case+seeMVar emptying blocking ModelMVar{..} c threadid threads = C.readIORef mvarRef >>= \case   val@(Just _) -> do     let effect = case emptying of-          Emptying -> C.writeCRef mvarRef Nothing+          Emptying -> C.writeIORef mvarRef Nothing           NonEmptying -> pure ()     let (threads', woken) = wake (OnMVarEmpty mvarId) threads     effect

@@ -100,7 +100,7 @@ -- value. data ModelTVar n a = ModelTVar   { tvarId  :: TVarId-  , tvarRef :: C.CRef n a+  , tvarRef :: C.IORef n a   }  --------------------------------------------------------------------------------@@ -145,7 +145,7 @@ doTransaction ma idsource = do   (c, ref) <- runRefCont SStop (Just . Right) (runModelSTM ma)   (idsource', undo, readen, written, trace) <- go ref c (pure ()) idsource [] [] []-  res <- C.readCRef ref+  res <- C.readIORef ref    case res of     Just (Right val) -> pure (Success (nub readen) (nub written) val, undo, idsource', reverse trace)@@ -166,10 +166,10 @@       case tact of         TStop  -> pure (newIDSource, newUndo, newReaden, newWritten, TStop:newSofar)         TRetry -> do-          C.writeCRef ref Nothing+          C.writeIORef ref Nothing           pure (newIDSource, newUndo, newReaden, newWritten, TRetry:newSofar)         TThrow -> do-          C.writeCRef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)+          C.writeIORef ref (Just . Left $ case act of SThrow e -> toException e; _ -> undefined)           pure (newIDSource, newUndo, newReaden, newWritten, TThrow:newSofar)         _ -> go ref newAct newUndo newIDSource newReaden newWritten newSofar @@ -199,17 +199,17 @@         Nothing   -> pure (SThrow exc, nothing, idsource, [], [], TCatch trace Nothing))      stepRead ModelTVar{..} c = do-      val <- C.readCRef tvarRef+      val <- C.readIORef tvarRef       pure (c val, nothing, idsource, [tvarId], [], TRead tvarId)      stepWrite ModelTVar{..} a c = do-      old <- C.readCRef tvarRef-      C.writeCRef tvarRef a-      pure (c, C.writeCRef tvarRef old, idsource, [], [tvarId], TWrite tvarId)+      old <- C.readIORef tvarRef+      C.writeIORef tvarRef a+      pure (c, C.writeIORef tvarRef old, idsource, [], [tvarId], TWrite tvarId)      stepNew n a c = do       let (idsource', tvid) = nextTVId n idsource-      ref <- C.newCRef a+      ref <- C.newIORef a       let tvar = ModelTVar tvid ref       pure (c tvar, nothing, idsource', [], [tvid], TNew tvid) 

@@ -65,17 +65,17 @@ -- | The number of ID parameters was getting a bit unwieldy, so this -- hides them all away. data IdSource = IdSource-  { _crids :: (Int, [String])-  , _mvids :: (Int, [String])-  , _tvids :: (Int, [String])-  , _tids  :: (Int, [String])+  { _iorids :: (Int, [String])+  , _mvids  :: (Int, [String])+  , _tvids  :: (Int, [String])+  , _tids   :: (Int, [String])   } deriving (Eq, Ord, Show, Generic, NFData) --- | Get the next free 'CRefId'.-nextCRId :: String -> IdSource -> (IdSource, CRefId)-nextCRId name idsource =-  let (crid, crids') = nextId name (_crids idsource)-  in (idsource { _crids = crids' }, CRefId crid)+-- | Get the next free 'IORefId'.+nextIORId :: String -> IdSource -> (IdSource, IORefId)+nextIORId name idsource =+  let (iorid, iorids') = nextId name (_iorids idsource)+  in (idsource { _iorids = iorids' }, IORefId iorid)  -- | Get the next free 'MVarId'. nextMVId :: String -> IdSource -> (IdSource, MVarId)@@ -176,14 +176,14 @@ rewind (TakeMVar c _) = WillTakeMVar c rewind (BlockedTakeMVar c) = WillTakeMVar c rewind (TryTakeMVar c _ _) = WillTryTakeMVar c-rewind (NewCRef _) = WillNewCRef-rewind (ReadCRef c) = WillReadCRef c-rewind (ReadCRefCas c) = WillReadCRefCas c-rewind (ModCRef c) = WillModCRef c-rewind (ModCRefCas c) = WillModCRefCas c-rewind (WriteCRef c) = WillWriteCRef c-rewind (CasCRef c _) = WillCasCRef c-rewind (CommitCRef t c) = WillCommitCRef t c+rewind (NewIORef _) = WillNewIORef+rewind (ReadIORef c) = WillReadIORef c+rewind (ReadIORefCas c) = WillReadIORefCas c+rewind (ModIORef c) = WillModIORef c+rewind (ModIORefCas c) = WillModIORefCas c+rewind (WriteIORef c) = WillWriteIORef c+rewind (CasIORef c _) = WillCasIORef c+rewind (CommitIORef t c) = WillCommitIORef t c rewind (STM _ _) = WillSTM rewind (BlockedSTM _) = WillSTM rewind Catching = WillCatching@@ -224,21 +224,21 @@  -- | A simplified view of the possible actions a thread can perform. data ActionType =-    UnsynchronisedRead  CRefId-  -- ^ A 'readCRef' or a 'readForCAS'.-  | UnsynchronisedWrite CRefId-  -- ^ A 'writeCRef'.+    UnsynchronisedRead  IORefId+  -- ^ A 'readIORef' or a 'readForCAS'.+  | UnsynchronisedWrite IORefId+  -- ^ A 'writeIORef'.   | UnsynchronisedOther   -- ^ Some other action which doesn't require cross-thread   -- communication.-  | PartiallySynchronisedCommit CRefId+  | PartiallySynchronisedCommit IORefId   -- ^ A commit.-  | PartiallySynchronisedWrite  CRefId-  -- ^ A 'casCRef'-  | PartiallySynchronisedModify CRefId-  -- ^ A 'modifyCRefCAS'-  | SynchronisedModify  CRefId-  -- ^ An 'atomicModifyCRef'.+  | PartiallySynchronisedWrite  IORefId+  -- ^ A 'casIORef'+  | PartiallySynchronisedModify IORefId+  -- ^ A 'modifyIORefCAS'+  | SynchronisedModify  IORefId+  -- ^ An 'atomicModifyIORef'.   | SynchronisedRead    MVarId   -- ^ A 'readMVar' or 'takeMVar' (or @try@/@blocked@ variants).   | SynchronisedWrite   MVarId@@ -256,26 +256,26 @@ isBarrier SynchronisedOther = True isBarrier _ = False --- | Check if an action commits a given 'CRef'.-isCommit :: ActionType -> CRefId -> Bool+-- | Check if an action commits a given 'IORef'.+isCommit :: ActionType -> IORefId -> Bool isCommit (PartiallySynchronisedCommit c) r = c == r isCommit (PartiallySynchronisedWrite  c) r = c == r isCommit (PartiallySynchronisedModify c) r = c == r isCommit _ _ = False --- | Check if an action synchronises a given 'CRef'.-synchronises :: ActionType -> CRefId -> Bool+-- | Check if an action synchronises a given 'IORef'.+synchronises :: ActionType -> IORefId -> Bool synchronises a r = isCommit a r || isBarrier a --- | Get the 'CRef' affected.-crefOf :: ActionType -> Maybe CRefId-crefOf (UnsynchronisedRead  r) = Just r-crefOf (UnsynchronisedWrite r) = Just r-crefOf (SynchronisedModify  r) = Just r-crefOf (PartiallySynchronisedCommit r) = Just r-crefOf (PartiallySynchronisedWrite  r) = Just r-crefOf (PartiallySynchronisedModify r) = Just r-crefOf _ = Nothing+-- | Get the 'IORef' affected.+iorefOf :: ActionType -> Maybe IORefId+iorefOf (UnsynchronisedRead  r) = Just r+iorefOf (UnsynchronisedWrite r) = Just r+iorefOf (SynchronisedModify  r) = Just r+iorefOf (PartiallySynchronisedCommit r) = Just r+iorefOf (PartiallySynchronisedWrite  r) = Just r+iorefOf (PartiallySynchronisedModify r) = Just r+iorefOf _ = Nothing  -- | Get the 'MVar' affected. mvarOf :: ActionType -> Maybe MVarId@@ -291,7 +291,7 @@ tidsOf (TryPutMVar _ _ tids) = S.fromList tids tidsOf (TakeMVar _ tids) = S.fromList tids tidsOf (TryTakeMVar _ _ tids) = S.fromList tids-tidsOf (CommitCRef tid _) = S.singleton tid+tidsOf (CommitIORef tid _) = S.singleton tid tidsOf (STM _ tids) = S.fromList tids tidsOf (ThrowTo tid _) = S.singleton tid tidsOf (BlockedThrowTo tid) = S.singleton tid@@ -313,13 +313,13 @@ simplifyLookahead (WillTryReadMVar c) = SynchronisedRead c simplifyLookahead (WillTakeMVar c)    = SynchronisedRead c simplifyLookahead (WillTryTakeMVar c)  = SynchronisedRead c-simplifyLookahead (WillReadCRef r)     = UnsynchronisedRead r-simplifyLookahead (WillReadCRefCas r)  = UnsynchronisedRead r-simplifyLookahead (WillModCRef r)      = SynchronisedModify r-simplifyLookahead (WillModCRefCas r)   = PartiallySynchronisedModify r-simplifyLookahead (WillWriteCRef r)    = UnsynchronisedWrite r-simplifyLookahead (WillCasCRef r)      = PartiallySynchronisedWrite r-simplifyLookahead (WillCommitCRef _ r) = PartiallySynchronisedCommit r+simplifyLookahead (WillReadIORef r)     = UnsynchronisedRead r+simplifyLookahead (WillReadIORefCas r)  = UnsynchronisedRead r+simplifyLookahead (WillModIORef r)      = SynchronisedModify r+simplifyLookahead (WillModIORefCas r)   = PartiallySynchronisedModify r+simplifyLookahead (WillWriteIORef r)    = UnsynchronisedWrite r+simplifyLookahead (WillCasIORef r)      = PartiallySynchronisedWrite r+simplifyLookahead (WillCommitIORef _ r) = PartiallySynchronisedCommit r simplifyLookahead WillSTM         = SynchronisedOther simplifyLookahead (WillThrowTo _) = SynchronisedOther simplifyLookahead _ = UnsynchronisedOther@@ -393,8 +393,8 @@   => (n () -> x)   -> (a -> Maybe b)   -> ((a -> x) -> x)-  -> n (x, C.CRef n (Maybe b))+  -> n (x, C.IORef n (Maybe b)) runRefCont act f k = do-  ref <- C.newCRef Nothing-  let c = k (act . C.writeCRef ref . f)+  ref <- C.newIORef Nothing+  let c = k (act . C.writeIORef ref . f)   pure (c, ref)

@@ -69,7 +69,7 @@   => Way   -- ^ How to run the concurrent program.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ConcT n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)]@@ -82,7 +82,7 @@   => Way   -- ^ How to run the concurrent program.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ConcT n a   -- ^ The computation to run many times.   -> n (Set (Either Failure a))@@ -100,7 +100,7 @@   -> Way   -- ^ How to run the concurrent program.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ConcT n a   -- ^ The computation to run many times.   -> n [(Either Failure a, Trace)]@@ -116,7 +116,7 @@   -> Way   -- ^ How to run the concurrent program.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> ConcT n a   -- ^ The computation to run many times.   -> n (Set (Either Failure a))@@ -373,7 +373,7 @@ -- @since 1.0.0.0 sctBound :: MonadConc n   => MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> Bounds   -- ^ The combined bounds.   -> ConcT n a@@ -392,7 +392,7 @@   => (Either Failure a -> Maybe Discard)   -- ^ Selectively discard results.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> Bounds   -- ^ The combined bounds.   -> ConcT n a@@ -412,7 +412,7 @@ -- @since 1.0.0.0 sctUniformRandom :: (MonadConc n, RandomGen g)   => MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> g   -- ^ The random number generator.   -> Int@@ -433,7 +433,7 @@   => (Either Failure a -> Maybe Discard)   -- ^ Selectively discard results.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> g   -- ^ The random number generator.   -> Int@@ -455,7 +455,7 @@ -- @since 1.7.0.0 sctWeightedRandom :: (MonadConc n, RandomGen g)   => MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> g   -- ^ The random number generator.   -> Int@@ -476,7 +476,7 @@   => (Either Failure a -> Maybe Discard)   -- ^ Selectively discard results.   -> MemType-  -- ^ The memory model to use for non-synchronised @CRef@ operations.+  -- ^ The memory model to use for non-synchronised @IORef@ operations.   -> g   -- ^ The random number generator.   -> Int@@ -533,7 +533,7 @@  -- | Determine if an action is a commit or not. isCommitRef :: ThreadAction -> Bool-isCommitRef (CommitCRef _ _) = True+isCommitRef (CommitIORef _ _) = True isCommitRef _ = False  -- | Get the maximum difference between two ints in a list.

@@ -70,8 +70,8 @@       sfun       (srun (runSnap snap))       (runSnap snap)-      (toId $ 1 + fst (_tids  idsrc))-      (toId $ 1 + fst (_crids idsrc))+      (toId $ 1 + fst (_tids idsrc))+      (toId $ 1 + fst (_iorids idsrc))      runFull sched s = runConcurrent sched (_memtype settings) s conc     runSnap snap sched s = runWithDCSnapshot sched (_memtype settings) s snap@@ -93,8 +93,8 @@   -- ^ Just run the computation   -> ThreadId   -- ^ The first available @ThreadId@-  -> CRefId-  -- ^ The first available @CRefId@+  -> IORefId+  -- ^ The first available @IORefId@   -> n [(Either Failure a, Trace)] sct' settings s0 sfun srun run nTId nCRId = go Nothing [] s0 where   go (Just res) _ _ | earlyExit res = pure []@@ -154,8 +154,8 @@   -- ^ Just run the computation   -> ThreadId   -- ^ The first available @ThreadId@-  -> CRefId-  -- ^ The first available @CRefId@+  -> IORefId+  -- ^ The first available @IORefId@   -> Either Failure a   -- ^ The expected result   -> Trace@@ -244,7 +244,7 @@ dropCommits :: Bool -> MemType -> [(ThreadId, ThreadAction)] -> [(ThreadId, ThreadAction)] dropCommits _ SequentialConsistency = id dropCommits safeIO memtype = go initialDepState where-  go ds (t1@(tid1, ta1@(CommitCRef _ _)):t2@(tid2, ta2):trc)+  go ds (t1@(tid1, ta1@(CommitIORef _ _)):t2@(tid2, ta2):trc)     | isBarrier (simplifyAction ta2) = go ds (t2:trc)     | independent safeIO ds tid1 ta1 tid2 ta2 = t2 : go (updateDepState memtype ds tid2 ta2) (t1:trc)   go ds (t@(tid,ta):trc) = t : go (updateDepState memtype ds tid ta) trc@@ -302,11 +302,11 @@       | otherwise = Nothing     fgo _ _ = Nothing --- | Re-number threads and CRefs.+-- | Re-number threads and IORefs. ----- Permuting forks or newCRefs makes the existing numbering invalid,+-- Permuting forks or newIORefs makes the existing numbering invalid, -- which then causes problems for scheduling.  Just re-numbering--- threads isn't enough, as CRef IDs are used to determine commit+-- threads isn't enough, as IORef IDs are used to determine commit -- thread IDs. -- -- Renumbered things will not fix their names, so don't rely on those@@ -317,14 +317,14 @@   -> Int   -- ^ First free thread ID.   -> Int-  -- ^ First free @CRef@ ID.+  -- ^ First free @IORef@ ID.   -> [(ThreadId, ThreadAction)]   -> [(ThreadId, ThreadAction)] renumber memtype tid0 crid0 = snd . mapAccumL go (I.empty, tid0, I.empty, crid0) where-  go s@(tidmap, _, cridmap, _) (_, CommitCRef tid crid) =+  go s@(tidmap, _, cridmap, _) (_, CommitIORef tid crid) =     let tid'  = renumbered tidmap  tid         crid' = renumbered cridmap crid-        act' = CommitCRef tid' crid'+        act' = CommitIORef tid' crid'     in case memtype of          PartialStoreOrder -> (s, (commitThreadId tid' (Just crid'), act'))          _ -> (s, (commitThreadId tid' Nothing, act'))@@ -351,22 +351,22 @@     (s, TakeMVar mvid (map (renumbered tidmap) olds))   updateAction s@(tidmap, _, _, _) (TryTakeMVar mvid b olds) =     (s, TryTakeMVar mvid b (map (renumbered tidmap) olds))-  updateAction (tidmap, nTId, cridmap, nCRId) (NewCRef old) =+  updateAction (tidmap, nTId, cridmap, nCRId) (NewIORef old) =     let cridmap' = I.insert (fromId old) nCRId cridmap         nCRId' = nCRId + 1-    in ((tidmap, nTId, cridmap', nCRId'), NewCRef (toId nCRId))-  updateAction s@(_, _, cridmap, _) (ReadCRef old) =-    (s, ReadCRef (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (ReadCRefCas old) =-    (s, ReadCRefCas (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (ModCRef old) =-    (s, ModCRef (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (ModCRefCas old) =-    (s, ModCRefCas (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (WriteCRef old) =-    (s, WriteCRef (renumbered cridmap old))-  updateAction s@(_, _, cridmap, _) (CasCRef old b) =-    (s, CasCRef (renumbered cridmap old) b)+    in ((tidmap, nTId, cridmap', nCRId'), NewIORef (toId nCRId))+  updateAction s@(_, _, cridmap, _) (ReadIORef old) =+    (s, ReadIORef (renumbered cridmap old))+  updateAction s@(_, _, cridmap, _) (ReadIORefCas old) =+    (s, ReadIORefCas (renumbered cridmap old))+  updateAction s@(_, _, cridmap, _) (ModIORef old) =+    (s, ModIORef (renumbered cridmap old))+  updateAction s@(_, _, cridmap, _) (ModIORefCas old) =+    (s, ModIORefCas (renumbered cridmap old))+  updateAction s@(_, _, cridmap, _) (WriteIORef old) =+    (s, WriteIORef (renumbered cridmap old))+  updateAction s@(_, _, cridmap, _) (CasIORef old b) =+    (s, CasIORef (renumbered cridmap old) b)   updateAction s@(tidmap, _, _, _) (STM tas olds) =     (s, STM tas (map (renumbered tidmap) olds))   updateAction s@(tidmap, _, _, _) (ThrowTo old b) =

@@ -572,7 +572,7 @@     -- See #191 / #190     check _ (ThrowTo t _) tid _ | t == tid = True     check _ (BlockedThrowTo t) tid _ | t == tid = True-    -- can't re-order an unsynchronised write with something which synchronises that CRef.+    -- can't re-order an unsynchronised write with something which synchronises that IORef.     check _ (simplifyAction -> UnsynchronisedWrite r) _ (simplifyAction -> a) | synchronises a r = True     check _ _ _ _ = False @@ -674,14 +674,14 @@   (SynchronisedWrite v1, SynchronisedRead  v2) | v1 == v2 -> True   (SynchronisedRead  v1, SynchronisedWrite v2) | v1 == v2 -> True -  (_, _) -> maybe False (\r -> Just r == crefOf a2) (crefOf a1)+  (_, _) -> maybe False (\r -> Just r == iorefOf a2) (iorefOf a1)  ------------------------------------------------------------------------------- -- ** Dependency function state  data DepState = DepState-  { depCRState :: Map CRefId Bool-  -- ^ Keep track of which @CRef@s have buffered writes.+  { depIOState :: Map IORefId Bool+  -- ^ Keep track of which @IORef@s have buffered writes.   , depMVState :: Set MVarId   -- ^ Keep track of which @MVar@s are full.   , depMaskState :: Map ThreadId MaskingState@@ -692,7 +692,7 @@   } deriving (Eq, Show)  instance NFData DepState where-  rnf depstate = rnf ( depCRState depstate+  rnf depstate = rnf ( depIOState depstate                      , depMVState depstate                      , [(t, m `seq` ()) | (t, m) <- M.toList (depMaskState depstate)]                      )@@ -705,17 +705,17 @@ -- happened. updateDepState :: MemType -> DepState -> ThreadId -> ThreadAction -> DepState updateDepState memtype depstate tid act = DepState-  { depCRState   = updateCRState memtype act $ depCRState   depstate+  { depIOState   = updateCRState memtype act $ depIOState   depstate   , depMVState   = updateMVState         act $ depMVState   depstate   , depMaskState = updateMaskState tid   act $ depMaskState depstate   } --- | Update the @CRef@ buffer state with the action that has just+-- | Update the @IORef@ buffer state with the action that has just -- happened.-updateCRState :: MemType -> ThreadAction -> Map CRefId Bool -> Map CRefId Bool+updateCRState :: MemType -> ThreadAction -> Map IORefId Bool -> Map IORefId Bool updateCRState SequentialConsistency _ = const M.empty-updateCRState _ (CommitCRef _ r) = M.delete r-updateCRState _ (WriteCRef    r) = M.insert r True+updateCRState _ (CommitIORef _ r) = M.delete r+updateCRState _ (WriteIORef    r) = M.insert r True updateCRState _ ta   | isBarrier $ simplifyAction ta = const M.empty   | otherwise = id@@ -743,9 +743,9 @@ updateMaskState tid Stop = M.delete tid updateMaskState _ _ = id --- | Check if a @CRef@ has a buffered write pending.-isBuffered :: DepState -> CRefId -> Bool-isBuffered depstate r = M.findWithDefault False r (depCRState depstate)+-- | Check if a @IORef@ has a buffered write pending.+isBuffered :: DepState -> IORefId -> Bool+isBuffered depstate r = M.findWithDefault False r (depIOState depstate)  -- | Check if an @MVar@ is full. isFull :: DepState -> MVarId -> Bool

@@ -59,22 +59,22 @@    -- ** The @MemType@ -  -- | When executed on a multi-core processor some @CRef@ / @IORef@+  -- | When executed on a multi-core processor some @IORef@ / @IORef@   -- programs can exhibit \"relaxed memory\" behaviours, where the   -- apparent behaviour of the program is not a simple interleaving of   -- the actions of each thread.   ---  -- __Example:__ This is a simple program which creates two @CRef@s+  -- __Example:__ This is a simple program which creates two @IORef@s   -- containing @False@, and forks two threads.  Each thread writes-  -- @True@ to one of the @CRef@s and reads the other.  The value that+  -- @True@ to one of the @IORef@s and reads the other.  The value that   -- each thread reads is communicated back through an @MVar@:   --   -- > >>> :{   -- > let relaxed = do-  -- >       r1 <- newCRef False-  -- >       r2 <- newCRef False-  -- >       x <- spawn $ writeCRef r1 True >> readCRef r2-  -- >       y <- spawn $ writeCRef r2 True >> readCRef r1+  -- >       r1 <- newIORef False+  -- >       r2 <- newIORef False+  -- >       x <- spawn $ writeIORef r1 True >> readIORef r2+  -- >       y <- spawn $ writeIORef r2 True >> readIORef r1   -- >       (,) <$> readMVar x <*> readMVar y   -- > :}   --@@ -94,12 +94,12 @@   -- > False   --   -- It's possible for both threads to read the value @False@, even-  -- though each writes @True@ to the other @CRef@ before reading.+  -- though each writes @True@ to the other @IORef@ before reading.   -- This is because processors are free to re-order reads and writes   -- to independent memory addresses in the name of performance.   --   -- Execution traces for relaxed memory computations can include-  -- \"C\" actions, as above, which show where @CRef@ writes were+  -- \"C\" actions, as above, which show where @IORef@ writes were   -- explicitly /committed/, and made visible to other threads.   --   -- However, modelling this behaviour can require more executions.

@@ -39,17 +39,14 @@ -- | @since 1.3.1.0 deriving instance Generic ThreadId --- | Every @CRef@ has a unique identifier.+-- | Every @IORef@ has a unique identifier. ----- @since 1.0.0.0-newtype CRefId = CRefId Id-  deriving (Eq, Ord, NFData)--instance Show CRefId where-  show (CRefId id_) = show id_+-- @since 1.11.0.0+newtype IORefId = IORefId Id+  deriving (Eq, Ord, NFData, Generic) --- | @since 1.3.1.0-deriving instance Generic CRefId+instance Show IORefId where+  show (IORefId id_) = show id_  -- | Every @MVar@ has a unique identifier. --@@ -75,7 +72,7 @@ -- | @since 1.3.1.0 deriving instance Generic TVarId --- | An identifier for a thread, @MVar@, @CRef@, or @TVar@.+-- | An identifier for a thread, @MVar@, @IORef@, or @TVar@. -- -- The number is the important bit.  The string is to make execution -- traces easier to read, but is meaningless.@@ -109,7 +106,7 @@  -- | All the actions that a thread can perform. ----- @since 1.9.0.0+-- @since 1.11.0.0 data ThreadAction =     Fork ThreadId   -- ^ Start a new thread.@@ -147,23 +144,23 @@   -- ^ Get blocked on a take.   | TryTakeMVar MVarId Bool [ThreadId]   -- ^ Try to take from a 'MVar', possibly waking up some threads.-  | NewCRef CRefId-  -- ^ Create a new 'CRef'.-  | ReadCRef CRefId-  -- ^ Read from a 'CRef'.-  | ReadCRefCas CRefId-  -- ^ Read from a 'CRef' for a future compare-and-swap.-  | ModCRef CRefId-  -- ^ Modify a 'CRef'.-  | ModCRefCas CRefId-  -- ^ Modify a 'CRef' using a compare-and-swap.-  | WriteCRef CRefId-  -- ^ Write to a 'CRef' without synchronising.-  | CasCRef CRefId Bool-  -- ^ Attempt to to a 'CRef' using a compare-and-swap, synchronising+  | NewIORef IORefId+  -- ^ Create a new 'IORef'.+  | ReadIORef IORefId+  -- ^ Read from a 'IORef'.+  | ReadIORefCas IORefId+  -- ^ Read from a 'IORef' for a future compare-and-swap.+  | ModIORef IORefId+  -- ^ Modify a 'IORef'.+  | ModIORefCas IORefId+  -- ^ Modify a 'IORef' using a compare-and-swap.+  | WriteIORef IORefId+  -- ^ Write to a 'IORef' without synchronising.+  | CasIORef IORefId Bool+  -- ^ Attempt to to a 'IORef' using a compare-and-swap, synchronising   -- it.-  | CommitCRef ThreadId CRefId-  -- ^ Commit the last write to the given 'CRef' by the given thread,+  | CommitIORef ThreadId IORefId+  -- ^ Commit the last write to the given 'IORef' by the given thread,   -- so that all threads can see the updated value.   | STM [TAction] [ThreadId]   -- ^ An STM transaction was executed, possibly waking up some@@ -203,10 +200,7 @@   -- ^ Stop executing an action with @subconcurrency@.   | DontCheck Trace   -- ^ Execute an action with @dontCheck@.-  deriving (Eq, Show)---- | @since 1.3.1.0-deriving instance Generic ThreadAction+  deriving (Eq, Generic, Show)  -- this makes me sad instance NFData ThreadAction where@@ -228,14 +222,14 @@   rnf (TakeMVar m ts) = rnf (m, ts)   rnf (BlockedTakeMVar m) = rnf m   rnf (TryTakeMVar m b ts) = rnf (m, b, ts)-  rnf (NewCRef c) = rnf c-  rnf (ReadCRef c) = rnf c-  rnf (ReadCRefCas c) = rnf c-  rnf (ModCRef c) = rnf c-  rnf (ModCRefCas c) = rnf c-  rnf (WriteCRef c) = rnf c-  rnf (CasCRef c b) = rnf (c, b)-  rnf (CommitCRef t c) = rnf (t, c)+  rnf (NewIORef c) = rnf c+  rnf (ReadIORef c) = rnf c+  rnf (ReadIORefCas c) = rnf c+  rnf (ModIORef c) = rnf c+  rnf (ModIORefCas c) = rnf c+  rnf (WriteIORef c) = rnf c+  rnf (CasIORef c b) = rnf (c, b)+  rnf (CommitIORef t c) = rnf (t, c)   rnf (STM as ts) = rnf (as, ts)   rnf (BlockedSTM as) = rnf as   rnf Catching = ()@@ -254,7 +248,7 @@  -- | A one-step look-ahead at what a thread will do next. ----- @since 1.1.0.0+-- @since 1.11.0.0 data Lookahead =     WillFork   -- ^ Will start a new thread.@@ -288,23 +282,23 @@   -- ^ Will take from a 'MVar', possibly waking up some threads.   | WillTryTakeMVar MVarId   -- ^ Will try to take from a 'MVar', possibly waking up some threads.-  | WillNewCRef-  -- ^ Will create a new 'CRef'.-  | WillReadCRef CRefId-  -- ^ Will read from a 'CRef'.-  | WillReadCRefCas CRefId-  -- ^ Will read from a 'CRef' for a future compare-and-swap.-  | WillModCRef CRefId-  -- ^ Will modify a 'CRef'.-  | WillModCRefCas CRefId-  -- ^ Will modify a 'CRef' using a compare-and-swap.-  | WillWriteCRef CRefId-  -- ^ Will write to a 'CRef' without synchronising.-  | WillCasCRef CRefId-  -- ^ Will attempt to to a 'CRef' using a compare-and-swap,+  | WillNewIORef+  -- ^ Will create a new 'IORef'.+  | WillReadIORef IORefId+  -- ^ Will read from a 'IORef'.+  | WillReadIORefCas IORefId+  -- ^ Will read from a 'IORef' for a future compare-and-swap.+  | WillModIORef IORefId+  -- ^ Will modify a 'IORef'.+  | WillModIORefCas IORefId+  -- ^ Will modify a 'IORef' using a compare-and-swap.+  | WillWriteIORef IORefId+  -- ^ Will write to a 'IORef' without synchronising.+  | WillCasIORef IORefId+  -- ^ Will attempt to to a 'IORef' using a compare-and-swap,   -- synchronising it.-  | WillCommitCRef ThreadId CRefId-  -- ^ Will commit the last write by the given thread to the 'CRef'.+  | WillCommitIORef ThreadId IORefId+  -- ^ Will commit the last write by the given thread to the 'IORef'.   | WillSTM   -- ^ Will execute an STM transaction, possibly waking up some   -- threads.@@ -337,10 +331,7 @@   -- ^ Will stop executing an extion with @subconcurrency@.   | WillDontCheck   -- ^ Will execute an action with @dontCheck@.-  deriving (Eq, Show)---- | @since 1.3.1.0-deriving instance Generic Lookahead+  deriving (Eq, Generic, Show)  -- this also makes me sad instance NFData Lookahead where@@ -359,14 +350,14 @@   rnf (WillTryReadMVar m) = rnf m   rnf (WillTakeMVar m) = rnf m   rnf (WillTryTakeMVar m) = rnf m-  rnf WillNewCRef = ()-  rnf (WillReadCRef c) = rnf c-  rnf (WillReadCRefCas c) = rnf c-  rnf (WillModCRef c) = rnf c-  rnf (WillModCRefCas c) = rnf c-  rnf (WillWriteCRef c) = rnf c-  rnf (WillCasCRef c) = rnf c-  rnf (WillCommitCRef t c) = rnf (t, c)+  rnf WillNewIORef = ()+  rnf (WillReadIORef c) = rnf c+  rnf (WillReadIORefCas c) = rnf c+  rnf (WillModIORef c) = rnf c+  rnf (WillModIORefCas c) = rnf c+  rnf (WillWriteIORef c) = rnf c+  rnf (WillCasIORef c) = rnf c+  rnf (WillCommitIORef t c) = rnf (t, c)   rnf WillSTM = ()   rnf WillCatching = ()   rnf WillPopCatching = ()@@ -715,13 +706,13 @@ ------------------------------------------------------------------------------- -- * Memory Models --- | The memory model to use for non-synchronised 'CRef' operations.+-- | The memory model to use for non-synchronised 'IORef' operations. -- -- @since 0.4.0.0 data MemType =     SequentialConsistency   -- ^ The most intuitive model: a program behaves as a simple-  -- interleaving of the actions in different threads. When a 'CRef'+  -- interleaving of the actions in different threads. When a 'IORef'   -- is written to, that write is immediately visible to all threads.   | TotalStoreOrder   -- ^ Each thread has a write buffer. A thread sees its writes@@ -729,9 +720,9 @@   -- committed, which may happen later. Writes are committed in the   -- same order that they are created.   | PartialStoreOrder-  -- ^ Each 'CRef' has a write buffer. A thread sees its writes+  -- ^ Each 'IORef' has a write buffer. A thread sees its writes   -- immediately, but other threads will only see writes when they are-  -- committed, which may happen later. Writes to different 'CRef's+  -- committed, which may happen later. Writes to different 'IORef's   -- are not necessarily committed in the same order that they are   -- created.   deriving (Eq, Show, Read, Ord, Enum, Bounded)

@@ -34,7 +34,7 @@ showTrace :: Trace -> String showTrace []  = "<trace discarded>" showTrace trc = intercalate "\n" $ go False trc : strkey where-  go _ ((_,_,CommitCRef _ _):rest) = "C-" ++ go False rest+  go _ ((_,_,CommitIORef _ _):rest) = "C-" ++ go False rest   go _ ((Start    (ThreadId (Id _ i)),_,a):rest) = "S" ++ show i ++ "-" ++ go (didYield a) rest   go y ((SwitchTo (ThreadId (Id _ i)),_,a):rest) = (if y then "p" else "P") ++ show i ++ "-" ++ go (didYield a) rest   go _ ((Continue,_,a):rest) = '-' : go (didYield a) rest@@ -63,7 +63,7 @@   choose  = minimumBy . comparing $ \(_, trc) ->     let switchTos = length . filter (\(d,_,_) -> case d of SwitchTo _ -> True; _ -> False)         starts    = length . filter (\(d,_,_) -> case d of Start    _ -> True; _ -> False)-        commits   = length . filter (\(_,_,a) -> case a of CommitCRef _ _ -> True; _ -> False)+        commits   = length . filter (\(_,_,a) -> case a of CommitIORef _ _ -> True; _ -> False)     in (switchTos trc, commits trc, length trc, starts trc)    groupBy' res _ [] = res

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                dejafu-version:             1.10.1.0+version:             1.11.0.0 synopsis:            A library for unit-testing concurrent programs.  description:@@ -33,7 +33,7 @@ source-repository this   type:     git   location: https://github.com/barrucadu/dejafu.git-  tag:      dejafu-1.10.1.0+  tag:      dejafu-1.11.0.0  library   exposed-modules:     Test.DejaFu@@ -58,7 +58,7 @@   -- other-modules:          -- other-extensions:       build-depends:       base              >=4.9 && <5-                     , concurrency       >=1.5 && <1.6+                     , concurrency       >=1.6 && <1.7                      , containers        >=0.5 && <0.6                      , contravariant     >=1.2 && <1.5                      , deepseq           >=1.1 && <2