Property-testing Side Effects

dejafu-0.7.0.0 brings with it a new module for property-testing the side-effects of stateful expressions. It’s just a wrapper around the unit-testing stuff dejafu always did, but it’s more convenient than handling things like supplying random arguments and comparing results yourself.

We can check if two expressions have equivalent behaviours, or if one has fewer behaviours than the other. Such properties can serve both as documentation and as regression tests.

Let’s dive straight into an example:

Is readMVar equivalent to a takeMVar followed by a putMVar?

We might phrase this property like so:

prop_read_equiv_take_put =
  sig readMVar `equivalentTo` sig (\v -> takeMVar v >>= putMVar v)

Set-up

The property-testing uses signatures, where a signature tells dejafu how to (1) create a new state; (2) make some observation of the state; (3) concurrently interfere with the state in some way; and (4) the expression to evaluate.

State type

Properties are monomorphic, so we can’t directly express a property about any MVar, we need to pick a concrete type for its contents. Let’s just pick Int:

type State = MVar ConcIO Int

Properties operate in the ConcIO monad. There is no option to use ConcST yet, as I couldn’t get a nice interface working which didn’t break type inference in GHCi.

Initialisation

The state is constructed using a pure seed value the property-checker generates. We want to consider both full and empty MVars, so we’ll ask it to supply a Maybe Int:

type Seed = Maybe Int

The initialisation function we will include in the signature then just calls newMVar or newEmptyMVar as appropriate:

makeMVar :: Seed -> ConcIO State
makeMVar (Just x) = newMVar x
makeMVar Nothing  = newEmptyMVar

Seed values are generated using LeanCheck, an enumerative property-based testing library.

Observation

We want to know if the MVar contains a value when we observe it, and we want to know what that value is; another Maybe:

type Observation = Maybe Int

It is important that the observation function does not block, so we use tryReadMVar here rather than readMVar or takeMVar:

observeMVar :: State -> Seed -> ConcIO Observation
observeMVar v _ = tryReadMVar v

It does not matter if making the observation has side-effects, so tryTakeMVar would have been equally valid.

Interference

Our interference function will just mess with the value in the MVar:

interfereMVar :: State -> Seed -> ConcIO ()
interfereMVar mvar mx = do
  tryTakeMVar mvar
  void . tryPutMVar mvar $ case mx of
    Just x  -> (x+1) * 3000
    Nothing -> 7000

As LeanCheck is enumerative, large values like 3000 and 7000 will stand out if the tool reports a failure.

Signature

Now we package these operations up into a signature:

sig :: (State -> ConcIO a) -> Sig State Observation Seed
sig e = Sig
  { initialise = makeMVar
  , observe    = observeMVar
  , interfere  = interfereMVar
  , expression = void . e
  }

We could, of course, have defined all this inside sig without the top-level functions and type synonyms.

Properties

Now we can test the property:

> check $ sig readMVar `equivalentTo` sig (\v -> takeMVar v >>= putMVar v)
*** Failure: (seed Just 0)
    left:  [(Nothing,Just 3000)]
    right: [(Nothing,Just 0),(Nothing,Just 3000),(Just Deadlock,Just 3000)]

We get a failure! This is because the left term is atomic, whereas the right is not: another thread writing to the MVar has the opportunity to swoop in and insert a new value after the takeMVar but before the putMVar. The right has strictly more behaviours than the left.

We can capture this, by using a different comparison:

> check $ sig readMVar `strictlyRefines` sig (\v -> takeMVar v >>= putMVar v)
+++ OK

To “strictly refine” something is to have a proper subset of the behaviour. There is also a “refines” comparison, which does not require the subset to be proper.

Wait a minute…

• Doesn’t readMVar v return a different thing to takeMVar v >>= putMVar v?

  Yes!

  If they return at all, the former returns the value in the MVar, whereas the latter returns unit. Properties do not care about the return value of an expression, only the effects.

  You can see this by looking at the definition of sig again: it throws away the result of the expression using void.

• Both of our properties are of the form sig f `cmp` sig g, can’t that redundancy be removed?

  No!

  You can use different signatures with different state types! As long as the seed and observation types are the same, check can compare them.

  You can use this to compare different implementations of a similar concurrent data structure.

Properties with arguments

Properties can also have arguments, using LeanCheck to generate their values. This doesn’t work in any mysterious way, here’s a property about the QSemN functions:

> check $ \x y -> sig' (\v -> signalQSemN v (x + y)) `equivalentTo` sig' (\v -> signalQSemN v x >> signalQSemN v y)
*** Failure: -1 1 (seed 0)
    left:  [(Nothing,0)]
    right: [(Nothing,0),(Just Deadlock,0)]

You can even use your own types, as long as they have a Listable (the typeclass LeanCheck uses) instance:

> :{
newtype Nat n = Nat n deriving Show
instance (Num n, Ord n, Listable n) => Listable (Nat n) where
  list = [Nat n | n <- list, n >= 0]
:}

> check $ \(Nat x) (Nat y) -> sig' (\v -> signalQSemN v (x + y)) `equivalentTo` sig' (\v -> signalQSemN v x >> signalQSemN v y)
+++ OK!

Currently it’s a bit slow as I need to fiddle with the implementation and work out what a good number of tests to run is. check uses 10 seed values with 100 variable assignments each (1000 tests total), you can use checkFor to reduce that.

Fin

So there you have it, property-testing for side-effects of stateful operations.

This has come out of my work on CoCo, a tool for automatically discovering these properties (paper here). In the CoCo repository are a few more examples. CoCo is still a work-in-progress, but one of the goals is to be able to generate dejafu-compatible output, so that CoCo can discover properties which dejafu can immediately begin using for regression testing.