quickcheck-state-machine-distributed (empty) → 0.0.0
raw patch · 13 files changed
+1534/−0 lines, 13 filesdep +QuickCheckdep +basedep +binarysetup-changed
Dependencies added: QuickCheck, base, binary, containers, directory, distributed-process, mtl, network-transport, network-transport-tcp, quickcheck-state-machine-distributed, random, stm, strict, tasty, tasty-quickcheck, temporary
Files
- CHANGELOG.md +5/−0
- LICENSE +25/−0
- README.md +67/−0
- Setup.hs +2/−0
- quickcheck-state-machine-distributed.cabal +82/−0
- src/Linearisability.hs +135/−0
- src/QuickCheckHelpers.hs +155/−0
- src/Scheduler.hs +205/−0
- src/StateMachine.hs +152/−0
- src/Utils.hs +51/−0
- test/Bank.hs +287/−0
- test/Main.hs +21/−0
- test/TicketDispenser.hs +347/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+## Changelog for quickcheck-state-machine-distributed++#### 0.0.0++* Initial release.
+ LICENSE view
@@ -0,0 +1,25 @@+Copyright (c) 2018 Stevan Andjelkovic, Robert Danitz++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ 1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+ + 2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the+ distribution.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS+IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED+TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A+PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED+TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,67 @@+## quickcheck-state-machine-distributed++[](https://hackage.haskell.org/package/quickcheck-state-machine-distributed)+[](http://stackage.org/nightly/package/quickcheck-state-machine-distributed)+[](http://stackage.org/lts/package/quickcheck-state-machine-distributed)+[](https://travis-ci.org/advancedtelematic/quickcheck-state-machine-distributed)++`quickcheck-state-machine-distributed` is Haskell library for testing stateful,+possibly distributed, programs. It's based on QuickCheck, but differs from the+[`Test.QuickCheck.Monadic`](https://hackage.haskell.org/package/QuickCheck/docs/Test-QuickCheck-Monadic.html)+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 appeared in Erlang's proprietary QuickCheck. The+`quickcheck-state-machine-distributed` library can be seen as an attempt to+provide similar functionality to Haskell's QuickCheck library.++The `quickcheck-state-machine-distributed` library builds upon ideas from the+[`quickcheck-state-machine`](https://github.com/advancedtelematic/quickcheck-state-machine)+sister library. The most significant difference is that the former is based on+the `distributed-process` library, hence the name. A more detailed comparison+follows below.++## Example++See+[`test/TicketDispenser.hs`](https://github.com/advancedtelematic/quickcheck-state-machine-distributed/blob/master/test/TicketDispenser.hs)+for a full example of how to implement and test a ticket dispenser -- think of+one of those machines in the pharmacy which gives you a piece of paper with your+number in line on it.++This example also appears in the *Testing a Database for Race Conditions with+QuickCheck* and *Testing the Hard Stuff and Staying Sane*+[[PDF](http://publications.lib.chalmers.se/records/fulltext/232550/local_232550.pdf),+[video](https://www.youtube.com/watch?v=zi0rHwfiX1Q)] papers.++## `quickcheck-state-machine-distributed` vs `quickcheck-state-machine`++Apart from the already mentioned difference that `-distributed` is based on+`distributed-process`es, it's also different in that it:++* Decouples requests from responses (opening up the possibility for testing+ asynchronous interfaces);++* Takes a more lightweight approach; no GADTs, no references (which hopefully+ makes the library easier to understand and use).++## Contributing++The `quickcheck-state-machine-distributed` 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++The README of the sister library+[`quickcheck-state-machine`](https://github.com/advancedtelematic/quickcheck-state-machine#readme)+library contains many links and examples that could be useful for a better+understanding of this library and the underlying principles.++## License++BSD-style (see the file LICENSE).
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ quickcheck-state-machine-distributed.cabal view
@@ -0,0 +1,82 @@+-- This file has been generated from package.yaml by hpack version 0.20.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: 3757460f9c072a73f3ad960c2c738649d6f77eba17ae9c37400656995aaebbc9++name: quickcheck-state-machine-distributed+version: 0.0.0+synopsis: Test monadic programs using state machine based models+description: Please see the README on Github at <https://github.com/advancedtelematic/quickcheck-state-machine-distributed#readme>+category: Testing+homepage: https://github.com/advancedtelematic/quickcheck-state-machine-distributed#readme+bug-reports: https://github.com/advancedtelematic/quickcheck-state-machine-distributed/issues+author: Stevan Andjelkovic+maintainer: stevan.andjelkovic@here.com+copyright: Copyright (C) 2018, HERE Europe B.V.+license: BSD2+license-file: LICENSE+build-type: Simple+cabal-version: >= 1.10++extra-source-files:+ CHANGELOG.md+ README.md++source-repository head+ type: git+ location: https://github.com/advancedtelematic/quickcheck-state-machine-distributed++library+ hs-source-dirs:+ src+ ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints+ build-depends:+ QuickCheck >=2.11.3+ , base >=4.7 && <5+ , binary+ , containers+ , distributed-process >=0.7.3+ , mtl+ , network-transport >=0.5.2+ , network-transport-tcp >=0.6.0+ , random+ , stm+ exposed-modules:+ Linearisability+ QuickCheckHelpers+ Scheduler+ StateMachine+ Utils+ other-modules:+ Paths_quickcheck_state_machine_distributed+ default-language: Haskell2010++test-suite quickcheck-state-machine-distributed-test+ type: exitcode-stdio-1.0+ main-is: Main.hs+ hs-source-dirs:+ test+ ghc-options: -Wall -Wcompat -Wincomplete-record-updates -Wincomplete-uni-patterns -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N+ build-depends:+ QuickCheck >=2.11.3+ , base >=4.7 && <5+ , binary+ , containers+ , directory+ , distributed-process >=0.7.3+ , mtl+ , network-transport >=0.5.2+ , network-transport-tcp >=0.6.0+ , quickcheck-state-machine-distributed+ , random+ , stm+ , strict+ , tasty+ , tasty-quickcheck+ , temporary+ other-modules:+ Bank+ TicketDispenser+ Paths_quickcheck_state_machine_distributed+ default-language: Haskell2010
+ src/Linearisability.hs view
@@ -0,0 +1,135 @@+module Linearisability+ ( History+ , linearisable+ , trace+ , wellformed+ )+ where++import Control.Distributed.Process+ (ProcessId)+import Data.Tree+ (Forest, Tree(Node))+import Text.Printf+ (printf)++------------------------------------------------------------------------++type History pid inv resp = [(pid, Either inv resp)]++data Operation pid inv resp = Operation pid inv resp+ deriving Show++------------------------------------------------------------------------++takeInvocations :: History pid inv resp -> [(pid, inv)]+takeInvocations [] = []+takeInvocations ((pid, Left inv) : hist) = (pid, inv) : takeInvocations hist+takeInvocations ((_, Right _) : _) = []++findResponse :: Eq pid => pid -> History pid inv resp -> [(resp, History pid inv resp)]+findResponse _ [] = []+findResponse pid ((pid', Right resp) : es) | pid == pid' = [(resp, es)]+findResponse pid (e : es) =+ [ (resp, e : es') | (resp, es') <- findResponse pid es ]++interleavings :: Eq pid => History pid inv resp -> Forest (Operation pid inv resp)+interleavings [] = []+interleavings es =+ [ Node (Operation pid inv resp) (interleavings es')+ | (pid, inv) <- takeInvocations es+ , (resp, es') <- findResponse pid (filter1 (not . matchInvocation pid) es)+ ]+ where+ matchInvocation pid (pid', Left _) = pid == pid'+ matchInvocation _ _ = False++ filter1 :: (a -> Bool) -> [a] -> [a]+ filter1 _ [] = []+ filter1 p (x : xs) | p x = x : filter1 p xs+ | otherwise = xs++linearisable+ :: Eq pid+ => (model -> Either inv resp -> model)+ -> (model -> inv -> resp -> Bool)+ -> model+ -> History pid inv resp+ -> Bool+linearisable _ _ _ [] = True+linearisable transition postcondition model0 es =+ any (step model0) (interleavings es)+ where+ step model (Node (Operation _ inv resp) roses) =+ postcondition model inv resp &&+ any' (step (transition (transition model (Left inv)) (Right resp))) roses+ where+ any' :: (a -> Bool) -> [a] -> Bool+ any' _ [] = True+ any' p xs = any p xs++------------------------------------------------------------------------++prettyPrintProcessId :: ProcessId -> String+prettyPrintProcessId = reverse . takeWhile (/= ':') . reverse . show++trace+ :: (Show model, Show inv, Show resp)+ => (model -> Either inv resp -> model) -> model -> History ProcessId inv resp -> String+trace transitions = go+ where+ go _ [] = ""+ go model ((pid, Left inv) : hist) =+ printf "%s\n ==> %s [%s]\n%s"+ (show model)+ (show inv)+ (prettyPrintProcessId pid)+ (go (transitions model (Left inv)) hist)+ go model ((pid, Right resp) : hist) =+ printf "%s\n <== %s [%s]\n%s"+ (show model)+ (show resp)+ (prettyPrintProcessId pid)+ (go (transitions model (Right resp)) hist)++------------------------------------------------------------------------++data NotSequential pid inv resp+ = FirstEventIsntInvocation pid resp+ | InvocationFollowedByInvocation pid inv pid inv+ | InvocationFollowedByNonMatchingResponse pid inv pid resp+ | ResponseFollowedByResponse pid resp pid resp+ | ResponseFollowedByInvocation pid resp pid inv+ | LoneResponse pid resp+ deriving Show++processSubhistory :: Eq pid => pid -> History pid inv resp -> History pid inv resp+processSubhistory pid = filter ((== pid) . fst)++isSequential :: Eq pid => History pid inv resp -> Either (NotSequential pid inv resp) ()+isSequential history = case history of+ (pid, Right resp) : _ -> Left (FirstEventIsntInvocation pid resp)+ _ -> go history+ where+ go []+ = Right ()+ go [(pid, Right resp)]+ = Left (LoneResponse pid resp)+ go [(_, Left _)]+ = Right ()+ go ((pid, Left inv) : (pid', Right resp) : hist)+ | pid == pid' = go hist+ | otherwise = Left (InvocationFollowedByNonMatchingResponse pid inv pid' resp)+ go ((pid, Left inv) : (pid', Left inv') : _)+ = Left (InvocationFollowedByInvocation pid inv pid' inv')+ go ((pid, Right resp) : (pid', Right resp') : _)+ = Left (ResponseFollowedByResponse pid resp pid' resp')+ go ((pid, Right resp) : (pid', Left inv) : _)+ = Left (ResponseFollowedByInvocation pid resp pid' inv)++wellformed :: Eq pid => [pid] -> History pid inv resp -> Either (NotSequential pid inv resp) ()+wellformed pids history = allRight+ [ isSequential (processSubhistory pid history) | pid <- pids ]+ where+ allRight :: [Either a b] -> Either a ()+ allRight = foldr (>>) (Right ())
+ src/QuickCheckHelpers.hs view
@@ -0,0 +1,155 @@+module QuickCheckHelpers+ ( generateRequests+ , shrinkRequests+ , generateParallelRequests+ , shrinkParallelRequests+ , monadicProcess+ )+ where++import Control.Arrow+ (second)+import Control.Distributed.Process+ (Process)+import Control.Monad.State+ (StateT, evalStateT, get, lift, put, runStateT)+import Data.List+ (permutations)+import Test.QuickCheck+ (Gen, Property, Testable, choose, ioProperty,+ shrinkList, sized, suchThat)+import Test.QuickCheck.Monadic+ (PropertyM, monadic)++import Utils++------------------------------------------------------------------------++generateRequestsStateT+ :: (model -> Gen req)+ -> (model -> req -> Bool)+ -> (model -> Either req resp -> model)+ -> StateT model Gen [req]+generateRequestsStateT generator preconditions transitions =+ go =<< lift (sized (\k -> choose (0, k)))+ where+ go 0 = return []+ go size = do+ model <- get+ msg <- lift (generator model `suchThat` preconditions model)+ put (transitions model (Left msg))+ (msg :) <$> go (size - 1)++generateRequests+ :: (model -> Gen req)+ -> (model -> req -> Bool)+ -> (model -> Either req resp -> model)+ -> model+ -> Gen [req]+generateRequests generator preconditions transitions =+ evalStateT (generateRequestsStateT generator preconditions transitions)++generateParallelRequests+ :: (model -> Gen req)+ -> (model -> req -> Bool)+ -> (model -> Either req resp -> model)+ -> model+ -> Gen ([req], [req])+generateParallelRequests generator preconditions transitions model = do+ (prefix, model') <- runStateT (generateRequestsStateT generator preconditions transitions) model+ suffix <- generateParallelSafeRequests generator preconditions transitions model'+ return (prefix, suffix)++generateParallelSafeRequests+ :: (model -> Gen req)+ -> (model -> req -> Bool)+ -> (model -> Either req resp -> model)+ -> model+ -> Gen [req]+generateParallelSafeRequests generator preconditions transitions = go []+ where+ go reqs model = do+ req <- generator model `suchThat` preconditions model+ let reqs' = req : reqs+ if length reqs' <= 6 && parallelSafe preconditions transitions model reqs'+ then go reqs' model+ else return (reverse reqs)++parallelSafe+ :: (model -> req -> Bool)+ -> (model -> Either req resp -> model)+ -> model+ -> [req]+ -> Bool+parallelSafe preconditions transitions model0+ = all (preconditionsHold model0)+ . permutations+ where+ preconditionsHold _ [] = True+ preconditionsHold model (req : reqs) = preconditions model req &&+ preconditionsHold (transitions model (Left req)) reqs++shrinkRequests+ :: (model -> req -> [req])+ -> (model -> req -> Bool)+ -> (model -> Either req resp -> model)+ -> model+ -> [req] -> [[req]]+shrinkRequests shrinker preconditions transitions model0+ = filter (validRequests preconditions transitions model0)+ . shrinkList (shrinker model0)++validRequests :: (model -> req -> Bool) -> (model -> Either req resp -> model) -> model -> [req] -> Bool+validRequests preconditions transitions = go+ where+ go _ [] = True+ go model (req : reqs) = preconditions model req &&+ go (transitions model (Left req)) reqs++validParallelRequests+ :: (model -> req -> Bool)+ -> (model -> Either req resp -> model)+ -> model+ -> ([req], [req])+ -> Bool+validParallelRequests preconditions transitions model (prefix, suffix)+ = validRequests preconditions transitions model prefix+ && parallelSafe preconditions transitions model' suffix+ where+ model' = foldl transitions model (map Left prefix)++shrinkParallelRequests+ :: (model -> req -> [req])+ -> (model -> req -> Bool)+ -> (model -> Either req resp -> model)+ -> model+ -> ([req], [req]) -> [([req], [req])]+shrinkParallelRequests shrinker preconditions transitions model (prefix, suffix)+ = filter (validParallelRequests preconditions transitions model)+ [ (prefix', suffix')+ | (prefix', suffix') <- shrinkPair (shrinkList (shrinker model)) (prefix, suffix)+ ]+ +++ moveSuffixToPrefix+ where+ pickOneReturnRest :: [a] -> [(a, [a])]+ pickOneReturnRest [] = []+ pickOneReturnRest (x : xs) = (x, xs) : map (second (x :)) (pickOneReturnRest xs)++ moveSuffixToPrefix =+ [ (prefix ++ [prefix'], suffix')+ | (prefix', suffix') <- pickOneReturnRest suffix+ ]++monadicProcess :: Testable a => PropertyM Process a -> Property+monadicProcess = monadic (ioProperty . runLocalProcess)++-- | Given shrinkers for the components of a pair we can shrink the pair.+shrinkPair' :: (a -> [a]) -> (b -> [b]) -> ((a, b) -> [(a, b)])+shrinkPair' shrinkerA shrinkerB (x, y) =+ [ (x', y) | x' <- shrinkerA x ] +++ [ (x, y') | y' <- shrinkerB y ]++-- | Same above, but for homogeneous pairs.+shrinkPair :: (a -> [a]) -> ((a, a) -> [(a, a)])+shrinkPair shrinker = shrinkPair' shrinker shrinker
+ src/Scheduler.hs view
@@ -0,0 +1,205 @@+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE ScopedTypeVariables #-}++module Scheduler+ ( SchedulerSupervisor(..)+ , SchedulerCount(..)+ , SchedulerSequential(..)+ , SchedulerHistory(..)+ , SchedulerEnv(..)+ , schedulerP+ , makeSchedulerState+ )+ where++import Control.Concurrent+ (threadDelay)+import Control.Distributed.Process+ (Process, ProcessId, expect, getSelfPid, send,+ spawnLocal)+import Control.Monad+ (forever)+import Control.Monad.IO.Class+ (liftIO)+import Control.Monad.Reader+ (ask)+import Control.Monad.State+ (get, gets, modify)+import Data.Binary+ (Binary)+import Data.Map+ (Map)+import qualified Data.Map as M+import Data.Maybe+ (catMaybes)+import Data.Sequence+ (Seq)+import qualified Data.Sequence as Seq+import Data.Typeable+ (Typeable)+import GHC.Generics+ (Generic)+import System.Random+ (StdGen, mkStdGen, randomR)++import Linearisability+ (History)+import StateMachine++------------------------------------------------------------------------++newtype SchedulerSupervisor = SchedulerSupervisor ProcessId+ deriving Generic++instance Binary SchedulerSupervisor++newtype SchedulerCount = SchedulerCount Int+ deriving Generic++instance Binary SchedulerCount++newtype SchedulerSequential = SchedulerSequential [(ProcessId, ProcessId)]+ deriving Generic++instance Binary SchedulerSequential++newtype SchedulerHistory pid inv resp = SchedulerHistory (History pid inv resp)+ deriving Generic++instance (Binary pid, Binary inv, Binary resp) => Binary (SchedulerHistory pid inv resp)++------------------------------------------------------------------------++data SchedulerEnv input output model = SchedulerEnv+ { transitions :: model -> Either input output -> model+ , invariants :: model -> Bool+ }++data Mailbox input output+ = Incoming (Seq input) (Seq output)+ | Outgoing (Seq output) (Seq input)+ deriving (Show, Foldable)++data SchedulerState input output model = SchedulerState+ { mailboxes :: Map (ProcessId, ProcessId) (Mailbox input output)+ , stdGen :: StdGen+ , schedulerModel :: model+ , messageCount :: Int+ , sequential :: [(ProcessId, ProcessId)]+ }++makeSchedulerState :: Int -> model -> SchedulerState input output model+makeSchedulerState seed model = SchedulerState+ { mailboxes = M.empty+ , stdGen = mkStdGen seed+ , schedulerModel = model+ , messageCount = 0+ , sequential = []+ }++------------------------------------------------------------------------++pickProcessPair :: Scheduler input output model (Maybe (ProcessId, ProcessId))+pickProcessPair = do+ SchedulerState {..} <- get+ case sequential of+ processPair : _ -> return (Just processPair)+ [] -> case M.keys mailboxes of+ [] -> return Nothing+ processPairs -> do+ let (i, stdGen') = randomR (0, length processPairs - 1) stdGen+ processPair = processPairs !! i+ modify $ \s -> s { stdGen = stdGen' }+ return (Just processPair)++type Scheduler input output model a =+ StateMachine+ (SchedulerEnv input output model)+ (SchedulerState input output model)+ input output+ a++schedulerSM+ :: SchedulerMessage input output+ -> Scheduler input output model (Maybe (ProcessId, Either input output))+schedulerSM SchedulerTick = do+ count <- gets messageCount+ if count == 0+ then halt+ else do+ mprocessPair <- pickProcessPair+ case mprocessPair of+ Nothing -> return Nothing+ Just processPair -> do+ mboxes <- gets mailboxes+ case mboxes M.! processPair of+ Incoming reqs resps -> case Seq.viewl reqs of+ Seq.EmptyL -> return Nothing+ req Seq.:< reqs' -> do+ SchedulerEnv {..} <- ask+ -- unless (invariants model) $ do+ -- tell (printf "scheduler: invariant broken by `%s'" (show msg))+ -- halt+ modify $ \s -> s+ { mailboxes = M.insert processPair (Outgoing resps reqs') (mailboxes s)+ , schedulerModel = transitions (schedulerModel s) (Left req)+ , messageCount = messageCount s - 1+ , sequential = drop 1 (sequential s)+ }+ let (from, to) = processPair+ to ? req+ return (Just (from, Left req))+ Outgoing resps reqs -> case Seq.viewl resps of+ Seq.EmptyL -> return Nothing+ resp Seq.:< resps' -> do+ SchedulerEnv {..} <- ask+ -- unless (invariants model) $ do+ -- tell (printf "scheduler: invariant broken by `%s'" (show msg))+ -- halt+ modify $ \s -> s+ { mailboxes = M.insert processPair (Incoming reqs resps') (mailboxes s)+ , schedulerModel = transitions (schedulerModel s) (Right resp)+ , messageCount = messageCount s - 1+ , sequential = drop 1 (sequential s)+ }+ let (to, _from) = processPair+ to ! resp+ return (Just (to, Right resp))+schedulerSM (SchedulerRequest from req to) = do+ modify $ \s -> s { mailboxes = M.alter f (from, to) (mailboxes s) }+ return Nothing+ where+ f Nothing = Just (Incoming (Seq.singleton req) Seq.empty)+ f (Just mbox) = case mbox of+ Incoming reqs resps -> Just (Incoming (reqs Seq.|> req) resps)+ Outgoing resps reqs -> Just (Outgoing resps (reqs Seq.|> req))+schedulerSM (SchedulerResponse from resp to) = do+ modify $ \s -> s { mailboxes = M.alter f (to, from) (mailboxes s) }+ return Nothing+ where+ f Nothing = Just (Outgoing (Seq.singleton resp) Seq.empty)+ f (Just mbox) = case mbox of+ Incoming reqs resps -> Just (Incoming reqs (resps Seq.|> resp))+ Outgoing resps reqs -> Just (Outgoing (resps Seq.|> resp) reqs)++schedulerP+ :: forall input output model+ . (Binary input, Typeable input)+ => (Binary output, Typeable output)+ => SchedulerEnv input output model+ -> SchedulerState input output model+ -> Process ()+schedulerP env st = do+ self <- getSelfPid+ SchedulerSupervisor supervisor <- expect+ SchedulerCount count <- expect+ SchedulerSequential processPairs <- expect+ let st' = st { messageCount = count, sequential = processPairs }+ _ <- spawnLocal $ forever $ do+ liftIO (threadDelay 1000)+ send self (SchedulerTick :: SchedulerMessage input output)+ hist <- catMaybes <$> stateMachineProcess env st' False schedulerSM+ send supervisor (SchedulerHistory hist)
+ src/StateMachine.hs view
@@ -0,0 +1,152 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE ExplicitForAll #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}++module StateMachine+ ( MonadStateMachine+ , StateMachine+ , stateMachineProcess+ , stateMachineProcess_+ , halt+ , StateMachine.tell+ , (!)+ , (?)+ , SchedulerMessage(..) -- XXX+ , SchedulerPid(..) -- XXX+ , getSchedulerPid+ )+ where++import Control.Distributed.Process+ (Process, ProcessId, expect, getSelfPid, match,+ receiveWait, say, send)+import Control.Monad+ (forM_, void)+import Control.Monad.Except+ (ExceptT, MonadError, runExceptT, throwError)+import Control.Monad.IO.Class+ (MonadIO, liftIO)+import Control.Monad.Reader+ (MonadReader, ReaderT, runReaderT)+import Control.Monad.State+ (MonadState, StateT, runStateT)+import Control.Monad.Writer as Writer+ (MonadWriter, WriterT, runWriterT, tell)+import Data.Binary+ (Binary)+import Data.Typeable+ (Typeable)+import GHC.Generics+ (Generic)++------------------------------------------------------------------------++data SchedulerMessage input output+ = SchedulerTick+ | SchedulerRequest ProcessId input ProcessId+ | SchedulerResponse ProcessId output ProcessId+ deriving (Typeable, Generic, Show)++instance (Binary input, Binary output) => Binary (SchedulerMessage input output)++newtype SchedulerPid = SchedulerPid ProcessId+ deriving Generic++instance Binary SchedulerPid++getSchedulerPid :: Bool -> Process (Maybe ProcessId)+getSchedulerPid False = return Nothing+getSchedulerPid True = do+ SchedulerPid pid <- expect+ return (Just pid)++------------------------------------------------------------------------++type MonadStateMachine config state output1 output2 m =+ ( MonadReader config m+ , MonadWriter [Either String (ProcessId, Either output1 output2)] m+ , MonadState state m+ , MonadError HaltStateMachine m+ , MonadIO m+ )++data HaltStateMachine = HaltStateMachine++type StateMachine config state output1 output2 =+ ReaderT config+ (StateT state+ (ExceptT HaltStateMachine+ (WriterT [Either String (ProcessId, Either output1 output2)] IO)))++------------------------------------------------------------------------++runStateMachine+ :: config -> state -> StateMachine config state output1 output2 a+ -> IO (Either HaltStateMachine (a, state),+ [Either String (ProcessId, Either output1 output2)])+runStateMachine cfg st+ = runWriterT+ . runExceptT+ . flip runStateT st+ . flip runReaderT cfg++stateMachineProcess_+ :: (Binary input, Typeable input)+ => (Binary output1, Typeable output1)+ => (Binary output2, Typeable output2)+ => config -> state+ -> Bool+ -> (input -> StateMachine config state output1 output2 ())+ -> Process ()+stateMachineProcess_ cfg st testing = void . stateMachineProcess cfg st testing++stateMachineProcess+ :: forall input output1 output2 config state result+ . (Binary input, Typeable input)+ => (Binary output1, Typeable output1)+ => (Binary output2, Typeable output2)+ => config -> state+ -> Bool+ -> (input -> StateMachine config state output1 output2 result)+ -> Process [result]+stateMachineProcess cfg st0 testing k = do+ mscheduler <- getSchedulerPid testing+ go st0 mscheduler+ where+ go st mscheduler = do+ (continue, outputs) <- receiveWait [ match (liftIO . runStateMachine cfg st . k) ]+ forM_ outputs $ \output -> case output of+ Left str -> say str+ Right (pid, msg) -> case mscheduler of+ Nothing -> either (send pid) (send pid) msg+ Just scheduler -> do+ self <- getSelfPid+ case msg of+ Left req -> do+ let sreq :: SchedulerMessage output1 output2+ sreq = SchedulerRequest self req pid+ send scheduler sreq+ Right resp -> do+ let sresp :: SchedulerMessage output1 output2+ sresp = SchedulerResponse self resp pid+ send scheduler sresp+ case continue of+ Left HaltStateMachine -> return []+ Right (x, st') -> (x :) <$> go st' mscheduler++------------------------------------------------------------------------++halt :: MonadStateMachine config state output1 output2 m => m a+halt = throwError HaltStateMachine++(!) :: MonadStateMachine config state output1 output2 m => ProcessId -> output2 -> m ()+pid ! msg = Writer.tell [Right (pid, Right msg)]++(?) :: MonadStateMachine config state output1 output2 m => ProcessId -> output1 -> m ()+pid ? msg = Writer.tell [Right (pid, Left msg)]++tell :: MonadStateMachine config state output1 output2 m => String -> m ()+tell = Writer.tell . (:[]) . Left
+ src/Utils.hs view
@@ -0,0 +1,51 @@+module Utils+ ( withLocalNode+ , runLocalProcess+ )+ where++import Control.Concurrent.STM+ (atomically, newEmptyTMVar, putTMVar, takeTMVar)+import Control.Distributed.Process+ (Process, liftIO)+import Control.Distributed.Process.Node+ (LocalNode(..), closeLocalNode, initRemoteTable,+ newLocalNode, runProcess)+import Control.Exception+ (bracket)+import Network.Transport+ (closeTransport)+import Network.Transport.TCP+ (createTransport, defaultTCPParameters)+import System.Random+ (randomRIO)++------------------------------------------------------------------------++withLocalNode :: (LocalNode -> IO a) -> IO a+withLocalNode k = bracket setup cleanup (k . snd)+ where+ setup = do+ transport <- makeTransport+ localNode <- newLocalNode transport initRemoteTable+ return (transport, localNode)++ cleanup (transport, localNode) = do+ closeLocalNode localNode+ closeTransport transport++ makeTransport = do+ port <- randomRIO (1024, 65535 :: Int)+ etransport <- createTransport "127.0.0.1" (show port)+ (\port' -> ("127.0.0.1", port')) defaultTCPParameters+ case etransport of+ Left _ -> makeTransport+ Right transport -> return transport++runLocalProcess :: Process a -> IO a+runLocalProcess process = withLocalNode $ \node -> do+ resultVar <- atomically newEmptyTMVar+ runProcess node $ do+ result <- process+ liftIO (atomically (putTMVar resultVar result))+ atomically (takeTMVar resultVar)
+ test/Bank.hs view
@@ -0,0 +1,287 @@+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeSynonymInstances #-}++module Bank where++import Control.Distributed.Process+ (Process, ProcessId, expect, getSelfPid, liftIO,+ send, spawnLocal)+import Control.Monad+ (forM_, unless, void)+import Control.Monad.State+ (MonadIO, MonadState, get, lift)+import Data.Binary+ (Binary)+import Data.IORef+ (IORef, newIORef, readIORef, writeIORef)+import Data.Map+ (Map)+import qualified Data.Map as M+import GHC.Generics+ (Generic)+import Test.QuickCheck+ (Gen, Property, arbitrary, elements, forAllShrink,+ frequency, getPositive, shrink)+import Test.QuickCheck.Monadic+ (PropertyM)+import Text.Printf+ (printf)++import Linearisability+import QuickCheckHelpers+import Scheduler+import StateMachine++------------------------------------------------------------------------++type Account = ProcessId+type Money = Integer++data BankRequestF acc+ = OpenAccount acc+ | Deposit acc Money+ | Withdraw acc Money+ | CheckBalance acc+ | Transfer acc Money acc+ deriving (Eq, Show, Generic, Functor)++type BankRequest = BankRequestF ProcessId++fromPid :: BankRequestF pid -> pid+fromPid req = case req of+ OpenAccount pid -> pid+ Deposit pid _ -> pid+ Withdraw pid _ -> pid+ CheckBalance pid -> pid+ Transfer pid _ _ -> pid++instance Binary BankRequest++data BankResponse+ = AccountCreated+ | DepositMade+ | WithdrawalMade+ | TransferMade+ | AccountAlreadyExists+ | AccountDoesntExist+ | InsufficientFunds+ | Balance Money+ deriving (Eq, Show, Generic)++instance Binary BankResponse++------------------------------------------------------------------------++type ModelF acc = Map acc Money++type Model = ModelF ProcessId++initModel :: Model+initModel = initModel'++initModel' :: ModelF acc+initModel' = M.empty++next :: Model -> Either BankRequest BankResponse -> Model+next = next'++next' :: Ord acc => ModelF acc -> Either (BankRequestF acc) BankResponse -> ModelF acc+next' model (Left req) = case req of+ OpenAccount acc | acc `notElem` M.keys model -> M.insert acc 0 model+ | otherwise -> model+ Deposit acc money -> M.insertWith (+) acc money model+ Withdraw acc money -> M.insertWith (\new old -> old - new) acc money model+ CheckBalance _ -> model+ Transfer from money to -> next' (next' model (Left (Withdraw from money)))+ (Left (Deposit to money))+next' model (Right _resp) = model++invariant :: ModelF acc -> Bool+invariant = all (\balance -> balance >= 0) . M.elems++precondition :: Ord acc => ModelF acc -> BankRequestF acc -> Bool+precondition model req = case req of+ OpenAccount acc -> acc `M.notMember` model+ Deposit acc _money -> acc `M.member` model+ Withdraw acc money -> acc `M.member` model && model M.! acc >= money+ CheckBalance acc -> acc `M.member` model+ Transfer from money to+ -> from `elem` M.keys model+ && to `elem` M.keys model+ && model M.! from >= money+ && from /= to++post :: Ord acc => ModelF acc -> BankRequestF acc -> BankResponse -> Bool+post model req resp = Bank.invariant model && case req of+ OpenAccount acc+ | M.notMember acc model -> resp == AccountCreated+ | otherwise -> resp == AccountAlreadyExists+ Deposit _acc _money -> resp == DepositMade+ Withdraw acc money+ | M.lookup acc model >= Just money -> resp == WithdrawalMade+ | otherwise -> resp == InsufficientFunds++ CheckBalance acc -> resp == Balance (model M.! acc)+ Transfer from money _to+ | M.lookup from model >= Just money -> resp == TransferMade+ | otherwise -> resp == InsufficientFunds++generator1 :: [acc] -> ModelF acc -> Gen (BankRequestF acc)+generator1 workers model+ | M.null model = OpenAccount <$> elements workers+ | otherwise = frequency+ [ (1, OpenAccount <$> elements (M.keys model ++ workers))+ , (5, Deposit <$> elements (M.keys model)+ <*> fmap getPositive arbitrary)+ , (5, Withdraw <$> elements (M.keys model)+ <*> fmap getPositive arbitrary)+ , (8, Transfer <$> elements (M.keys model)+ <*> fmap getPositive arbitrary+ <*> elements (M.keys model))+ , (5, CheckBalance <$> elements (M.keys model))+ ]++generator :: Ord acc => [acc] -> Gen ([BankRequestF acc], [BankRequestF acc])+generator workers = generateParallelRequests (generator1 workers) precondition next' initModel'++shrinker1 :: ModelF acc -> BankRequestF acc -> [BankRequestF acc]+shrinker1 _ (Deposit acc money) = [ Deposit acc money' | money' <- shrink money ]+shrinker1 _ (Withdraw acc money) = [ Withdraw acc money' | money' <- shrink money ]+shrinker1 _ (Transfer from money to) = [ Transfer from money' to | money' <- shrink money ]+shrinker1 _ _ = []++shrinker+ :: Ord acc+ => ModelF acc+ -> ([BankRequestF acc], [BankRequestF acc])+ -> [([BankRequestF acc], [BankRequestF acc])]+shrinker = shrinkParallelRequests shrinker1 precondition next'++------------------------------------------------------------------------++clientP :: Bool -> Process ()+clientP testing = stateMachineProcess_ () () testing clientSM++clientSM :: BankResponse -> StateMachine () () BankRequest BankRequest ()+clientSM _ = return ()++bankP :: Bool -> Process ()+bankP testing = do+ ref <- liftIO (newIORef M.empty)+ stateMachineProcess_ () ref testing bankSM++type Implementation = IORef (Map ProcessId Money)++accountExists :: (MonadIO m, MonadState Implementation m) => ProcessId -> m Bool+accountExists acc = do+ ref <- get+ bank <- liftIO (readIORef ref)+ return (M.member acc bank)++newAccount :: (MonadIO m, MonadState Implementation m) => ProcessId -> m ()+newAccount acc = do+ ref <- get+ bank <- liftIO (readIORef ref)+ liftIO (writeIORef ref (M.insert acc 0 bank))++depositMoney :: (MonadIO m, MonadState Implementation m) => ProcessId -> Money -> m ()+depositMoney acc money = do+ ref <- get+ bank <- liftIO (readIORef ref)+ liftIO (writeIORef ref (M.insertWith (\new old -> new + old) acc money bank))++withdrawMoney :: (MonadIO m, MonadState Implementation m) => ProcessId -> Money -> m ()+withdrawMoney acc money = do+ ref <- get+ bank <- liftIO (readIORef ref)+ liftIO (writeIORef ref (M.insertWith (\new old -> old - new) acc money bank))++accountBalance :: (MonadIO m, MonadState Implementation m) => ProcessId -> m (Maybe Money)+accountBalance acc = do+ ref <- get+ bank <- liftIO (readIORef ref)+ return (M.lookup acc bank)++transferMoney :: (MonadIO m, MonadState Implementation m) => ProcessId -> Money -> ProcessId -> m ()+transferMoney from money to = do+ ref <- get+ void $ liftIO $ do+ bank <- readIORef ref+ writeIORef ref (M.insertWith (\new old -> new + old) to money $+ M.insertWith (\new old -> old - new) from money bank)++bankSM+ :: MonadStateMachine () Implementation BankRequest BankResponse m+ => BankRequest -> m ()+bankSM req = do+ case req of+ OpenAccount acc -> do+ member <- accountExists acc+ if member+ then acc ! AccountAlreadyExists+ else do+ newAccount acc+ acc ! AccountCreated+ Deposit acc money -> do+ depositMoney acc money+ acc ! DepositMade+ Withdraw acc money -> do+ withdrawMoney acc money+ acc ! WithdrawalMade+ CheckBalance acc -> do+ mbal <- accountBalance acc+ case mbal of+ Nothing -> acc ! AccountDoesntExist+ Just bal -> acc ! Balance bal+ Transfer from money to -> do+ transferMoney from money to+ from ! TransferMade++------------------------------------------------------------------------++setup :: Int -> Process ([ProcessId], ProcessId, ProcessId)+setup seed = do+ schedulerPid <- spawnLocal (schedulerP (SchedulerEnv next Bank.invariant)+ (makeSchedulerState seed initModel))+ bankPid <- spawnLocal (bankP True)+ client1Pid <- spawnLocal (clientP True)+ client2Pid <- spawnLocal (clientP True)+ mapM_ (`send` SchedulerPid schedulerPid) [bankPid, client1Pid, client2Pid]+ return ([client1Pid, client2Pid], bankPid, schedulerPid)++prop_bank :: Int -> Property+prop_bank seed =+ forAllShrink (Bank.generator [True, False]) (shrinker initModel') $ \(prefix, suffix) -> monadicProcess $ do+ self <- lift getSelfPid+ ([client1Pid, client2Pid], bankPid, schedulerPid) <- lift (setup seed)+ lift $ send schedulerPid (SchedulerSupervisor self)+ lift $ send schedulerPid (SchedulerCount ((length prefix + length suffix) * 2))++ let prefix' = map (fmap (\b -> if b then client1Pid else client2Pid)) prefix+ suffix' = map (fmap (\b -> if b then client1Pid else client2Pid)) suffix++ seqPairs = foldr (\req ih -> (fromPid req, bankPid) : (fromPid req, bankPid) : ih) [] prefix'++ lift (send schedulerPid (SchedulerSequential seqPairs))++ lift $ forM_ prefix' $ \req ->+ send schedulerPid (SchedulerRequest (fromPid req) req bankPid+ :: SchedulerMessage BankRequest BankResponse)+ lift $ forM_ suffix' $ \req ->+ send schedulerPid (SchedulerRequest (fromPid req) req bankPid+ :: SchedulerMessage BankRequest BankResponse)++ SchedulerHistory hist <- lift expect+ :: PropertyM Process (SchedulerHistory ProcessId BankRequest BankResponse)++ case wellformed [client1Pid, client2Pid] hist of+ Right () -> return ()+ Left err -> fail (printf "history isn't well-formed: %s" (show err))++ unless (linearisable next post initModel hist) $+ fail (printf "Can't linearise:\n%s\n"+ (trace next initModel hist))
+ test/Main.hs view
@@ -0,0 +1,21 @@+module Main where++import Test.Tasty+import Test.Tasty.QuickCheck ++import Bank+ (prop_bank)+import TicketDispenser+ (prop_ticketDispenser, prop_ticketDispenserParallel)++------------------------------------------------------------------------++main :: IO ()+main = defaultMain $ testGroup "Properties"+ [ testGroup "Ticket dispenser"+ [ testProperty "sequential" prop_ticketDispenser+ , testProperty "parallel" prop_ticketDispenserParallel+ ]+ , testGroup "Bank"+ [ testProperty "sequential" prop_bank ]+ ]
+ test/TicketDispenser.hs view
@@ -0,0 +1,347 @@+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE ScopedTypeVariables #-}++module TicketDispenser where++import Control.Distributed.Process+ (Process, ProcessId, expect, getSelfPid, liftIO,+ send, spawnLocal)+import Control.Monad+ (forM_, unless)+import Control.Monad.Reader+ (ask)+import Control.Monad.Trans+ (lift)+import Data.Binary+ (Binary)+import GHC.Generics+ (Generic)+import Prelude hiding+ (readFile)+import System.Directory+ (removePathForcibly)+import System.IO.Strict+ (readFile)+import System.IO.Temp+ (emptySystemTempFile)+import Test.QuickCheck+ (Gen, Property, expectFailure, forAllShrink,+ frequency)+import Text.Printf+ (printf)++import Linearisability+import QuickCheckHelpers+import Scheduler+import StateMachine++------------------------------------------------------------------------++-- In this example we will implement and test a ticket dispenser; think+-- of one of those machines in the pharmacy which gives you a piece of+-- paper with your number in line on it.+--+-- This example also appears in the "Testing a Database for Race+-- Conditions with QuickCheck" and "Testing the Hard Stuff and Staying+-- Sane" papers.+++-- Our ticket dispenser support two actions; you can take a ticket and+-- reset the dispenser (refill it with new paper tickets).+data Request+ = TakeTicket+ | Reset+ deriving (Eq, Show, Generic)++instance Binary Request++-- If you take a ticket the dispenser will return you a number, and if+-- you reset it you get an acknowledgement.+data Response+ = Number Int+ | Ok+ deriving (Eq, Show, Generic)++instance Binary Response++------------------------------------------------------------------------++-- We use a maybe integer as a model, where nothing means that the+-- dispenser hasn't been reset or filled with paper yet.++type Model = Maybe Int++initModel :: Model+initModel = Nothing++-- The transition function describes how actions advance the model. When+-- we take a ticket the counter is incremented by one, and when we reset+-- the counter is set to zero.++transition :: Model -> Either Request Response -> Model+transition m (Left req) = case req of+ TakeTicket -> succ <$> m+ Reset -> Just 0+transition m (Right _resp) = m++-- Pre-conditions describe in what state an action is allowed, and is+-- used to generate well-formed (or legal) programs.++precondition :: Model -> Request -> Bool+precondition Nothing TakeTicket = False+precondition (Just _) TakeTicket = True+precondition _ Reset = True++-- The assertions about our ticket dispenser are made by+-- post-conditions. Post-conditions provide a way to make sure that the+-- responses given by the implementation match the model.++postcondition :: Model -> Request -> Response -> Bool+postcondition m TakeTicket (Number i) = Just i == (succ <$> m)+postcondition _ Reset Ok = True+postcondition _ _ _ = False++-- We can also make assertions using a global invariant of the model,+-- but in the ticket dispenser case we don't need this.++invariant :: Model -> Bool+invariant _ = True++------------------------------------------------------------------------++-- To generate programs (lists of requests) we need to describe what+-- actions can occure with what frequency for each state.++generator :: Model -> Gen Request+generator Nothing = return Reset+generator (Just _) = frequency+ [ (1, return Reset)+ , (8, return TakeTicket)+ ]++-- From that the library can, using the state machine model and the+-- precondition, generate whole well-formed programs.++genRequests :: Gen [Request]+genRequests = generateRequests generator precondition transition initModel++-- The library also provides a way of shrinking whole programs given how+-- to shrink individual requests.++shrink1 :: Model -> Request -> [Request]+shrink1 _ _ = []++shrRequests :: [Request] -> [[Request]]+shrRequests = shrinkRequests shrink1 precondition transition initModel++------------------------------------------------------------------------++-- We are now done with the modelling and QuickCheck specific parts, and+-- can proceed with the actual implementation of the ticket dispenser.++-- Haskell's typed actors, distributed-processes, are used to implement+-- the programs we want to test, or as a thin layer on top of the+-- programs we want to test (which may we written without using+-- distributed-processes).++-- We don't write our programs using distributed-process' Process monad+-- directly, but instead we use a StateMachine monad which is+-- essentially a RWS (reader writer state) as described in the following+-- blog post:+--+-- http://yager.io/Distributed/Distributed.html+--+-- The reason for this is that it allows us to run the distributed+-- process in "testing mode", where we drop in a deterministic user-land+-- message scheduler in place of distributed-process' scheduler. By+-- being able to deterministically control the flow of messages between+-- our actors we can easier test for race conditions. See the paper+-- "Finding Race Conditions in Erlang with QuickCheck and PULSE" for+-- more information about deterministic scheduling.++clientP :: ProcessId -> FilePath -> Process ()+clientP pid dbFile = stateMachineProcess_ (pid, dbFile) () True clientSM++-- The True above indicates that we want to run in "testing mode". After+-- we are done with testing we can deploy the distributed process using+-- the real scheduler, i.e. passing False instead.++-- The actual implementation uses a file to store the next ticket+-- number. The reader part of the state machine monad contains the+-- process id to which we send the responses and a file path to the+-- ticket database.++clientSM :: Request -> StateMachine (ProcessId, FilePath) () Request Response ()+clientSM req = case req of+ Reset -> do+ (pid, db) <- ask+ liftIO (reset db)+ pid ! Ok+ TakeTicket -> do+ (pid, db) <- ask+ n <- liftIO (takeTicket db)+ pid ! Number n+ where+ reset :: FilePath -> IO ()+ reset db = writeFile db (show (0 :: Int))++ takeTicket :: FilePath -> IO Int+ takeTicket db = do+ n <- read <$> readFile db+ writeFile db (show (n + 1))+ return (n + 1)++-- For testing, we will set up two clients (so we can test for race+-- conditions) and a deterministic scheduler.++setup :: ProcessId -> Int -> Process (ProcessId, ProcessId, ProcessId, FilePath)+setup self seed = do+ schedulerPid <- spawnLocal (schedulerP (SchedulerEnv transition invariant)+ (makeSchedulerState seed initModel))+ dbFile <- liftIO (emptySystemTempFile "ticket-dispenser")+ client1Pid <- spawnLocal (clientP self dbFile)+ client2Pid <- spawnLocal (clientP self dbFile)+ mapM_ (`send` SchedulerPid schedulerPid) [client1Pid, client2Pid]+ return (client1Pid, client2Pid, schedulerPid, dbFile)++-- Now we have everything we need to write QuickCheck properties.+-- We start with a sequential property, which assures that using a+-- single client the implementation matches the model.++-- We use QuickCheck's @forAllShrink@ combinator together with the+-- generator and shrinker for requests that we defined above. The+-- library provides a new combinator for writing properties involving+-- @Process@es, called @monadicProcess :: Testable a => PropertyM+-- Process a -> Property@. It's analogue to QuickCheck's @monadicIO@+-- combinator.++prop_ticketDispenser :: Property+prop_ticketDispenser =+ forAllShrink genRequests shrRequests $ \reqs -> monadicProcess $ lift $ do++ -- The tests themselves will have a process id, which will be the+ -- used to communicate with the implementation of the ticket+ -- dispenser.+ self <- getSelfPid+ (client1Pid, _, schedulerPid, dbFile) <- setup self 25++ -- Next we tell the scheduler where to send the result, how many+ -- messages it should expect, and which messages should be sent in a+ -- sequential fashion (all messages will be sent sequentially in+ -- this property, as we only are using one client).+ send schedulerPid (SchedulerSupervisor self)+ send schedulerPid (SchedulerCount (length reqs * 2))+ send schedulerPid (SchedulerSequential [])++ -- Send the generated requests from the tests, via the scheduler, to+ -- the client.+ forM_ reqs $ \req ->+ send schedulerPid (SchedulerRequest self req client1Pid+ :: SchedulerMessage Request Response)++ -- Once all requests have been processed the scheduler will send us+ -- a trace/history of the messages.+ SchedulerHistory hist <- expect++ -- Clean up after ourselves.+ liftIO (removePathForcibly dbFile)++ -- Finally we check if the model agrees with the responeses from the+ -- implementation. The way this is done is by starting from the+ -- initial model, for each request and response pair we advance the+ -- model and check the post-condition for that pair.+ unless (linearisable transition postcondition initModel hist) $+ fail (printf "Can't linearise:\n%s\n"+ (trace transition initModel hist))++------------------------------------------------------------------------++-- The above property passes, even though there's a bug in the+-- implementation. Have a look at how @takeTicket@ is implemented! It+-- first reads a file and then writes to it. If two of those actions+-- happen concurrently one write might overwrite the other causing a+-- race condition!++-- We shall now see how the state machine approach can catch race+-- conditions for nearly no extra work.++-- First we need to explain how to generate and shrink+-- parallel/concurrent programs. We will model concurrent programs as a+-- pair of normal programs, where the first component is a sequential+-- prefix (run on one thread) that sets some state up (in our case+-- resets the ticket dispenser). The second component is the concurrent+-- part which will be run using multiple threads.++genParallelRequests :: Gen ([Request], [Request])+genParallelRequests = generateParallelRequests generator precondition transition initModel++shrParallelRequests :: ([Request], [Request]) -> [([Request], [Request])]+shrParallelRequests = shrinkParallelRequests shrink1 precondition transition initModel++-- The concurrent/parallel property looks quite similar to the+-- sequential one, except we generate and shrink parallel programs.++prop_ticketDispenserParallel :: Property+prop_ticketDispenserParallel = expectFailure $+ forAllShrink genParallelRequests shrParallelRequests $ \(prefix, suffix) -> monadicProcess $ lift $ do+ self <- getSelfPid++ -- First difference, is that we will use two clients this time.+ (client1Pid, client2Pid, schedulerPid, dbFile) <- setup self 15+ send schedulerPid (SchedulerSupervisor self)+ let count = (length prefix + length suffix) * 2+ send schedulerPid (SchedulerCount count)++ -- We need to tell the scheduler to run the prefix sequentially.+ let seqPairs = foldr (\_ ih -> (self, client1Pid) : (self, client1Pid) : ih) [] prefix+ send schedulerPid (SchedulerSequential seqPairs)++ -- Send the generates prefix requests from the tests, via the+ -- scheduler, to the first client.+ forM_ prefix $ \req ->+ send schedulerPid (SchedulerRequest self req client1Pid+ :: SchedulerMessage Request Response)++ -- Send the generated parallel suffix from an alternation between+ -- the two clients.+ forM_ (zip (cycle [True, False]) suffix) $ \(client, req) ->+ send schedulerPid (SchedulerRequest self req (if client then client1Pid else client2Pid)+ :: SchedulerMessage Request Response)++ SchedulerHistory hist <- expect++ liftIO (removePathForcibly dbFile)++ -- When we have a concurrent history, we try to find a possible+ -- sequential interleaving of requests and responses that respects+ -- the post-conditions. This technique was first described in the+ -- paper "Linearizability: A Correctness Condition for Concurrent+ -- Objects".+ unless (linearisable transition postcondition initModel hist) $+ fail (printf "Can't linearise:\n%s\n"+ (trace transition initModel hist))++------------------------------------------------------------------------++-- Example output:+{-+> quickCheck prop_ticketDispenserParallel++++ OK, failed as expected. (after 3 tests and 3 shrinks):+Exception:+ user error (Can't linearise:+ Nothing+ ==> Reset [8]+ Just 0+ <== Ok [8]+ Just 0+ ==> TakeTicket [8]+ Just 1+ ==> TakeTicket [8]+ Just 2+ <== Number 2 [8]+ Just 2+ <== Number 1 [8]++ )+([Reset],[TakeTicket,TakeTicket])+-}