diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +## Changelog for quickcheck-state-machine-distributed + +#### 0.0.0 + +* Initial release. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,67 @@ +## quickcheck-state-machine-distributed + +[![Hackage](https://img.shields.io/hackage/v/quickcheck-state-machine-distributed.svg)](https://hackage.haskell.org/package/quickcheck-state-machine-distributed) +[![Stackage Nightly](http://stackage.org/package/quickcheck-state-machine-distributed/badge/nightly)](http://stackage.org/nightly/package/quickcheck-state-machine-distributed) +[![Stackage LTS](http://stackage.org/package/quickcheck-state-machine-distributed/badge/lts)](http://stackage.org/lts/package/quickcheck-state-machine-distributed) +[![Build Status](https://api.travis-ci.org/advancedtelematic/quickcheck-state-machine-distributed.svg?branch=master)](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). diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/quickcheck-state-machine-distributed.cabal b/quickcheck-state-machine-distributed.cabal new file mode 100644 --- /dev/null +++ b/quickcheck-state-machine-distributed.cabal @@ -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 +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 diff --git a/src/Linearisability.hs b/src/Linearisability.hs new file mode 100644 --- /dev/null +++ b/src/Linearisability.hs @@ -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 ()) diff --git a/src/QuickCheckHelpers.hs b/src/QuickCheckHelpers.hs new file mode 100644 --- /dev/null +++ b/src/QuickCheckHelpers.hs @@ -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 diff --git a/src/Scheduler.hs b/src/Scheduler.hs new file mode 100644 --- /dev/null +++ b/src/Scheduler.hs @@ -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) diff --git a/src/StateMachine.hs b/src/StateMachine.hs new file mode 100644 --- /dev/null +++ b/src/StateMachine.hs @@ -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 diff --git a/src/Utils.hs b/src/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Utils.hs @@ -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) diff --git a/test/Bank.hs b/test/Bank.hs new file mode 100644 --- /dev/null +++ b/test/Bank.hs @@ -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)) diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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 ] + ] diff --git a/test/TicketDispenser.hs b/test/TicketDispenser.hs new file mode 100644 --- /dev/null +++ b/test/TicketDispenser.hs @@ -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]) +-}