Property-testing Side Effects

Date
Tags coco, dejafu, haskell, programming
Target Audience Haskell programmers.
Attention Conservation Notice dejafu-0.7.0.0 can check if a concurrent program is equivalent to or a refinement of another, using observational equivalence of side-effects.

de­jafu-0.7.0.0 brings with it a new module for prop­er­ty-testing the side-ef­fects of stateful ex­pres­sions. It’s just a wrapper around the unit-testing stuff de­jafu al­ways did, but it’s more con­venient than hand­ling things like sup­plying random ar­gu­ments and com­paring res­ults your­self.

We can check if two ex­pres­sions have equi­valent be­ha­viours, or if one has fewer be­ha­viours than the other. Such prop­er­ties can serve both as doc­u­ment­a­tion and as re­gres­sion tests.

Let’s dive straight into an ex­ample:

Is read­MVar equi­valent to a takeMVar fol­lowed by a put­MVar?

We might phrase this prop­erty like so:

prop_read_equiv_­take_put =
  sig read­MVar `equi­val­entTo` sig (\v -> takeMVar v >>= put­MVar v)

Set-up

The prop­er­ty-testing uses sig­na­tures, where a sig­na­ture tells de­jafu how to (1) create a new state; (2) make some ob­ser­va­tion of the state; (3) con­cur­rently in­ter­fere with the state in some way; and (4) the ex­pres­sion to eval­u­ate.

State type

Prop­er­ties are mono­morphic, so we can’t dir­ectly ex­press a prop­erty about any MVar, we need to pick a con­crete type for its con­tents. Let’s just pick Int:

type State = MVar ConcIO Int

Prop­er­ties op­erate in the ConcIO monad. There is no op­tion to use ConcST yet, as I couldn’t get a nice in­ter­face working which didn’t break type in­fer­ence in GHCi.

Ini­tial­isa­tion

The state is con­structed using a pure seed value the prop­er­ty-checker gen­er­ates. We want to con­sider both full and empty MVars, so we’ll ask it to supply a Maybe Int:

type Seed = Maybe Int

The ini­tial­isa­tion func­tion we will in­clude in the sig­na­ture then just calls new­MVar or newEmptyMVar as ap­pro­pri­ate:

makeMVar :: Seed -> ConcIO State
makeMVar (Just x) = new­MVar x
makeMVar Nothing  = newEmptyMVar

Seed values are gen­er­ated using LeanCheck, an enu­mer­ative prop­er­ty-­based testing lib­rary.

Ob­ser­va­tion

We want to know if the MVar con­tains a value when we ob­serve it, and we want to know what that value is; an­other Maybe:

type Ob­ser­va­tion = Maybe Int

It is im­portant that the ob­ser­va­tion func­tion does not block, so we use tryRead­MVar here rather than read­MVar or takeMVar:

ob­serveMVar :: State -> Seed -> ConcIO Ob­ser­va­tion
ob­serveMVar v _ = tryRead­MVar v

It does not matter if making the ob­ser­va­tion has side-ef­fects, so tryTakeMVar would have been equally valid.

In­ter­fer­ence

Our in­ter­fer­ence func­tion will just mess with the value in the MVar:

in­ter­fereMVar :: State -> Seed -> ConcIO ()
in­ter­fereMVar mvar mx = do
  tryTakeMVar mvar
  void . try­Put­MVar mvar $ case mx of
    Just x  -> (x+1) * 3000
    Nothing -> 7000

As LeanCheck is enu­mer­at­ive, large values like 3000 and 7000 will stand out if the tool re­ports a fail­ure.

Sig­na­ture

Now we package these op­er­a­tions up into a sig­na­ture:

sig :: (State -> ConcIO a) -> Sig State Ob­ser­va­tion Seed
sig e = Sig
  { ini­tialise = makeMVar
  , ob­serve    = ob­serveMVar
  , in­ter­fere  = in­ter­fereMVar
  , ex­pres­sion = void . e
  }

