search

advancedtelematic / quickcheck-state-machine

Test monadic programs using state machine based models
Other
203 stars 25 forks source link

Generalize to N threads #294

Closed kderme closed 5 years ago

kderme commented 5 years ago

This pr is WIP. Related issue https://github.com/advancedtelematic/quickcheck-state-machine/issues/15 So far Parallel Commands were executed by 2 threads. In this Pr I generalize this: each suffix, instead of a Pair of Commands is now a list of Commands and each thread executes one of them.

Things TODO/future improvements:

About the BUG (Edit: Fixed):

The bug is on shrinking, probably at shrinkAndValidateGeneralParallel, somewhere in the combination of environments (I have left a comment in code). The bug some times appears, when I run prop_general_parallel of MemoryReference, with 2,3 or 4 threads and a Race Bug:

OK (0.66s)
      +++ OK, failed as expected. (after 9 tests and 3 shrinks):
      Exception:
        executeCommands: impossible 
        Left (EnvironmentValueNotFound (Var 0))
        CallStack (from HasCallStack):
          error, called at src/Test/StateMachine/Sequential.hs:336:33 in quickcheck-state-machine-0.6.0-34jzR3JpmPESvqdQjrvbB:Test.StateMachine.Sequential
      ParallelCommands
        { prefix =
            Commands
              { unCommands =
                  [ Command Create (Created (Reference (Symbolic (Var 0)))) [ Var 0 ]
                  ]
              }
        , suffixes =
            [ []
            , [ Commands
                  { unCommands =
                      [ Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 0) [] ]
                  }
              ]
            ]
        }
      *** Exception running callback: 
      executeCommands: impossible 
      Left (EnvironmentValueNotFound (Var 0))
      CallStack (from HasCallStack):
        error, called at src/Test/StateMachine/Sequential.hs:336:33 in quickcheck-state-machine-0.6.0-34jzR3JpmPESvqdQjrvbB:Test.StateMachine.Sequential

The test seems to succeed (or maybe fail as expected), but it fails for the wrong reason. I am not quite sure why the example above throws the EnvironmentValueNotFound, I need to dig a bit deeper.

(By the way these kind of false positives makes me think expectFailure should fail in such cases, something you mention there https://github.com/nick8325/quickcheck/issues/230)

kderme commented 5 years ago

Most of the times, it successfully shrinks

+++ OK, failed as expected. Falsifiable (after 16 tests and 12 shrinks):
 ParallelCommands
        { prefix =
            Commands
              { unCommands =
                  [ Command Create (Created (Reference (Symbolic (Var 0)))) [ Var 0 ]
                  ]
              }
        , suffixes =
            [ [ Commands
                  { unCommands =
                      [ Command (Increment (Reference (Symbolic (Var 0)))) Incremented []
                      , Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 1) []
                      ]
                  }
              , Commands
                  { unCommands =
                      [ Command (Write (Reference (Symbolic (Var 0))) 2) Written [] ]
                  }
              ]
            ]
        }
kderme commented 5 years ago

review mostly addressed and added new examples. At the new examples the bug never appears, only on MemoryReference.

stevana commented 5 years ago

At the new examples the bug never appears, only on MemoryReference

The bug is probably related to references. Neither the echo nor ticket dispenser examples use references. The error encountered example does use them, but it also shortcuts generation quite early due to the ErrorEncountered state, which perhaps makes the bug manifest itself less often.

kderme commented 5 years ago

@stevana I found some time to fix this bug. The issue was that it's possible to shrink to less threads than initially specified, so you could end up with a suffix which is an empty list. In my generalisation, I use mconcat to combine the resulting environments of each thread, but when the list is empty, mconcat gives an empty environment, which later resulted in EnvironmentValueNotFound when the next suffix was executed,

stevana commented 5 years ago

Regarding optimisation: there's a section called "Parallelism in test cases" in the paper Finding Race Conditions in Erlang with QuickCheck and PULSE that contains some useful analysis.

stevana commented 5 years ago

Their setting is slightly different than ours though, as we execute batches of commands in parallel, then synchronise...

stevana commented 5 years ago

Regarding visualisation: perhaps it's easier to use/read graphviz (dot) instead of ASCII?

Examples:

kderme commented 5 years ago

Regarding visualisation: perhaps it's easier to use/read graphviz (dot) instead of ASCII?

Examples:

Agree ASCII gets messed up sometimes.

kderme commented 5 years ago

First commit is the one from here https://github.com/advancedtelematic/quickcheck-state-machine/pull/315 (Ci fails, but I think this is because some test takes too long..). Also shrinking properties are now added.

stevana commented 5 years ago

I agree that visualising counterexamples for N-parallel programs can be a separate PR.

kderme commented 5 years ago

Closed in favor of https://github.com/advancedtelematic/quickcheck-state-machine/pull/324