rawlock 0.1.1.0 → 0.1.2.0

raw patch · 4 files changed

+342/−308 lines, 4 filesdep −strict-mvardep −strict-stmdep ~basedep ~io-classesdep ~nothunksPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies removed: strict-mvar, strict-stm

Dependency ranges changed: base, io-classes, nothunks

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• rawlock.cabal +6/−9
• src/Control/RAWLock.hs +106/−94
• test/Main.hs +226/−205

@@ -2,6 +2,10 @@  # Changelog entries +## 0.1.2.0 — 2025-05-15++* Use `io-classes-1.8`.+ ## 0.1.1.0 -- 2024-11-22  * Added `Generic` and `NoThunks` instance for `RAWState`.

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: rawlock-version: 0.1.1.0+version: 0.1.2.0 synopsis: A writer-biased RAW lock. description:   A writer-biased RAW lock.@@ -26,7 +26,7 @@   README.md  bug-reports: https://github.com/IntersectMBO/io-classes-extra/issues-tested-with: ghc ==8.10 || ==9.2 || ==9.4 || ==9.6 || ==9.8 || ==9.10+tested-with: ghc ==9.6 || ==9.8 || ==9.10 || ==9.12  source-repository head   type: git@@ -37,7 +37,7 @@   type: git   location: https://github.com/IntersectMBO/io-classes-extra   subdir: rawlock-  tag: rawlock-0.1.0.0+  tag: rawlock-0.1.2.0  common warnings   ghc-options:@@ -59,11 +59,9 @@   exposed-modules: Control.RAWLock   default-extensions: ImportQualifiedPost   build-depends:-    base >=4.14 && <4.21,-    io-classes ^>=1.5,+    base >=4.18 && <4.22,+    io-classes:{io-classes, strict-mvar, strict-stm} ^>=1.8,     nothunks ^>=0.2,-    strict-mvar ^>=1.5,-    strict-stm ^>=1.5,  test-suite rawlock-test   import: warnings@@ -74,10 +72,9 @@   build-depends:     QuickCheck,     base,-    io-classes,+    io-classes:{io-classes, strict-stm},     io-sim,     mtl,     rawlock,-    strict-stm,     tasty,     tasty-quickcheck,