We could, of course, have defined all this in­side sig without the top-­level func­tions and type syn­onyms.

Prop­er­ties

Now we can test the prop­erty:

> check $ sig read­MVar `equi­val­entTo` sig (\v -> takeMVar v >>= put­MVar v)
*** Fail­ure: (seed Just 0)
    left:  [(Noth­ing,Just 3000)]
    right: [(Noth­ing,Just 0),(Noth­ing,Just 3000),(Just Dead­lock­,Just 3000)]

We get a fail­ure! This is be­cause the left term is atomic, whereas the right is not: an­other thread writing to the MVar has the op­por­tunity to swoop in and in­sert a new value after the takeMVar but be­fore the put­MVar. The right has strictly more be­ha­viours than the left.

We can cap­ture this, by using a dif­ferent com­par­ison:

> check $ sig read­MVar `strict­lyRe­fines` sig (\v -> takeMVar v >>= put­MVar v)
+++ OK

To “strictly re­fine” some­thing is to have a proper subset of the be­ha­viour. There is also a “re­fines” com­par­ison, which does not re­quire the subset to be proper.

Wait a minute…

  • Doesn’t read­MVar v re­turn a dif­ferent thing to takeMVar v >>= put­MVar v?

    Yes!

    If they re­turn at all, the former re­turns the value in the MVar, whereas the latter re­turns unit. Prop­er­ties do not care about the re­turn value of an ex­pres­sion, only the ef­fects.

    You can see this by looking at the defin­i­tion of sig again: it throws away the result of the ex­pres­sion using void.

  • Both of our prop­er­ties are of the form sig f `cmp` sig g, can’t that re­dund­ancy be re­moved?

    No!

    You can use dif­ferent sig­na­tures with dif­ferent state types! As long as the seed and ob­ser­va­tion types are the same, check can com­pare them.

    You can use this to com­pare dif­ferent im­ple­ment­a­tions of a sim­ilar con­cur­rent data struc­ture.

Prop­er­ties with ar­gu­ments

Prop­er­ties can also have ar­gu­ments, using LeanCheck to gen­erate their val­ues. This doesn’t work in any mys­ter­ious way, here’s a prop­erty about the QSemN func­tions:

> check $ \x y -> sig' (\v -> sig­nalQSemN v (x + y)) `equi­val­entTo` sig' (\v -> sig­nalQSemN v x >> sig­nalQSemN v y)
*** Fail­ure: -1 1 (seed 0)
    left:  [(Noth­ing,0)]
    right: [(Noth­ing,0),(Just Dead­lock­,0)]

You can even use your own types, as long as they have a Listable (the type­class LeanCheck uses) in­stance:

> :{
new­type Nat n = Nat n de­riving Show
in­stance (Num n, Ord n, Listable n) => Listable (Nat n) where
  list = [Nat n | n <- list, n >= 0]
:}

> check $ \(Nat x) (Nat y) -> sig' (\v -> sig­nalQSemN v (x + y)) `equi­val­entTo` sig' (\v -> sig­nalQSemN v x >> sig­nalQSemN v y)
+++ OK!

Cur­rently it’s a bit slow as I need to fiddle with the im­ple­ment­a­tion and work out what a good number of tests to run is. check uses 10 seed values with 100 vari­able as­sign­ments each (1000 tests total), you can use checkFor to re­duce that.

Fin

So there you have it, prop­er­ty-testing for side-ef­fects of stateful op­er­a­tions.

This has come out of my work on CoCo, a tool for auto­mat­ic­ally dis­cov­ering these prop­er­ties (paper here). In the CoCo re­pos­itory are a few more ex­amples. CoCo is still a work-in-­pro­gress, but one of the goals is to be able to gen­erate de­jafu-­com­pat­ible out­put, so that CoCo can dis­cover prop­er­ties which de­jafu can im­me­di­ately begin using for re­gres­sion test­ing.