Repository files navigation

quickcheck-state-machine is a Haskell library, basedonQuickCheck, for testingstateful programs. The library is different fromtheTest.QuickCheck.Monadic approachin that it lets the user specify the correctness by means of a state machinebased model using pre- and post-conditions. The advantage of the state machineapproach is twofold: 1) specifying the correctness of your programs becomes lessadhoc, and 2) you get testing for race conditions for free.

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

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

dataCommandr=Create  |Read      (Reference (Opaque (IORefInt))r)  |Write     (Reference (Opaque (IORefInt))r)Int  |Increment (Reference (Opaque (IORefInt))r)dataResponser=Created (Reference (Opaque (IORefInt))r)  |ReadValueInt  |Written  |Incremented

When we generate actions we won't be able to create arbitraryIORefs, that'swhy all uses ofIORefs are wrapped inReference _ r, where the parameterrwill let us use symbolic references while generating (and concrete ones whenexecuting).

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

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

dataBug=None |Logic |RacederivingEqsemantics::Bug->CommandConcrete->IO (ResponseConcrete)semantics bug cmd=case cmdofCreate->Created<$> (reference.Opaque<$> newIORef0)Read ref->ReadValue<$> readIORef  (opaque ref)Write ref i->Written<$  writeIORef (opaque ref) i'where-- One of the problems is a bug that writes a wrong value to the-- reference.      i'| bug==Logic&& i`elem` [5..10]= i+1|otherwise= iIncrement ref->do-- The other problem is that we introduce a possible race condition-- when incrementing.if bug==Racethendo      i<- readIORef (opaque ref)      threadDelay=<< randomRIO (0,5000)      writeIORef (opaque ref) (i+1)else      atomicModifyIORef' (opaque ref) (\i-> (i+1,()))returnIncremented

Note that abover is instantiated toConcrete, which is essentially theidentity type, so while writing the semantics we have access to realIORefs.

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

newtypeModelr=Model [(Reference (Opaque (IORefInt))r,Int)]initModel::ModelrinitModel=Model[]

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

precondition::ModelSymbolic->CommandSymbolic->Logicprecondition (Model m) cmd=case cmdofCreate->TopRead  ref-> ref`member`mapfst mWrite ref _-> ref`member`mapfst mIncrement ref-> ref`member`mapfst m

The transition function explains how actions change the model. Note that thetransition function is polymorphic inr. The reason for this is that we usethe transition function both while generating and executing.

transition::Eq1r=>Modelr->Commandr->Responser->Modelrtransition m@(Model model) cmd resp=case (cmd, resp)of  (Create,Created ref)->Model ((ref,0): model)  (Read _,ReadValue _)-> m  (Write ref x,Written)->Model (update ref x model)  (Increment ref,Incremented)->caselookup ref modelofJust i->Model (update ref (succ i) model)update::Eqa=>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 theresult.

postcondition::ModelConcrete->CommandConcrete->ResponseConcrete->Logicpostcondition (Model m) cmd resp=case (cmd, resp)of  (Create,Created ref)-> m'! ref.==0.//"Create"whereModel m'= transition (Model m) cmd resp  (Read ref,ReadValue v)-> v.== m! ref.//"Read"  (Write _ref _x,Written)->Top  (Increment _ref,Incremented)->Top

Next we have to explain how to generate and shrink actions.

generator::ModelSymbolic->Maybe (Gen (CommandSymbolic))generator (Model[])=Just (pureCreate)generator model=Just$ frequency  [ (1,pureCreate)  , (4,Read<$> elements (mapfst model))  , (4,Write<$> elements (mapfst model)<*> arbitrary)  , (4,Increment<$> elements (domain model))  ]shrinker::ModelSymbolic->CommandSymbolic-> [CommandSymbolic]shrinker _ (Write ref i)= [Write ref i'| i'<- shrink i ]shrinker _ _=[]

To stop the generation of new commands, e.g., when the model has reached aterminal or error state, letgenerator returnNothing.

Finally, we show how to mock responses given a model.

mock::ModelSymbolic->CommandSymbolic->GenSym (ResponseSymbolic)mock (Model m) cmd=case cmdofCreate->Created<$> genSymRead ref->ReadValue<$>pure (m! ref)Write _ _->pureWrittenIncrement _->pureIncremented

