quickcheck-state-machine: Test monadic programs using state machine based models

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

See README at https://github.com/advancedtelematic/quickcheck-state-machine#readme

[Skip to Readme]


Versions 0.0.0, 0.1.0, 0.2.0, 0.3.0, 0.3.1, 0.3.1, 0.4.0, 0.4.1, 0.4.2, 0.4.3, 0.5.0, 0.6.0, 0.7.0, 0.7.1, 0.7.2, 0.7.3, 0.8.0, 0.9.0
Change log CHANGELOG.md
Dependencies ansi-wl-pprint (>=, async (>=, base (>=4.7 && <5), containers (>=, lifted-async (>=0.9.3), lifted-base (>=, monad-control (>=, mtl (>=2.2.1), QuickCheck (>=2.9.2), quickcheck-with-counterexamples (>=1.0), random (>=1.1), stm (>=, template-haskell (>=, th-abstraction (>= [details]
License BSD-3-Clause
Copyright Copyright (C) 2017, ATS Advanced Telematic Systems GmbH
Author Stevan Andjelkovic
Maintainer Stevan Andjelkovic <stevan@advancedtelematic.com>
Category Testing
Home page https://github.com/advancedtelematic/quickcheck-state-machine#readme
Source repo head: git clone https://github.com/advancedtelematic/quickcheck-state-machine
Uploaded by stevana at 2018-01-15T13:37:23Z




Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Readme for quickcheck-state-machine-0.3.1

[back to package description]


Hackage Stackage Nightly Stackage LTS Build Status

quickcheck-state-machine is a Haskell library, based on QuickCheck, for testing stateful programs. The library is different from the Test.QuickCheck.Monadic approach in that it lets the user specify the correctness by means of a state machine based model using pre- and post-conditions. The advantage of the state machine approach is twofold: 1) specifying the correctness of your programs becomes less adhoc, and 2) you get testing for race conditions for free.

The combination of state machine based model specification and property based testing first appeard in Erlang's proprietary QuickCheck. The quickcheck-state-machine library can be seen as an attempt to provide similar functionality to Haskell's QuickCheck library.


As a first example, let's implement and test programs using mutable references. Our implementation will be using IORefs, but let's start with a representation of what actions are possible with programs using mutable references. Our mutable references can be created, read from, written to and incremented:

data Action (v :: * -> *) :: * -> * where
  New   ::                                     Action v (Opaque (IORef Int))
  Read  :: Reference v (Opaque (IORef Int)) -> Action v Int
  Write :: Reference v (Opaque (IORef Int)) -> Int -> Action v ()
  Inc   :: Reference v (Opaque (IORef Int)) -> Action v ()

When we generate actions we won't be able to create arbitrary IORefs, that's why all uses of IORefs are wrapped in Reference v, where the parameter v will let us use symbolic references while generating (and concrete ones when executing).

In order to be able to show counterexamples, we need a show instance for our actions. IORefs don't have a show instance, thats why we wrap them in Opaque; which gives a show instance to a type that doesn't have one.

Next, we give the actual implementation of our mutable references. To make things more interesting, we parametrise the semantics by a possible problem.

data Problem = None | Bug | RaceCondition
  deriving Eq

semantics :: Problem -> Action Concrete resp -> IO resp
semantics _   New           = Opaque <$> newIORef 0
semantics _   (Read  ref)   = readIORef  (opaque ref)
semantics prb (Write ref i) = writeIORef (opaque ref) i'
  -- One of the problems is a bug that writes a wrong value to the
  -- reference.
  i' | i `elem` [5..10] = if prb == Bug then i + 1 else i
     | otherwise        = i
semantics prb (Inc   ref)   =
  -- The other problem is that we introduce a possible race condition
  -- when incrementing.
  if prb == RaceCondition
  then do
    i <- readIORef (opaque ref)
    threadDelay =<< randomRIO (0, 5000)
    writeIORef (opaque ref) (i + 1)
    atomicModifyIORef' (opaque ref) (\i -> (i + 1, ()))

Note that above v is instantiated to Concrete, which is essentially the identity type, so while writing the semantics we have access to real IORefs.

We now have an implementation, the next step is to define a model for the implementation to be tested against. We'll use a simple map between references and integers as a model.

newtype Model v = Model [(Reference v (Opaque (IORef Int)), Int)]

initModel :: Model v
initModel = Model []

The pre-condition of an action specifies in what context the action is well-defined. For example, we can always create a new mutable reference, but we can only read from references that already have been created. The pre-conditions are used while generating programs (lists of actions).

precondition :: Model Symbolic -> Action Symbolic resp -> Bool
precondition _         New           = True
precondition (Model m) (Read  ref)   = ref `elem` map fst m
precondition (Model m) (Write ref _) = ref `elem` map fst m
precondition (Model m) (Inc   ref)   = ref `elem` map fst m

The transition function explains how actions change the model. Note that the transition function is polymorphic in v. The reason for this is that we use the transition function both while generating and executing.

transition :: Model v -> Action v resp -> v resp -> Model v
transition (Model m) New           ref = Model (m ++ [(Reference ref, 0)])
transition m         (Read  _)     _   = m
transition (Model m) (Write ref i) _   = Model (update ref i         m)
transition (Model m) (Inc   ref)   _   = Model (update ref (old + 1) m)
  Just old = lookup ref m

update :: Eq a => a -> b -> [(a, b)] -> [(a, b)]
update ref i m = (ref, i) : filter ((/= ref) . fst) m

Post-conditions are checked after we executed an action and got access to the result.

postcondition :: Model Concrete -> Action Concrete resp -> resp -> Bool
postcondition _         New         _    = True
postcondition (Model m) (Read ref)  resp = lookup ref m == Just resp
postcondition _         (Write _ _) _    = True
postcondition _         (Inc _)     _    = True

Finally, we have to explain how to generate and shrink actions.

generator :: Model Symbolic -> Gen (Untyped Action)
generator (Model m)
  | null m    = pure (Untyped New)
  | otherwise = frequency
      [ (1, pure (Untyped New))
      , (8, Untyped .    Read  <$> elements (map fst m))
      , (8, Untyped <$> (Write <$> elements (map fst m) <*> arbitrary))
      , (8, Untyped .    Inc   <$> elements (map fst m))

shrinker :: Action v resp -> [Action v resp]
shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]
shrinker _             = []

To be able to fit the code on a line we pack up all of them above into a record.

sm :: Problem -> StateMachine Model Action IO
sm prb = stateMachine
  generator shrinker precondition transition
  postcondition initModel (semantics prb) id

We can now define a sequential property as follows.

prop_references :: Problem -> PropertyOf (Program Action)
prop_references prb = monadicSequentialC sm' $ \prog -> do
  (hist, _, res) <- runProgram sm' prog
  prettyProgram sm' hist $
    checkActionNames prog (res === Ok)
  sm' = sm prb

If we run the sequential property without introducing any problems to the semantics function, i.e. quickCheck (prop_references None), then the property passes. If we however introduce the bug problem, then it will fail with the minimal counterexample:

> quickCheck (prop_references Bug)
*** Failed! Falsifiable (after 19 tests and 3 shrinks):

Model []

    New --> Opaque

Model [(Reference Concrete Opaque,0)]

    Write (Reference (Symbolic (Var 0))) 5 --> ()

Model [(Reference Concrete Opaque,5)]

    Read (Reference (Symbolic (Var 0))) --> 6

Model [(Reference Concrete Opaque,5)]

PostconditionFailed /= Ok

Recall that the bug problem causes the write of values i `elem` [5..10] to actually write i + 1.

Running the sequential property with the race condition problem will not uncover the race condition.

If we however define a parallel property as follows.

prop_referencesParallel :: Problem -> Property
prop_referencesParallel prb = monadicParallel (sm prb) $ \prog ->
  prettyParallelProgram prog =<< runParallelProgram (sm prb) prog

And run it using the race condition problem, then we'll find the race condition:

> quickCheck (prop_referencesParallel RaceCondition)
*** Failed! (after 8 tests and 6 shrinks):

Couldn't linearise:

│ Var 0 ← New                    │
│                       → Opaque │
┌─────────────┐ │
│ Inc (Var 0) │ │
│             │ │ ┌──────────────┐
│             │ │ │ Inc (Var 0)  │
│        → () │ │ │              │
└─────────────┘ │ │              │
                │ │         → () │
                │ └──────────────┘
                │ ┌──────────────┐
                │ │ Read (Var 0) │
                │ │          → 1 │
                │ └──────────────┘
Just 2 /= Just 1

As we can see above, a mutable reference is first created, and then in parallel (concurrently) we do two increments of said reference, and finally we read the value 1 while the model expects 2.

Recall that incrementing is implemented by first reading the reference and then writing it, if two such actions are interleaved then one of the writes might end up overwriting the other one -- creating the race condition.

We shall come back to this example below, but if your are impatient you can find the full source code here.

How it works

The rough idea is that the user of the library is asked to provide:

The library then gives back a bunch of combinators that let you define a sequential and a parallel property.

Sequential property

The sequential property checks if the model is consistent with respect to the semantics. The way this is done is:

  1. generate a list of actions;

  2. starting from the initial model, for each action do the the following:

    1. check that the pre-condition holds;
    2. if so, execute the action using the semantics;
    3. check if the the post-condition holds;
    4. advance the model using the transition function.
  3. If something goes wrong, shrink the initial list of actions and present a minimal counterexample.

Parallel property

The parallel property checks if parallel execution of the semantics can be explained in terms of the sequential model. This is useful for trying to find race conditions -- which normally can be tricky to test for. It works as follows:

  1. generate a list of actions that will act as a sequential prefix for the parallel program (think of this as an initialisation bit that setups up some state);

  2. generate two lists of actions that will act as parallel suffixes;

  3. execute the prefix sequentially;

  4. execute the suffixes in parallel and gather the a trace (or history) of invocations and responses of each action;

  5. try to find a possible sequential interleaving of action invocations and responses that respects the post-conditions.

The last step basically tries to find a linearisation of calls that could have happend on a single thread.

More examples

Here are some more examples to get you started:

All examples have an associated Spec module located in the example/test directory. These make use of the properties in the examples, and get tested as part of Travis CI.

To get a better feel for the examples it might be helpful to git clone this repo, cd into the example/ directory and fire up stack ghci and run the different properties interactively.

How to contribute

The quickcheck-state-machine library is still very experimental.

We would like to encourage users to try it out, and join the discussion of how we can improve it on the issue tracker!

See also


BSD-style (see the file LICENSE).