multiple threads + cleanup

Author: MaximilianAlgehed

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

@@ -2,7 +2,8 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 module Test.QuickCheck.ParallelActions where
 
-
+import Data.Set qualified as Set
+import Control.Monad
 import Control.Monad.Reader
 import Control.Monad.Writer
 import Data.Data
@@ -12,7 +13,7 @@ import Test.QuickCheck.Monadic
 import Test.QuickCheck.StateModel.Variables
 import Test.QuickCheck.StateModel
 import Control.Concurrent
-import Control.Arrow (first)
+import Control.Arrow (first, second)
 import Data.Tree
 
 class RunModel state m => RunModelPar state m where
@@ -24,51 +25,49 @@ class RunModel state m => RunModelPar state m where
 
 data ParallelActions state =
   ParallelActions { linearActions :: Actions state
-                  , threadATags :: [Int]
-                  , threadBTags :: [Int]
+                  , threads :: [[Int]]
                   } deriving (Eq, Generic)
 
 commonActions :: ParallelActions state -> [Step state]
 commonActions ParallelActions{linearActions = Actions steps, ..} =
-  [ step | step@(v := _) <- steps, notElem (unsafeVarIndex v) $ threadATags ++ threadBTags ]
-
-threadAActions :: ParallelActions state -> [Step state]
-threadAActions ParallelActions{linearActions = Actions steps, ..} =
-  [ v := s{polarity = PosPolarity} | v := s <- steps, elem (unsafeVarIndex v) threadATags ]
+  [ step | step@(v := _) <- steps, notElem (unsafeVarIndex v) $ concat threads ]
 
-threadBActions :: ParallelActions state -> [Step state]
-threadBActions ParallelActions{linearActions = Actions steps, ..} =
-  [ v := s{polarity = PosPolarity} | v := s <- steps, elem (unsafeVarIndex v) threadBTags ]
+threadActions :: ParallelActions state -> [[Step state]]
+threadActions ParallelActions{linearActions = Actions steps, ..} =
+  [ [ v := s{polarity = PosPolarity}
+    | v := s <- steps, elem (unsafeVarIndex v) thread ]
+  | thread <- threads
+  ]
 
 instance StateModel state => Show (ParallelActions state) where
   show pas =
-    unlines [ "-- Common Prefix:"
-            , showWithUsed (combineContexts (allVariables threadA) (allVariables threadB)) common
-            , "-- Thread A"
-            , show threadA
-            , "-- Thread B"
-            , show threadB
-            ]
+    unlines $ [ "-- Common Prefix:"
+              , showWithUsed (foldMap allVariables threads) common
+              ] ++ concat [ [ "-- Thread " ++ [n]
+                            , show thread
+                            ]
+                          | (n, thread) <- zip ['A'..'Z'] threads
+                          ]
     where
       common = Actions $ commonActions pas
-      threadA = Actions $ threadAActions pas
-      threadB = Actions $ threadBActions pas
+      threads = Actions <$> threadActions pas
 
 instance StateModel state => Arbitrary (ParallelActions state) where
   arbitrary = genParActions
 