(mock is a hack to make it possible for responses to have multiple reference,and an experiment which maybe one day will let us create mocked APIs. See issue#236for further details.)

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

sm::Bug->StateMachineModelCommandIOResponsesm bug=StateMachine initModel transition precondition postconditionNothing generator shrinker (semantics bug) mock

We can now define a sequential property as follows.

prop_sequential::Bug->Propertyprop_sequential bug= forAllCommands sm'Nothing$\cmds-> monadicIO$do  (hist, _model, res)<- runCommands sm' cmds  prettyCommands sm' hist (checkCommandNames cmds (res===Ok))where      sm'= sm bug

If we run the sequential property without introducing any problems to thesemantics function, i.e.quickCheck (prop_sequential None), then the propertypasses. If we however introduce the logic bug problem, then it will fail with theminimal counterexample:

> quickCheck (prop_sequential Logic)*** Failed! Falsifiable (after 12 tests and 2 shrinks):Commands  { unCommands =      [ Command Create [ Var 0 ]      , Command (Write (Reference (Symbolic (Var 0))) 5) []      , Command (Read (Reference (Symbolic (Var 0)))) []      ]  }Model []   == Create ==> Created (Reference (Concrete Opaque)) [ 0 ]Model [+_×_ (Reference Opaque)          0]   == Write (Reference (Concrete Opaque)) 5 ==> Written [ 0 ]Model [_×_ (Reference Opaque)         -0         +5]   == Read (Reference (Concrete Opaque)) ==> ReadValue 6 [ 0 ]Model [_×_ (Reference Opaque) 5]PostconditionFailed "AnnotateC \"Read\" (PredicateC (6 :/= 5))" /= Ok

Recall that the bug problem causes the write of valuesi `elem` [5..10] toactually writei + 1. Also notice how the diff of the model is displayedbetween each action.

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

If we however define a parallel property as follows.

prop_parallel::Bug->Propertyprop_parallel bug= forAllParallelCommands sm'$\cmds-> monadicIO$do  prettyParallelCommands cmds=<< runParallelCommands sm' cmdswhere      sm'= sm bug

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

> quickCheck (prop_parallel Race)*** Failed! Falsifiable (after 26 tests and 6 shrinks):ParallelCommands  { prefix =      Commands { unCommands = [ Command Create [ Var 0 ] ] }  , suffixes =      [ Pair          { proj1 =              Commands                { unCommands =                    [ Command (Increment (Reference (Symbolic (Var 0)))) []                    , Command (Read (Reference (Symbolic (Var 0)))) []                    ]                }          , proj2 =              Commands                { unCommands =                    [ Command (Increment (Reference (Symbolic (Var 0)))) []                    ]                }          }      ]  }┌─────────────────────────────────────────────────────────────────────────────────────────────────┐│ [Var 0] ← Create                                                                                ││                                                         → Created (Reference (Concrete Opaque)) │└─────────────────────────────────────────────────────────────────────────────────────────────────┘┌──────────────────────────────────────────────┐ ││ [] ← Increment (Reference (Concrete Opaque)) │ ││                                              │ │ ┌──────────────────────────────────────────────┐│                                              │ │ │ [] ← Increment (Reference (Concrete Opaque)) ││                                              │ │ │                                → Incremented ││                                              │ │ └──────────────────────────────────────────────┘│                                → Incremented │ │└──────────────────────────────────────────────┘ │┌──────────────────────────────────────────────┐ ││ [] ← Read (Reference (Concrete Opaque))      │ ││                                → ReadValue 1 │ │└──────────────────────────────────────────────┘ │AnnotateC "Read" (PredicateC (1 :/= 2))

As we can see above, a mutable reference is first created, and then inparallel (concurrently) we do two increments of said reference, and finally weread the value1 while the model expects2.

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

We shall come back to this example below, but if your are impatient you canfind the full sourcecodehere.

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

• a datatype of actions;
• a datatype model;
• pre- and post-conditions of the actions on the model;
• a state transition function that given a model and an action advances themodel to its next state;
• a way to generate and shrink actions;
• semantics for executing the actions.

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

Thesequential property checks if the model is consistent with respect to thesemantics. 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 aminimal counterexample.

Theparallel property checks if parallel execution of the semantics can beexplained in terms of the sequential model. This is useful for trying to findrace conditions -- which normally can be tricky to test for. It works asfollows:

1. generate a list of actions that will act as a sequential prefix for theparallel program (think of this as an initialisation bit that setups upsome 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) ofinvocations and responses of each action;

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

The last step basically tries to findalinearisation of calls thatcould have happend on a single thread.

Here are some more examples to get you started:

• The water jug problem fromDie Hard 3 -- this is asimpleexample ofa specification where we use the sequential property to find a solution(counterexample) to a puzzle from an action movie. Note that this examplehas no meaningful semantics, we merely model-check. It might be helpful tocompare the solution to theHedgehogsolution andtheTLA+solution;

• The Tower of Hanoi puzzle -- thisexample usesproperty based testing in a very similar manner to theDie Hardexampleto find a solution to the classicTower of Hanoi puzzle;

• Mutablereferenceexample --this is a bigger example that shows both how the sequential property canfind normal bugs, and how the parallel property can find race conditions;

• Circular bufferexample-- another example that shows how the sequential property can find help finddifferent kind of bugs. This example is borrowed from the paperTesting theHard Stuff and Staying Sane[PDF,video]. For a more directtranslation from the paper, see the followingvariant which uses the C FFI;

• The union-findexample-- an imperative implementation of the union-find algorithm. It could beuseful to compare the solution to the one that appears in the paperTestingMonadic Code with QuickCheck[PS], which theTest.QuickCheck.Monadicmodule is based on;

• Ticketdispenserexample --a simple example where the parallel property is used once again to find arace condition. The semantics in this example uses a simple database filethat needs to be setup and cleaned up. This example also appears in theTesting a Database for Race Conditions with QuickCheck andTesting theHard Stuff and StayingSane[PDF,video] papers;

• CRUD webserver where create returns uniqueidsexample --create, read, update and delete users in a postgres database on a webserverusing an API writtenusingServant. Creating a userwill return a unique id, which subsequent reads, updates, and deletes needto use. In this example, unlike in the last one, the server is setup andtorn down once per property rather than generate program;

• Bookstoreexample-- another database application, that uses simple SQL queries to manage a bookstore.It is based on acase studyin Erlang from online version of Fred Hebert'sPropEr Testingbook;

• Process registryexample-- an example often featured in the Erlang QuickCheck papers. This exampleshows how one can tag the specification with which requirements are coveredand then generate (minimal) examples of test cases that cover eachrequirement, as shown in theHow well are your requirements tested?[PDF]andUnderstanding Formal Specifications through Good Examples[PDF,video] papers.

All properties from the examples can be found in theSpecmodule located in thetestdirectory. The properties from the examples get tested as part ofTravisCI.

To get a better feel for the examples it might be helpful togit clone thisrepo,cd into it, fire upstack ghci --test, load the different examples,e.g.:l test/CrudWebserverDb.hs, and run the different propertiesinteractively.

More examples from the "real world":

• IOHK are using a state machine models in severalplaces.For examplehereis a test of a mock file system that they in turn use to simulate filesystem errors when testing a blockchain database. The following blogpost describes theirtests in more detail;

• Wire are using a state machine model totestthe lower bound of running threads in their push notification system;

• Adjoint's (now abandoned?) implementation of the Raft consensus algorithm,contains state machinetestscombined with fault injection (node and network failures).

Thequickcheck-state-machine library is still very experimental.

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

• The QuickCheck bugtrackissue -- where theinitial discussion about how to add state machine based testing toQuickCheck started;

• John Hughes' Midlands Graduate School 2019course on property-basedtesting, which covers the basics of state machine modelling and testing. Italso contains a minimal implementation of a state machine testing librarybuilt on top of Haskell's QuickCheck;

• Finding Race Conditions in Erlang with QuickCheck andPULSE[PDF,video] -- this is the first paper to describehow Erlang's QuickCheck works (including the parallel testing);

• Linearizability: a correctness condition for concurrent objects[PDF, TLA+formalisation], this is a classicpaper that describes the main technique of the parallel property;

• Aphyr's blogposts aboutJepsen, whichalso uses the linearisability technique, and has found bugs in manydistributed systems:

  • Knossos: Redis and linearizability;
  • Strong consistency models;
  • Computational techniques in Knossos;
  • Serializability, linearizability, and locality.

• The use of state machines to model and verify properties about programs isquite well-established, as witnessed by several books on the subject:

  • SpecifyingSystems:The TLA+ Language and Tools for Hardware and Software Engineers.Parts of this book are also presented by the author, LeslieLamport, in the following videocourse;

  • Modeling in Event-B: Systemand Software Engineering. Parts of this book are covered in thefollowing (video) course given at Microsoft Research by theauthor, Jean-Raymond Abrial, himself:

    • Lecture 1:introduction to modelling and Event-B (chapter 1 of thebook) and start of "controlling cars on bridge" example(chapter 2);

    • Lecture 2:refining the "controlling cars on a bridge" example(sections 2.6 and 2.7);

    • Lecture 3:design patterns and the "mechanical press controller"example (chapter 3);

    • Lecture 4:sorting algorithm example (chapter 15);

    • Lecture 5:designing sequential programs (chapter 15);

    • Lecture 6:status report of the hypervisor that Microsoft Research aredeveloping using Event-B.

  • Abstract State Machines: AMethod for High-Level System Design and Analysis.

  The books contain general advice how to model systems using state machines,and are hence relevant to us. For shorter texts on why state machines areimportant for modelling, see:

  • Lamport'sComputation and State Machines;

  • Gurevich'sEvolving Algebras 1993: Lipari Guide andSequential Abstract State Machines Capture SequentialAlgorithms[PDF].

• Other similar libraries:

  • Erlang QuickCheck,eqc, the firstproperty based testing library to have support for state machines(closed source);

  • The Erlang libraryPropEr iseqc-inspired, open source, and has support for statemachinetesting;

  • The HaskelllibraryHedgehog, alsohas support for state machine based testing;

  • ScalaCheck, likewise has support for statemachinebasedtesting (noparallel property);

  • The PythonlibraryHypothesis, alsohas support for state machinebasedtesting (noparallel property).

BSD-style (see the file LICENSE).