First draft of parallel state machines

quickcheck-dynamic/quickcheck-dynamic.cabal

@@ -80,6 +80,7 @@ library
   build-depends:
     , base        >=4.7 && <5
     , containers
+    , io-classes
     , mtl
     , QuickCheck
     , random

quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 -- | Model-Based Testing library for use with Haskell QuickCheck.
@@ -38,9 +39,12 @@ module Test.QuickCheck.StateModel (
   computePrecondition,
   computeArbitraryAction,
   computeShrinkAction,
+  runParallelActions,
+  ParActions (..),
 ) where
 
 import Control.Monad
+import Control.Monad.Class.MonadAsync
 import Control.Monad.Identity
 import Control.Monad.Reader
 import Control.Monad.State
@@ -193,12 +197,18 @@ newtype PostconditionM m a = PostconditionM {runPost :: WriterT (Endo Property,
 instance MonadTrans PostconditionM where
   lift = PostconditionM . lift
 
+-- | Evaluate a postcondition in @PropertyM m@ and make the property fail if
+-- postcondition results in @False@
 evaluatePostCondition :: Monad m => PostconditionM m Bool -> PropertyM m ()
-evaluatePostCondition post = do
+evaluatePostCondition post = assert =<< evaluatePostCondition' post
+
+-- | Evaluate a postcondition in @PropertyM m@ and return the boolean result
+evaluatePostCondition' :: Monad m => PostconditionM m Bool -> PropertyM m Bool
+evaluatePostCondition' post = do
   (b, (Endo mon, Endo onFail)) <- run . runWriterT . runPost $ post
   monitor mon
   unless b $ monitor onFail
-  assert b
+  pure b
 
 -- | Apply the property transformation to the property after evaluating
 -- the postcondition. Useful for collecting statistics while avoiding
@@ -223,6 +233,8 @@ class (forall a. Show (Action state a), Monad m) => RunModel state m where
   -- a` instances from previous steps.
   perform :: Typeable a => state -> Action state a -> LookUp m -> m (PerformResult (Error state) (Realized m a))
 
+  perform' :: Typeable a => Action state a -> LookUp m -> m (PerformResult (Error state) (Realized m a))
+
   -- | Postcondition on the `a` value produced at some step.
   -- The result is `assert`ed and will make the property fail should it be `False`. This is useful
   -- to check the implementation produces expected values.
@@ -310,6 +322,26 @@ infix 5 :=
 instance (forall a. HasVariables (Action state a)) => HasVariables (Step state) where
   getAllVariables (var := act) = Set.insert (Some var) $ getAllVariables (polarAction act)
 
+{-
+      do action $ Inc
+         action $ Inc
+         action $ Inc
+         action $ Inc
+         action $ Inc
+         action $ Reset
+         action $ Inc
+         action $ Inc
+         action $ Inc
+         action $ Inc
+         pure ()
+      do action $ Inc
+         pure ()
+      do action $ Inc
+         pure ()
+
+as = ParActions (Actions_ [] (Smart 0 [mkVar 0 := ActionWithPolarity Inc PosPolarity, mkVar 1 := ActionWithPolarity Inc PosPolarity, mkVar 2 := ActionWithPolarity Inc PosPolarity, mkVar 3 := ActionWithPolarity Inc PosPolarity, mkVar 4 := ActionWithPolarity Inc PosPolarity, mkVar 5 := ActionWithPolarity Reset PosPolarity, mkVar 6 := ActionWithPolarity Inc PosPolarity, mkVar 7 := ActionWithPolarity Inc PosPolarity, mkVar 8 := ActionWithPolarity Inc PosPolarity, mkVar 9 := ActionWithPolarity Inc PosPolarity])) [Actions_ [] (Smart 0 [mkVar 10 := ActionWithPolarity Inc PosPolarity]), Actions_ [] (Smart 0 [mkVar 11 := ActionWithPolarity Inc PosPolarity])]
+-}
+
 funName :: Polarity -> String
 funName PosPolarity = "action"
 funName _ = "failingAction"
@@ -585,3 +617,200 @@ runSteps s env ((v := act) : as) = do
           stateTransition = (underlyingState s, underlyingState s')
       monitor $ monitoring @state @m stateTransition action (lookUpVar env') ret
       pure (s', env', stateTransition)
+
+{-------------------------------------------------------------------------------
+  Parallel State Machines
+-------------------------------------------------------------------------------}
+
+-- | A sequential prefix and some number of parallel suffixes
+data ParActions state = ParActions (Actions state) [Actions state]
+
+instance StateModel state => Show (ParActions state) where
+  show (ParActions as ass) =
+    unlines $
+      [ "Sequential prefix"
+      , unlines $ map ('\t' :) $ lines $ show as
+      , "Parallel suffixes"
+      ]
+        ++ ( concatMap
+              ( \(idx, acts) ->
+                  [ [idx] <> ":"
+                  , unlines $ map ('\t' :) $ lines $ show acts
+                  ]
+              )
+              (zip ['a' ..] ass)
+           )
+
+-- | Existential on @a@
+data Performed m state where
+  Performed
+    :: (Typeable a, Eq (Action state a), Show (Action state a))
+    => Var a
+    -> ActionWithPolarity state a
+    -> Either (Error state) (Realized m a)
+    -> Performed m state
+
+runParallelActions
+  :: forall state m e
+   . ( StateModel state
+     , RunModel state m
+     , e ~ Error state
+     , forall a. IsPerformResult e a
+     , MonadAsync m
+     )
+  => ParActions state
+  -> PropertyM m ()
+runParallelActions (ParActions (Actions_ _ (Smart _ seqPrefix)) suffixes) = do
+  (env, seqPerformed) <- run $ runParallelSteps [] [] seqPrefix
+  results <- run $ mapConcurrently (\(Actions_ _ (Smart _ actions)) -> runParallelSteps env [] actions) suffixes
+  let possibleLinearizations = interleavings (env, seqPerformed) results
+
+  hasOneSucceded <-
+    if null possibleLinearizations
+      then pure True
+      else
+        fmap or
+          . mapM
+            ( \(anEnv, anInterleaving) ->
+                snd <$> foldM (foldModel anEnv) (initialAnnotatedState, True) anInterleaving
+            )
+          $ possibleLinearizations
+  assert hasOneSucceded
+  where
+    foldModel
+      :: Env m
+      -> (Annotated state, Bool)
+      -> Performed m state
+      -> PropertyM m (Annotated state, Bool)
+    foldModel _ (s, False) _ = pure (s, False)
+    foldModel env (s, _) (Performed var act ret) =
+      case (polar, ret) of
+        (PosPolarity, Left err) ->
+          (s,) <$> positiveActionFailed err
+        (PosPolarity, Right val) -> do
+          positiveActionSucceeded val
+        (NegPolarity, _) -> do
+          negativeActionResult
+      where
+        action = polarAction act
+        polar = polarity act
+
+        positiveActionFailed err = do
+          monitor $
+            monitoringFailure @state @m
+              (underlyingState s)
+              action
+              (lookUpVar env)
+              err
+          pure False
+
+        positiveActionSucceeded val = do
+          (s', stateTransition) <- computeNewState
+          b <-
+            evaluatePostCondition' $
+              postcondition
+                stateTransition
+                action
+                (lookUpVar env)
+                val
+          pure (s', b)
+
+        negativeActionResult = do
+          (s', stateTransition) <- computeNewState
+          b <-
+            evaluatePostCondition' $
+              postconditionOnFailure
+                stateTransition
+                action
+                (lookUpVar env)
+                ret
+          pure (s', b)
+
+        computeNewState = do
+          let s' = computeNextState s act var
+              stateTransition = (underlyingState s, underlyingState s')
+          monitor $ monitoring @state @m stateTransition action (lookUpVar env) ret
+          pure (s', stateTransition)
+
+runParallelSteps
+  :: forall state m e
+   . ( StateModel state
+     , RunModel state m
+     , e ~ Error state
+     , forall a. IsPerformResult e a
+     )
+  => Env m
+  -> [Performed m state]
+  -> [Step state]
+  -> m (Env m, [Performed m state])
+runParallelSteps env rets [] = return (reverse env, reverse rets)
+runParallelSteps env rets ((v := act) : as) = do
+  let action = polarAction act
+  (ret, env') <- runStep action
+  runParallelSteps env' (Performed v act ret : rets) as
+  where
+    runStep
+      :: forall a
+       . Typeable a
+      => Action state a
+      -> m (Either (Error state) (Realized m a), Env m)
+    runStep action = do
+      ret :: Either (Error state) (Realized m a) <- performResultToEither <$> perform' action (lookUpVar env)
+      let var :: Var a
+          var = unsafeCoerceVar v
+          env'
+            | Right (val :: Realized m a) <- ret = (var :== val) : env
+            | otherwise = env
+      pure (ret, env')
+
+instance forall state. StateModel state => Arbitrary (ParActions state) where
+  arbitrary = do
+    (Actions_ rej (Smart _ allActions)) <- arbitrary
+    foo rej allActions
+    where
+      foo rej allActions = do
+        seqLength <- chooseInt (0, length allActions - 1)
+        let (prefix, suffix) = splitAt seqLength allActions
+            (suff1, suff2) = splitAt (length suffix `div` 2) suffix
+            f :: (state, Bool) -> Step state -> (state, Bool)
+            f (st, False) _ = (st, False)
+            f (st, b) (v := act) =
+              ( nextState st (polarAction act) v
+              , b && precondition st (polarAction act)
+              )
+        if and $
+          map (\anInterleaving -> snd $ foldl' f (initialState, True) anInterleaving) (interleaves [suff1, suff2])
+          then
+            pure
+              ( ParActions
+                  (Actions_ rej (Smart 0 prefix))
+                  [(Actions_ rej (Smart 0 suff1)), (Actions_ rej (Smart 0 suff2))]
+              )
+          else foo rej allActions
+
+-- | Generate all possible interleavings.
+--
+-- Note that the environment should be able to handle duplicates so we just
+-- concat all environments together.
+interleavings
+  :: (Env m, [Performed m state])
+  -> [(Env m, [Performed m state])]
+  -> [(Env m, [Performed m state])]
+interleavings (_, seqPrefix) parallelSuffixes =
+  let env = concat [e | (e, _) <- parallelSuffixes]
+   in map ((env,) . (seqPrefix ++)) $ interleaves $ map snd parallelSuffixes
+
+-- | All interleavings of a list of lists (preserving the relative order)
+interleaves :: [[a]] -> [[a]]
+interleaves [] = []
+interleaves [as] = [as]
+interleaves (a : as) = foldl' (\b x -> concatMap (interleave x) b) [a] as
+
+-- | All interleavings of two lists (preserving the relative order)
+interleave :: [a] -> [a] -> [[a]]
+interleave [] [] = []
+interleave as [] = [as]
+interleave [] bs = [bs]
+interleave a@(ah : as) b@(bh : bs) =
+  [ah : arest | arest <- interleave as b]
+    ++ [bh : brest | brest <- interleave a bs]

quickcheck-dynamic/test/Spec/DynamicLogic/Counters.hs

@@ -34,6 +34,10 @@ instance RunModel SimpleCounter (ReaderT (IORef Int) IO) where
     ref <- ask
     lift $ atomicModifyIORef' ref (\count -> (succ count, count))
 
+  perform' IncSimple _ = do
+    ref <- ask
+    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+
 -- A very simple model with a single action whose postcondition fails in a
 -- predictable way. This model is useful for testing the runtime.
 newtype FailingCounter = FailingCounter {failingCount :: Int}
@@ -59,6 +63,10 @@ instance RunModel FailingCounter (ReaderT (IORef Int) IO) where
     ref <- ask
     lift $ atomicModifyIORef' ref (\count -> (succ count, count))
 
+  perform' Inc' _ = do
+    ref <- ask
+    lift $ atomicModifyIORef' ref (\count -> (succ count, count))
+
   postcondition (_, FailingCounter{failingCount}) _ _ _ = pure $ failingCount < 4
 
 -- A generic but simple counter model
@@ -93,5 +101,12 @@ instance RunModel Counter (ReaderT (IORef Int) IO) where
       writeIORef ref 0
       pure n
 
+  perform' Inc _ = do
+    ref <- ask
+    lift $ atomicModifyIORef' ref ((,()) . succ)
+  perform' Reset _ = do
+    ref <- ask
+    lift $ atomicModifyIORef' ref (\n -> (0, n))
+
   postcondition (Counter n, _) Reset _ res = pure $ n == res
   postcondition _ _ _ _ = pure True

quickcheck-dynamic/test/Spec/DynamicLogic/RegistryModel.hs

@@ -128,6 +128,24 @@ instance RunModel RegState RegM where
     lift $ threadDelay 100
     pure $ Right ()
 
+  perform' Spawn _ = do
+    tid <- lift $ forkIO (threadDelay 10000000)
+    pure $ Right tid
+  perform' (Register name tid) env = do
+    reg <- ask
+    lift $ try $ register reg name (env tid)
+  perform' (Unregister name) _ = do
+    reg <- ask
+    lift $ try $ unregister reg name
+  perform' (WhereIs name) _ = do
+    reg <- ask
+    res <- lift $ whereis reg name
+    pure $ Right res
+  perform' (KillThread tid) env = do
+    lift $ killThread (env tid)
+    lift $ threadDelay 100
+    pure $ Right ()
+
   postcondition (s, _) (WhereIs name) env mtid = do
     pure $ (env <$> Map.lookup name (regs s)) == mtid
   postcondition _ _ _ _ = pure True

quickcheck-dynamic/test/Test/QuickCheck/StateModelSpec.hs

@@ -12,9 +12,11 @@ import Test.QuickCheck.Extras (runPropertyReaderT)
 import Test.QuickCheck.Monadic (assert, monadicIO, monitor, pick)
 import Test.QuickCheck.StateModel (
   Actions,
+  ParActions,
   lookUpVarMaybe,
   mkVar,
   runActions,
+  runParallelActions,
   underlyingState,
   viewAtType,
   pattern Actions,
@@ -29,6 +31,7 @@ tests =
   testGroup
     "Running actions"
     [ testProperty "simple counter" $ prop_counter
+    , testProperty "par simple counter" $ prop_counter'
     , testProperty "returns final state updated from actions" prop_returnsFinalState
     , testProperty "environment variables indices are 1-based " prop_variablesIndicesAre1Based
     , testCase "prints distribution of actions and polarity" $ do
@@ -51,6 +54,12 @@ prop_counter as = monadicIO $ do
   runPropertyReaderT (runActions as) ref
   assert True
 
+prop_counter' :: ParActions Counter -> Property
+prop_counter' as = monadicIO $ do
+  ref <- lift $ newIORef (0 :: Int)
+  runPropertyReaderT (runParallelActions as) ref
+  assert True
+
 prop_returnsFinalState :: Actions SimpleCounter -> Property
 prop_returnsFinalState actions@(Actions as) =
   monadicIO $ do