{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | Tests for the RAW lock mechanism.
--
-- The volatile DB uses an abstraction we call a @RAWLock@, a lock that allows
-- the following combinations of readers, appender and writer:
--
--
-- >          │ Reader │ Appender │ Writer │
-- > ─────────┼────────┼──────────┼────────┤
-- > Reader   │   V    │     V    │    X   │
-- > Appender │░░░░░░░░│     X    │    X   │
-- > Writer   │░░░░░░░░│░░░░░░░░░░│    X   │
--
-- It improves concurrent access. In the test we generate lots of threads, some
-- readers, some appenders, some writers, each concurrently accessing some data
-- protected by the lock. We then record the access pattern; the test would fail
-- if at any point it would see a forbidden combination (for example, a writer
-- and a reader both having access at the same time).
--
module Test.Consensus.Util.MonadSTM.RAWLock (tests) where

import           Control.Exception (throw)
import           Control.Monad.Except
import           Control.Monad.IOSim (IOSim, SimEventType (..), SimTrace,
                     runSimTrace, selectTraceEvents, traceResult)
import           Data.Time.Clock (picosecondsToDiffTime)
import           Ouroboros.Consensus.Util.IOLike
import           Ouroboros.Consensus.Util.MonadSTM.RAWLock (RAWLock)
import qualified Ouroboros.Consensus.Util.MonadSTM.RAWLock as RAWLock
import           Ouroboros.Consensus.Util.ResourceRegistry
import           Test.QuickCheck
import           Test.QuickCheck.Gen.Unsafe (Capture (..), capture)
import           Test.QuickCheck.Monadic
import           Test.Tasty
import           Test.Tasty.QuickCheck
import           Test.Util.Orphans.IOLike ()

tests :: TestTree
tests :: TestTree
tests = String -> (TestSetup -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"RAWLock correctness" TestSetup -> Property
prop_RAWLock_correctness

-- | Test the correctness of the RAWLock
--
-- For a generated number of readers, appenders, and writers: spawn a thread
-- for each. Each thread will process a list of 'ThreadDelays'. For each
-- 'ThreadDelays': wait the generated 'beforeLockTime', then lock the RAWLock
-- with the respective @RAWLock.withXAccess@, increment a 'TVar' that stores
-- the number of readers/appenders/writers that have access, hold the lock for
-- a generated 'withLockTime', decrement the 'TVar', and release the lock.
--
-- In a separate thread, we watch for any changes in the three 'TVar's and
-- write each changed 'RAWState' to a trace (in a separate 'TVar').
-- Afterwards, we check the 'RAWState's in the trace for consistency (using
-- 'isConsistent'), e.g., not more than one concurrent appender.
prop_RAWLock_correctness :: TestSetup -> Property
prop_RAWLock_correctness :: TestSetup -> Property
prop_RAWLock_correctness (TestSetup RAW [[ThreadDelays]]
rawDelays) =
    (forall x. SimTrace x -> Property -> Property)
-> (forall s. PropertyM (IOSim s) ()) -> Property
forall a.
Testable a =>
(forall x. SimTrace x -> Property -> Property)
-> (forall s. PropertyM (IOSim s) a) -> Property
monadicSimWithTrace SimTrace x -> Property -> Property
forall x. SimTrace x -> Property -> Property
tabulateBlockeds PropertyM (IOSim s) ()
forall s. PropertyM (IOSim s) ()
forall (m :: * -> *). IOLike m => PropertyM m ()
test
  where
    RAW [[ThreadDelays]]
readerDelays [[ThreadDelays]]
appenderDelays [[ThreadDelays]]
writerDelays = RAW [[ThreadDelays]]
rawDelays

    test :: forall m. IOLike m => PropertyM m ()
    test :: forall (m :: * -> *). IOLike m => PropertyM m ()
test = do
      rawVars :: RAWVars m
rawVars@(RAW StrictTVar m Int
varReaders StrictTVar m Int
varAppenders StrictTVar m Int
varWriters) <- m (RAWVars m) -> PropertyM m (RAWVars m)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run m (RAWVars m)
forall (m :: * -> *). IOLike m => m (RAWVars m)
newRAWVars

      [RAWState]
trace <- m [RAWState] -> PropertyM m [RAWState]
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m [RAWState] -> PropertyM m [RAWState])
-> m [RAWState] -> PropertyM m [RAWState]
forall a b. (a -> b) -> a -> b
$ (ResourceRegistry m -> m [RAWState]) -> m [RAWState]
forall (m :: * -> *) a.
(IOLike m, HasCallStack) =>
(ResourceRegistry m -> m a) -> m a
withRegistry ((ResourceRegistry m -> m [RAWState]) -> m [RAWState])
-> (ResourceRegistry m -> m [RAWState]) -> m [RAWState]
forall a b. (a -> b) -> a -> b
$ \ResourceRegistry m
registry -> do
        RAWLock m ()
rawLock  <- () -> m (RAWLock m ())
forall (m :: * -> *) st.
(IOLike m, NoThunks st) =>
st -> m (RAWLock m st)
RAWLock.new ()
        StrictTVar m [RAWState]
varTrace <- [RAWState] -> m (StrictTVar m [RAWState])
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
uncheckedNewTVarM []

        let traceState :: STM m ()
            traceState :: STM m ()
traceState = do
              RAWState
rawState <- RAWVars m -> STM m RAWState
forall (m :: * -> *). IOLike m => RAWVars m -> STM m RAWState
readRAWState RAWVars m
rawVars
              StrictTVar m [RAWState] -> ([RAWState] -> [RAWState]) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m [RAWState]
varTrace (RAWState
rawStateRAWState -> [RAWState] -> [RAWState]
forall a. a -> [a] -> [a]
:)

        [Thread m ()]
threads <- (m () -> m (Thread m ())) -> [m ()] -> m [Thread m ()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ResourceRegistry m -> String -> m () -> m (Thread m ())
forall (m :: * -> *) a.
(IOLike m, HasCallStack) =>
ResourceRegistry m -> String -> m a -> m (Thread m a)
forkLinkedThread ResourceRegistry m
registry String
"testThread") ([m ()] -> m [Thread m ()]) -> [m ()] -> m [Thread m ()]
forall a b. (a -> b) -> a -> b
$
          ([ThreadDelays] -> m ()) -> [[ThreadDelays]] -> [m ()]
forall a b. (a -> b) -> [a] -> [b]
map (RAWLock m ()
-> STM m () -> StrictTVar m Int -> [ThreadDelays] -> m ()
forall (m :: * -> *).
IOLike m =>
RAWLock m ()
-> STM m () -> StrictTVar m Int -> [ThreadDelays] -> m ()
runReader   RAWLock m ()
rawLock STM m ()
traceState StrictTVar m Int
varReaders)   [[ThreadDelays]]
readerDelays   [m ()] -> [m ()] -> [m ()]
forall a. Semigroup a => a -> a -> a
<>
          ([ThreadDelays] -> m ()) -> [[ThreadDelays]] -> [m ()]
forall a b. (a -> b) -> [a] -> [b]
map (RAWLock m ()
-> STM m () -> StrictTVar m Int -> [ThreadDelays] -> m ()
forall (m :: * -> *).
IOLike m =>
RAWLock m ()
-> STM m () -> StrictTVar m Int -> [ThreadDelays] -> m ()
runAppender RAWLock m ()
rawLock STM m ()
traceState StrictTVar m Int
varAppenders) [[ThreadDelays]]
appenderDelays [m ()] -> [m ()] -> [m ()]
forall a. Semigroup a => a -> a -> a
<>
          ([ThreadDelays] -> m ()) -> [[ThreadDelays]] -> [m ()]
forall a b. (a -> b) -> [a] -> [b]
map (RAWLock m ()
-> STM m () -> StrictTVar m Int -> [ThreadDelays] -> m ()
forall (m :: * -> *).
IOLike m =>
RAWLock m ()
-> STM m () -> StrictTVar m Int -> [ThreadDelays] -> m ()
runWriter   RAWLock m ()
rawLock STM m ()
traceState StrictTVar m Int
varWriters)   [[ThreadDelays]]
writerDelays

        (Thread m () -> m ()) -> [Thread m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Thread m () -> m ()
forall (m :: * -> *) a. IOLike m => Thread m a -> m a
waitThread [Thread m ()]
threads
        [RAWState] -> [RAWState]
forall a. [a] -> [a]
reverse ([RAWState] -> [RAWState]) -> m [RAWState] -> m [RAWState]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM m [RAWState] -> m [RAWState]
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (StrictTVar m [RAWState] -> STM m [RAWState]
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m [RAWState]
varTrace)

      [RAWState] -> PropertyM m ()
forall (m :: * -> *). Monad m => [RAWState] -> PropertyM m ()
checkRAWTrace [RAWState]
trace

    runReader
      :: IOLike m
      => RAWLock m ()
      -> STM m ()  -- ^ Trace the 'RAWState'
      -> StrictTVar m Int
      -> [ThreadDelays]
      -> m ()
    runReader :: forall (m :: * -> *).
IOLike m =>
RAWLock m ()
-> STM m () -> StrictTVar m Int -> [ThreadDelays] -> m ()
runReader RAWLock m ()
rawLock STM m ()
traceState StrictTVar m Int
varReaders =
      (ThreadDelays -> m ()) -> [ThreadDelays] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((ThreadDelays -> m ()) -> [ThreadDelays] -> m ())
-> (ThreadDelays -> m ()) -> [ThreadDelays] -> m ()
forall a b. (a -> b) -> a -> b
$ \(ThreadDelays DiffTime
before DiffTime
with) -> do
        DiffTime -> m ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
before
        RAWLock m () -> (() -> m ()) -> m ()
forall (m :: * -> *) st a.
IOLike m =>
RAWLock m st -> (st -> m a) -> m a
RAWLock.withReadAccess RAWLock m ()
rawLock ((() -> m ()) -> m ()) -> (() -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> () -> m ()
forall a b. a -> b -> a
const (m () -> () -> m ()) -> m () -> () -> m ()
forall a b. (a -> b) -> a -> b
$ do
          STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ StrictTVar m Int -> (Int -> Int) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m Int
varReaders Int -> Int
forall a. Enum a => a -> a
succ STM m () -> STM m () -> STM m ()
forall a b. STM m a -> STM m b -> STM m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> STM m ()
traceState
          DiffTime -> m ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
with
          STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ StrictTVar m Int -> (Int -> Int) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m Int
varReaders Int -> Int
forall a. Enum a => a -> a
pred STM m () -> STM m () -> STM m ()
forall a b. STM m a -> STM m b -> STM m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> STM m ()
traceState

    runAppender
      :: IOLike m
      => RAWLock m ()
      -> STM m ()  -- ^ Trace the 'RAWState'
      -> StrictTVar m Int
      -> [ThreadDelays]
      -> m ()
    runAppender :: forall (m :: * -> *).
IOLike m =>
RAWLock m ()
-> STM m () -> StrictTVar m Int -> [ThreadDelays] -> m ()
runAppender RAWLock m ()
rawLock STM m ()
traceState StrictTVar m Int
varAppenders =
      (ThreadDelays -> m ()) -> [ThreadDelays] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((ThreadDelays -> m ()) -> [ThreadDelays] -> m ())
-> (ThreadDelays -> m ()) -> [ThreadDelays] -> m ()
forall a b. (a -> b) -> a -> b
$ \(ThreadDelays DiffTime
before DiffTime
with) -> do
        DiffTime -> m ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
before
        RAWLock m () -> (() -> m ((), ())) -> m ()
forall (m :: * -> *) st a.
IOLike m =>
RAWLock m st -> (st -> m (st, a)) -> m a
RAWLock.withAppendAccess RAWLock m ()
rawLock ((() -> m ((), ())) -> m ()) -> (() -> m ((), ())) -> m ()
forall a b. (a -> b) -> a -> b
$ m ((), ()) -> () -> m ((), ())
forall a b. a -> b -> a
const (m ((), ()) -> () -> m ((), ())) -> m ((), ()) -> () -> m ((), ())
forall a b. (a -> b) -> a -> b
$ do
          STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ StrictTVar m Int -> (Int -> Int) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m Int
varAppenders Int -> Int
forall a. Enum a => a -> a
succ STM m () -> STM m () -> STM m ()
forall a b. STM m a -> STM m b -> STM m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> STM m ()
traceState
          DiffTime -> m ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
with
          STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ StrictTVar m Int -> (Int -> Int) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m Int
varAppenders Int -> Int
forall a. Enum a => a -> a
pred STM m () -> STM m () -> STM m ()
forall a b. STM m a -> STM m b -> STM m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> STM m ()
traceState
          ((), ()) -> m ((), ())
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((), ())

    runWriter
      :: IOLike m
      => RAWLock m ()
      -> STM m ()  -- ^ Trace the 'RAWState'
      -> StrictTVar m Int
      -> [ThreadDelays]
      -> m ()
    runWriter :: forall (m :: * -> *).
IOLike m =>
RAWLock m ()
-> STM m () -> StrictTVar m Int -> [ThreadDelays] -> m ()
runWriter RAWLock m ()
rawLock STM m ()
traceState StrictTVar m Int
varWriters =
      (ThreadDelays -> m ()) -> [ThreadDelays] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((ThreadDelays -> m ()) -> [ThreadDelays] -> m ())
-> (ThreadDelays -> m ()) -> [ThreadDelays] -> m ()
forall a b. (a -> b) -> a -> b
$ \(ThreadDelays DiffTime
before DiffTime
with) -> do
        DiffTime -> m ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
before
        RAWLock m () -> (() -> m ((), ())) -> m ()
forall (m :: * -> *) st a.
IOLike m =>
RAWLock m st -> (st -> m (st, a)) -> m a
RAWLock.withWriteAccess RAWLock m ()
rawLock ((() -> m ((), ())) -> m ()) -> (() -> m ((), ())) -> m ()
forall a b. (a -> b) -> a -> b
$ m ((), ()) -> () -> m ((), ())
forall a b. a -> b -> a
const (m ((), ()) -> () -> m ((), ())) -> m ((), ()) -> () -> m ((), ())
forall a b. (a -> b) -> a -> b
$ do
          STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ StrictTVar m Int -> (Int -> Int) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m Int
varWriters Int -> Int
forall a. Enum a => a -> a
succ STM m () -> STM m () -> STM m ()
forall a b. STM m a -> STM m b -> STM m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> STM m ()
traceState
          DiffTime -> m ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
threadDelay DiffTime
with
          STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ StrictTVar m Int -> (Int -> Int) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m Int
varWriters Int -> Int
forall a. Enum a => a -> a
pred STM m () -> STM m () -> STM m ()
forall a b. STM m a -> STM m b -> STM m b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> STM m ()
traceState
          ((), ()) -> m ((), ())
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
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
monadicSimWithTrace :: forall a.
Testable a =>
(forall x. SimTrace x -> Property -> Property)
-> (forall s. PropertyM (IOSim s) a) -> Property
monadicSimWithTrace forall x. SimTrace x -> Property -> Property
attachTrace forall s. PropertyM (IOSim s) a
m = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ do
    SimTrace Property
tr <- (forall s. Gen (IOSim s Property)) -> Gen (SimTrace Property)
forall a. (forall s. Gen (IOSim s a)) -> Gen (SimTrace a)
runSimGenWithTrace (PropertyM (IOSim s) a -> Gen (IOSim s Property)
forall a (m :: * -> *).
(Testable a, Monad m) =>
PropertyM m a -> Gen (m Property)
monadic' PropertyM (IOSim s) a
forall s. PropertyM (IOSim s) a
m)
    case Bool -> SimTrace Property -> Either Failure Property
forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
False SimTrace Property
tr of
      Left Failure
failure -> Failure -> Gen Property
forall a e. Exception e => e -> a
throw Failure
failure
      Right Property
prop   -> Property -> Gen Property
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ SimTrace Property -> Property -> Property
forall x. SimTrace x -> Property -> Property
attachTrace SimTrace Property
tr Property
prop
  where
    runSimGenWithTrace :: (forall s. Gen (IOSim s a)) -> Gen (SimTrace a)
    runSimGenWithTrace :: forall a. (forall s. Gen (IOSim s a)) -> Gen (SimTrace a)
runSimGenWithTrace forall s. Gen (IOSim s a)
f = do
      Capture forall a. Gen a -> a
eval <- Gen Capture
capture
      SimTrace a -> Gen (SimTrace a)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> Gen (SimTrace a)) -> SimTrace a -> Gen (SimTrace a)
forall a b. (a -> b) -> a -> b
$ (forall s. IOSim s a) -> SimTrace a
forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace (Gen (IOSim s a) -> IOSim s a
forall a. Gen a -> a
eval Gen (IOSim s a)
forall s. Gen (IOSim s a)
f)

-- | Tabulate the number of times a thread is blocked.
--
-- The higher this number, the higher the contention. If there's no
-- contention, we're not testing the lock properly.
tabulateBlockeds :: SimTrace a -> Property -> Property
tabulateBlockeds :: forall x. SimTrace x -> Property -> Property
tabulateBlockeds SimTrace a
tr =
    String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"number of times blocked" [Int -> String
classifyBand ((SimEventType -> Maybe ()) -> SimTrace a -> Int
forall x a. (SimEventType -> Maybe x) -> SimTrace a -> Int
count SimEventType -> Maybe ()
isBlocked SimTrace a
tr)]
  where
    isBlocked :: SimEventType -> Maybe ()
isBlocked (EventTxBlocked {}) = () -> Maybe ()
forall a. a -> Maybe a
Just ()
    isBlocked SimEventType
_                   = Maybe ()
forall a. Maybe a
Nothing

    count :: (SimEventType -> Maybe x) -> SimTrace a -> Int
    count :: forall x a. (SimEventType -> Maybe x) -> SimTrace a -> Int
count SimEventType -> Maybe x
p = [x] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([x] -> Int) -> (SimTrace a -> [x]) -> SimTrace a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Time -> SimEventType -> Maybe x) -> SimTrace a -> [x]
forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents ((SimEventType -> Maybe x) -> Time -> SimEventType -> Maybe x
forall a b. a -> b -> a
const SimEventType -> Maybe x
p)

    classifyBand :: Int -> String
    classifyBand :: Int -> String
classifyBand Int
n
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
10
      = String
"n < 10"
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
100
      = String
"n < 100"
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1000
      = String
"n < 1,000"
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
10_000
      = String
"1,000 < n < 10,000"
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
100_000
      = String
"10,000 < n < 100,000"
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1000_000
      = String
"100,000 < n < 1,000,000"
      | Bool
otherwise
      = String
"1,000,000 < n"

{-------------------------------------------------------------------------------
  State checking
-------------------------------------------------------------------------------}

-- | Data type reused whenever we need something for all three of them.
data RAW a = RAW
    { forall a. RAW a -> a
readers   :: a
    , forall a. RAW a -> a
appenders :: a
    , forall a. RAW a -> a
writers   :: a
    }
  deriving (Int -> RAW a -> ShowS
[RAW a] -> ShowS
RAW a -> String
(Int -> RAW a -> ShowS)
-> (RAW a -> String) -> ([RAW a] -> ShowS) -> Show (RAW a)
forall a. Show a => Int -> RAW a -> ShowS
forall a. Show a => [RAW a] -> ShowS
forall a. Show a => RAW a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> RAW a -> ShowS
showsPrec :: Int -> RAW a -> ShowS
$cshow :: forall a. Show a => RAW a -> String
show :: RAW a -> String
$cshowList :: forall a. Show a => [RAW a] -> ShowS
showList :: [RAW a] -> ShowS
Show, RAW a -> RAW a -> Bool
(RAW a -> RAW a -> Bool) -> (RAW a -> RAW a -> Bool) -> Eq (RAW a)
forall a. Eq a => RAW a -> RAW a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => RAW a -> RAW a -> Bool
== :: RAW a -> RAW a -> Bool
$c/= :: forall a. Eq a => RAW a -> RAW a -> Bool
/= :: RAW a -> RAW a -> Bool
Eq, (forall a b. (a -> b) -> RAW a -> RAW b)
-> (forall a b. a -> RAW b -> RAW a) -> Functor RAW
forall a b. a -> RAW b -> RAW a
forall a b. (a -> b) -> RAW a -> RAW b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> RAW a -> RAW b
fmap :: forall a b. (a -> b) -> RAW a -> RAW b
$c<$ :: forall a b. a -> RAW b -> RAW a
<$ :: forall a b. a -> RAW b -> RAW a
Functor)

type RAWVars m = RAW (StrictTVar m Int)

newRAWVars :: IOLike m => m (RAWVars m)
newRAWVars :: forall (m :: * -> *). IOLike m => m (RAWVars m)
newRAWVars = StrictTVar m Int
-> StrictTVar m Int -> StrictTVar m Int -> RAW (StrictTVar m Int)
forall a. a -> a -> a -> RAW a
RAW (StrictTVar m Int
 -> StrictTVar m Int -> StrictTVar m Int -> RAW (StrictTVar m Int))
-> m (StrictTVar m Int)
-> m (StrictTVar m Int
      -> StrictTVar m Int -> RAW (StrictTVar m Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> m (StrictTVar m Int)
forall (m :: * -> *) a.
(HasCallStack, MonadSTM m, NoThunks a) =>
a -> m (StrictTVar m a)
newTVarIO Int
0 m (StrictTVar m Int -> StrictTVar m Int -> RAW (StrictTVar m Int))
-> m (StrictTVar m Int)
-> m (StrictTVar m Int -> RAW (StrictTVar m Int))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> m (StrictTVar m Int)
forall (m :: * -> *) a.
(HasCallStack, MonadSTM m, NoThunks a) =>
a -> m (StrictTVar m a)
newTVarIO Int
0 m (StrictTVar m Int -> RAW (StrictTVar m Int))
-> m (StrictTVar m Int) -> m (RAW (StrictTVar m Int))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Int -> m (StrictTVar m Int)
forall (m :: * -> *) a.
(HasCallStack, MonadSTM m, NoThunks a) =>
a -> m (StrictTVar m a)
newTVarIO Int
0

type RAWState = RAW Int

readRAWState :: IOLike m => RAWVars m -> STM m RAWState
readRAWState :: forall (m :: * -> *). IOLike m => RAWVars m -> STM m RAWState
readRAWState RAW { StrictTVar m Int
readers :: forall a. RAW a -> a
readers :: StrictTVar m Int
readers, StrictTVar m Int
appenders :: forall a. RAW a -> a
appenders :: StrictTVar m Int
appenders, StrictTVar m Int
writers :: forall a. RAW a -> a
writers :: StrictTVar m Int
writers } =
    Int -> Int -> Int -> RAWState
forall a. a -> a -> a -> RAW a
RAW
      (Int -> Int -> Int -> RAWState)
-> STM m Int -> STM m (Int -> Int -> RAWState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m Int -> STM m Int
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m Int
readers
      STM m (Int -> Int -> RAWState)
-> STM m Int -> STM m (Int -> RAWState)
forall a b. STM m (a -> b) -> STM m a -> STM m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictTVar m Int -> STM m Int
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m Int
appenders
      STM m (Int -> RAWState) -> STM m Int -> STM m RAWState
forall a b. STM m (a -> b) -> STM m a -> STM m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StrictTVar m Int -> STM m Int
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m Int
writers

isConsistent :: RAWState -> Except String ()
isConsistent :: RAWState -> Except String ()
isConsistent RAW { Int
readers :: forall a. RAW a -> a
readers :: Int
readers, Int
appenders :: forall a. RAW a -> a
appenders :: Int
appenders, Int
writers :: forall a. RAW a -> a
writers :: Int
writers }
    | Int
appenders Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
    = String -> Except String ()
forall a. String -> ExceptT String Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Except String ()) -> String -> Except String ()
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
appenders String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" appenders while at most 1 is allowed"
    | Int
writers Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
    = String -> Except String ()
forall a. String -> ExceptT String Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Except String ()) -> String -> Except String ()
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
writers String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" writers while at most 1 is allowed"
    | Int
writers Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1, Int
readers Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
    = String -> Except String ()
forall a. String -> ExceptT String Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Except String ()) -> String -> Except String ()
forall a b. (a -> b) -> a -> b
$ String
"writer concurrent with " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
readers String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"reader(s)"
    | Int
writers Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1, Int
appenders Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
    = String -> Except String ()
forall a. String -> ExceptT String Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Except String ()) -> String -> Except String ()
forall a b. (a -> b) -> a -> b
$ String
"writer concurrent with an appender"
    | Bool
