Merge pull request #43 from jasagredo/js/replicate-in-forall

Replicate parallel executions in `forallParallelCommands`
stevana · Apr 2, 2024 · bce278e · bce278e
2 parents 3748220 + 7553d3e
commit bce278e
Show file tree

Hide file tree

Showing 17 changed files with 398 additions and 614 deletions.
diff --git a/README.md b/README.md
@@ -313,8 +313,6 @@ ParallelCommands
 └──────────────────────────────────────────────┘ │
 
 AnnotateC "Read" (PredicateC (1 :/= 2))
-
-However, some repetitions of this sequence of commands passed. Maybe there is a race condition?
 ```
 
 As we can see above, a mutable reference is first created, and then in
@@ -380,12 +378,10 @@ follows:
          times with the part of the generated list that doesn't belong to the
          prefix.
 
-  2. initialize the state machine if necessary (see [this](#sut-initialization));
-
-  3. execute the prefix sequentially as in the section above (checking pre- and
+  2. execute the prefix sequentially as in the section above (checking pre- and
      post-conditions);
 
-  4. execute the suffixes in parallel without checking pre/post-conditions
+  3. execute the suffixes in parallel without checking pre/post-conditions
      and gather the trace (or history) of invocations and responses of each
      action;
 
@@ -409,24 +405,24 @@ Commands: [A, B] ─┤        ├──┤        │     ├─ executed `conc
                 executed sequentially
 ```
 
-  5. if something goes wrong when executing the commands, shrink the generated
+  4. if something goes wrong when executing the commands, shrink the generated
      commands and present a minimal counterexample;
 
-  6. otherwise, try to find a possible sequential interleaving of action
+  5. otherwise, try to find a possible sequential interleaving of action
      invocations and responses that respects the post-conditions. For each
      interleaving, this is done by advancing the `Concrete` model (starting at
      `initialModel`) through the sequence of pairs of invocations to `command
      Concrete` and the returned `response Concrete` emitted at step 3, and
      checking the post-condition for each pair.
 
-  7. if no possible sequential interleaving was found, then shrink the generated
+  6. if no possible sequential interleaving was found, then shrink the generated
      commands and present a minimal counterexample.
 
 The last two steps basically try to find
 a [linearisation](https://en.wikipedia.org/wiki/Linearizability) of calls that
 could have happend on a single thread.
 
-Notice that step 6 above introduces a subtlety in the post-condition checks and
+Notice that step 5 above introduces a subtlety in the post-condition checks and
 transitions for the `model Concrete`. Despite the system under test running in a
 concurrent way, the model can still be designed to work sequentially as *it will
 not be run in parallel*, it will only be advanced in a sequential way when
@@ -435,117 +431,11 @@ be correct with respect to sequential execution before used in parallel testing.
 
 As we cannot control the actual scheduling of the tasks, each sequence of
 commands (already fixed in a concrete prefix and a concrete list of suffixes) is
-actually executed several times by default, i.e. steps 2 to 7 will be executed
+actually executed several times by default, i.e. steps 2 to 6 will be executed
 multiple times for the same test case expecting that the scheduling of events
 varies between runs. One can further increase entropy by introducing random
 `threadDelay`s in the semantic function.
 
-#### Why is a parallel property failing?
-
-Unless in presence of more severe bugs, parallel properties can fail because of
-mainly two reasons: a race condition is happening or a logic bug is present in
-the code. Taking advantage of the fact that we are repeating multiple times each
-sequence of commands, we can have some insight on which one of those cases seems
-to be the cause.
-
-The parallel counterexample will show one of the following messages:
-
-- `However, some repetitions of this sequence of commands passed. Maybe there is
-  a race condition?`: In this case as some parallel executions of a given
-  sequence of commands have passed, it seems that the test outcome is being
-  affected by a race condition or a non-deterministic error. This message is
-  accurate in the sense that a logic bug will not result in some repetitions
-  succeeding.
-- `And all repetitions of this sequence of commands failed. Maybe there is a
-  logic bug? Try with more repetitions to be sure that it happens consistently`:
-  In this case, one of two things can happen. Either there is a logic bug that
-  is triggered always (which is what the message suggest) or we were just super
-  unlucky (or super lucky, as we found an error) in this run and a race
-  condition manifested in all runs. In order to rule out this last case, one can
-  run the tests with more repetitions, which if the problem is that there is
-  indeed a race condition, should result in the other message being printed
-  instead.
-
-#### SUT initialization
-
-Some tests might require an environment that is used by the SUT to perform its
-actions, for example some mutable variable. In these cases, the environment
-should be isolated from other executions, and in parallel testing each sequence
-of commands is executed several times as noted in the previous paragraph. The
-way to ensure that the environment is not shared among those repetitions is by
-defining the state machine inside a monadic action and use the
-`runXCommandsXWithSetup` variants of the functions:
-
-``` haskell
-
-semantics :: Env -> Command Concrete -> m (Response Concrete)
-semantics = ...
-
-sm :: m (StateMachine Model Command m Response)
-sm = do
-  env <- initEnv {- initialize the environment -}
-  pure $ StateMachine {
-    ...
-    , QSM.semantics = semantics env
-  }
-
-smUnused :: StateMachine Model Command m Response
-smUnused = StateMachine {
-  ...
-  , QSM.semantics = error "SUT must not be used during command generation or shrinking"
-}
-
-prop = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $
-  prettyParallelCommands cmds =<< runParallelCommandsWithSetup sm cmds
-```
-
-This will ensure that each execution of the testcase initializes the environment
-as a first step.
-
-Note however that when running **sequential properties**, each test case is only
-executed once, therefore these two are completely equivalent:
-
-``` haskell
-sm :: m (StateMachine Model Command m Response)
-sm = do
-  env <- initEnv {- initialize the environment -}
-  pure $ StateMachine {
-    ...
-    , QSM.semantics = semantics env
-  }
-
-smUnused :: StateMachine Model Command m Response
-smUnused = StateMachine {
-  ...
-  , QSM.semantics = error "SUT must not be used during command generation or shrinking"
-}
-
-prop = forAllCommands smUnused $ \cmds -> monadicIO $
-  (hist, _model, res) <- runCommandsWithSetup sm cmds
-  prettyCommands smUnused hist (checkCommandNames cmds (res === Ok))
-```
-
-versus
-
-``` haskell
-sm :: Env -> StateMachine Model Command m Response
-sm env = StateMachine {
-    ...
-    , QSM.semantics = semantics env
-  }
-
-smUnused :: StateMachine Model Command m Response
-smUnused = StateMachine {
-  ...
-  , QSM.semantics = error "SUT must not be used during command generation or shrinking"
-}
-
-prop = forAllCommands smUnused $ \cmds -> monadicIO $
-  env <- initEnv {- initialize the environment -}
-  (hist, _model, res) <- runCommands (sm env) cmds
-  prettyCommands smUnused hist (checkCommandNames cmds (res === Ok))
-```
-
 ### More examples
 
 Here are some more examples to get you started:

diff --git a/src/Test/StateMachine.hs b/src/Test/StateMachine.hs
@@ -19,7 +19,6 @@ module Test.StateMachine
     forAllCommands
   , existsCommands
   , runCommands
-  , runCommandsWithSetup
   , prettyCommands
   , prettyCommands'
   , checkCommandNames
@@ -35,17 +34,12 @@ module Test.StateMachine
   -- * Parallel property combinators
   , forAllParallelCommands
   , forAllNParallelCommands
+  , forAllParallelCommandsNTimes
+  , forAllNParallelCommandsNTimes
   , runNParallelCommands
-  , runNParallelCommandsWithSetup
   , runParallelCommands
-  , runParallelCommandsWithSetup
   , runParallelCommands'
-  , runParallelCommandsNTimes
-  , runParallelCommandsNTimesWithSetup
-  , runNParallelCommandsNTimes'
-  , runParallelCommandsNTimes'
-  , runNParallelCommandsNTimes
-  , runNParallelCommandsNTimesWithSetup
+  , runNParallelCommands'
   , prettyNParallelCommands
   , prettyParallelCommands
   , prettyParallelCommandsWithOpts

diff --git a/src/Test/StateMachine/ConstructorName.hs b/src/Test/StateMachine/ConstructorName.hs
@@ -19,9 +19,9 @@ import           Data.Kind
 import           Data.Proxy
                    (Proxy(Proxy))
 import           GHC.Generics
-                   ((:*:)((:*:)), (:+:)(L1, R1), C, Constructor, D,
-                   Generic1, K1, M1, Rec1, Rep1, S, U1, conName, from1,
-                   unM1, unRec1)
+                   (C, Constructor, D, Generic1, K1, M1, Rec1, Rep1, S,
+                   U1, conName, from1, unM1, unRec1, (:*:)((:*:)),
+                   (:+:)(L1, R1))
 import           Prelude
 
 import           Test.StateMachine.Types