@@ -109,8 +109,8 @@ --    'NoThunks' check when enabled. -- --  * All public functions are exception-safe.-module Control.RAWLock (-    -- * API+module Control.RAWLock+  ( -- * API     RAWLock   , new   , poison@@ -118,6 +118,7 @@   , withAppendAccess   , withReadAccess   , withWriteAccess+     -- * Unsafe API     -- $unsafe-api   , unsafeAcquireAppendAccess@@ -139,31 +140,32 @@ -- | Any non-negative number of readers newtype Readers = Readers Word   deriving newtype (Eq, Ord, Enum, Num, NoThunks)-  deriving stock (Show)+  deriving stock Show  -- | Any non-negative number of writers newtype Writers = Writers Word   deriving newtype (Eq, Ord, Enum, Num, NoThunks)-  deriving stock (Show)+  deriving stock Show  -- | Any non-negative number of appenders newtype Appenders = Appenders Word   deriving newtype (Eq, Ord, Enum, Num, NoThunks)-  deriving stock (Show)+  deriving stock Show -data RAWState = RAWState {-    waitingReaders   :: !Readers+data RAWState = RAWState+  { waitingReaders :: !Readers   , waitingAppenders :: !Appenders-  , waitingWriters   :: !Writers-  } deriving (Show, Generic, NoThunks)+  , waitingWriters :: !Writers+  }+  deriving (Show, Generic, NoThunks)  noWriters :: Poisonable RAWState -> Bool noWriters (Healthy (RAWState _ _ w)) = w == 0-noWriters _                          = True+noWriters _ = True  onlyWriters :: Poisonable RAWState -> Bool onlyWriters (Healthy (RAWState r a _)) = r == 0 && a == 0-onlyWriters _                          = True+onlyWriters _ = True  pushReader :: Poisonable RAWState -> Poisonable RAWState pushReader = fmap (\(RAWState r a w) -> RAWState (r + 1) a w)@@ -185,28 +187,31 @@  -- | Data that can be replaced with an exception that should be thrown when -- found.-data Poisonable st =-    Healthy !st+data Poisonable st+  = Healthy !st   | Poisoned !(AllowThunk SomeException)   deriving (Generic, NoThunks, Functor) -data RAWLock m st = RAWLock {-    resource :: !(StrictTMVar m (Poisonable st))+data RAWLock m st = RAWLock+  { resource :: !(StrictTMVar m (Poisonable st))   , appender :: !(StrictMVar m ())-  , queues   :: !(StrictTVar m (Poisonable RAWState))-  } deriving (Generic)+  , queues :: !(StrictTVar m (Poisonable RAWState))+  }+  deriving Generic -deriving instance ( NoThunks (StrictTMVar m (Poisonable st))-                  , NoThunks (StrictMVar m ())-                  , NoThunks (StrictTVar m (Poisonable RAWState))-                  ) => NoThunks (RAWLock m st)+deriving instance+  ( NoThunks (StrictTMVar m (Poisonable st))+  , NoThunks (StrictMVar m ())+  , NoThunks (StrictTVar m (Poisonable RAWState))+  ) =>+  NoThunks (RAWLock m st)  new ::-     ( MonadMVar m-     , MonadLabelledSTM m-     )-  => st-  -> m (RAWLock m st)+  ( MonadMVar m+  , MonadLabelledSTM m+  ) =>+  st ->+  m (RAWLock m st) new !st = do   s <- newTMVarIO (Healthy st)   atomically $ labelTMVar s "state"@@ -226,23 +231,24 @@ -- There is no need (although it is harmless) to release again the current -- actor once it has poisoned the lock. poison ::-     (Exception e, MonadMVar m, MonadSTM m, MonadThrow (STM m), HasCallStack)-  => RAWLock m st-  -> (CallStack -> e)-  -> m (Maybe st)+  (Exception e, MonadMVar m, MonadSTM m, MonadThrow (STM m), HasCallStack) =>+  RAWLock m st ->+  (CallStack -> e) ->+  m (Maybe st) poison (RAWLock var apm q) mkExc = do-  st <- atomically $-    tryReadTMVar var >>= \case-      -- Keep original exception-      Just (Poisoned (AllowThunk exc)) -> throwIO exc-      Just (Healthy st) -> do-        writeTMVar var (Poisoned (AllowThunk (toException (mkExc callStack))))-        writeTVar q (Poisoned (AllowThunk (toException (mkExc callStack))))-        pure (Just st)-      Nothing -> do-        writeTMVar var (Poisoned (AllowThunk (toException (mkExc callStack))))-        writeTVar q (Poisoned (AllowThunk (toException (mkExc callStack))))-        pure Nothing+  st <-+    atomically $+      tryReadTMVar var >>= \case+        -- Keep original exception+        Just (Poisoned (AllowThunk exc)) -> throwIO exc+        Just (Healthy st) -> do+          writeTMVar var (Poisoned (AllowThunk (toException (mkExc callStack))))+          writeTVar q (Poisoned (AllowThunk (toException (mkExc callStack))))+          pure (Just st)+        Nothing -> do+          writeTMVar var (Poisoned (AllowThunk (toException (mkExc callStack))))+          writeTVar q (Poisoned (AllowThunk (toException (mkExc callStack))))+          pure Nothing   _ <- tryPutMVar apm ()   pure st @@ -256,10 +262,10 @@ -- Will block when there is a writer or when a writer is waiting to take the -- lock. withReadAccess ::-     (MonadSTM m, MonadCatch m, MonadThrow (STM m))-  => RAWLock m st-  -> (st -> m a)-  -> m a+  (MonadSTM m, MonadCatch m, MonadThrow (STM m)) =>+  RAWLock m st ->+  (st -> m a) ->+  m a withReadAccess lock =   bracket     (atomically (unsafeAcquireReadAccess lock))@@ -269,42 +275,44 @@ -- -- Will block when there is another writer, readers or appenders. withWriteAccess ::-     (MonadSTM m, MonadCatch m, MonadThrow (STM m))-  => RAWLock m st-  -> (st -> m (a, st))-  -> m a+  (MonadSTM m, MonadCatch m, MonadThrow (STM m)) =>+  RAWLock m st ->+  (st -> m (a, st)) ->+  m a withWriteAccess lock f =-  fst . fst <$> generalBracket-   (unsafeAcquireWriteAccess lock)-   (\orig -> \case-       ExitCaseSuccess (_, st) -> unsafeReleaseWriteAccess lock st-       _ -> unsafeReleaseWriteAccess lock orig-   )-   f+  fst . fst+    <$> generalBracket+      (unsafeAcquireWriteAccess lock)+      ( \orig -> \case+          ExitCaseSuccess (_, st) -> unsafeReleaseWriteAccess lock st+          _ -> unsafeReleaseWriteAccess lock orig+      )+      f  -- | Acquire the 'RAWLock' as an appender. -- -- Will block when there is a writer or when there is another appender. withAppendAccess ::-     (MonadThrow (STM m), MonadSTM m, MonadCatch m, MonadMVar m)-  => RAWLock m st-  -> (st -> m (a, st))-  -> m a+  (MonadThrow (STM m), MonadSTM m, MonadCatch m, MonadMVar m) =>+  RAWLock m st ->+  (st -> m (a, st)) ->+  m a withAppendAccess lock f = do-  fst . fst <$> generalBracket-   (unsafeAcquireAppendAccess lock)-   (\orig -> \case-       ExitCaseSuccess (_, st) -> unsafeReleaseAppendAccess lock st-       _ -> unsafeReleaseAppendAccess lock orig-   )-   f+  fst . fst+    <$> generalBracket+      (unsafeAcquireAppendAccess lock)+      ( \orig -> \case+          ExitCaseSuccess (_, st) -> unsafeReleaseAppendAccess lock st+          _ -> unsafeReleaseAppendAccess lock orig+      )+      f  {-------------------------------------------------------------------------------   Unsafe API -------------------------------------------------------------------------------}  throwPoisoned :: MonadThrow m => Poisonable st -> m st-throwPoisoned (Healthy st)                = pure st+throwPoisoned (Healthy st) = pure st throwPoisoned (Poisoned (AllowThunk exc)) = throwIO exc  -- $unsafe-api@@ -320,9 +328,9 @@ -- presence of an exception!  unsafeAcquireReadAccess ::-     (MonadThrow (STM m), MonadSTM m)-  => RAWLock m st-  -> STM m st+  (MonadThrow (STM m), MonadSTM m) =>+  RAWLock m st ->+  STM m st unsafeAcquireReadAccess (RAWLock var _ qs) = do   -- wait until there are no writers   readTVar qs >>= check . noWriters@@ -337,9 +345,9 @@   modifyTVar qs popReader  unsafeAcquireWriteAccess ::-     (MonadThrow (STM m), MonadCatch m, MonadSTM m)-  => RAWLock m st-  -> m st+  (MonadThrow (STM m), MonadCatch m, MonadSTM m) =>+  RAWLock m st ->+  m st unsafeAcquireWriteAccess (RAWLock var _ qs) = do   -- queue myself if there are no other writers   atomically $ do@@ -347,18 +355,21 @@     readTVar qs >>= check . noWriters     -- queue myself     modifyTVar qs pushWriter-  atomically (do-    -- wait until there are no readers (and as I queued myself above, I'm the-    -- only waiting writer)-    readTVar qs >>= check . onlyWriters-    -- acquire the state-    throwPoisoned =<< takeTMVar var) `onException` atomically (modifyTVar qs popWriter)+  atomically+    ( do+        -- wait until there are no readers (and as I queued myself above, I'm the+        -- only waiting writer)+        readTVar qs >>= check . onlyWriters+        -- acquire the state+        throwPoisoned =<< takeTMVar var+    )+    `onException` atomically (modifyTVar qs popWriter)  unsafeReleaseWriteAccess ::-     (MonadThrow (STM m), MonadSTM m)-  => RAWLock m st-  -> st-  -> m ()+  (MonadThrow (STM m), MonadSTM m) =>+  RAWLock m st ->+  st ->+  m () unsafeReleaseWriteAccess (RAWLock var _ qs) !st =   atomically $ do     -- write the new state@@ -370,27 +381,28 @@     modifyTVar qs popWriter  unsafeAcquireAppendAccess ::-     (MonadThrow (STM m), MonadCatch m, MonadMVar m, MonadSTM m)-  => RAWLock m st-  -> m st+  (MonadThrow (STM m), MonadCatch m, MonadMVar m, MonadSTM m) =>+  RAWLock m st ->+  m st unsafeAcquireAppendAccess (RAWLock var apm qs) = do   atomically $ do     -- wait until there are no writers     readTVar qs >>= check . noWriters     -- queue myself     modifyTVar qs pushAppender-  (do+  ( do       -- lock the append access       takeMVar apm       -- acquire the state       atomically (readTMVar var >>= throwPoisoned) `onException` putMVar apm ()-    ) `onException` atomically (modifyTVar qs popAppender)+    )+    `onException` atomically (modifyTVar qs popAppender)  unsafeReleaseAppendAccess ::-     (MonadThrow (STM m), MonadMVar m, MonadSTM m)-  => RAWLock m st-  -> st-  -> m ()+  (MonadThrow (STM m), MonadMVar m, MonadSTM m) =>+  RAWLock m st ->+  st ->+  m () unsafeReleaseAppendAccess (RAWLock var apm qs) !st = do   atomically $ do     -- write the new state

@@ -26,44 +26,51 @@ import Test.Tasty.QuickCheck  main :: IO ()-main = defaultMain $ testGroup "RAWLock" [-    testProperty "Exception safe" $ conjoin (map prop_exception_safe allCommandCombinations)-  , testProperty "correctness" prop_correctness-  , testProperty "unsafe functions do not deadlock" $ conjoin (map prop_unsafe_actions allCommandCombinations)-  ]+main =+  defaultMain $+    testGroup+      "RAWLock"+      [ testProperty "Exception safe" $ conjoin (map prop_exception_safe allCommandCombinations)+      , testProperty "correctness" prop_correctness+      , testProperty "unsafe functions do not deadlock" $+          conjoin (map prop_unsafe_actions allCommandCombinations)+      ]  {-------------------------------------------------------------------------------   Exception safe -------------------------------------------------------------------------------}  data Action = Read | Incr | Append-  deriving (Show)+  deriving Show  allCommandCombinations :: [(Action, Action, Action)] allCommandCombinations =-  [ (a, b, c) | let cmds = [Read, Incr, Append], a <- cmds, b <- cmds, c <- cmds ]+  [(a, b, c) | let cmds = [Read, Incr, Append], a <- cmds, b <- cmds, c <- cmds]  prop_exception_safe :: (Action, Action, Action) -> Property-prop_exception_safe actions@(a1, a2, a3) = counterexample (show actions) $-    exploreSimTrace id action+prop_exception_safe actions@(a1, a2, a3) =+  counterexample (show actions) $+    exploreSimTrace+      id+      action       (\_ tr -> counterexample (ppTrace tr) . property . isRight . traceResult False $ tr)-  where-    action :: IOSim s ()-    action = do-      exploreRaces-      l <- new (0 :: Int)-      let c = \case-            Read -> withReadAccess l $ \s -> say (show s)-            Incr -> withWriteAccess l $ \s -> say (show s) >> pure ((), s + 1)-            Append -> withAppendAccess l $ \s -> say (show s) >> pure ((), s + 1)-      t1 <- async $ c a1-      t2 <- async $ c a2-      t3 <- async $ c a3-      async (cancel t1) >>= wait-      (_ :: Either SomeException ()) <- waitCatch t1-      (_ :: Either SomeException ()) <- waitCatch t2-      (_ :: Either SomeException ()) <- waitCatch t3-      pure ()+ where+  action :: IOSim s ()+  action = do+    exploreRaces+    l <- new (0 :: Int)+    let c = \case+          Read -> withReadAccess l $ \s -> say (show s)+          Incr -> withWriteAccess l $ \s -> say (show s) >> pure ((), s + 1)+          Append -> withAppendAccess l $ \s -> say (show s) >> pure ((), s + 1)+    t1 <- async $ c a1+    t2 <- async $ c a2+    t3 <- async $ c a3+    async (cancel t1) >>= wait+    (_ :: Either SomeException ()) <- waitCatch t1+    (_ :: Either SomeException ()) <- waitCatch t2+    (_ :: Either SomeException ()) <- waitCatch t3+    pure ()  {-------------------------------------------------------------------------------   Correctness@@ -84,94 +91,98 @@ -- 'isConsistent'), e.g., not more than one concurrent appender. prop_correctness :: TestSetup -> Property prop_correctness (TestSetup rawDelays) =-    monadicSimWithTrace tabulateBlockeds test-  where-    RAW readerDelays appenderDelays writerDelays = rawDelays+  monadicSimWithTrace tabulateBlockeds test+ where+  RAW readerDelays appenderDelays writerDelays = rawDelays -    test :: forall s. PropertyM (IOSim s) ()-    test = do-      rawVars@(RAW varReaders varAppenders varWriters) <- run newRAWVars+  test :: forall s. PropertyM (IOSim s) ()+  test = do+    rawVars@(RAW varReaders varAppenders varWriters) <- run newRAWVars -      trace <- run $ do-        rawLock  <- new ()-        varTrace <- newTVarIO []+    trace <- run $ do+      rawLock <- new ()+      varTrace <- newTVarIO [] -        let traceState :: STM (IOSim s) ()-            traceState = do-              rawState <- readRAWState rawVars-              modifyTVar varTrace (rawState:)+      let traceState :: STM (IOSim s) ()+          traceState = do+            rawState <- readRAWState rawVars+            modifyTVar varTrace (rawState :) -        threads <- mapM (async . (labelThisThread "testThread" >>)) $-          map (runReader   rawLock traceState varReaders)   readerDelays   <>-          map (runAppender rawLock traceState varAppenders) appenderDelays <>-          map (runWriter   rawLock traceState varWriters)   writerDelays+      threads <-+        mapM (async . (labelThisThread "testThread" >>)) $+          map (runReader rawLock traceState varReaders) readerDelays+            <> map (runAppender rawLock traceState varAppenders) appenderDelays+            <> map (runWriter rawLock traceState varWriters) writerDelays -        mapM_ wait threads-        reverse <$> atomically (readTVar varTrace)+      mapM_ wait threads+      reverse <$> atomically (readTVar varTrace) -      checkRAWTrace trace+    checkRAWTrace trace -    runReader-      :: RAWLock (IOSim s) ()-      -> STM (IOSim s) ()  -- ^ Trace the 'RAWState'-      -> StrictTVar (IOSim s) Int-      -> [ThreadDelays]-      -> IOSim s ()-    runReader rawLock traceState varReaders =-      mapM_ $ \(ThreadDelays before with) -> do-        threadDelay before-        withReadAccess rawLock $ const $ do-          atomically $ modifyTVar varReaders succ *> traceState-          threadDelay with-          atomically $ modifyTVar varReaders pred *> traceState+  runReader ::+    RAWLock (IOSim s) () ->+    STM (IOSim s) () ->+    -- \^ Trace the 'RAWState'+    StrictTVar (IOSim s) Int ->+    [ThreadDelays] ->+    IOSim s ()+  runReader rawLock traceState varReaders =+    mapM_ $ \(ThreadDelays before with) -> do+      threadDelay before+      withReadAccess rawLock $ const $ do+        atomically $ modifyTVar varReaders succ *> traceState+        threadDelay with+        atomically $ modifyTVar varReaders pred *> traceState -    runAppender-      :: RAWLock (IOSim s) ()-      -> STM (IOSim s) ()  -- ^ Trace the 'RAWState'-      -> StrictTVar (IOSim s) Int-      -> [ThreadDelays]-      -> IOSim s ()-    runAppender rawLock traceState varAppenders =-      mapM_ $ \(ThreadDelays before with) -> do-        threadDelay before-        withAppendAccess rawLock $ const $ do-          atomically $ modifyTVar varAppenders succ *> traceState-          threadDelay with-          atomically $ modifyTVar varAppenders pred *> traceState-          return ((), ())+  runAppender ::+    RAWLock (IOSim s) () ->+    STM (IOSim s) () ->+    -- \^ Trace the 'RAWState'+    StrictTVar (IOSim s) Int ->+    [ThreadDelays] ->+    IOSim s ()+  runAppender rawLock traceState varAppenders =+    mapM_ $ \(ThreadDelays before with) -> do+      threadDelay before+      withAppendAccess rawLock $ const $ do+        atomically $ modifyTVar varAppenders succ *> traceState+        threadDelay with+        atomically $ modifyTVar varAppenders pred *> traceState+        return ((), ()) -    runWriter-      :: RAWLock (IOSim s) ()-      -> STM (IOSim s) ()  -- ^ Trace the 'RAWState'-      -> StrictTVar (IOSim s) Int-      -> [ThreadDelays]-      -> IOSim s ()-    runWriter rawLock traceState varWriters =-      mapM_ $ \(ThreadDelays before with) -> do-        threadDelay before-        withWriteAccess rawLock $ const $ do-          atomically $ modifyTVar varWriters succ *> traceState-          threadDelay with-          atomically $ modifyTVar varWriters pred *> traceState-          return ((), ())+  runWriter ::+    RAWLock (IOSim s) () ->+    STM (IOSim s) () ->+    -- \^ Trace the 'RAWState'+    StrictTVar (IOSim s) Int ->+    [ThreadDelays] ->+    IOSim s ()+  runWriter rawLock traceState varWriters =+    mapM_ $ \(ThreadDelays before with) -> do+      threadDelay before+      withWriteAccess rawLock $ const $ do+        atomically $ modifyTVar varWriters succ *> traceState+        threadDelay with+        atomically $ modifyTVar varWriters pred *> traceState+        return ((), ())  -- | Like 'monadicSim' (which is like 'monadicIO' for the IO simulator), but -- allows inspecting the trace for labelling purposes. monadicSimWithTrace ::-     Testable a-  => (forall x. SimTrace x -> Property -> Property)-  -> (forall s. PropertyM (IOSim s) a)-  -> Property+  Testable a =>+  (forall x. SimTrace x -> Property -> Property) ->+  (forall s. PropertyM (IOSim s) a) ->+  Property monadicSimWithTrace attachTrace m = property $ do-    tr <- runSimGenWithTrace (monadic' m)-    case traceResult False tr of-      Left failure -> throw failure-      Right prop   -> return $ attachTrace tr prop-  where-    runSimGenWithTrace :: (forall s. Gen (IOSim s a)) -> Gen (SimTrace a)-    runSimGenWithTrace f = do-      Capture eval <- capture-      return $ runSimTrace (eval f)+  tr <- runSimGenWithTrace (monadic' m)+  case traceResult False tr of+    Left failure -> throw failure+    Right prop -> return $ attachTrace tr prop+ where+  runSimGenWithTrace :: (forall s. Gen (IOSim s a)) -> Gen (SimTrace a)+  runSimGenWithTrace f = do+    Capture eval <- capture+    return $ runSimTrace (eval f)  -- | Tabulate the number of times a thread is blocked. --@@ -179,30 +190,30 @@ -- contention, we're not testing the lock properly. tabulateBlockeds :: SimTrace a -> Property -> Property tabulateBlockeds tr =-    tabulate "number of times blocked" [classifyBand (count isBlocked tr)]-  where-    isBlocked (EventTxBlocked {}) = Just ()-    isBlocked _                   = Nothing+  tabulate "number of times blocked" [classifyBand (count isBlocked tr)]+ where+  isBlocked (EventTxBlocked{}) = Just ()+  isBlocked _ = Nothing -    count :: (SimEventType -> Maybe x) -> SimTrace a -> Int-    count p = length . selectTraceEvents (const p)+  count :: (SimEventType -> Maybe x) -> SimTrace a -> Int+  count p = length . selectTraceEvents (const p) -    classifyBand :: Int -> String-    classifyBand n-      | n < 10-      = "n < 10"-      | n < 100-      = "n < 100"-      | n < 1000-      = "n < 1,000"-      | n < 10_000-      = "1,000 < n < 10,000"-      | n < 100_000-      = "10,000 < n < 100,000"-      | n < 1000_000-      = "100,000 < n < 1,000,000"-      | otherwise-      = "1,000,000 < n"+  classifyBand :: Int -> String+  classifyBand n+    | n < 10 =+        "n < 10"+    | n < 100 =+        "n < 100"+    | n < 1000 =+        "n < 1,000"+    | n < 10_000 =+        "1,000 < n < 10,000"+    | n < 100_000 =+        "10,000 < n < 100,000"+    | n < 1000_000 =+        "100,000 < n < 1,000,000"+    | otherwise =+        "1,000,000 < n"  {-------------------------------------------------------------------------------   State checking@@ -210,10 +221,10 @@  -- | Data type reused whenever we need something for all three of them. data RAW a = RAW-    { readers   :: a-    , appenders :: a-    , writers   :: a-    }+  { readers :: a+  , appenders :: a+  , writers :: a+  }   deriving (Show, Eq, Functor)  type RAWVars m = RAW (StrictTVar m Int)@@ -224,114 +235,124 @@ type RAWState' = RAW Int  readRAWState :: RAWVars (IOSim s) -> STM (IOSim s) RAWState'-readRAWState RAW { readers, appenders, writers } =-    RAW-      <$> readTVar readers-      <*> readTVar appenders-      <*> readTVar writers+readRAWState RAW{readers, appenders, writers} =+  RAW+    <$> readTVar readers+    <*> readTVar appenders+    <*> readTVar writers  isConsistent :: RAWState' -> Except String ()-isConsistent RAW { readers, appenders, writers }-    | appenders > 1-    = throwError $ show appenders <> " appenders while at most 1 is allowed"-    | writers > 1-    = throwError $ show writers <> " writers while at most 1 is allowed"-    | writers == 1, readers > 0-    = throwError $ "writer concurrent with " <> show readers <> "reader(s)"-    | writers == 1, appenders > 0-    = throwError $ "writer concurrent with an appender"-    | otherwise-    = return ()+isConsistent RAW{readers, appenders, writers}+  | appenders > 1 =+      throwError $ show appenders <> " appenders while at most 1 is allowed"+  | writers > 1 =+      throwError $ show writers <> " writers while at most 1 is allowed"+  | writers == 1+  , readers > 0 =+      throwError $ "writer concurrent with " <> show readers <> "reader(s)"+  | writers == 1+  , appenders > 0 =+      throwError $ "writer concurrent with an appender"+  | otherwise =+      return ()  type RAWTrace = [RAWState']  checkRAWTrace :: Monad m => RAWTrace -> PropertyM m () checkRAWTrace = mapM_ $ \rawState ->-    case runExcept $ isConsistent rawState of-      Left msg -> do-        monitor (counterexample msg)-        Test.QuickCheck.Monadic.assert False-      Right () ->-        return ()+  case runExcept $ isConsistent rawState of+    Left msg -> do+      monitor (counterexample msg)+      Test.QuickCheck.Monadic.assert False+    Right () ->+      return ()  {-------------------------------------------------------------------------------   Generators -------------------------------------------------------------------------------}  newtype TestSetup = TestSetup (RAW [[ThreadDelays]])-  deriving (Show)+  deriving Show  instance Arbitrary TestSetup where   arbitrary = do-    nbReaders   <- choose (0, 3)+    nbReaders <- choose (0, 3)     nbAppenders <- choose (0, 3)-    nbWriters   <- choose (0, 3)-    readers   <- vectorOf nbReaders   arbitrary+    nbWriters <- choose (0, 3)+    readers <- vectorOf nbReaders arbitrary     appenders <- vectorOf nbAppenders arbitrary-    writers   <- vectorOf nbWriters   arbitrary-    return $ TestSetup RAW { readers, appenders, writers }-  shrink (TestSetup raw@RAW { readers, appenders, writers }) =-    [TestSetup raw { readers   = readers'   } | readers'   <- shrink readers  ] <>-    [TestSetup raw { appenders = appenders' } | appenders' <- shrink appenders] <>-    [TestSetup raw { writers   = writers'   } | writers'   <- shrink writers  ]+    writers <- vectorOf nbWriters arbitrary+    return $ TestSetup RAW{readers, appenders, writers}+  shrink (TestSetup raw@RAW{readers, appenders, writers}) =+    [TestSetup raw{readers = readers'} | readers' <- shrink readers]+      <> [TestSetup raw{appenders = appenders'} | appenders' <- shrink appenders]+      <> [TestSetup raw{writers = writers'} | writers' <- shrink writers]  data ThreadDelays = ThreadDelays-    { beforeLockTime :: Int-      -- ^ How long the thread should wait before it starts to take the lock-    , withLockTime   :: Int-      -- ^ How long the thread should wait while holding the lock-    }+  { beforeLockTime :: Int+  -- ^ How long the thread should wait before it starts to take the lock+  , withLockTime :: Int+  -- ^ How long the thread should wait while holding the lock+  }   deriving (Eq, Show)  instance Arbitrary ThreadDelays where   arbitrary = do     beforeLockTime <- choose (0, 1000)-    withLockTime   <- choose (0, 2000)-    return ThreadDelays { beforeLockTime, withLockTime }+    withLockTime <- choose (0, 2000)+    return ThreadDelays{beforeLockTime, withLockTime}  {-------------------------------------------------------------------------------   unsafe functions -------------------------------------------------------------------------------}  prop_unsafe_actions :: (Action, Action, Action) -> Property-prop_unsafe_actions actions@(a1, a2, a3) = counterexample (show actions) $-  exploreSimTrace id action+prop_unsafe_actions actions@(a1, a2, a3) =+  counterexample (show actions) $+    exploreSimTrace+      id+      action       (\_ tr -> counterexample (ppTrace tr) . property . isRight . traceResult False $ tr)-  where-    action :: IOSim s ()-    action = do-      exploreRaces-      l <- new (0 :: Int)-      let c = \case-            Read -> bracket-                      (atomically (unsafeAcquireReadAccess l))-                      (const $ atomically (unsafeReleaseReadAccess l))-                      (say . ("Read: " <>) . show)-            Incr -> generalBracket-                      (unsafeAcquireWriteAccess l)-                      (\orig -> \case-                          ExitCaseSuccess s' -> unsafeReleaseWriteAccess l s'-                          _ -> unsafeReleaseWriteAccess l orig-                      )-                      (\s -> do-                          say ("Incr: " <> show s)-                          pure (s + 1)-                      ) >> pure ()-            Append -> generalBracket-                        (unsafeAcquireAppendAccess l)-                        (\orig -> \case-                            ExitCaseSuccess s' -> unsafeReleaseAppendAccess l s'-                            _ -> unsafeReleaseAppendAccess l orig-                        )-                        (\s -> do-                            say ("Append: " <> show s)-                            pure (s + 1)-                        ) >> pure ()-      t1 <- async $ c a1-      t2 <- async $ c a2-      t3 <- async $ c a3-      async (cancel t1) >>= wait-      (_ :: Either SomeException ()) <- waitCatch t1-      (_ :: Either SomeException ()) <- waitCatch t2-      (_ :: Either SomeException ()) <- waitCatch t3-      pure ()+ where+  action :: IOSim s ()+  action = do+    exploreRaces+    l <- new (0 :: Int)+    let c = \case+          Read ->+            bracket+              (atomically (unsafeAcquireReadAccess l))+              (const $ atomically (unsafeReleaseReadAccess l))+              (say . ("Read: " <>) . show)+          Incr ->+            generalBracket+              (unsafeAcquireWriteAccess l)+              ( \orig -> \case+                  ExitCaseSuccess s' -> unsafeReleaseWriteAccess l s'+                  _ -> unsafeReleaseWriteAccess l orig+              )+              ( \s -> do+                  say ("Incr: " <> show s)+                  pure (s + 1)+              )+              >> pure ()+          Append ->+            generalBracket+              (unsafeAcquireAppendAccess l)+              ( \orig -> \case+                  ExitCaseSuccess s' -> unsafeReleaseAppendAccess l s'+                  _ -> unsafeReleaseAppendAccess l orig+              )+              ( \s -> do+                  say ("Append: " <> show s)+                  pure (s + 1)+              )+              >> pure ()+    t1 <- async $ c a1+    t2 <- async $ c a2+    t3 <- async $ c a3+    async (cancel t1) >>= wait+    (_ :: Either SomeException ()) <- waitCatch t1+    (_ :: Either SomeException ()) <- waitCatch t2+    (_ :: Either SomeException ()) <- waitCatch t3+    pure ()