otherwise
    = () -> Except String ()
forall a. a -> ExceptT String Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

type RAWTrace = [RAWState]

checkRAWTrace :: Monad m => RAWTrace -> PropertyM m ()
checkRAWTrace :: forall (m :: * -> *). Monad m => [RAWState] -> PropertyM m ()
checkRAWTrace = (RAWState -> PropertyM m ()) -> [RAWState] -> PropertyM m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((RAWState -> PropertyM m ()) -> [RAWState] -> PropertyM m ())
-> (RAWState -> PropertyM m ()) -> [RAWState] -> PropertyM m ()
forall a b. (a -> b) -> a -> b
$ \RAWState
rawState ->
    case Except String () -> Either String ()
forall e a. Except e a -> Either e a
runExcept (Except String () -> Either String ())
-> Except String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ RAWState -> Except String ()
isConsistent RAWState
rawState of
      Left String
msg -> do
        (Property -> Property) -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
(Property -> Property) -> PropertyM m ()
monitor (String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
msg)
        Bool -> PropertyM m ()
forall (m :: * -> *). Monad m => Bool -> PropertyM m ()
assert Bool
False
      Right () ->
        () -> PropertyM m ()
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

{-------------------------------------------------------------------------------
  Generators
-------------------------------------------------------------------------------}

