# 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.