{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
-----------------------------------------------------------------------------
-- |
-- Module : TicketDispenser
-- Copyright : (C) 2017, ATS Advanced Telematic Systems GmbH
-- License : BSD-style (see the file LICENSE)
--
-- Maintainer : Stevan Andjelkovic <stevan.andjelkovic@here.com>
-- Stability : provisional
-- Portability : non-portable (GHC extensions)
--
-- This module contains a specification of a simple ticket dispenser.
--
-----------------------------------------------------------------------------
module TicketDispenser
( prop_ticketDispenser
, prop_ticketDispenserParallel
, prop_ticketDispenserParallelOK
, prop_ticketDispenserParallelBad
, withDbLock
, setupLock
, cleanupLock
)
where
import Control.Exception
(IOException, catch)
import Data.TreeDiff
(ToExpr)
import GHC.Generics
(Generic, Generic1)
import Prelude hiding
(readFile)
import System.Directory
(createDirectoryIfMissing, getTemporaryDirectory,
removeFile)
import System.FileLock
(SharedExclusive(..), lockFile, unlockFile)
import System.FilePath
((</>))
import System.IO
(hClose, openTempFile)
import System.IO.Strict
(readFile)
import Test.QuickCheck
(Gen, Property, frequency, (===))
import Test.QuickCheck.Monadic
(monadicIO)
import Test.StateMachine
import qualified Test.StateMachine.Types.Rank2 as Rank2
------------------------------------------------------------------------
-- The actions of the ticket dispenser are:
data Action (r :: * -> *)
= TakeTicket
| Reset
deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)
data Response (r :: * -> *)
= GotTicket Int
| ResetOk
deriving (Show, Generic1, Rank2.Foldable)
-- Which correspond to taking a ticket and getting the next number, and
-- resetting the number counter of the dispenser.
------------------------------------------------------------------------
-- The dispenser has to be reset before use, hence the maybe integer.
newtype Model (r :: * -> *) = Model (Maybe Int)
deriving (Eq, Show, Generic)
deriving instance ToExpr (Model Concrete)
initModel :: Model r
initModel = Model Nothing
preconditions :: Model Symbolic -> Action Symbolic -> Logic
preconditions (Model Nothing) TakeTicket = Bot
preconditions (Model (Just _)) TakeTicket = Top
preconditions _ Reset = Top
transitions :: Model r -> Action r -> Response r -> Model r
transitions (Model m) cmd _ = case cmd of
TakeTicket -> Model (succ <$> m)
Reset -> Model (Just 0)
postconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic
postconditions (Model m) TakeTicket (GotTicket n) = Just n .== (succ <$> m)
postconditions _ Reset ResetOk = Top
postconditions _ _ _ = error "postconditions"
------------------------------------------------------------------------
-- With stateful generation we ensure that the dispenser is reset before
-- use.
generator :: Model Symbolic -> Maybe (Gen (Action Symbolic))
generator _ = Just $ frequency
[ (1, pure Reset)
, (4, pure TakeTicket)
]
shrinker :: Action Symbolic -> [Action Symbolic]
shrinker _ = []
------------------------------------------------------------------------
-- We will implement the dispenser using a simple database file which
-- stores the next number. A file lock is used to allow concurrent use.
semantics
:: SharedExclusive -- ^ Indicates if the file
-- lock should be shared
-- between threads or if it
-- should be exclusive.
-- Sharing it could cause
-- race conditions.
-> (FilePath, FilePath) -- ^ File paths to the
-- database storing the
-- ticket counter and the
-- file lock used for
-- synchronisation.
-> Action Concrete
-> IO (Response Concrete)
semantics se (tdb, tlock) cmd = case cmd of
TakeTicket -> do
lock <- lockFile tlock se
i <- read <$> readFile tdb
`catch` (\(_ :: IOException) -> return "-1")
writeFile tdb (show (i + 1))
`catch` (\(_ :: IOException) -> return ())
unlockFile lock
return (GotTicket (i + 1))
Reset -> do
lock <- lockFile tlock se
writeFile tdb (show (0 :: Integer))
`catch` (\(_ :: IOException) -> return ())
unlockFile lock
return ResetOk
mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)
mock (Model Nothing) TakeTicket = error "mock: TakeTicket"
mock (Model (Just n)) TakeTicket = GotTicket <$> pure n
mock _ Reset = pure ResetOk
------------------------------------------------------------------------
type DbLock = (FilePath, FilePath)
setupLock :: IO DbLock
setupLock = do
tmp <- getTemporaryDirectory
let tmpTD = tmp </> "ticket-dispenser"
createDirectoryIfMissing True tmpTD
(tdb, dbh) <- openTempFile tmpTD "ticket-dispenser.db"
hClose dbh
(tlock, lockh) <- openTempFile tmpTD "ticket-dispenser.lock"
hClose lockh
return (tdb, tlock)
cleanupLock :: DbLock -> IO ()
cleanupLock (tdb, tlock) = do
removeFile tdb
removeFile tlock
withDbLock :: (DbLock -> IO ()) -> IO ()
withDbLock run = do
lock <- setupLock
run lock
cleanupLock lock
sm :: SharedExclusive -> DbLock -> StateMachine Model Action IO Response
sm se files = StateMachine
initModel transitions preconditions postconditions
Nothing generator Nothing shrinker (semantics se files) mock
-- Sequentially the model is consistent (even though the lock is
-- shared).
prop_ticketDispenser :: DbLock -> Property
prop_ticketDispenser files = forAllCommands sm' Nothing $ \cmds -> monadicIO $ do
(hist, _, res) <- runCommands sm' cmds
prettyCommands sm' hist $
checkCommandNames cmds (res === Ok)
where
sm' = sm Shared files
prop_ticketDispenserParallel :: SharedExclusive -> DbLock -> Property
prop_ticketDispenserParallel se files =
forAllParallelCommands sm' $ \cmds -> monadicIO $
prettyParallelCommands cmds =<< runParallelCommandsNTimes 100 sm' cmds
where
sm' = sm se files
-- So long as the file locks are exclusive, i.e. not shared, the
-- parallel property passes.
prop_ticketDispenserParallelOK :: DbLock -> Property
prop_ticketDispenserParallelOK = prop_ticketDispenserParallel Exclusive
prop_ticketDispenserParallelBad :: DbLock -> Property
prop_ticketDispenserParallelBad = prop_ticketDispenserParallel Shared