newtype TestSetup = TestSetup (RAW [[ThreadDelays]])
  deriving (Int -> TestSetup -> ShowS
[TestSetup] -> ShowS
TestSetup -> String
(Int -> TestSetup -> ShowS)
-> (TestSetup -> String)
-> ([TestSetup] -> ShowS)
-> Show TestSetup
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TestSetup -> ShowS
showsPrec :: Int -> TestSetup -> ShowS
$cshow :: TestSetup -> String
show :: TestSetup -> String
$cshowList :: [TestSetup] -> ShowS
showList :: [TestSetup] -> ShowS
Show)

instance Arbitrary TestSetup where
  arbitrary :: Gen TestSetup
arbitrary = do
    Int
nbReaders   <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
3)
    Int
nbAppenders <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
3)
    Int
nbWriters   <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
3)
    [[ThreadDelays]]
readers   <- Int -> Gen [ThreadDelays] -> Gen [[ThreadDelays]]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
nbReaders   Gen [ThreadDelays]
forall a. Arbitrary a => Gen a
arbitrary
    [[ThreadDelays]]
appenders <- Int -> Gen [ThreadDelays] -> Gen [[ThreadDelays]]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
nbAppenders Gen [ThreadDelays]
forall a. Arbitrary a => Gen a
arbitrary
    [[ThreadDelays]]