-  shrink (ParallelActions actions as bs) =
-    filter checkParallelActions $ [ ParallelActions actions as bs | actions <- shrink actions ] ++
-                                  [ ParallelActions actions (tail as) bs | not $ null as ] ++
-                                  [ ParallelActions actions as (tail bs) | not $ null bs ]
+  shrink (ParallelActions actions trs) =
+    filter checkParallelActions $ [ ParallelActions actions $ filter (not . null) $ map (filter (`Set.member` vars)) trs
+                                  | actions <- shrink actions
+                                  , let vars = unsafeIndexSet $ allVariables actions
+                                  ] ++
+                                  [ ParallelActions actions $ trs ++ [ tr | not $ null tr ] ++ trs'
+                                  | (trs, _:tr, trs') <- holes' trs ]
 
 checkParallelActions :: StateModel state => ParallelActions state -> Bool
-checkParallelActions pas = checkWellTypedness commonCtx threadA && checkWellTypedness commonCtx threadB
+checkParallelActions pas = all (checkWellTypedness commonCtx) (threadActions pas)
   where
     commonCtx = allVariables common
     common = Actions $ commonActions pas
-    threadA = threadAActions pas
-    threadB = threadBActions pas
 
 checkWellTypedness :: StateModel state => VarContext -> [Step state] -> Bool
 checkWellTypedness _ [] = True
@@ -82,24 +81,22 @@ genParActions = do
   split <- choose (max 0 (n - 20), n - 1)
   let (common, post) = splitAt split steps
       commonCtx = allVariables common
-  (threadA, threadB) <- go post commonCtx commonCtx [] []
-  return $ ParallelActions as threadA threadB
-  where go :: [Step state] -> VarContext -> VarContext -> [Int] -> [Int] -> Gen ([Int], [Int])
-        go [] _ctxA _ctxB tA tB = return (reverse tA, reverse tB)
-        go ((v := a) : ss) ctxA ctxB tA tB = do
-          let candidates = [ 'a' | a `wellTypedIn` ctxA ] ++ [ 'b' | a `wellTypedIn` ctxB ]
-              i = unsafeVarIndex v
+  tc <- choose (2, 5)
+  threads <- go post $ replicate tc (commonCtx, [])
+  return $ ParallelActions as $ filter (not . null) threads
+  where go :: [Step state] -> [(VarContext, [Int])] -> Gen [[Int]]
+        go [] trs = return $ map (reverse . snd) trs
+        go ((v := a) : ss) trs = do
+          let candidates = [ (ctx, tr, trs) | ((ctx, tr), trs) <- holes trs
+                                            , a `wellTypedIn` ctx ]
           if null candidates
           -- This means we made a mistake earlier and split two actions whose
           -- result variables were used together later. At this point we just
           -- give up and don't extend the traces.
-          then go [] ctxA ctxB tA tB
+          then go [] trs
           else do
-            c <- elements candidates
-            case c of
-              'a' -> go ss (extendContext ctxA v) ctxB (i : tA) tB
-              'b' -> go ss ctxA (extendContext ctxB v) tA (i : tB)
-              _   -> error "I'm the pope"
+            (ctx, tr, trs) <- elements candidates
+            go ss $ (extendContext ctx v, unsafeVarIndex v:tr) : trs
 
 data TraceStep state m where
   TraceStep :: (Typeable a, Show a)
@@ -123,16 +120,16 @@ runTracing env ((v := ap):as) = do
            | otherwise      = env
   (first (step :)) <$> runTracing env' as
 
-class Monad m => ForkYou m where
+class Monad m => Forking m where
   forkThread :: m a -> m (m a)
 
-instance ForkYou IO where
+instance Forking IO where
   forkThread io = do
     t <- newEmptyMVar
     forkIO $ io >>= putMVar t
     return $ takeMVar t
 
-instance ForkYou m => ForkYou (ReaderT r m) where
+instance Forking m => Forking (ReaderT r m) where
   forkThread m = do
     reg <- ask
     lift $ fmap lift (forkThread  $ runReaderT m reg)
@@ -141,22 +138,19 @@ runParActions :: ( StateModel state
                  , RunModelPar state m
                  , e ~ Error state m
                  , forall a. IsPerformResult e a
-                 , ForkYou m
+                 , Forking m
                  ) => ParallelActions state -> PropertyM m ()
 runParActions pas = do
   (trC, env) <- run $ runTracing mempty $ commonActions pas
-  joinA <- run $ forkThread $ runTracing env (threadAActions pas)
-  joinB <- run $ forkThread $ runTracing env (threadBActions pas)
-  (trA, _) <- run joinA
-  (trB, _) <- run joinB
+  joins <- mapM (run . forkThread . runTracing env) (threadActions pas)
+  trs <- mapM (fmap fst . run) joins
   let used = varsUsedInActions $ linearActions pas
   monitor $ counterexample "-- Main thread:"
   monitorTrace used mempty trC
-  monitor $ counterexample "\n-- Thread A:"
-  monitorTrace used env trA
-  monitor $ counterexample "\n-- Thread B:"
-  monitorTrace used env trB
-  let ilvs = prepend trC $ interleavings trA trB
+  forM (zip ['A'..'Z'] trs) $ \ (n, tr) -> do
+    monitor $ counterexample $ "\n-- Thread " ++ [n, ':']
+    monitorTrace used env tr
+  let ilvs = prepend trC $ interleavings trs
   monitor $ tabulate "TraceTree size" (map (bucket . length) ilvs)
   assert $ null ilvs || any (checkTrace initialAnnotatedState mempty) ilvs
   -- TODO: stats collection and cleanup
@@ -201,15 +195,21 @@ prepend :: [a] -> [Tree a] -> [Tree a]
 prepend []     ts = ts
 prepend (p:ps) ts = [Node p $ prepend ps ts]
 
-interleavings :: [a] -> [a] -> [Tree a]
-interleavings [] bs = prepend bs []
-interleavings as [] = prepend as []
-interleavings (a:as) (b:bs) = [Node a (interleavings as (b:bs)), Node b (interleavings (a:as) bs)]
+interleavings :: [[a]] -> [Tree a]
+interleavings aas = do
+  (a:as, os) <- holes aas
+  pure $ Node a (interleavings (as:os))
+
+holes :: [a] -> [(a, [a])]
+holes [] = []
+holes (a:as) = (a, as) : map (second (a:)) (holes as)
+
+holes' :: [a] -> [([a], a, [a])]
+holes' [] = []
+holes' (a:as) = ([], a, as) : [ (a:bs, a', as') | (bs, a', as') <- holes' as ]
 
 -- TODO:
---  - Decide how much of the old QCD interface we can afford to break
---  - Refactor normal QCD so that you don't have two implementations
---  - More than two threads
 --  - More examples
+--  - Refactor normal QCD so that you don't have two implementations
 --  - Clean everything up
 --  - All the statistics and monitoring

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

@@ -352,11 +352,11 @@ instance Eq (Actions state) where
   Actions as == Actions as' = as == as'
 
 instance StateModel state => Show (Actions state) where
-  show = showWithUsed emptyContext
+  show = showWithUsed mempty
 
 showWithUsed :: StateModel state => VarContext -> Actions state -> String
 showWithUsed ctx (Actions as) =
-    let as' = WithUsedVars (combineContexts ctx $ varsUsedInActions (Actions as)) <$> as
+    let as' = WithUsedVars (ctx <> varsUsedInActions (Actions as)) <$> as
      in intercalate "\n" $ zipWith (++) ("do " : repeat "   ") (map show as' ++ ["pure ()" | null as'])
 
 varsUsedInActions :: forall state. StateModel state => Actions state -> VarContext

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

@@ -16,12 +16,11 @@ module Test.QuickCheck.StateModel.Variables (
   isWellTyped,
   allVariables,
   isEmptyCtx,
+  wellTypedIn,
   unsafeVarIndex,
   unsafeCoerceVar,
   unsafeNextVarIndex,
-  wellTypedIn,
-  combineContexts,
-  emptyContext,
+  unsafeIndexSet,
 ) where
 
 import Data.Data
@@ -114,6 +113,9 @@ instance Show VarContext where
       -- The use of typeRep here is on purpose to avoid printing `Var` unnecessarily.
       showBinding (Some v) = show v ++ " :: " ++ show (typeRep v)
 
+unsafeIndexSet :: VarContext -> Set Int
+unsafeIndexSet (VarCtx ctx) = Set.map (\(Some v) -> unsafeVarIndex v) ctx
+
 isEmptyCtx :: VarContext -> Bool
 isEmptyCtx (VarCtx ctx) = null ctx
 
@@ -132,12 +134,6 @@ wellTypedIn a ctx = all (\(Some v) -> v `isWellTyped` ctx) (getAllVariables a)
 extendContext :: (Typeable a, Show a) => VarContext -> Var a -> VarContext
 extendContext (VarCtx ctx) v = VarCtx $ Set.insert (Some v) ctx
 
-emptyContext :: VarContext
-emptyContext = VarCtx mempty
-
-combineContexts :: VarContext -> VarContext -> VarContext
-combineContexts (VarCtx c0) (VarCtx c1) = VarCtx $ c0 <> c1
-
 allVariables :: HasVariables a => a -> VarContext
 allVariables = VarCtx . getAllVariables
 

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

@@ -181,7 +181,7 @@ showDictAction KillThread{} = ShowDict
 instance GoodMonad m => DynLogicModel (RegState m) where
   restricted _ = False
 
-instance ForkYou (IOSim s) where
+instance Forking (IOSim s) where
   forkThread io = do
     t <- atomically newEmptyTMVar
     forkIO $ io >>= atomically . putTMVar t