TicketDispenser.hs

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE DeriveGeneric       #-}
{-# LANGUAGE DerivingStrategies  #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  TicketDispenser
-- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH
-- License     :  BSD-style (see the file LICENSE)
--
-- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
-- Stability   :  provisional
-- Portability :  non-portable (GHC extensions)
--
-- This module contains a specification of a simple ticket dispenser.
--
-----------------------------------------------------------------------------

module TicketDispenser
  ( prop_ticketDispenser
  , prop_ticketDispenserParallel
  , prop_ticketDispenserNParallelOK
  , prop_ticketDispenserParallelOK
  , prop_ticketDispenserNParallelBad
  , prop_ticketDispenserParallelBad
  , withDbLock
  , setupLock
  , cleanupLock
  )
  where

import           Control.Exception
                   (IOException, catch)
import           Control.Monad.IO.Class
                   (liftIO)
import           Data.Kind
                   (Type)
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
                   (PropertyM, monadicIO)

import           Test.StateMachine
import qualified Test.StateMachine.Types.Rank2 as Rank2

------------------------------------------------------------------------

-- The actions of the ticket dispenser are:

data Action (r :: Type -> Type)
  = TakeTicket
  | Reset
  deriving stock (Show, Generic1)
  deriving anyclass (Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)

data Response (r :: Type -> Type)
  = GotTicket Int
  | ResetOk
  deriving stock (Show, Generic1)
  deriving anyclass 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 :: Type -> Type) = Model (Maybe Int)
  deriving stock (Eq, Show, Generic)

deriving anyclass 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 :: Model Symbolic -> 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 -> PropertyM IO ()) -> PropertyM IO ()
withDbLock run = do
  lock <- liftIO setupLock
  run lock
  liftIO $ cleanupLock lock

sm :: SharedExclusive -> DbLock -> StateMachine Model Action IO Response
sm se files = StateMachine
  initModel transitions preconditions postconditions
  Nothing generator shrinker (semantics se files) mock noCleanup

smUnused :: SharedExclusive -> StateMachine Model Action IO Response
smUnused se = sm se (error "dblock used during command creation")

-- Sequentially the model is consistent (even though the lock is
-- shared).

prop_ticketDispenser :: Property
prop_ticketDispenser =
  forAllCommands (smUnused Shared) Nothing $ \cmds -> monadicIO $
    withDbLock $ \ioLock -> do
      let sm' = sm Shared ioLock
      (hist, _, res) <- runCommands sm' cmds
      prettyCommands sm' hist $
        checkCommandNames cmds (res === Ok)

prop_ticketDispenserParallel :: SharedExclusive -> Property
prop_ticketDispenserParallel se =
  forAllParallelCommands (smUnused se) Nothing $ \cmds -> monadicIO $
    withDbLock $ \ioLock -> do
      let sm' = sm se ioLock
      prettyParallelCommands cmds =<< runParallelCommandsNTimes 100 sm' cmds

prop_ticketDispenserNParallel :: SharedExclusive -> Int -> Property
prop_ticketDispenserNParallel se np =
  forAllNParallelCommands (smUnused se) np $ \cmds -> monadicIO $
    withDbLock $ \ioLock -> do
      let sm' = sm se ioLock
      prettyNParallelCommands cmds =<< runNParallelCommands sm' cmds

-- So long as the file locks are exclusive, i.e. not shared, the
-- parallel property passes.
prop_ticketDispenserParallelOK :: Property
prop_ticketDispenserParallelOK = prop_ticketDispenserParallel Exclusive

prop_ticketDispenserParallelBad :: Property
prop_ticketDispenserParallelBad = prop_ticketDispenserParallel Shared

prop_ticketDispenserNParallelOK :: Int -> Property
prop_ticketDispenserNParallelOK = prop_ticketDispenserNParallel Exclusive

prop_ticketDispenserNParallelBad :: Int -> Property
prop_ticketDispenserNParallelBad = prop_ticketDispenserNParallel Shared