writers   <- Int -> Gen [ThreadDelays] -> Gen [[ThreadDelays]]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
nbWriters   Gen [ThreadDelays]
forall a. Arbitrary a => Gen a
arbitrary
    TestSetup -> Gen TestSetup
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (TestSetup -> Gen TestSetup) -> TestSetup -> Gen TestSetup
forall a b. (a -> b) -> a -> b
$ RAW [[ThreadDelays]] -> TestSetup
TestSetup RAW { [[ThreadDelays]]
readers :: [[ThreadDelays]]
readers :: [[ThreadDelays]]
readers, [[ThreadDelays]]
appenders :: [[ThreadDelays]]
appenders :: [[ThreadDelays]]
appenders, [[ThreadDelays]]
writers :: [[ThreadDelays]]
writers :: [[ThreadDelays]]
writers }
  shrink :: TestSetup -> [TestSetup]
shrink (TestSetup raw :: RAW [[ThreadDelays]]
raw@RAW { [[ThreadDelays]]
readers :: forall a. RAW a -> a
readers :: [[ThreadDelays]]
readers, [[ThreadDelays]]
appenders :: forall a. RAW a -> a
appenders :: [[ThreadDelays]]
appenders, [[ThreadDelays]]
writers :: forall a. RAW a -> a
writers :: [[ThreadDelays]]
writers }) =
    [RAW [[ThreadDelays]] -> TestSetup
TestSetup RAW [[ThreadDelays]]
raw { readers   = readers'   } | [[ThreadDelays]]
readers'   <- [[ThreadDelays]] -> [[[ThreadDelays]]]
forall a. Arbitrary a => a -> [a]
shrink [[ThreadDelays]]
readers  ] [TestSetup] -> [TestSetup] -> [TestSetup]
forall a. Semigroup a => a -> a -> a
<>
    [RAW [[ThreadDelays]] -> TestSetup
TestSetup RAW [[ThreadDelays]]
raw { appenders = appenders' } | [[ThreadDelays]]
appenders' <- [[ThreadDelays]] -> [[[ThreadDelays]]]
forall a. Arbitrary a => a -> [a]
shrink [[ThreadDelays]]
appenders] [TestSetup] -> [TestSetup] -> [TestSetup]
forall a. Semigroup a => a -> a -> a
<>
    [RAW [[ThreadDelays]] -> TestSetup
TestSetup RAW [[ThreadDelays]]
raw { writers   = writers'   } | [[ThreadDelays]]
writers'   <- [[ThreadDelays]] -> [[[ThreadDelays]]]
forall a. Arbitrary a => a -> [a]
shrink [[ThreadDelays]]
writers  ]

data ThreadDelays = ThreadDelays
    { ThreadDelays -> DiffTime
beforeLockTime :: DiffTime
      -- ^ How long the thread should wait before it starts to take the lock
    , ThreadDelays -> DiffTime
withLockTime   :: DiffTime
      -- ^ How long the thread should wait while holding the lock
    }
  deriving (ThreadDelays -> ThreadDelays -> Bool
(ThreadDelays -> ThreadDelays -> Bool)
-> (ThreadDelays -> ThreadDelays -> Bool) -> Eq ThreadDelays
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ThreadDelays -> ThreadDelays -> Bool
== :: ThreadDelays -> ThreadDelays -> Bool
$c/= :: ThreadDelays -> ThreadDelays -> Bool
/= :: ThreadDelays -> ThreadDelays -> Bool
Eq, Int -> ThreadDelays -> ShowS
[ThreadDelays] -> ShowS
ThreadDelays -> String
(Int -> ThreadDelays -> ShowS)
-> (ThreadDelays -> String)
-> ([ThreadDelays] -> ShowS)
-> Show ThreadDelays
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ThreadDelays -> ShowS
showsPrec :: Int -> ThreadDelays -> ShowS
$cshow :: ThreadDelays -> String
show :: ThreadDelays -> String
$cshowList :: [ThreadDelays] -> ShowS
showList :: [ThreadDelays] -> ShowS
Show)

instance Arbitrary ThreadDelays where
  arbitrary :: Gen ThreadDelays
arbitrary = do
    DiffTime
beforeLockTime <- Integer -> DiffTime
picosecondsToDiffTime (Integer -> DiffTime) -> Gen Integer -> Gen DiffTime
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
1000)
    DiffTime
withLockTime   <- Integer -> DiffTime
picosecondsToDiffTime (Integer -> DiffTime) -> Gen Integer -> Gen DiffTime
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
0, Integer
2000)
    ThreadDelays -> Gen ThreadDelays
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ThreadDelays { DiffTime
beforeLockTime :: DiffTime
beforeLockTime :: DiffTime
beforeLockTime, DiffTime
withLockTime :: DiffTime
withLockTime :: DiffTime
withLockTime }