lsm-tree-1.0.0.1: test/Test/Database/LSMTree/StateMachine.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
#if MIN_VERSION_GLASGOW_HASKELL(9,8,1,0)
{-# LANGUAGE TypeAbstractions #-}
#endif
{-# OPTIONS_GHC -Wno-orphans #-}
{-
TODO: improve generation and shrinking of dependencies. See
https://github.com/IntersectMBO/lsm-tree/pull/4#discussion_r1334295154.
TODO: The 'RetrieveBlobs' action will currently only retrieve blob references
that come from a single batch lookup or range lookup. It would be interesting
to also retrieve blob references from a mix of different batch lookups and/or
range lookups. This would require some non-trivial changes, such as changes to
'Op' to also include expressions for manipulating lists, such that we can map
@'Var' ['R.BlobRef' b]@ to @'Var' ('R.BlobRef' b)@. 'RetrieveBlobs'
would then hold a list of variables (e.g., @['Var' ('R.BlobRef b')]@)
instead of a variable of a list (@'Var' ['R.BlobRef' b]@).
TODO: it is currently not correctly modelled what happens if blob references
are retrieved from an incorrect table.
-}
module Test.Database.LSMTree.StateMachine (
tests
, labelledExamples
-- * Properties
, propLockstep_ModelIOImpl
, propLockstep_RealImpl_RealFS_IO
, propLockstep_RealImpl_MockFS_IO
, propLockstep_RealImpl_MockFS_IOSim
, CheckCleanup (..)
, CheckFS (..)
, CheckRefs (..)
-- * Lockstep
, ModelState (..)
, Key (..)
, Value (..)
, Blob (..)
, StateModel (..)
, Action (..)
, Action' (..)
) where
import Control.ActionRegistry (AbortActionRegistryError (..),
CommitActionRegistryError (..), getActionError,
getReasonExitCaseException)
import Control.Concurrent.Class.MonadMVar.Strict
import Control.Concurrent.Class.MonadSTM.Strict
import Control.Exception (assert)
import Control.Monad (forM_, (<=<))
import Control.Monad.Class.MonadST (MonadST)
import Control.Monad.Class.MonadThrow (Exception (..), Handler (..),
MonadCatch (..), MonadMask, MonadThrow (..), SomeException,
catches, displayException, fromException)
import Control.Monad.IOSim
import Control.Monad.Primitive
import Control.Monad.Reader (ReaderT (..))
import Control.RefCount (disableForgottenRefChecks,
enableForgottenRefChecks)
import Control.Tracer (Tracer, nullTracer)
import Data.Bifunctor (Bifunctor (..))
import Data.Constraint (Dict (..))
import Data.Either (partitionEithers)
import Data.Kind (Type)
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty (..))
import qualified Data.List.NonEmpty as NE
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes, fromMaybe)
import Data.Monoid (First (..))
import Data.Primitive.MutVar
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable (Proxy (..), Typeable, cast)
import qualified Data.Vector as V
import Database.LSMTree (BlobRefInvalidError (..),
CursorClosedError (..), SessionClosedError (..),
SessionDirCorruptedError (..),
SessionDirDoesNotExistError (..),
SessionDirLockedError (..), SnapshotCorruptedError (..),
SnapshotDoesNotExistError (..), SnapshotExistsError (..),
SnapshotNotCompatibleError (..), TableClosedError (..),
TableCorruptedError (..),
TableUnionNotCompatibleError (..))
import qualified Database.LSMTree as R
import Database.LSMTree.Class (Entry (..), LookupResult (..))
import qualified Database.LSMTree.Class as Class
import Database.LSMTree.Extras (showPowersOf)
import Database.LSMTree.Extras.Generators ()
import Database.LSMTree.Extras.NoThunks (propNoThunks)
import qualified Database.LSMTree.Internal.Config as R (TableConfig (..))
import Database.LSMTree.Internal.Serialise (SerialisedBlob,
SerialisedKey, SerialisedValue)
import qualified Database.LSMTree.Internal.Types as R.Types
import qualified Database.LSMTree.Internal.Unsafe as R.Unsafe
import qualified Database.LSMTree.Model.IO as ModelIO
import qualified Database.LSMTree.Model.Session as Model
import NoThunks.Class
import Prelude hiding (init)
import System.Directory (removeDirectoryRecursive)
import System.FS.API (FsError (..), HasFS, MountPoint (..), mkFsPath)
import System.FS.BlockIO.API (HasBlockIO, close)
import System.FS.BlockIO.IO (defaultIOCtxParams, ioHasBlockIO)
import System.FS.IO (HandleIO)
import qualified System.FS.Sim.Error as FSSim
import System.FS.Sim.Error (Errors)
import qualified System.FS.Sim.MockFS as MockFS
import System.FS.Sim.MockFS (MockFS)
import System.FS.Sim.Stream (Stream)
import System.IO.Temp (createTempDirectory,
getCanonicalTemporaryDirectory)
import Test.Database.LSMTree.StateMachine.Op (HasBlobRef (getBlobRef),
Op (..))
import qualified Test.QuickCheck as QC
import Test.QuickCheck (Arbitrary, Gen, Property)
import Test.QuickCheck.StateModel hiding (Var)
import Test.QuickCheck.StateModel.Lockstep
import qualified Test.QuickCheck.StateModel.Lockstep.Defaults as Lockstep.Defaults
import qualified Test.QuickCheck.StateModel.Lockstep.Run as Lockstep.Run
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.FS
import Test.Util.FS.Error
import Test.Util.PrettyProxy
import Test.Util.QC (Choice)
import qualified Test.Util.QLS as QLS
import Test.Util.TypeFamilyWrappers (WrapBlob (..), WrapBlobRef (..),
WrapCursor (..), WrapTable (..))
{-------------------------------------------------------------------------------
Test tree
-------------------------------------------------------------------------------}
tests :: TestTree
tests = testGroup "Test.Database.LSMTree.StateMachine" [
testProperty "propLockstep_ModelIOImpl"
propLockstep_ModelIOImpl
, testProperty "propLockstep_RealImpl_RealFS_IO" $
propLockstep_RealImpl_RealFS_IO nullTracer
, testProperty "propLockstep_RealImpl_MockFS_IO" $
propLockstep_RealImpl_MockFS_IO nullTracer CheckCleanup CheckFS CheckRefs
, testProperty "propLockstep_RealImpl_MockFS_IOSim" $
propLockstep_RealImpl_MockFS_IOSim nullTracer CheckCleanup CheckFS CheckRefs
]
labelledExamples :: IO ()
labelledExamples = QC.labelledExamples $ Lockstep.Run.tagActions (Proxy @(ModelState IO R.Table))
{-------------------------------------------------------------------------------
propLockstep: reference implementation
-------------------------------------------------------------------------------}
instance Arbitrary Model.TableConfig where
arbitrary :: Gen Model.TableConfig
arbitrary = pure Model.TableConfig
deriving via AllowThunk (ModelIO.Session IO)
instance NoThunks (ModelIO.Session IO)
propLockstep_ModelIOImpl ::
Actions (Lockstep (ModelState IO ModelIO.Table))
-> QC.Property
propLockstep_ModelIOImpl =
runActionsBracket
(Proxy @(ModelState IO ModelIO.Table))
CheckCleanup
acquire
release
(\r (session, errsVar, logVar) -> do
faultsVar <- newMutVar []
let
env :: RealEnv ModelIO.Table IO
env = RealEnv {
envSession = session
, envHandlers = [handler]
, envErrors = errsVar
, envErrorsLog = logVar
, envInjectFaultResults = faultsVar
}
prop <- runReaderT r env
faults <- readMutVar faultsVar
pure $ QC.tabulate "Fault results" (fmap show faults) prop
)
tagFinalState'
where
acquire :: IO (Class.Session ModelIO.Table IO, StrictTVar IO Errors, StrictTVar IO ErrorsLog)
acquire = do
session <- Class.openSession ModelIO.NoSessionArgs
errsVar <- newTVarIO FSSim.emptyErrors
logVar <- newTVarIO emptyLog
pure (session, errsVar, logVar)
release :: (Class.Session ModelIO.Table IO, StrictTVar IO Errors, StrictTVar IO ErrorsLog) -> IO ()
release (session, _, _) = Class.closeSession session
handler :: Handler IO (Maybe Model.Err)
handler = Handler $ pure . handler'
where
handler' :: ModelIO.Err -> Maybe Model.Err
handler' (ModelIO.Err err) = Just err
{-------------------------------------------------------------------------------
propLockstep: real implementation
-------------------------------------------------------------------------------}
instance Arbitrary R.TableConfig where
arbitrary = do
confMergeSchedule <- QC.frequency [
(1, pure R.OneShot)
, (4, pure R.Incremental)
]
confWriteBufferAlloc <- QC.arbitrary
confFencePointerIndex <- QC.arbitrary
confMergeBatchSize <- QC.sized $ \sz ->
R.MergeBatchSize <$> QC.chooseInt (1, sz)
pure $ R.TableConfig {
R.confMergePolicy = R.LazyLevelling
, R.confSizeRatio = R.Four
, confWriteBufferAlloc
, R.confBloomFilterAlloc = R.AllocFixed 10
, confFencePointerIndex
, R.confDiskCachePolicy = R.DiskCacheNone
, confMergeSchedule
, confMergeBatchSize
}
shrink R.TableConfig{..} =
[ R.TableConfig {
confWriteBufferAlloc = confWriteBufferAlloc'
, confFencePointerIndex = confFencePointerIndex'
, ..
}
| ( confWriteBufferAlloc', confFencePointerIndex')
<- QC.shrink (confWriteBufferAlloc, confFencePointerIndex)
]
-- TODO: the current generator is suboptimal, and should be improved. There are
-- some aspects to consider, and since they are at tension with each other, we
-- should try find a good balance.
--
-- Say the write buffer allocation is @n@.
--
-- * If @n@ is too large, then the tests degrade to only testing the write
-- buffer, because there are no flushes/merges.
--
-- * If @n@ is too small, then the resulting runs are also small. They might
-- consist of only a few disk pages, or they might consist of only 1 underfull
-- disk page. This means there are some parts of the code that we would rarely
-- cover in the state machine tests.
--
-- * If @n@ is too small, then we flush/merge very frequently, which may exhaust
-- the number of open file handles when using the real file system. Specially
-- if the test fails and the shrinker kicks in, then @n@ can currently become
-- very small. This is good for finding a minimal counterexample, but it might
-- also make the real filesystem run out of file descriptors. Arguably, you
-- could overcome this specific issue by only generating or shrinking to small
-- @n@ when we use the mocked file system. This would require some boilerplate
-- to add type level tags to distinguish between the two cases.
instance Arbitrary R.WriteBufferAlloc where
arbitrary = QC.scale (max 30) $ do
QC.Positive x <- QC.arbitrary
pure (R.AllocNumEntries x)
shrink (R.AllocNumEntries x) =
[ R.AllocNumEntries x'
| QC.Positive x' <- QC.shrink (QC.Positive x)
]
deriving stock instance Enum R.FencePointerIndexType
deriving stock instance Bounded R.FencePointerIndexType
instance Arbitrary R.FencePointerIndexType where
arbitrary = QC.arbitraryBoundedEnum
shrink R.OrdinaryIndex = []
shrink R.CompactIndex = [R.OrdinaryIndex]
propLockstep_RealImpl_RealFS_IO ::
Tracer IO R.LSMTreeTrace
-> QC.Fixed R.Salt
-> Actions (Lockstep (ModelState IO R.Table))
-> QC.Property
propLockstep_RealImpl_RealFS_IO tr (QC.Fixed salt) =
runActionsBracket
(Proxy @(ModelState IO R.Table))
CheckCleanup
acquire
release
(\r (_, session, _, errsVar, logVar) -> do
faultsVar <- newMutVar []
let
env :: RealEnv R.Table IO
env = RealEnv {
envSession = session
, envHandlers = realErrorHandlers @IO
, envErrors = errsVar
, envErrorsLog = logVar
, envInjectFaultResults = faultsVar
}
prop <- runReaderT r env
faults <- readMutVar faultsVar
pure $ QC.tabulate "Fault results" (fmap show faults) prop
)
tagFinalState'
where
acquire :: IO (FilePath, Class.Session R.Table IO, HasBlockIO IO HandleIO, StrictTVar IO Errors, StrictTVar IO ErrorsLog)
acquire = do
(tmpDir, hasFS, hasBlockIO) <- createSystemTempDirectory "prop_lockstepIO_RealImpl_RealFS"
session <- R.openSession tr hasFS hasBlockIO salt (mkFsPath [])
toggleForgottenRefChecksSession CheckRefs session
errsVar <- newTVarIO FSSim.emptyErrors
logVar <- newTVarIO emptyLog
pure (tmpDir, session, hasBlockIO, errsVar, logVar)
release :: (FilePath, Class.Session R.Table IO, HasBlockIO IO HandleIO, StrictTVar IO Errors, StrictTVar IO ErrorsLog) -> IO Property
release (tmpDir, !session, hasBlockIO, _, _) = do
!prop <- propNoThunks session
R.closeSession session
close hasBlockIO
removeDirectoryRecursive tmpDir
pure prop
propLockstep_RealImpl_MockFS_IO ::
Tracer IO R.LSMTreeTrace
-> CheckCleanup
-> CheckFS
-> CheckRefs
-> QC.Fixed R.Salt
-> Actions (Lockstep (ModelState IO R.Table))
-> QC.Property
propLockstep_RealImpl_MockFS_IO tr cleanupFlag fsFlag refsFlag (QC.Fixed salt) =
runActionsBracket
(Proxy @(ModelState IO R.Table))
cleanupFlag
(acquire_RealImpl_MockFS tr refsFlag salt)
(release_RealImpl_MockFS fsFlag)
(\r (_, session, errsVar, logVar) -> do
faultsVar <- newMutVar []
let
env :: RealEnv R.Table IO
env = RealEnv {
envSession = session
, envHandlers = realErrorHandlers @IO
, envErrors = errsVar
, envErrorsLog = logVar
, envInjectFaultResults = faultsVar
}
prop <- runReaderT r env
faults <- readMutVar faultsVar
pure $ QC.tabulate "Fault results" (fmap show faults) prop
)
tagFinalState'
propLockstep_RealImpl_MockFS_IOSim ::
(forall s. Tracer (IOSim s) R.LSMTreeTrace)
-> CheckCleanup
-> CheckFS
-> CheckRefs
-> QC.Fixed R.Salt
-> Actions (Lockstep (ModelState (IOSim RealWorld) R.Table))
-> QC.Property
propLockstep_RealImpl_MockFS_IOSim tr cleanupFlag fsFlag refsFlag (QC.Fixed salt) =
runActionsBracket
(Proxy @(ModelState (IOSim RealWorld) R.Table))
cleanupFlag
(acquire_RealImpl_MockFS tr refsFlag salt)
(release_RealImpl_MockFS fsFlag)
(\r (_, session, errsVar, logVar) -> do
faultsVar <- newMutVar []
let
env :: RealEnv R.Table (IOSim RealWorld)
env = RealEnv {
envSession = session
, envHandlers = realErrorHandlers @(IOSim RealWorld)
, envErrors = errsVar
, envErrorsLog = logVar
, envInjectFaultResults = faultsVar
}
prop <- runReaderT r env
faults <- readMutVar faultsVar
pure $ QC.tabulate "Fault results" (fmap show faults) prop
)
tagFinalState'
acquire_RealImpl_MockFS ::
R.IOLike m
=> Tracer m R.LSMTreeTrace
-> CheckRefs
-> R.Salt
-> m (StrictTMVar m MockFS, Class.Session R.Table m, StrictTVar m Errors, StrictTVar m ErrorsLog)
acquire_RealImpl_MockFS tr refsFlag salt = do
fsVar <- newTMVarIO MockFS.empty
errsVar <- newTVarIO FSSim.emptyErrors
logVar <- newTVarIO emptyLog
(hfs, hbio) <- simErrorHasBlockIOLogged fsVar errsVar logVar
session <- R.openSession tr hfs hbio salt (mkFsPath [])
toggleForgottenRefChecksSession refsFlag session
pure (fsVar, session, errsVar, logVar)
-- | Flag that turns on\/off file system checks.
data CheckFS = CheckFS | NoCheckFS
release_RealImpl_MockFS ::
(R.IOLike m)
=> CheckFS
-> (StrictTMVar m MockFS, Class.Session R.Table m, StrictTVar m Errors, StrictTVar m ErrorsLog)
-> m Property
release_RealImpl_MockFS fsFlag (fsVar, session, _, _) = do
sts <- getAllSessionTables session
forM_ sts $ \(SomeTable t) -> R.closeTable t
scs <- getAllSessionCursors session
forM_ scs $ \(SomeCursor c) -> R.closeCursor c
mockfs1 <- atomically $ readTMVar fsVar
R.closeSession session
mockfs2 <- atomically $ readTMVar fsVar
pure $ case fsFlag of
CheckFS -> propNumOpenHandles 1 mockfs1 QC..&&. propNoOpenHandles mockfs2
NoCheckFS -> QC.property ()
data SomeTable m
= SomeTable (forall k v b. R.Table m k v b)
data SomeCursor m
= SomeCursor (forall k v b. R.Cursor m k v b)
getAllSessionTables ::
(MonadSTM m, MonadThrow m, MonadMVar m)
=> R.Session m
-> m [SomeTable m]
getAllSessionTables (R.Types.Session s) = do
R.Unsafe.withKeepSessionOpen s $ \seshEnv -> do
ts <- readMVar (R.Unsafe.sessionOpenTables seshEnv)
pure ((\x -> SomeTable (R.Types.Table x)) <$> Map.elems ts)
getAllSessionCursors ::
(MonadSTM m, MonadThrow m, MonadMVar m)
=> R.Session m
-> m [SomeCursor m]
getAllSessionCursors (R.Types.Session s) =
R.Unsafe.withKeepSessionOpen s $ \seshEnv -> do
cs <- readMVar (R.Unsafe.sessionOpenCursors seshEnv)
pure ((\x -> SomeCursor (R.Types.Cursor x)) <$> Map.elems cs)
createSystemTempDirectory :: [Char] -> IO (FilePath, HasFS IO HandleIO, HasBlockIO IO HandleIO)
createSystemTempDirectory prefix = do
systemTempDir <- getCanonicalTemporaryDirectory
tempDir <- createTempDirectory systemTempDir prefix
(hasFS, hasBlockIO) <- ioHasBlockIO (MountPoint tempDir) defaultIOCtxParams
pure (tempDir, hasFS, hasBlockIO)
{-------------------------------------------------------------------------------
Error handlers
-------------------------------------------------------------------------------}
realErrorHandlers :: Applicative f => [Handler f (Maybe Model.Err)]
realErrorHandlers = [Handler $ pure . Just . handleSomeException]
handleSomeException :: SomeException -> Model.Err
handleSomeException e =
fromMaybe (Model.ErrOther $ displayException e) . getFirst . mconcat . fmap First $
[ handleCommitActionRegistryError <$> fromException e
, handleAbortActionRegistryError <$> fromException e
, handleSessionDirDoesNotExistError <$> fromException e
, handleSessionDirLockedError <$> fromException e
, handleSessionDirCorruptedError <$> fromException e
, handleSessionClosedError <$> fromException e
, handleTableClosedError <$> fromException e
, handleTableCorruptedError <$> fromException e
, handleTableUnionNotCompatibleError <$> fromException e
, handleSnapshotExistsError <$> fromException e
, handleSnapshotDoesNotExistError <$> fromException e
, handleSnapshotCorruptedError <$> fromException e
, handleSnapshotNotCompatibleError <$> fromException e
, handleBlobRefInvalidError <$> fromException e
, handleCursorClosedError <$> fromException e
, handleFsError <$> fromException e
]
handleCommitActionRegistryError :: CommitActionRegistryError -> Model.Err
handleCommitActionRegistryError = \case
CommitActionRegistryError actionErrors ->
Model.ErrCommitActionRegistry $
handleSomeException <$> (getActionError <$> actionErrors)
handleAbortActionRegistryError :: AbortActionRegistryError -> Model.Err
handleAbortActionRegistryError = \case
AbortActionRegistryError abortReason actionErrors ->
Model.ErrAbortActionRegistry
(handleSomeException <$> getReasonExitCaseException abortReason)
(handleSomeException . getActionError <$> actionErrors)
handleSessionDirDoesNotExistError :: SessionDirDoesNotExistError -> Model.Err
handleSessionDirDoesNotExistError = \case
ErrSessionDirDoesNotExist _dir -> Model.ErrSessionDirDoesNotExist
handleSessionDirLockedError :: SessionDirLockedError -> Model.Err
handleSessionDirLockedError = \case
ErrSessionDirLocked _dir -> Model.ErrSessionDirLocked
handleSessionDirCorruptedError :: SessionDirCorruptedError -> Model.Err
handleSessionDirCorruptedError = \case
ErrSessionDirCorrupted _reason _dir -> Model.ErrSessionDirCorrupted
handleSessionClosedError :: SessionClosedError -> Model.Err
handleSessionClosedError = \case
ErrSessionClosed -> Model.ErrSessionClosed
handleTableClosedError :: TableClosedError -> Model.Err
handleTableClosedError = \case
ErrTableClosed -> Model.ErrTableClosed
handleTableCorruptedError :: TableCorruptedError -> Model.Err
handleTableCorruptedError = \case
ErrLookupByteCountDiscrepancy{} -> Model.ErrTableCorrupted
handleTableUnionNotCompatibleError :: TableUnionNotCompatibleError -> Model.Err
handleTableUnionNotCompatibleError = \case
ErrTableUnionHandleTypeMismatch{} -> Model.ErrTableUnionHandleTypeMismatch
ErrTableUnionSessionMismatch{} -> Model.ErrTableUnionSessionMismatch
handleSnapshotExistsError :: SnapshotExistsError -> Model.Err
handleSnapshotExistsError = \case
ErrSnapshotExists name -> Model.ErrSnapshotExists name
handleSnapshotDoesNotExistError :: SnapshotDoesNotExistError -> Model.Err
handleSnapshotDoesNotExistError = \case
ErrSnapshotDoesNotExist name -> Model.ErrSnapshotDoesNotExist name
handleSnapshotCorruptedError :: SnapshotCorruptedError -> Model.Err
handleSnapshotCorruptedError = \case
ErrSnapshotCorrupted name _ -> Model.ErrSnapshotCorrupted name
handleSnapshotNotCompatibleError :: SnapshotNotCompatibleError -> Model.Err
handleSnapshotNotCompatibleError = \case
ErrSnapshotWrongLabel name _ _ -> Model.ErrSnapshotWrongLabel name
handleBlobRefInvalidError :: BlobRefInvalidError -> Model.Err
handleBlobRefInvalidError = \case
ErrBlobRefInvalid _ -> Model.ErrBlobRefInvalid
handleCursorClosedError :: CursorClosedError -> Model.Err
handleCursorClosedError = \case
ErrCursorClosed -> Model.ErrCursorClosed
handleFsError :: FsError -> Model.Err
handleFsError = Model.ErrFsError . displayException
{-------------------------------------------------------------------------------
Key and value types
-------------------------------------------------------------------------------}
newtype Key = Key SerialisedKey
deriving stock (Show, Eq, Ord)
deriving newtype (Arbitrary, R.SerialiseKey)
newtype Value = Value SerialisedValue
deriving stock (Show, Eq)
deriving newtype (Arbitrary, R.SerialiseValue)
newtype Blob = Blob SerialisedBlob
deriving stock (Show, Eq)
deriving newtype (Arbitrary, R.SerialiseValue)
keyValueBlobLabel :: R.SnapshotLabel
keyValueBlobLabel = R.SnapshotLabel "Key Value Blob"
instance R.ResolveValue Value where
resolveSerialised _ = (<>)
{-------------------------------------------------------------------------------
Model state
-------------------------------------------------------------------------------}
type ModelState :: (Type -> Type) -> ((Type -> Type) -> Type -> Type -> Type -> Type) -> Type
data ModelState m h = ModelState Model.Model Stats
deriving stock Show
initModelState :: ModelState m h
initModelState = ModelState Model.initModel initStats
{-------------------------------------------------------------------------------
Type synonyms
-------------------------------------------------------------------------------}
type Act m h a = Action (Lockstep (ModelState m h)) a
type Act' m h a = Action' m h (Either Model.Err a)
type Var m h a = ModelVar (ModelState m h) a
type Val m h a = ModelValue (ModelState m h) a
type Obs m h a = Observable (ModelState m h) a
type K a = (
Class.C_ a
, R.SerialiseKey a
, Arbitrary a
)
type V a = (
Class.C_ a
, R.SerialiseValue a
, R.ResolveValue a
, Arbitrary a
)
type B a = (
Class.C_ a
, R.SerialiseValue a
, Arbitrary a
)
-- | Common constraints for keys, values and blobs
type C k v b = (K k, V v, B b)
{-------------------------------------------------------------------------------
StateModel
-------------------------------------------------------------------------------}
newtype SilentCorruption = SilentCorruption {bitChoice :: Choice}
deriving stock (Eq, Show)
deriving newtype (Arbitrary)
instance ( Show (Class.TableConfig h)
, Eq (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
, Typeable m
) => StateModel (Lockstep (ModelState m h)) where
data instance Action (Lockstep (ModelState m h)) a where
Action :: Maybe Errors -> Action' m h a -> Act m h a
initialState = Lockstep.Defaults.initialState initModelState
nextState = Lockstep.Defaults.nextState
precondition = Lockstep.Defaults.precondition
arbitraryAction = Lockstep.Defaults.arbitraryAction
shrinkAction = Lockstep.Defaults.shrinkAction
-- Does not use the default implementation, because that would print "Action".
-- We print the name of the inner 'Action'' instead.
actionName (Action _ action') = head . words . show $ action'
deriving stock instance Show (Class.TableConfig h)
=> Show (LockstepAction (ModelState m h) a)
instance ( Eq (Class.TableConfig h)
, Typeable h
, Typeable m
) => Eq (LockstepAction (ModelState m h) a) where
(==) :: LockstepAction (ModelState m h) a -> LockstepAction (ModelState m h) a -> Bool
Action merrs1 x == Action merrs2 y = merrs1 == merrs2 && x == y
where
_coveredAllCases :: Action (Lockstep (ModelState m h)) a -> ()
_coveredAllCases = \case
Action{} -> ()
data Action' m h a where
-- Tables
NewTableWith ::
C k v b
=> {-# UNPACK #-} !(PrettyProxy (k, v, b))
-> Class.TableConfig h
-> Act' m h (WrapTable h m k v b)
CloseTable ::
C k v b
=> Var m h (WrapTable h m k v b)
-> Act' m h ()
-- Queries
Lookups ::
C k v b
=> V.Vector k -> Var m h (WrapTable h m k v b)
-> Act' m h (V.Vector (LookupResult v (WrapBlobRef h m b)))
RangeLookup ::
(C k v b, Ord k)
=> R.Range k -> Var m h (WrapTable h m k v b)
-> Act' m h (V.Vector (Entry k v (WrapBlobRef h m b)))
-- Cursor
NewCursor ::
C k v b
=> Maybe k
-> Var m h (WrapTable h m k v b)
-> Act' m h (WrapCursor h m k v b)
CloseCursor ::
C k v b
=> Var m h (WrapCursor h m k v b)
-> Act' m h ()
ReadCursor ::
C k v b
=> Int
-> Var m h (WrapCursor h m k v b)
-> Act' m h (V.Vector (Entry k v (WrapBlobRef h m b)))
-- Updates
Updates ::
C k v b
=> V.Vector (k, R.Update v b) -> Var m h (WrapTable h m k v b)
-> Act' m h ()
Inserts ::
C k v b
=> V.Vector (k, v, Maybe b) -> Var m h (WrapTable h m k v b)
-> Act' m h ()
Deletes ::
C k v b
=> V.Vector k -> Var m h (WrapTable h m k v b)
-> Act' m h ()
Upserts ::
C k v b
=> V.Vector (k, v) -> Var m h (WrapTable h m k v b)
-> Act' m h ()
-- Blobs
RetrieveBlobs ::
B b
=> Var m h (V.Vector (WrapBlobRef h m b))
-> Act' m h (V.Vector (WrapBlob b))
-- Snapshots
SaveSnapshot ::
C k v b
=> Maybe SilentCorruption
-> R.SnapshotName
-> R.SnapshotLabel
-> Var m h (WrapTable h m k v b)
-> Act' m h ()
OpenTableFromSnapshot ::
C k v b
=> {-# UNPACK #-} !(PrettyProxy (k, v, b))
-> R.SnapshotName
-> R.SnapshotLabel
-> Act' m h (WrapTable h m k v b)
DeleteSnapshot :: R.SnapshotName -> Act' m h ()
ListSnapshots :: Act' m h [R.SnapshotName]
-- Duplicate tables
Duplicate ::
C k v b
=> Var m h (WrapTable h m k v b)
-> Act' m h (WrapTable h m k v b)
-- Table union
Union ::
C k v b
=> Var m h (WrapTable h m k v b)
-> Var m h (WrapTable h m k v b)
-> Act' m h (WrapTable h m k v b)
Unions ::
C k v b
=> NonEmpty (Var m h (WrapTable h m k v b))
-> Act' m h (WrapTable h m k v b)
RemainingUnionDebt ::
C k v b
=> Var m h (WrapTable h m k v b)
-> Act' m h R.UnionDebt
SupplyUnionCredits ::
C k v b
=> Var m h (WrapTable h m k v b)
-> R.UnionCredits
-> Act' m h R.UnionCredits
-- | Alternative version of 'SupplyUnionCredits' that supplies a portion of
-- the table's current union debt as union credits.
--
-- 'SupplyUnionCredits' gets no information about union debt, so the union
-- credits we generate are arbitrary, and it would require precarious, manual
-- tuning to make sure the debt is ever paid off by an action sequence.
-- 'SupplyUnionCredits' supplies a portion (if not all) of the current debt,
-- so that unions are more likely to finish during a sequence of actions.
SupplyPortionOfDebt ::
C k v b
=> Var m h (WrapTable h m k v b)
-> Portion
-> Act' m h R.UnionCredits
portionOf :: Portion -> R.UnionDebt -> R.UnionCredits
portionOf (Portion denominator) (R.UnionDebt debt)
| denominator <= 0 = error "portion: denominator should be positive"
| debt < 0 = error "portion: debt should be non-negative"
| otherwise = R.UnionCredits (debt `div` denominator)
newtype Portion = Portion Int -- ^ Denominator: should be non-negative
deriving stock (Show, Eq)
deriving stock instance Show (Class.TableConfig h)
=> Show (Action' m h a)
instance ( Eq (Class.TableConfig h)
, Typeable h
, Typeable m
) => Eq (Action' m h a) where
x == y = go x y
where
go :: Action' m h a -> Action' m h a -> Bool
go
(NewTableWith (PrettyProxy :: PrettyProxy kvb) conf1)
(NewTableWith (PrettyProxy :: PrettyProxy kvb) conf2) =
conf1 == conf2
go (CloseTable var1) (CloseTable var2) =
Just var1 == cast var2
go (Lookups ks1 var1) (Lookups ks2 var2) =
Just ks1 == cast ks2 && Just var1 == cast var2
go (RangeLookup range1 var1) (RangeLookup range2 var2) =
range1 == range2 && var1 == var2
go (NewCursor k1 var1) (NewCursor k2 var2) =
k1 == k2 && var1 == var2
go (CloseCursor var1) (CloseCursor var2) =
Just var1 == cast var2
go (ReadCursor n1 var1) (ReadCursor n2 var2) =
n1 == n2 && var1 == var2
go (Updates ups1 var1) (Updates ups2 var2) =
Just ups1 == cast ups2 && Just var1 == cast var2
go (Inserts inss1 var1) (Inserts inss2 var2) =
Just inss1 == cast inss2 && Just var1 == cast var2
go (Deletes ks1 var1) (Deletes ks2 var2) =
Just ks1 == cast ks2 && Just var1 == cast var2
go (Upserts mups1 var1) (Upserts mups2 var2) =
Just mups1 == cast mups2 && Just var1 == cast var2
go (RetrieveBlobs vars1) (RetrieveBlobs vars2) =
Just vars1 == cast vars2
go (SaveSnapshot mcorr1 name1 label1 var1) (SaveSnapshot mcorr2 name2 label2 var2) =
mcorr1 == mcorr2 && name1 == name2 && label1 == label2 && Just var1 == cast var2
go
(OpenTableFromSnapshot (PrettyProxy :: PrettyProxy kvb) name1 label1)
(OpenTableFromSnapshot (PrettyProxy :: PrettyProxy kvb) name2 label2) =
label1 == label2 && name1 == name2
go (DeleteSnapshot name1) (DeleteSnapshot name2) =
name1 == name2
go ListSnapshots ListSnapshots =
True
go (Duplicate var1) (Duplicate var2) =
Just var1 == cast var2
go (Union var1_1 var1_2) (Union var2_1 var2_2) =
Just var1_1 == cast var2_1 && Just var1_2 == cast var2_2
go (Unions vars1) (Unions vars2) =
Just vars1 == cast vars2
go (RemainingUnionDebt var1) (RemainingUnionDebt var2) =
Just var1 == cast var2
go (SupplyUnionCredits var1 credits1) (SupplyUnionCredits var2 credits2) =
Just var1 == cast var2 && credits1 == credits2
go (SupplyPortionOfDebt var1 portion1) (SupplyPortionOfDebt var2 portion2) =
Just var1 == cast var2 && portion1 == portion2
go _ _ = False
_coveredAllCases :: Action' m h a -> ()
_coveredAllCases = \case
NewTableWith{} -> ()
CloseTable{} -> ()
Lookups{} -> ()
RangeLookup{} -> ()
NewCursor{} -> ()
CloseCursor{} -> ()
ReadCursor{} -> ()
Updates{} -> ()
Inserts{} -> ()
Deletes{} -> ()
Upserts{} -> ()
RetrieveBlobs{} -> ()
SaveSnapshot{} -> ()
OpenTableFromSnapshot{} -> ()
DeleteSnapshot{} -> ()
ListSnapshots{} -> ()
Duplicate{} -> ()
Union{} -> ()
Unions{} -> ()
RemainingUnionDebt{} -> ()
SupplyUnionCredits{} -> ()
SupplyPortionOfDebt{} -> ()
-- | This is not a fully lawful instance, because it uses 'approximateEqStream'.
instance Eq a => Eq (Stream a) where
(==) = approximateEqStream
-- | This is not a fully lawful instance, because it uses 'approximateEqStream'.
deriving stock instance Eq Errors
deriving stock instance Eq FSSim.Partial
deriving stock instance Eq FSSim.PutCorruption
deriving stock instance Eq FSSim.Blob
{-------------------------------------------------------------------------------
InLockstep
-------------------------------------------------------------------------------}
instance ( Eq (Class.TableConfig h)
, Show (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
, Typeable m
) => InLockstep (ModelState m h) where
type instance ModelOp (ModelState m h) = Op
data instance ModelValue (ModelState m h) a where
-- handle-like
MTable ::
Model.Table k v b ->
Val m h (WrapTable h m k v b)
MCursor :: Model.Cursor k v b -> Val m h (WrapCursor h m k v b)
MBlobRef ::
(Class.C_ b) =>
Model.BlobRef b ->
Val m h (WrapBlobRef h m b)
-- values
MLookupResult ::
(Class.C_ v, Class.C_ b) =>
LookupResult v (Val m h (WrapBlobRef h m b)) ->
Val m h (LookupResult v (WrapBlobRef h m b))
MEntry ::
(Class.C k v b) =>
Entry k v (Val m h (WrapBlobRef h m b)) ->
Val m h (Entry k v (WrapBlobRef h m b))
MBlob ::
(Show b, Typeable b, Eq b) =>
WrapBlob b ->
Val m h (WrapBlob b)
MSnapshotName :: R.SnapshotName -> Val m h R.SnapshotName
MUnionDebt :: R.UnionDebt -> Val m h R.UnionDebt
MUnionCredits :: R.UnionCredits -> Val m h R.UnionCredits
MUnionCreditsPortion :: R.UnionCredits -> Val m h R.UnionCredits
MErr :: Model.Err -> Val m h Model.Err
-- combinators
MUnit :: () -> Val m h ()
MPair :: (Val m h a, Val m h b) -> Val m h (a, b)
MEither :: Either (Val m h a) (Val m h b) -> Val m h (Either a b)
MList :: [Val m h a] -> Val m h [a]
MVector :: V.Vector (Val m h a) -> Val m h (V.Vector a)
data instance Observable (ModelState m h) a where
-- handle-like (opaque)
OTable :: Obs m h (WrapTable h m k v b)
OCursor :: Obs m h (WrapCursor h m k v b)
OBlobRef :: Obs m h (WrapBlobRef h m b)
-- values
OLookupResult ::
(Class.C_ v, Class.C_ b) =>
LookupResult v (Obs m h (WrapBlobRef h m b)) ->
Obs m h (LookupResult v (WrapBlobRef h m b))
OEntry ::
(Class.C k v b) =>
Entry k v (Obs m h (WrapBlobRef h m b)) ->
Obs m h (Entry k v (WrapBlobRef h m b))
OBlob ::
(Show b, Typeable b, Eq b) =>
WrapBlob b ->
Obs m h (WrapBlob b)
OUnionCredits :: R.UnionCredits -> Obs m h R.UnionCredits
OUnionCreditsPortion :: R.UnionCredits -> Obs m h R.UnionCredits
OId :: (Show a, Typeable a, Eq a) => a -> Obs m h a
-- combinators
OPair :: (Obs m h a, Obs m h b) -> Obs m h (a, b)
OEither :: Either (Obs m h a) (Obs m h b) -> Obs m h (Either a b)
OList :: [Obs m h a] -> Obs m h [a]
OVector :: V.Vector (Obs m h a) -> Obs m h (V.Vector a)
observeModel :: Val m h a -> Obs m h a
observeModel = \case
MTable _ -> OTable
MCursor _ -> OCursor
MBlobRef _ -> OBlobRef
MLookupResult x -> OLookupResult $ fmap observeModel x
MEntry x -> OEntry $ fmap observeModel x
MSnapshotName x -> OId x
MBlob x -> OBlob x
MUnionDebt x -> OId x
MUnionCredits x -> OUnionCredits x
MUnionCreditsPortion x -> OUnionCreditsPortion x
MErr x -> OId x
MUnit x -> OId x
MPair x -> OPair $ bimap observeModel observeModel x
MEither x -> OEither $ bimap observeModel observeModel x
MList x -> OList $ map observeModel x
MVector x -> OVector $ V.map observeModel x
modelNextState :: forall a.
LockstepAction (ModelState m h) a
-> ModelVarContext (ModelState m h)
-> ModelState m h
-> (ModelValue (ModelState m h) a, ModelState m h)
modelNextState action ctx (ModelState state stats) =
auxStats $ runModel (lookupVar ctx) action state
where
auxStats :: (Val m h a, Model.Model) -> (Val m h a, ModelState m h)
auxStats (result, state') = (result, ModelState state' stats')
where
stats' = updateStats action (lookupVar ctx) state state' result stats
usedVars :: LockstepAction (ModelState m h) a -> [AnyGVar (ModelOp (ModelState m h))]
usedVars (Action _ action') = case action' of
NewTableWith _ _ -> []
CloseTable tableVar -> [SomeGVar tableVar]
Lookups _ tableVar -> [SomeGVar tableVar]
RangeLookup _ tableVar -> [SomeGVar tableVar]
NewCursor _ tableVar -> [SomeGVar tableVar]
CloseCursor cursorVar -> [SomeGVar cursorVar]
ReadCursor _ cursorVar -> [SomeGVar cursorVar]
Updates _ tableVar -> [SomeGVar tableVar]
Inserts _ tableVar -> [SomeGVar tableVar]
Deletes _ tableVar -> [SomeGVar tableVar]
Upserts _ tableVar -> [SomeGVar tableVar]
RetrieveBlobs blobsVar -> [SomeGVar blobsVar]
SaveSnapshot _ _ _ tableVar -> [SomeGVar tableVar]
OpenTableFromSnapshot{} -> []
DeleteSnapshot _ -> []
ListSnapshots -> []
Duplicate tableVar -> [SomeGVar tableVar]
Union table1Var table2Var -> [SomeGVar table1Var, SomeGVar table2Var]
Unions tableVars -> [SomeGVar tableVar | tableVar <- NE.toList tableVars]
RemainingUnionDebt tableVar -> [SomeGVar tableVar]
SupplyUnionCredits tableVar _ -> [SomeGVar tableVar]
SupplyPortionOfDebt tableVar _ -> [SomeGVar tableVar]
arbitraryWithVars ::
ModelVarContext (ModelState m h)
-> ModelState m h
-> Gen (Any (LockstepAction (ModelState m h)))
arbitraryWithVars ctx st =
QC.scale (max 100) $
arbitraryActionWithVars (Proxy @(Key, Value, Blob)) keyValueBlobLabel ctx st
shrinkWithVars ::
ModelVarContext (ModelState m h)
-> ModelState m h
-> LockstepAction (ModelState m h) a
-> [Any (LockstepAction (ModelState m h))]
shrinkWithVars = shrinkActionWithVars
tagStep ::
(ModelState m h, ModelState m h)
-> LockstepAction (ModelState m h) a
-> Val m h a
-> [String]
tagStep states action = map show . tagStep' states action
deriving stock instance Show (Class.TableConfig h) => Show (Val m h a)
deriving stock instance Show (Obs m h a)
instance Eq (Obs m h a) where
obsReal == obsModel = case (obsReal, obsModel) of
-- The model is conservative about blob retrieval: the model invalidates a
-- blob reference immediately after an update to the table, and if the SUT
-- returns a blob, then that's okay. If both return a blob or both return
-- an error, then those must match exactly.
(OEither (Right (OVector vec)), OEither (Left (OId y)))
| Just Model.ErrBlobRefInvalid <- cast y ->
flip all vec $ \case
OBlob (WrapBlob _) -> True
_ -> False
-- When disk faults are injected, the model only knows /something/ went
-- wrong, but the SUT can throw much more specific errors. We allow this.
--
-- See also 'Model.runModelMWithInjectedErrors' and
-- 'runRealWithInjectedErrors'.
(OEither (Left (OId lhs)), OEither (Left (OId rhs)))
| Just (e :: Model.Err) <- cast lhs
, not $ Model.isOther e
, Just (Model.ErrDiskFault _) <- cast rhs
-> True
-- When snapshots are corrupted, the model only knows that the snapshot
-- was corrupted, but not how, but the SUT can throw much more specific
-- errors. We allow this.
(OEither (Left (OId lhs)), OEither (Left (OId rhs)))
| Just (e :: Model.Err) <- cast lhs
, not $ Model.isOther e
, Just (Model.ErrSnapshotCorrupted _) <- cast rhs
-> True
-- RemainingUnionDebt
--
-- Debt in the model is always 0, while debt in the real implementation
-- may be larger than 0.
(OEither (Right (OId lhs)), OEither (Right (OId rhs)))
| Just (lhsDebt :: R.UnionDebt) <- cast lhs
, Just (rhsDebt :: R.UnionDebt) <- cast rhs
-> lhsDebt >= R.UnionDebt 0 && rhsDebt == R.UnionDebt 0
-- SupplyUnionCredits
--
-- In the model, all supplied union credits are returned as leftovers,
-- whereas the real implementation may use up some union credits.
(OEither (Right (OUnionCredits lhsLeftovers)), OEither (Right (OUnionCredits rhsLeftovers)))
-> lhsLeftovers <= rhsLeftovers
-- SupplyPortionOfDebt
--
-- In the model, a portion of the debt is always 0, whereas in the real
-- implementation the portion of the debt is non-negative.
(OEither (Right (OUnionCreditsPortion lhsLeftovers)), OEither (Right (OUnionCreditsPortion rhsLeftovers)))
-> lhsLeftovers >= rhsLeftovers
-- default equalities
(OTable, OTable) -> True
(OCursor, OCursor) -> True
(OBlobRef, OBlobRef) -> True
(OLookupResult x, OLookupResult y) -> x == y
(OEntry x, OEntry y) -> x == y
(OBlob x, OBlob y) -> x == y
(OUnionCredits x, OUnionCredits y) -> x == y
(OUnionCreditsPortion x, OUnionCreditsPortion y) -> x == y
(OId x, OId y) -> x == y
(OPair x, OPair y) -> x == y
(OEither x, OEither y) -> x == y
(OList x, OList y) -> x == y
(OVector x, OVector y) -> x == y
(_, _) -> False
where
_coveredAllCases :: Obs m h a -> ()
_coveredAllCases = \case
OTable{} -> ()
OCursor{} -> ()
OBlobRef{} -> ()
OLookupResult{} -> ()
OEntry{} -> ()
OBlob{} -> ()
OUnionCredits{} -> ()
OUnionCreditsPortion{} -> ()
OId{} -> ()
OPair{} -> ()
OEither{} -> ()
OList{} -> ()
OVector{} -> ()
{-------------------------------------------------------------------------------
Real monad
-------------------------------------------------------------------------------}
type RealMonad h m = ReaderT (RealEnv h m) m
-- | An environment for implementations @h@ of the public API to run actions in
-- (see 'perform', 'runIO', 'runIOSim').
data RealEnv h m = RealEnv {
-- | The session to run actions in.
envSession :: !(Class.Session h m)
-- | Error handlers to convert thrown exceptions into pure error values.
--
-- Uncaught exceptions make the tests fail, so some handlers should be
-- provided that catch the exceptions and turn them into pure error values
-- if possible. The state machine infrastructure can then also compare the
-- error values obtained from running @h@ to the error values obtained by
-- running the model.
, envHandlers :: [Handler m (Maybe Model.Err)]
-- | A variable holding simulated disk faults,
--
-- This variable shared with the simulated file system (if in use). This
-- variable can be used to enable/disable errors locally, for example on a
-- per-action basis.
, envErrors :: !(StrictTVar m Errors)
-- | A variable holding a log of simulated disk faults.
--
-- Errors that are injected into the simulated file system using 'envErrors'
-- are logged here.
, envErrorsLog :: !(StrictTVar m ErrorsLog)
-- | The results of fault injection
, envInjectFaultResults :: !(MutVar (PrimState m) [InjectFaultResult])
}
data InjectFaultResult =
-- | No faults were injected.
InjectFaultNone
String -- ^ Action name
-- | Faults were injected, but the action accidentally succeeded, so the
-- action had to be rolled back
| InjectFaultAccidentalSuccess
String -- ^ Action name
-- | Faults were injected, which made the action fail with an error.
| InjectFaultInducedError
String -- ^ Action name
deriving stock Show
{-------------------------------------------------------------------------------
RunLockstep
-------------------------------------------------------------------------------}
instance ( Eq (Class.TableConfig h)
, Class.IsTable h
, Show (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
) => RunLockstep (ModelState IO h) (RealMonad h IO) where
observeReal ::
Proxy (RealMonad h IO)
-> LockstepAction (ModelState IO h) a
-> a
-> Obs IO h a
observeReal _proxy (Action _ action') result = case action' of
NewTableWith{} -> OEither $ bimap OId (const OTable) result
CloseTable{} -> OEither $ bimap OId OId result
Lookups{} -> OEither $
bimap OId (OVector . fmap (OLookupResult . fmap (const OBlobRef))) result
RangeLookup{} -> OEither $
bimap OId (OVector . fmap (OEntry . fmap (const OBlobRef))) result
NewCursor{} -> OEither $ bimap OId (const OCursor) result
CloseCursor{} -> OEither $ bimap OId OId result
ReadCursor{} -> OEither $
bimap OId (OVector . fmap (OEntry . fmap (const OBlobRef))) result
Updates{} -> OEither $ bimap OId OId result
Inserts{} -> OEither $ bimap OId OId result
Deletes{} -> OEither $ bimap OId OId result
Upserts{} -> OEither $ bimap OId OId result
RetrieveBlobs{} -> OEither $ bimap OId (OVector . fmap OBlob) result
SaveSnapshot{} -> OEither $ bimap OId OId result
OpenTableFromSnapshot{} -> OEither $ bimap OId (const OTable) result
DeleteSnapshot{} -> OEither $ bimap OId OId result
ListSnapshots{} -> OEither $ bimap OId (OList . fmap OId) result
Duplicate{} -> OEither $ bimap OId (const OTable) result
Union{} -> OEither $ bimap OId (const OTable) result
Unions{} -> OEither $ bimap OId (const OTable) result
RemainingUnionDebt{} -> OEither $ bimap OId OId result
SupplyUnionCredits{} -> OEither $ bimap OId OUnionCredits result
SupplyPortionOfDebt{} -> OEither $ bimap OId OUnionCreditsPortion result
showRealResponse ::
Proxy (RealMonad h IO)
-> LockstepAction (ModelState IO h) a
-> Maybe (Dict (Show a))
showRealResponse _ (Action _ action') = case action' of
NewTableWith{} -> Nothing
CloseTable{} -> Just Dict
Lookups{} -> Nothing
RangeLookup{} -> Nothing
NewCursor{} -> Nothing
CloseCursor{} -> Just Dict
ReadCursor{} -> Nothing
Updates{} -> Just Dict
Inserts{} -> Just Dict
Deletes{} -> Just Dict
Upserts{} -> Just Dict
RetrieveBlobs{} -> Just Dict
SaveSnapshot{} -> Just Dict
OpenTableFromSnapshot{} -> Nothing
DeleteSnapshot{} -> Just Dict
ListSnapshots{} -> Just Dict
Duplicate{} -> Nothing
Union{} -> Nothing
Unions{} -> Nothing
RemainingUnionDebt{} -> Just Dict
SupplyUnionCredits{} -> Just Dict
SupplyPortionOfDebt{} -> Just Dict
instance ( Eq (Class.TableConfig h)
, Class.IsTable h
, Show (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
, Typeable s
) => RunLockstep (ModelState (IOSim s) h) (RealMonad h (IOSim s)) where
observeReal ::
Proxy (RealMonad h (IOSim s))
-> LockstepAction (ModelState (IOSim s) h) a
-> a
-> Obs (IOSim s) h a
observeReal _proxy (Action _ action') result = case action' of
NewTableWith{} -> OEither $ bimap OId (const OTable) result
CloseTable{} -> OEither $ bimap OId OId result
Lookups{} -> OEither $
bimap OId (OVector . fmap (OLookupResult . fmap (const OBlobRef))) result
RangeLookup{} -> OEither $
bimap OId (OVector . fmap (OEntry . fmap (const OBlobRef))) result
NewCursor{} -> OEither $ bimap OId (const OCursor) result
CloseCursor{} -> OEither $ bimap OId OId result
ReadCursor{} -> OEither $
bimap OId (OVector . fmap (OEntry . fmap (const OBlobRef))) result
Updates{} -> OEither $ bimap OId OId result
Inserts{} -> OEither $ bimap OId OId result
Deletes{} -> OEither $ bimap OId OId result
Upserts{} -> OEither $ bimap OId OId result
RetrieveBlobs{} -> OEither $ bimap OId (OVector . fmap OBlob) result
SaveSnapshot{} -> OEither $ bimap OId OId result
OpenTableFromSnapshot{} -> OEither $ bimap OId (const OTable) result
DeleteSnapshot{} -> OEither $ bimap OId OId result
ListSnapshots{} -> OEither $ bimap OId (OList . fmap OId) result
Duplicate{} -> OEither $ bimap OId (const OTable) result
Union{} -> OEither $ bimap OId (const OTable) result
Unions{} -> OEither $ bimap OId (const OTable) result
RemainingUnionDebt{} -> OEither $ bimap OId OId result
SupplyUnionCredits{} -> OEither $ bimap OId OUnionCredits result
SupplyPortionOfDebt{} -> OEither $ bimap OId OUnionCreditsPortion result
showRealResponse ::
Proxy (RealMonad h (IOSim s))
-> LockstepAction (ModelState (IOSim s) h) a
-> Maybe (Dict (Show a))
showRealResponse _ (Action _ action') = case action' of
NewTableWith{} -> Nothing
CloseTable{} -> Just Dict
Lookups{} -> Nothing
RangeLookup{} -> Nothing
NewCursor{} -> Nothing
CloseCursor{} -> Just Dict
ReadCursor{} -> Nothing
Updates{} -> Just Dict
Inserts{} -> Just Dict
Deletes{} -> Just Dict
Upserts{} -> Just Dict
RetrieveBlobs{} -> Just Dict
SaveSnapshot{} -> Just Dict
OpenTableFromSnapshot{} -> Nothing
DeleteSnapshot{} -> Just Dict
ListSnapshots{} -> Just Dict
Duplicate{} -> Nothing
Union{} -> Nothing
Unions{} -> Nothing
RemainingUnionDebt{} -> Just Dict
SupplyUnionCredits{} -> Just Dict
SupplyPortionOfDebt{} -> Just Dict
{-------------------------------------------------------------------------------
RunModel
-------------------------------------------------------------------------------}
instance ( Eq (Class.TableConfig h)
, Class.IsTable h
, Show (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
) => RunModel (Lockstep (ModelState IO h)) (RealMonad h IO) where
perform _ = runIO
postcondition = Lockstep.Defaults.postcondition
monitoring = Lockstep.Defaults.monitoring (Proxy @(RealMonad h IO))
instance ( Eq (Class.TableConfig h)
, Class.IsTable h
, Show (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
, Typeable s
) => RunModel (Lockstep (ModelState (IOSim s) h)) (RealMonad h (IOSim s)) where
perform _ = runIOSim
postcondition = Lockstep.Defaults.postcondition
monitoring = Lockstep.Defaults.monitoring (Proxy @(RealMonad h (IOSim s)))
{-------------------------------------------------------------------------------
Interpreter for the model
-------------------------------------------------------------------------------}
-- TODO: there are a bunch of TODO(err) in 'runModel' on the last argument to
-- 'Model.runModelMWithInjectedErrors'. This last argument defines how the model
-- should respond to injected errors. Since we don't generate injected errors
-- for most of these actions yet, they are left open. We will fill these in as
-- we start generating injected errors for these actions and testing with them.
runModel ::
ModelLookUp (ModelState m h)
-> LockstepAction (ModelState m h) a
-> Model.Model -> (Val m h a, Model.Model)
runModel lookUp (Action merrs action') = case action' of
NewTableWith _ _cfg ->
wrap MTable
. Model.runModelMWithInjectedErrors merrs
(Model.new Model.TableConfig)
(pure ()) -- TODO(err)
CloseTable tableVar ->
wrap MUnit
. Model.runModelMWithInjectedErrors merrs
(Model.close (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
Lookups ks tableVar ->
wrap (MVector . fmap (MLookupResult . fmap MBlobRef))
. Model.runModelMWithInjectedErrors merrs
(Model.lookups ks (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
RangeLookup range tableVar ->
wrap (MVector . fmap (MEntry . fmap MBlobRef))
. Model.runModelMWithInjectedErrors merrs
(Model.rangeLookup range (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
NewCursor offset tableVar ->
wrap MCursor
. Model.runModelMWithInjectedErrors merrs
(Model.newCursor offset (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
CloseCursor cursorVar ->
wrap MUnit
. Model.runModelMWithInjectedErrors merrs
(Model.closeCursor (getCursor $ lookUp cursorVar))
(pure ()) -- TODO(err)
ReadCursor n cursorVar ->
wrap (MVector . fmap (MEntry . fmap MBlobRef))
. Model.runModelMWithInjectedErrors merrs
(Model.readCursor n (getCursor $ lookUp cursorVar))
(pure ()) -- TODO(err)
Updates kups tableVar ->
wrap MUnit
. Model.runModelMWithInjectedErrors merrs
(Model.updates Model.getResolve kups (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
Inserts kins tableVar ->
wrap MUnit
. Model.runModelMWithInjectedErrors merrs
(Model.inserts Model.getResolve kins (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
Deletes kdels tableVar ->
wrap MUnit
. Model.runModelMWithInjectedErrors merrs
(Model.deletes Model.getResolve kdels (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
Upserts kmups tableVar ->
wrap MUnit
. Model.runModelMWithInjectedErrors merrs
(Model.upserts Model.getResolve kmups (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
RetrieveBlobs blobsVar ->
wrap (MVector . fmap (MBlob . WrapBlob))
. Model.runModelMWithInjectedErrors merrs
(Model.retrieveBlobs (getBlobRefs . lookUp $ blobsVar))
(pure ()) -- TODO(err)
SaveSnapshot mcorr name label tableVar ->
wrap MUnit
. Model.runModelMWithInjectedErrors merrs
(do Model.saveSnapshot name label (getTable $ lookUp tableVar)
forM_ mcorr $ \_ -> Model.corruptSnapshot name)
(pure ()) -- TODO(err)
OpenTableFromSnapshot _ name label ->
wrap MTable
. Model.runModelMWithInjectedErrors merrs
(Model.openTableFromSnapshot name label)
(pure ())
DeleteSnapshot name ->
wrap MUnit
. Model.runModelMWithInjectedErrors merrs
(Model.deleteSnapshot name)
(pure ()) -- TODO(err)
ListSnapshots ->
wrap (MList . fmap MSnapshotName)
. Model.runModelMWithInjectedErrors merrs
Model.listSnapshots
(pure ()) -- TODO(err)
Duplicate tableVar ->
wrap MTable
. Model.runModelMWithInjectedErrors merrs
(Model.duplicate (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
Union table1Var table2Var ->
wrap MTable
. Model.runModelMWithInjectedErrors merrs
(Model.union Model.getResolve (getTable $ lookUp table1Var) (getTable $ lookUp table2Var))
(pure ()) -- TODO(err)
Unions tableVars ->
wrap MTable
. Model.runModelMWithInjectedErrors merrs
(Model.unions Model.getResolve (fmap (getTable . lookUp) tableVars))
(pure ()) -- TODO(err)
RemainingUnionDebt tableVar ->
wrap MUnionDebt
. Model.runModelMWithInjectedErrors merrs
(Model.remainingUnionDebt (getTable $ lookUp tableVar))
(pure ()) -- TODO(err)
SupplyUnionCredits tableVar credits ->
wrap MUnionCredits
. Model.runModelMWithInjectedErrors merrs
(Model.supplyUnionCredits (getTable $ lookUp tableVar) credits)
(pure ()) -- TODO(err)
SupplyPortionOfDebt tableVar portion ->
wrap MUnionCreditsPortion
. Model.runModelMWithInjectedErrors merrs
(do let table = getTable $ lookUp tableVar
Model.supplyPortionOfDebt table portion
)
(pure ()) -- TODO(err)
where
getTable ::
ModelValue (ModelState m h) (WrapTable h m k v b)
-> Model.Table k v b
getTable (MTable t) = t
getCursor ::
ModelValue (ModelState m h) (WrapCursor h m k v b)
-> Model.Cursor k v b
getCursor (MCursor t) = t
getBlobRefs :: ModelValue (ModelState m h) (V.Vector (WrapBlobRef h m b)) -> V.Vector (Model.BlobRef b)
getBlobRefs (MVector brs) = fmap (\(MBlobRef br) -> br) brs
wrap ::
(a -> Val m h b)
-> (Either Model.Err a, Model.Model)
-> (Val m h (Either Model.Err b), Model.Model)
wrap f = first (MEither . bimap MErr f)
{-------------------------------------------------------------------------------
Interpreters for @'IOLike' m@
-------------------------------------------------------------------------------}
-- TODO: there are a bunch of TODO(err) in 'runIO' and 'runIOSim' below on the
-- last argument to 'Model.runModelMWithInjectedErrors'. This last argument
-- defines how the SUT should recover from actions that accidentally succeeded
-- in the presence of disk faults. Since we don't generate injected errors for
-- most of these actions yet, they are left open. We will fill these in as we
-- start generating injected errors for these actions and testing with them.
runIO ::
forall a h. Class.IsTable h
=> LockstepAction (ModelState IO h) a
-> LookUp
-> RealMonad h IO a
runIO action lookUp = ReaderT $ \ !env -> do
aux env action
where
aux ::
RealEnv h IO
-> LockstepAction (ModelState IO h) a
-> IO a
aux env (Action merrs action') = case action' of
NewTableWith _ cfg ->
runRealWithInjectedErrors "NewTableWith" env merrs
(WrapTable <$> Class.newTableWith cfg session)
(\_ -> pure ()) -- TODO(err)
CloseTable tableVar ->
runRealWithInjectedErrors "CloseTable" env merrs
(Class.closeTable (unwrapTable $ lookUp' tableVar))
(\_ -> pure ()) -- TODO(err)
Lookups ks tableVar ->
runRealWithInjectedErrors "Lookups" env merrs
(fmap (fmap WrapBlobRef) <$> Class.lookups (unwrapTable $ lookUp' tableVar) ks)
(\_ -> pure ()) -- TODO(err)
RangeLookup range tableVar ->
runRealWithInjectedErrors "RangeLookup" env merrs
(fmap (fmap WrapBlobRef) <$> Class.rangeLookup (unwrapTable $ lookUp' tableVar) range)
(\_ -> pure ()) -- TODO(err)
NewCursor offset tableVar ->
runRealWithInjectedErrors "NewCursor" env merrs
(WrapCursor <$> Class.newCursor offset (unwrapTable $ lookUp' tableVar))
(\_ -> pure ()) -- TODO(err)
CloseCursor cursorVar ->
runRealWithInjectedErrors "CloseCursor" env merrs
(Class.closeCursor (Proxy @h) (unwrapCursor $ lookUp' cursorVar))
(\_ -> pure ()) -- TODO(err)
ReadCursor n cursorVar ->
runRealWithInjectedErrors "ReadCursor" env merrs
(fmap (fmap WrapBlobRef) <$> Class.readCursor (Proxy @h) n (unwrapCursor $ lookUp' cursorVar))
(\_ -> pure ()) -- TODO(err)
Updates kups tableVar ->
runRealWithInjectedErrors "Updates" env merrs
(Class.updates (unwrapTable $ lookUp' tableVar) kups)
(\_ -> pure ()) -- TODO(err)
Inserts kins tableVar ->
runRealWithInjectedErrors "Inserts" env merrs
(Class.inserts (unwrapTable $ lookUp' tableVar) kins)
(\_ -> pure ()) -- TODO(err)
Deletes kdels tableVar ->
runRealWithInjectedErrors "Deletes" env merrs
(Class.deletes (unwrapTable $ lookUp' tableVar) kdels)
(\_ -> pure ()) -- TODO(err)
Upserts kmups tableVar ->
runRealWithInjectedErrors "Upserts" env merrs
(Class.upserts (unwrapTable $ lookUp' tableVar) kmups)
(\_ -> pure ()) -- TODO(err)
RetrieveBlobs blobRefsVar ->
runRealWithInjectedErrors "RetrieveBlobs" env merrs
(fmap WrapBlob <$> Class.retrieveBlobs (Proxy @h) session (unwrapBlobRef <$> lookUp' blobRefsVar))
(\_ -> pure ()) -- TODO(err)
SaveSnapshot mcorr name label tableVar ->
let table = unwrapTable $ lookUp' tableVar in
runRealWithInjectedErrors "SaveSnapshot" env merrs
(do Class.saveSnapshot name label table
forM_ mcorr $ \corr -> Class.corruptSnapshot (bitChoice corr) name table)
(\() -> Class.deleteSnapshot session name) -- TODO(err)
OpenTableFromSnapshot _ name label ->
runRealWithInjectedErrors "OpenTableFromSnapshot" env merrs
(WrapTable <$> Class.openTableFromSnapshot session name label)
(\(WrapTable t) -> Class.closeTable t)
DeleteSnapshot name ->
runRealWithInjectedErrors "DeleteSnapshot" env merrs
(Class.deleteSnapshot session name)
(\_ -> pure ()) -- TODO(err)
ListSnapshots ->
runRealWithInjectedErrors "ListSnapshots" env merrs
(Class.listSnapshots session)
(\_ -> pure ()) -- TODO(err)
Duplicate tableVar ->
runRealWithInjectedErrors "Duplicate" env merrs
(WrapTable <$> Class.duplicate (unwrapTable $ lookUp' tableVar))
(\_ -> pure ()) -- TODO(err)
Union table1Var table2Var ->
runRealWithInjectedErrors "Union" env merrs
(WrapTable <$> Class.union (unwrapTable $ lookUp' table1Var) (unwrapTable $ lookUp' table2Var))
(\_ -> pure ()) -- TODO(err)
Unions tableVars ->
runRealWithInjectedErrors "Unions" env merrs
(WrapTable <$> Class.unions (fmap (unwrapTable . lookUp') tableVars))
(\_ -> pure ()) -- TODO(err)
RemainingUnionDebt tableVar ->
runRealWithInjectedErrors "RemainingUnionDebt" env merrs
(Class.remainingUnionDebt (unwrapTable $ lookUp' tableVar))
(\_ -> pure ()) -- TODO(err)
SupplyUnionCredits tableVar credits ->
runRealWithInjectedErrors "SupplyUnionCredits" env merrs
(Class.supplyUnionCredits (unwrapTable $ lookUp' tableVar) credits)
(\_ -> pure ()) -- TODO(err)
SupplyPortionOfDebt tableVar portion ->
runRealWithInjectedErrors "SupplyPortionOfDebt" env merrs
(do let table = unwrapTable $ lookUp' tableVar
debt <- Class.remainingUnionDebt table
Class.supplyUnionCredits table (portion `portionOf` debt))
(\_ -> pure ()) -- TODO(err)
where
session = envSession env
lookUp' :: Var m h x -> x
lookUp' = realLookupVar lookUp
runIOSim ::
forall s a h. Class.IsTable h
=> LockstepAction (ModelState (IOSim s) h) a
-> LookUp
-> RealMonad h (IOSim s) a
runIOSim action lookUp = ReaderT $ \ !env -> do
aux env action
where
aux ::
RealEnv h (IOSim s)
-> LockstepAction (ModelState (IOSim s) h) a
-> IOSim s a
aux env (Action merrs action') = case action' of
NewTableWith _ cfg ->
runRealWithInjectedErrors "NewTableWith" env merrs
(WrapTable <$> Class.newTableWith cfg session)
(\_ -> pure ()) -- TODO(err)
CloseTable tableVar ->
runRealWithInjectedErrors "CloseTable" env merrs
(Class.closeTable (unwrapTable $ lookUp' tableVar))
(\_ -> pure ()) -- TODO(err)
Lookups ks tableVar ->
runRealWithInjectedErrors "Lookups" env merrs
(fmap (fmap WrapBlobRef) <$> Class.lookups (unwrapTable $ lookUp' tableVar) ks)
(\_ -> pure ()) -- TODO(err)
RangeLookup range tableVar ->
runRealWithInjectedErrors "RangeLookup" env merrs
(fmap (fmap WrapBlobRef) <$> Class.rangeLookup (unwrapTable $ lookUp' tableVar) range)
(\_ -> pure ()) -- TODO(err)
NewCursor offset tableVar ->
runRealWithInjectedErrors "NewCursor" env merrs
(WrapCursor <$> Class.newCursor offset (unwrapTable $ lookUp' tableVar))
(\_ -> pure ()) -- TODO(err)
CloseCursor cursorVar ->
runRealWithInjectedErrors "CloseCursor" env merrs
(Class.closeCursor (Proxy @h) (unwrapCursor $ lookUp' cursorVar))
(\_ -> pure ()) -- TODO(err)
ReadCursor n cursorVar ->
runRealWithInjectedErrors "ReadCursor" env merrs
(fmap (fmap WrapBlobRef) <$> Class.readCursor (Proxy @h) n (unwrapCursor $ lookUp' cursorVar))
(\_ -> pure ()) -- TODO(err)
Updates kups tableVar ->
runRealWithInjectedErrors "Updates" env merrs
(Class.updates (unwrapTable $ lookUp' tableVar) kups)
(\_ -> pure ()) -- TODO(err)
Inserts kins tableVar ->
runRealWithInjectedErrors "Inserts" env merrs
(Class.inserts (unwrapTable $ lookUp' tableVar) kins)
(\_ -> pure ()) -- TODO(err)
Deletes kdels tableVar ->
runRealWithInjectedErrors "Deletes" env merrs
(Class.deletes (unwrapTable $ lookUp' tableVar) kdels)
(\_ -> pure ()) -- TODO(err)
Upserts kmups tableVar ->
runRealWithInjectedErrors "Upserts" env merrs
(Class.upserts (unwrapTable $ lookUp' tableVar) kmups)
(\_ -> pure ()) -- TODO(err)
RetrieveBlobs blobRefsVar ->
runRealWithInjectedErrors "RetrieveBlobs" env merrs
(fmap WrapBlob <$> Class.retrieveBlobs (Proxy @h) session (unwrapBlobRef <$> lookUp' blobRefsVar))
(\_ -> pure ()) -- TODO(err)
SaveSnapshot mcorr name label tableVar ->
let table = unwrapTable $ lookUp' tableVar in
runRealWithInjectedErrors "SaveSnapshot" env merrs
(do Class.saveSnapshot name label table
forM_ mcorr $ \corr -> Class.corruptSnapshot (bitChoice corr) name table)
(\() -> Class.deleteSnapshot session name) -- TODO(err)
OpenTableFromSnapshot _ name label ->
runRealWithInjectedErrors "OpenTableFromSnapshot" env merrs
(WrapTable <$> Class.openTableFromSnapshot session name label)
(\(WrapTable t) -> Class.closeTable t)
DeleteSnapshot name ->
runRealWithInjectedErrors "DeleteSnapshot" env merrs
(Class.deleteSnapshot session name)
(\_ -> pure ()) -- TODO(err)
ListSnapshots ->
runRealWithInjectedErrors "ListSnapshots" env merrs
(Class.listSnapshots session)
(\_ -> pure ()) -- TODO(err)
Duplicate tableVar ->
runRealWithInjectedErrors "Duplicate" env merrs
(WrapTable <$> Class.duplicate (unwrapTable $ lookUp' tableVar))
(\_ -> pure ()) -- TODO(err)
Union table1Var table2Var ->
runRealWithInjectedErrors "Union" env merrs
(WrapTable <$> Class.union (unwrapTable $ lookUp' table1Var) (unwrapTable $ lookUp' table2Var))
(\_ -> pure ()) -- TODO(err)
Unions tableVars ->
runRealWithInjectedErrors "Unions" env merrs
(WrapTable <$> Class.unions (fmap (unwrapTable . lookUp') tableVars))
(\_ -> pure ()) -- TODO(err)
RemainingUnionDebt tableVar ->
runRealWithInjectedErrors "RemainingUnionDebt" env merrs
(Class.remainingUnionDebt (unwrapTable $ lookUp' tableVar))
(\_ -> pure ()) -- TODO(err)
SupplyUnionCredits tableVar credits ->
runRealWithInjectedErrors "SupplyUnionCredits" env merrs
(Class.supplyUnionCredits (unwrapTable $ lookUp' tableVar) credits)
(\_ -> pure ()) -- TODO(err)
SupplyPortionOfDebt tableVar portion ->
runRealWithInjectedErrors "SupplyPortionOfDebt" env merrs
(do let table = unwrapTable $ lookUp' tableVar
debt <- Class.remainingUnionDebt table
Class.supplyUnionCredits table (portion `portionOf` debt))
(\_ -> pure ()) -- TODO(err)
where
session = envSession env
lookUp' :: Var m h x -> x
lookUp' = realLookupVar lookUp
-- | @'runRealWithInjectedErrors' _ errsVar merrs action rollback@ runs @action@
-- with injected errors if available in @merrs@.
--
-- See 'Model.runModelMWithInjectedErrors': the real system is not guaranteed to
-- fail with an error if there are injected disk faults, but the model *always*
-- fails. In case the real system accidentally succeeded in running @action@
-- when there were errors to inject, then we roll back the success using
-- @rollback@. This ensures that the model and system stay in sync. For example:
-- if creating a snapshot accidentally succeeded, then the rollback action is to
-- delete that snapshot.
runRealWithInjectedErrors ::
(MonadCatch m, MonadSTM m, PrimMonad m)
=> String -- ^ Name of the action
-> RealEnv h m
-> Maybe Errors
-> m t-- ^ Action to run
-> (t -> m ()) -- ^ Rollback if the action *accidentally* succeeded
-> m (Either Model.Err t)
runRealWithInjectedErrors s env merrs k rollback =
case merrs of
Nothing -> do
modifyMutVar faultsVar (InjectFaultNone s :)
catchErr handlers k
Just errs -> do
atomically $ writeTVar logVar emptyLog
eith <- catchErr handlers $ FSSim.withErrors errsVar errs k
errsLog <- readTVarIO logVar
case eith of
Left e | Model.isDiskFault e -> do
modifyMutVar faultsVar (InjectFaultInducedError s :)
if countNoisyErrors errsLog == 0 then
pure $ Left $ Model.ErrOther $
-- If we injected 0 disk faults, but we still found an
-- ErrDiskFault, then there is a bug in our code. ErrDiskFaults
-- should not occur on the happy path.
"Found a disk fault error, but no disk faults were injected: " <> show e
else
pure eith
Left e -> do
if countNoisyErrors errsLog > 0 then
pure $ Left $ Model.ErrOther $
-- If we injected 1 or more disk faults, but we did not find an
-- ErrDiskFault, then there is a bug in our code. An injected disk
-- fault should always lead to an ErrDiskFault.
"Found an error that isn't a disk fault error, but disk faults were injected: " <> show e
else
pure eith
Right x -> do
modifyMutVar faultsVar (InjectFaultAccidentalSuccess s :)
rollback x
if (countNoisyErrors errsLog > 0) then
pure $ Left $ Model.ErrOther $
-- If we injected 1 or more disk faults, but the action
-- accidentally succeeded, then 1 or more errors were swallowed
-- that should have been found as ErrDiskFault.
"Action succeeded, but disk faults were injected. Errors were swallowed!"
else
pure $ Left $ Model.ErrDiskFault ("dummy: " <> s)
where
errsVar = envErrors env
logVar = envErrorsLog env
faultsVar = envInjectFaultResults env
handlers = envHandlers env
catchErr ::
forall m a e. MonadCatch m
=> [Handler m (Maybe e)] -> m a -> m (Either e a)
catchErr hs action = catches (Right <$> action) (fmap f hs)
where
f (Handler h) = Handler $ \e -> maybe (throwIO e) (pure . Left) =<< h e
{-------------------------------------------------------------------------------
Generator and shrinking
-------------------------------------------------------------------------------}
arbitraryActionWithVars ::
forall m h k v b. (
C k v b
, Ord k
, Eq (Class.TableConfig h)
, Show (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
, Typeable m
)
=> Proxy (k, v, b)
-> R.SnapshotLabel
-> ModelVarContext (ModelState m h)
-> ModelState m h
-> Gen (Any (LockstepAction (ModelState m h)))
arbitraryActionWithVars _ label ctx (ModelState st _stats) =
QC.frequency $
concat
[ genActionsSession
, genActionsTables
, genActionsUnion
, genActionsCursor
, genActionsBlobRef
]
where
_coveredAllCases :: LockstepAction (ModelState m h) a -> ()
_coveredAllCases (Action _ action') = _coveredAllCases' action'
_coveredAllCases' :: Action' m h a -> ()
_coveredAllCases' = \case
NewTableWith{} -> ()
CloseTable{} -> ()
Lookups{} -> ()
RangeLookup{} -> ()
NewCursor{} -> ()
CloseCursor{} -> ()
ReadCursor{} -> ()
Updates{} -> ()
Inserts{} -> ()
Deletes{} -> ()
Upserts{} -> ()
RetrieveBlobs{} -> ()
SaveSnapshot{} -> ()
DeleteSnapshot{} -> ()
ListSnapshots{} -> ()
OpenTableFromSnapshot{} -> ()
Duplicate{} -> ()
Union{} -> ()
Unions{} -> ()
RemainingUnionDebt{} -> ()
SupplyUnionCredits{} -> ()
SupplyPortionOfDebt{} -> ()
genTableVar = QC.elements tableVars
tableVars :: [Var m h (WrapTable h m k v b)]
tableVars =
[ fromRight v
| v <- findVars ctx Proxy
, case lookupVar ctx v of
MEither (Left _) -> False
MEither (Right (MTable t)) ->
Map.member (Model.tableID t) (Model.tables st)
]
genUnionDescendantTableVar = QC.elements unionDescendantTableVars
unionDescendantTableVars :: [Var m h (WrapTable h m k v b)]
unionDescendantTableVars =
[ v
| v <- tableVars
, let t = case lookupVar ctx v of
MTable t' -> t'
, Model.isUnionDescendant t == Model.IsUnionDescendant
]
genCursorVar = QC.elements cursorVars
cursorVars :: [Var m h (WrapCursor h m k v b)]
cursorVars =
[ fromRight v
| v <- findVars ctx Proxy
, case lookupVar ctx v of
MEither (Left _) -> False
MEither (Right (MCursor c)) ->
Map.member (Model.cursorID c) (Model.cursors st)
]
genBlobRefsVar = QC.elements blobRefsVars
blobRefsVars :: [Var m h (V.Vector (WrapBlobRef h m b))]
blobRefsVars = fmap (mapGVar (OpComp OpLookupResults)) lookupResultVars
++ fmap (mapGVar (OpComp OpEntrys)) queryResultVars
where
lookupResultVars :: [Var m h (V.Vector (LookupResult v (WrapBlobRef h m b)))]
queryResultVars :: [Var m h (V.Vector (Entry k v (WrapBlobRef h m b)))]
lookupResultVars = fromRight <$> findVars ctx Proxy
queryResultVars = fromRight <$> findVars ctx Proxy
genUsedSnapshotName = QC.elements usedSnapshotNames
genUnusedSnapshotName = QC.elements unusedSnapshotNames
usedSnapshotNames, unusedSnapshotNames :: [R.SnapshotName]
(usedSnapshotNames, unusedSnapshotNames) =
partitionEithers
[ if Map.member snapshotname (Model.snapshots st)
then Left snapshotname -- used
else Right snapshotname -- unused
| name <- ["snap1", "snap2", "snap3" ]
, let snapshotname = R.toSnapshotName name
]
genActionsSession :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
genActionsSession =
[ (1, fmap Some $ (Action <$> genErrors <*>) $
NewTableWith @k @v @b <$> pure PrettyProxy <*> QC.arbitrary)
| length tableVars <= 5 -- no more than 5 tables at once
, let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (2, fmap Some $ (Action <$> genErrors <*>) $
OpenTableFromSnapshot @k @v @b PrettyProxy <$> genUsedSnapshotName <*> pure label)
| length tableVars <= 5 -- no more than 5 tables at once
, not (null usedSnapshotNames)
, -- TODO: bloomFilterFromFile swallows an FsReachedEOF error
let isFsReachedEOFError = maybe False (either isFsReachedEOF (const False))
, let genErrors = QC.frequency [
(3, pure Nothing)
, (1, Just . filterHGetBufSomeE (not . isFsReachedEOFError)
. noRemoveDirectoryRecursiveE
<$> QC.arbitrary)
]
]
++ [ (1, fmap Some $ (Action <$> genErrors <*>) $
DeleteSnapshot <$> genUsedSnapshotName)
| not (null usedSnapshotNames)
, let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (1, fmap Some $ (Action <$> genErrors <*>) $
pure ListSnapshots)
| not (null tableVars) -- otherwise boring!
, let genErrors = pure Nothing -- TODO: generate errors
]
genActionsTables :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
genActionsTables
| null tableVars = []
| otherwise =
[ (1, fmap Some $ (Action <$> genErrors <*>) $
CloseTable <$> genTableVar)
| let genErrors = pure Nothing
]
++ [ (10, fmap Some $ (Action <$> genErrors <*>) $
Lookups <$> genLookupKeys <*> genTableVar)
| let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (5, fmap Some $ (Action <$> genErrors <*>) $
RangeLookup <$> genRange <*> genTableVar)
| let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (10, fmap Some $ (Action <$> genErrors <*>) $
Updates <$> genUpdates <*> genTableVar)
| let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (10, fmap Some $ (Action <$> genErrors <*>) $
Inserts <$> genInserts <*> genTableVar)
| let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (10, fmap Some $ (Action <$> genErrors <*>) $
Deletes <$> genDeletes <*> genTableVar)
| let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (10, fmap Some $ (Action <$> genErrors <*>) $
Upserts <$> genMupserts <*> genTableVar)
| let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (3, fmap Some $ (Action <$> genErrors <*>) $
NewCursor <$> QC.arbitrary <*> genTableVar)
| length cursorVars <= 5 -- no more than 5 cursors at once
, let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (2, fmap Some $ (Action <$> genErrors <*>) $
SaveSnapshot <$> genCorruption <*> genUnusedSnapshotName <*> pure label <*> genTableVar)
| not (null unusedSnapshotNames)
-- TODO: should errors and corruption be generated at the same time,
-- or should they be mutually exclusive?
, let genErrors = pure Nothing -- TODO: generate errors
, let genCorruption = QC.frequency [
(3, pure Nothing)
, (1, Just <$> QC.arbitrary)
]
]
++ [ (5, fmap Some $ (Action <$> genErrors <*>) $
Duplicate <$> genTableVar)
| length tableVars <= 5 -- no more than 5 tables at once
, let genErrors = pure Nothing -- TODO: generate errors
]
-- | Generate table actions that have to do with unions.
genActionsUnion :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
genActionsUnion
| null tableVars = []
| otherwise =
[ (2, fmap Some $ (Action <$> genErrors <*>) $
Union <$> genTableVar <*> genTableVar)
| length tableVars <= 5 -- no more than 5 tables at once
, let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (2, fmap Some $ (Action <$> genErrors <*>) $ do
-- Generate at least a 2-way union, and at most a 3-way union.
--
-- Tests for 1-way unions are included in the UnitTests module.
-- n-way unions for n>3 lead to large unions, which are less
-- likely to be finished before the end of an action sequence.
n <- QC.chooseInt (2, 3)
Unions . NE.fromList <$> QC.vectorOf n genTableVar)
| length tableVars <= 5 -- no more than 5 tables at once
, let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (2, fmap Some $ (Action <$> genErrors <*>) $
RemainingUnionDebt <$> genUnionDescendantTableVar)
-- Tables not derived from unions are covered in UnitTests.
| not (null unionDescendantTableVars)
, let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (8, fmap Some $ (Action <$> genErrors <*>) $
SupplyUnionCredits <$> genUnionDescendantTableVar <*> genUnionCredits)
-- Tables not derived from unions are covered in UnitTests.
| not (null unionDescendantTableVars)
, let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (2, fmap Some $ (Action <$> genErrors <*>) $
SupplyPortionOfDebt <$> genUnionDescendantTableVar <*> genPortion)
-- Tables not derived from unions are covered in UnitTests.
| not (null unionDescendantTableVars)
, let genErrors = pure Nothing -- TODO: generate errors
]
where
-- The typical, interesting case is to supply a positive number of
-- union credits. Supplying 0 or less credits is a no-op. We cover
-- it in UnitTests so we don't have to cover it here.
genUnionCredits = R.UnionCredits . QC.getPositive <$> QC.arbitrary
-- TODO: tweak distribution once table unions are implemented
genPortion = Portion <$> QC.elements [1, 2, 3]
genActionsCursor :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
genActionsCursor
| null cursorVars = []
| otherwise =
[ (2, fmap Some $ (Action <$> genErrors <*>) $
CloseCursor <$> genCursorVar)
| let genErrors = pure Nothing -- TODO: generate errors
]
++ [ (10, fmap Some $ (Action <$> genErrors <*>) $
ReadCursor <$> (QC.getNonNegative <$> QC.arbitrary) <*> genCursorVar)
| let genErrors = pure Nothing -- TODO: generate errors
]
genActionsBlobRef :: [(Int, Gen (Any (LockstepAction (ModelState m h))))]
genActionsBlobRef =
[ (5, fmap Some $ (Action <$> genErrors <*>) $
RetrieveBlobs <$> genBlobRefsVar)
| not (null blobRefsVars)
, let genErrors = pure Nothing -- TODO: generate errors
]
fromRight ::
Var m h (Either Model.Err a)
-> Var m h a
fromRight = mapGVar (\op -> OpFromRight `OpComp` op)
genLookupKeys :: Gen (V.Vector k)
genLookupKeys = QC.arbitrary
genRange :: Gen (R.Range k)
genRange = QC.arbitrary
genUpdates :: Gen (V.Vector (k, R.Update v b))
genUpdates = QC.liftArbitrary ((,) <$> QC.arbitrary <*> QC.oneof [
R.Insert <$> QC.arbitrary <*> genBlob
, R.Upsert <$> QC.arbitrary
, pure R.Delete
])
where
_coveredAllCases :: R.Update v b -> ()
_coveredAllCases = \case
R.Insert{} -> ()
R.Upsert{} -> ()
R.Delete{} -> ()
genInserts :: Gen (V.Vector (k, v, Maybe b))
genInserts = QC.liftArbitrary ((,,) <$> QC.arbitrary <*> QC.arbitrary <*> genBlob)
genDeletes :: Gen (V.Vector k)
genDeletes = QC.arbitrary
genMupserts :: Gen (V.Vector (k, v))
genMupserts = QC.liftArbitrary ((,) <$> QC.arbitrary <*> QC.arbitrary)
genBlob :: Gen (Maybe b)
genBlob = QC.arbitrary
shrinkActionWithVars ::
forall m h a. (
Eq (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
, Typeable m
)
=> ModelVarContext (ModelState m h)
-> ModelState m h
-> LockstepAction (ModelState m h) a
-> [Any (LockstepAction (ModelState m h))]
shrinkActionWithVars _ctx _st (Action merrs action') =
[ -- TODO: it's somewhat unfortunate, but we have to dynamically
-- construct evidence that @a@ is typeable, which is a requirement
-- coming from the @Some@ existential. Could we find a different way
-- to solve this using just regular constraints?
case dictIsTypeable action' of
Dict -> Some $ Action merrs' action'
| merrs' <- QC.shrink merrs ]
++ [ Some $ Action merrs action''
| Some action'' <- shrinkAction'WithVars _ctx _st action'
]
-- | Dynamically construct evidence that the result type @a@ of an action is
-- typeable.
dictIsTypeable :: (Typeable m, Typeable h) => Action' m h a -> Dict (Typeable a)
dictIsTypeable = \case
NewTableWith{} -> Dict
CloseTable{} -> Dict
Lookups{} -> Dict
RangeLookup{} -> Dict
NewCursor{} -> Dict
CloseCursor{} -> Dict
ReadCursor{} -> Dict
Updates{} -> Dict
Inserts{} -> Dict
Deletes{} -> Dict
Upserts{} -> Dict
RetrieveBlobs{} -> Dict
SaveSnapshot{} -> Dict
OpenTableFromSnapshot{} -> Dict
DeleteSnapshot{} -> Dict
ListSnapshots{} -> Dict
Duplicate{} -> Dict
Union{} -> Dict
Unions{} -> Dict
RemainingUnionDebt{} -> Dict
SupplyUnionCredits{} -> Dict
SupplyPortionOfDebt{} -> Dict
shrinkAction'WithVars ::
forall m h a. (
Eq (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
, Typeable m
)
=> ModelVarContext (ModelState m h)
-> ModelState m h
-> Action' m h a
-> [Any (Action' m h)]
shrinkAction'WithVars _ctx _st a = case a of
NewTableWith p conf -> [
Some $ NewTableWith p conf'
| conf' <- QC.shrink conf
]
-- Shrink inserts and deletes towards updates.
Updates upds tableVar -> [
Some $ Updates upds' tableVar
| upds' <- QC.shrink upds
]
Inserts kvbs tableVar -> [
Some $ Inserts kvbs' tableVar
| kvbs' <- QC.shrink kvbs
] <> [
Some $ Updates (V.map f kvbs) tableVar
| let f (k, v, mb) = (k, R.Insert v mb)
]
Deletes ks tableVar -> [
Some $ Deletes ks' tableVar
| ks' <- QC.shrink ks
] <> [
Some $ Updates (V.map f ks) tableVar
| let f k = (k, R.Delete)
]
Upserts kvs tableVar -> [
Some $ Upserts kvs' tableVar
| kvs' <- QC.shrink kvs
] <> [
Some $ Updates (V.map f kvs) tableVar
| let f (k, v) = (k, R.Upsert v)
]
Lookups ks tableVar -> [
Some $ Lookups ks' tableVar
| ks' <- QC.shrink ks
]
-- * Unions
Unions tableVars -> [
Some $ Unions tableVars'
| tableVars' <- QC.liftShrink (const []) tableVars
]
SupplyUnionCredits tableVar (R.UnionCredits x) -> [
Some $ SupplyUnionCredits tableVar (R.UnionCredits x')
| x' <- QC.shrink x
]
-- Shrink portions to absolute union credits. The credits are all /positive/
-- powers of 2 that fit into a 64-bit Int. This choice is arbitrary, but the
-- model has no accurate debt information, so the best we can do is provide
-- a sensible distribution of union credits. This particular distribution is
-- skewed to smaller numbers, because the union debt is also likely to be on
-- the smaller side. Still, all larger powers of 2 are also included in case
-- the union debt is larger.
SupplyPortionOfDebt tableVar (Portion x) -> [
Some $ SupplyUnionCredits tableVar (R.UnionCredits x')
| x' <- [2 ^ i - 1 | (i :: Int) <- [0..20]]
, assert (x' >= 0) True
] ++ [
Some $ SupplyPortionOfDebt tableVar (Portion x')
| x' <- QC.shrink x
, x' > 0
]
_ -> []
{-------------------------------------------------------------------------------
Interpret 'Op' against 'ModelValue'
-------------------------------------------------------------------------------}
instance InterpretOp Op (ModelValue (ModelState m h)) where
intOp = \case
OpId -> Just
OpFst -> \case MPair x -> Just (fst x)
OpSnd -> \case MPair x -> Just (snd x)
OpLeft -> Just . MEither . Left
OpRight -> Just . MEither . Right
OpFromLeft -> \case MEither x -> either Just (const Nothing) x
OpFromRight -> \case MEither x -> either (const Nothing) Just x
OpComp g f -> intOp g <=< intOp f
OpLookupResults -> Just . MVector
. V.mapMaybe (\case MLookupResult x -> getBlobRef x)
. \case MVector x -> x
OpEntrys -> Just . MVector
. V.mapMaybe (\case MEntry x -> getBlobRef x)
. \case MVector x -> x
{-------------------------------------------------------------------------------
Statistics, labelling/tagging
-------------------------------------------------------------------------------}
data Stats = Stats {
-- === Tags
-- | Names for which snapshots exist
snapshotted :: !(Set R.SnapshotName)
-- === Final tags (per action sequence, across all tables)
-- | Number of successful lookups and their results
, numLookupsResults :: {-# UNPACK #-} !(Int, Int, Int)
-- (NotFound, Found, FoundWithBlob)
-- | Number of successful updates
, numUpdates :: {-# UNPACK #-} !(Int, Int, Int, Int)
-- (Insert, InsertWithBlob, Delete, Mupsert)
-- | Actions that succeeded
, successActions :: [String]
-- | Actions that failed with an error
, failActions :: [(String, Model.Err)]
-- === Final tags (per action sequence, per table)
-- | Number of actions per table (successful or failing)
, numActionsPerTable :: !(Map Model.TableID Int)
-- | The state of model tables at the point they were closed. This is used
-- to augment the tables from the final model state (which of course has
-- only tables still open in the final state).
, closedTables :: !(Map Model.TableID Model.SomeTable)
-- | The ultimate parents for each table. These are the 'TableId's of tables
-- created using 'new' or 'open'.
, parentTable :: !(Map Model.TableID [Model.TableID])
-- | Track the interleavings of operations via different but related tables.
-- This is a map from each ultimate parent table to a summary log of which
-- tables (derived from that parent table via duplicate or union) have had
-- \"interesting\" actions performed on them. We record only the
-- interleavings of different tables not multiple actions on the same table.
, dupTableActionLog :: !(Map Model.TableID [Model.TableID])
-- | The subset of tables (open or closed) that were created as a result
-- of a union operation. This can be used for example to select subsets of
-- the other per-table tracking maps above, or the state from the model.
-- The map value is the size of the union table at the point it was created,
-- so we can distinguish trivial empty unions from non-trivial.
, unionTables :: !(Map Model.TableID Int)
}
deriving stock Show
initStats :: Stats
initStats = Stats {
-- === Tags
snapshotted = Set.empty
-- === Final tags
, numLookupsResults = (0, 0, 0)
, numUpdates = (0, 0, 0, 0)
, successActions = []
, failActions = []
, numActionsPerTable = Map.empty
, closedTables = Map.empty
, parentTable = Map.empty
, dupTableActionLog = Map.empty
, unionTables = Map.empty
}
updateStats ::
forall m h a. ( Show (Class.TableConfig h)
, Eq (Class.TableConfig h)
, Arbitrary (Class.TableConfig h)
, Typeable h
, Typeable m
)
=> LockstepAction (ModelState m h) a
-> ModelLookUp (ModelState m h)
-> Model.Model
-> Model.Model
-> Val m h a
-> Stats
-> Stats
updateStats action@(Action _merrs action') lookUp modelBefore modelAfter result =
-- === Tags
updSnapshotted
-- === Final tags
. updNumLookupsResults
. updNumUpdates
. updSuccessActions
. updFailActions
. updNumActionsPerTable
. updClosedTables
. updDupTableActionLog
. updParentTable
. updUnionTables
where
-- === Tags
updSnapshotted stats = case (action', result) of
(SaveSnapshot _ name _ _, MEither (Right (MUnit ()))) -> stats {
snapshotted = Set.insert name (snapshotted stats)
}
(DeleteSnapshot name, MEither (Right (MUnit ()))) -> stats {
snapshotted = Set.delete name (snapshotted stats)
}
_ -> stats
-- === Final tags
updNumLookupsResults stats = case (action', result) of
(Lookups _ _, MEither (Right (MVector lrs))) -> stats {
numLookupsResults =
let count :: (Int, Int, Int)
-> Val m h (LookupResult v (WrapBlobRef h m blob))
-> (Int, Int, Int)
count (nf, f, fwb) (MLookupResult x) = case x of
NotFound -> (nf+1, f , fwb )
Found{} -> (nf , f+1, fwb )
FoundWithBlob{} -> (nf , f , fwb+1)
in V.foldl' count (numLookupsResults stats) lrs
}
_ -> stats
updNumUpdates stats = case (action', result) of
(Updates upds _, MEither (Right (MUnit ()))) -> stats {
numUpdates = countAll upds
}
(Inserts ins _, MEither (Right (MUnit ()))) -> stats {
numUpdates = countAll $ V.map (\(k, v, b) -> (k, R.Insert v b)) ins
}
(Deletes ks _, MEither (Right (MUnit ()))) -> stats {
numUpdates = countAll $ V.map (\k -> (k, R.Delete)) ks
}
(Upserts mups _, MEither (Right (MUnit ()))) -> stats {
numUpdates = countAll $ V.map (second R.Upsert) mups
}
_ -> stats
where
countAll :: forall k v b. V.Vector (k, R.Update v b) -> (Int, Int, Int, Int)
countAll upds =
let count :: (Int, Int, Int, Int)
-> (k, R.Update v blob)
-> (Int, Int, Int, Int)
count (i, iwb, d, m) (_, upd) = case upd of
R.Insert _ Nothing -> (i+1, iwb , d , m )
R.Insert _ Just{} -> (i , iwb+1, d , m )
R.Delete{} -> (i , iwb , d+1, m )
R.Upsert{} -> (i , iwb , d , m+1)
in V.foldl' count (numUpdates stats) upds
updSuccessActions stats = case result of
MEither (Right _) -> stats {
successActions = actionName action : successActions stats
}
_ -> stats
updFailActions stats = case result of
MEither (Left (MErr e)) -> stats {
failActions = (actionName action, e) : failActions stats
}
_ -> stats
updNumActionsPerTable :: Stats -> Stats
updNumActionsPerTable stats = case action' of
NewTableWith{}
| MEither (Right (MTable table)) <- result -> initCount table
| otherwise -> stats
OpenTableFromSnapshot{}
| MEither (Right (MTable table)) <- result -> initCount table
| otherwise -> stats
Duplicate{}
| MEither (Right (MTable table)) <- result -> initCount table
| otherwise -> stats
Union{}
| MEither (Right (MTable table)) <- result -> initCount table
| otherwise -> stats
Unions{}
| MEither (Right (MTable table)) <- result -> initCount table
| otherwise -> stats
-- Note that for the other actions we don't count success vs failure.
-- We don't need that level of detail. We just want to see the
-- distribution. Success / failure is detailed elsewhere.
Lookups _ tableVar -> updateCount tableVar
RangeLookup _ tableVar -> updateCount tableVar
NewCursor _ tableVar -> updateCount tableVar
Updates _ tableVar -> updateCount tableVar
Inserts _ tableVar -> updateCount tableVar
Deletes _ tableVar -> updateCount tableVar
Upserts _ tableVar -> updateCount tableVar
RemainingUnionDebt tableVar -> updateCount tableVar
SupplyUnionCredits tableVar _ -> updateCount tableVar
SupplyPortionOfDebt tableVar _ -> updateCount tableVar
-- Note that we don't remove tracking map entries for tables that get
-- closed. We want to know actions per table of all tables used, not
-- just those that were still open at the end of the sequence of
-- actions. We do also count CloseTable itself as an action.
CloseTable tableVar -> updateCount tableVar
-- The others are not counted as table actions. We list them here
-- explicitly so we don't miss any new ones we might add later.
CloseCursor{} -> stats
ReadCursor{} -> stats
RetrieveBlobs{} -> stats
SaveSnapshot{} -> stats
DeleteSnapshot{} -> stats
ListSnapshots{} -> stats
where
-- Init to 0 so we get an accurate count of tables with no actions.
initCount :: forall k v b. Model.Table k v b -> Stats
initCount table =
let tid = Model.tableID table
in stats {
numActionsPerTable = Map.insert tid 0 (numActionsPerTable stats)
}
-- Note that batches (of inserts lookups etc) count as one action.
updateCount :: forall k v b.
Var m h (WrapTable h m k v b)
-> Stats
updateCount tableVar =
let tid = getTableId (lookUp tableVar)
in stats {
numActionsPerTable = Map.insertWith (+) tid 1
(numActionsPerTable stats)
}
updClosedTables stats = case (action', result) of
(CloseTable tableVar, MEither (Right (MUnit ())))
| MTable t <- lookUp tableVar
, let tid = Model.tableID t
-- This lookup can fail if the table was already closed:
, Just (_, table) <- Map.lookup tid (Model.tables modelBefore)
-> stats {
closedTables = Map.insert tid table (closedTables stats)
}
_ -> stats
updParentTable stats = case (action', result) of
(NewTableWith{}, MEither (Right (MTable tbl))) ->
insertParentTableNew tbl stats
(OpenTableFromSnapshot{}, MEither (Right (MTable tbl))) ->
insertParentTableNew tbl stats
(Duplicate ptblVar, MEither (Right (MTable tbl))) ->
insertParentTableDerived [ptblVar] tbl stats
(Union ptblVar1 ptblVar2, MEither (Right (MTable tbl))) ->
insertParentTableDerived [ptblVar1, ptblVar2] tbl stats
(Unions ptblVars, MEither (Right (MTable tbl))) ->
insertParentTableDerived (NE.toList ptblVars) tbl stats
_ -> stats
-- insert an entry into the parentTable for a completely new table
insertParentTableNew :: forall k v b. Model.Table k v b -> Stats -> Stats
insertParentTableNew tbl stats =
stats {
parentTable = Map.insert (Model.tableID tbl)
[Model.tableID tbl]
(parentTable stats)
}
-- insert an entry into the parentTable for a table derived from a parent
insertParentTableDerived :: forall k v b.
[GVar Op (WrapTable h m k v b)]
-> Model.Table k v b -> Stats -> Stats
insertParentTableDerived ptblVars tbl stats =
let uptblIds :: [Model.TableID] -- the set of ultimate parent table ids
uptblIds = List.nub [
uptblId
| ptblVar <- ptblVars
-- immediate and ultimate parent table id:
, let iptblId = getTableId (lookUp ptblVar)
, uptblId <- parentTable stats Map.! iptblId
]
in stats {
parentTable = Map.insert (Model.tableID tbl)
uptblIds
(parentTable stats)
}
updDupTableActionLog stats | MEither (Right _) <- result =
case action' of
Lookups ks tableVar
| not (null ks) -> updateLastActionLog tableVar
| otherwise -> stats
RangeLookup r tableVar
| not (emptyRange r) -> updateLastActionLog tableVar
| otherwise -> stats
NewCursor _ tableVar -> updateLastActionLog tableVar
Updates upds tableVar
| not (null upds) -> updateLastActionLog tableVar
| otherwise -> stats
Inserts ins tableVar
| not (null ins) -> updateLastActionLog tableVar
| otherwise -> stats
Deletes ks tableVar
| not (null ks) -> updateLastActionLog tableVar
| otherwise -> stats
Upserts mups tableVar
| not (null mups) -> updateLastActionLog tableVar
| otherwise -> stats
CloseTable tableVar -> updateLastActionLog tableVar
-- Uninteresting actions
NewTableWith{} -> stats
CloseCursor{} -> stats
ReadCursor{} -> stats
RetrieveBlobs{} -> stats
SaveSnapshot{} -> stats
OpenTableFromSnapshot{} -> stats
DeleteSnapshot{} -> stats
ListSnapshots{} -> stats
Duplicate{} -> stats
Union{} -> stats
Unions{} -> stats
RemainingUnionDebt{} -> stats
SupplyUnionCredits{} -> stats
SupplyPortionOfDebt{} -> stats
where
-- add the current table to the front of the list of tables, if it's
-- not the latest one already
updateLastActionLog :: GVar Op (WrapTable h m k v b) -> Stats
updateLastActionLog tableVar =
stats {
dupTableActionLog = List.foldl'
(flip (Map.alter extendLog))
(dupTableActionLog stats)
(parentTable stats Map.! thid)
}
where
thid = getTableId (lookUp tableVar)
extendLog :: Maybe [Model.TableID] -> Maybe [Model.TableID]
extendLog (Just alog@(thid' : _)) | thid == thid'
= Just alog -- action via same table
extendLog (Just alog) = Just (thid : alog) -- action via different table
extendLog Nothing = Just (thid : []) -- first action on table
emptyRange (R.FromToExcluding l u) = l >= u
emptyRange (R.FromToIncluding l u) = l > u
updDupTableActionLog stats = stats
updUnionTables stats = case action' of
Union{} -> insertUnionTable
Unions{} -> insertUnionTable
_ -> stats
where
insertUnionTable
| MEither (Right (MTable t)) <- result
, let tid = Model.tableID t
, Just (_,tbl) <- Map.lookup tid (Model.tables modelAfter)
, let sz = Model.withSomeTable Model.size tbl
= stats {
unionTables = Map.insert tid sz (unionTables stats)
}
| otherwise
= stats
getTableId :: ModelValue (ModelState m h) (WrapTable h m k v b)
-> Model.TableID
getTableId (MTable t) = Model.tableID t
-- | Tags for every step
data Tag =
-- | Snapshot with a name that already exists
SnapshotTwice
-- | Open an existing snapshot
| OpenExistingSnapshot
-- | Open a missing snapshot
| OpenMissingSnapshot
-- | Delete an existing snapshot
| DeleteExistingSnapshot
-- | Delete a missing snapshot
| DeleteMissingSnapshot
-- | A corrupted snapshot was created successfully
| SaveSnapshotCorrupted R.SnapshotName
-- | An /un/corrupted snapshot was created successfully
| SaveSnapshotUncorrupted R.SnapshotName
-- | A snapshot failed to open because we detected that the snapshot was
-- corrupt
| OpenTableFromSnapshotDetectsCorruption R.SnapshotName
-- | Opened a snapshot (successfully) for a table involving a union
| OpenTableFromSnapshotUnion
deriving stock (Show, Eq, Ord)
-- | This is run for after every action
tagStep' ::
(ModelState m h, ModelState m h)
-> LockstepAction (ModelState m h) a
-> Val m h a
-> [Tag]
tagStep' (ModelState _stateBefore statsBefore,
ModelState _stateAfter _statsAfter)
(Action _ action') result =
catMaybes [
tagSnapshotTwice
, tagOpenExistingSnapshot
, tagOpenExistingSnapshot
, tagOpenMissingSnapshot
, tagDeleteExistingSnapshot
, tagDeleteMissingSnapshot
, tagSaveSnapshotCorruptedOrUncorrupted
, tagOpenTableFromSnapshotDetectsCorruption
, tagOpenTableFromSnapshotUnion
]
where
tagSnapshotTwice
| SaveSnapshot _ name _ _ <- action'
, name `Set.member` snapshotted statsBefore
= Just SnapshotTwice
| otherwise
= Nothing
tagOpenExistingSnapshot
| OpenTableFromSnapshot _ name _ <- action'
, name `Set.member` snapshotted statsBefore
= Just OpenExistingSnapshot
| otherwise
= Nothing
tagOpenMissingSnapshot
| OpenTableFromSnapshot _ name _ <- action'
, not (name `Set.member` snapshotted statsBefore)
= Just OpenMissingSnapshot
| otherwise
= Nothing
tagDeleteExistingSnapshot
| DeleteSnapshot name <- action'
, name `Set.member` snapshotted statsBefore
= Just DeleteExistingSnapshot
| otherwise
= Nothing
tagDeleteMissingSnapshot
| DeleteSnapshot name <- action'
, not (name `Set.member` snapshotted statsBefore)
= Just DeleteMissingSnapshot
| otherwise
= Nothing
tagSaveSnapshotCorruptedOrUncorrupted
| SaveSnapshot mcorr name _ _ <- action'
, MEither (Right (MUnit ())) <- result
= Just $ case mcorr of
Just (_ :: SilentCorruption) -> SaveSnapshotCorrupted name
_ -> SaveSnapshotUncorrupted name
| otherwise
= Nothing
tagOpenTableFromSnapshotDetectsCorruption
| OpenTableFromSnapshot _ name _ <- action'
, MEither (Left (MErr (Model.ErrSnapshotCorrupted _))) <- result
= Just (OpenTableFromSnapshotDetectsCorruption name)
| otherwise
= Nothing
tagOpenTableFromSnapshotUnion
| OpenTableFromSnapshot{} <- action'
, MEither (Right (MTable t)) <- result
, Model.isUnionDescendant t == Model.IsUnionDescendant
= Just OpenTableFromSnapshotUnion
| otherwise
= Nothing
-- | Tags for the final state
data FinalTag =
-- | Total number of lookup results that were 'SUT.NotFound'
NumLookupsNotFound String
-- | Total number of lookup results that were 'SUT.Found'
| NumLookupsFound String
-- | Total number of lookup results that were 'SUT.FoundWithBlob'
| NumLookupsFoundWithBlob String
-- | Number of 'Class.Insert's successfully submitted to a table
-- (this includes submissions through both 'Class.updates' and
-- 'Class.inserts')
| NumInserts String
-- | Number of 'Class.InsertWithBlob's successfully submitted to a table
-- (this includes submissions through both 'Class.updates' and
-- 'Class.inserts')
| NumInsertsWithBlobs String
-- | Number of 'Class.Delete's successfully submitted to a table
-- (this includes submissions through both 'Class.updates' and
-- 'Class.deletes')
| NumDeletes String
-- | Number of 'Class.Mupsert's successfully submitted to a table
-- (this includes submissions through both 'Class.updates' and
-- 'Class.upserts')
| NumMupserts String
-- | Total number of actions (failing, succeeding, either)
| NumActions String
-- | Which actions succeeded
| ActionSuccess String
-- | Which actions failed
| ActionFail String Model.Err
-- | Number of tables created (new, open or duplicate)
| NumTables String
-- | Number of actions on each table
| NumTableActions String
-- | Total /logical/ size of a table
| TableSize String
-- | Number of interleaved actions on duplicate tables
| DupTableActionLog String
deriving stock Show
-- | This is run only after completing every action
tagFinalState' :: Lockstep (ModelState m h) -> [(String, [FinalTag])]
tagFinalState' (getModel -> ModelState finalState finalStats) = concat [
tagNumLookupsResults
, tagNumUpdates
, tagNumActions
, tagSuccessActions
, tagFailActions
, tagNumTables
, tagNumTableActions
, tagTableSizes
, tagDupTableActionLog
, tagNumUnionTables
, tagNumUnionTableActions
]
where
tagNumLookupsResults = [
("Lookups not found" , [NumLookupsNotFound $ showPowersOf 10 nf])
, ("Lookups found" , [NumLookupsFound $ showPowersOf 10 f])
, ("Lookups found with blob", [NumLookupsFoundWithBlob $ showPowersOf 10 fwb])
]
where (nf, f, fwb) = numLookupsResults finalStats
tagNumUpdates = [
("Inserts" , [NumInserts $ showPowersOf 10 i])
, ("Inserts with blobs" , [NumInsertsWithBlobs $ showPowersOf 10 iwb])
, ("Deletes" , [NumDeletes $ showPowersOf 10 d])
, ("Upserts" , [NumMupserts $ showPowersOf 10 m])
]
where (i, iwb, d, m) = numUpdates finalStats
tagNumActions =
[ let n = length (successActions finalStats) in
("Actions that succeeded total", [NumActions (showPowersOf 10 n)])
, let n = length (failActions finalStats) in
("Actions that failed total", [NumActions (showPowersOf 10 n)])
, let n = length (successActions finalStats)
+ length (failActions finalStats) in
("Actions total", [NumActions (showPowersOf 10 n)])
]
tagSuccessActions =
[ ("Actions that succeeded", [ActionSuccess c])
| c <- successActions finalStats ]
tagFailActions =
[ ("Actions that failed", [ActionFail c e])
| (c, e) <- failActions finalStats ]
tagNumTables =
[ ("Number of tables", [NumTables (showPowersOf 2 n)])
| let n = Map.size (numActionsPerTable finalStats)
]
tagNumTableActions =
[ ("Number of actions per table", [ NumTableActions (showPowersOf 2 n) ])
| n <- Map.elems (numActionsPerTable finalStats)
]
tagTableSizes =
[ ("Table sizes", [ TableSize (showPowersOf 2 size) ])
| let openSizes, closedSizes :: Map Model.TableID Int
openSizes = Model.withSomeTable Model.size . snd <$>
Model.tables finalState
closedSizes = Model.withSomeTable Model.size <$>
closedTables finalStats
, size <- Map.elems (openSizes `Map.union` closedSizes)
]
tagDupTableActionLog =
[ ("Interleaved actions on table duplicates or unions",
[DupTableActionLog (showPowersOf 2 n)])
| (_, alog) <- Map.toList (dupTableActionLog finalStats)
, let n = length alog
]
tagNumUnionTables =
[ ("Number of union tables (empty)",
[NumTables (showPowersOf 2 (Map.size trivial))])
, ("Number of union tables (non-empty)",
[NumTables (showPowersOf 2 (Map.size nonTrivial))])
]
where
(nonTrivial, trivial) = Map.partition (> 0) (unionTables finalStats)
tagNumUnionTableActions =
[ ("Number of actions per table with non-empty unions",
[ NumTableActions (showPowersOf 2 n) ])
| n <- Map.elems $ numActionsPerTable finalStats
`Map.intersection`
Map.filter (> 0) (unionTables finalStats)
]
{-------------------------------------------------------------------------------
Utils
-------------------------------------------------------------------------------}
-- | Version of 'QLS.runActionsBracket' with tagging of the final state.
--
-- The 'tagStep' feature tags each step (i.e., 'Action'), but there are cases
-- where one wants to tag a /list of/ 'Action's. For example, if one wants to
-- count how often something happens over the course of running these actions,
-- then we would want to only tag the final state, not intermediate steps.
runActionsBracket ::
forall state st m n e prop. (
RunLockstep state m
, e ~ Error (Lockstep state) m
, forall a. IsPerformResult e a
, QC.Testable prop
, MonadMask n
, MonadST n
, QLS.IOProperty n
)
=> Proxy state
-> CheckCleanup
-> n st
-> (st -> n prop)
-> (m QC.Property -> st -> n QC.Property)
-> (Lockstep state -> [(String, [FinalTag])])
-> Actions (Lockstep state) -> QC.Property
runActionsBracket p cleanupFlag init cleanup runner tagger actions =
tagFinalState actions tagger
$ QLS.runActionsBracket p init cleanup' runner actions
where
cleanup' st = propCleanup cleanupFlag $ cleanup st
tagFinalState ::
forall state. StateModel (Lockstep state)
=> Actions (Lockstep state)
-> (Lockstep state -> [(String, [FinalTag])])
-> Property
-> Property
tagFinalState actions tagger =
flip (foldr (\(key, values) -> QC.tabulate key (fmap show values))) finalTags
where
finalAnnState :: Annotated (Lockstep state)
finalAnnState = stateAfter @(Lockstep state) actions
finalTags = tagger $ underlyingState finalAnnState
propException :: (Exception e, QC.Testable prop) => String -> Either e prop -> Property
propException s (Left e) = QC.counterexample (s <> displayException e) False
propException _ (Right prop) = QC.property prop
{-------------------------------------------------------------------------------
Cleanup exceptions
-------------------------------------------------------------------------------}
-- | Flag that turns on\/off cleanup checks.
--
-- If injected errors left the database in an inconsistent state, then property
-- cleanup might throw exceptions. If 'CheckCleanup' is used, this will lead to
-- failing properties, otherwise the exceptions are ignored.
data CheckCleanup = CheckCleanup | NoCheckCleanup
propCleanup :: (MonadCatch m, QC.Testable prop) => CheckCleanup -> m prop -> m Property
propCleanup flag cleanupAction =
propException "Cleanup exception: " <$> checkCleanupM flag cleanupAction
checkCleanupM :: (MonadCatch m, QC.Testable prop) => CheckCleanup -> m prop -> m (Either SomeException Property)
checkCleanupM flag cleanupAction = do
eith <- try @_ @SomeException cleanupAction
case flag of
CheckCleanup -> pure $ QC.property <$> eith
NoCheckCleanup -> pure (Right $ QC.property ())
{-------------------------------------------------------------------------------
Reference checks
-------------------------------------------------------------------------------}
-- | Flag that turns on\/off reference checks.
--
-- If injected errors left the database in an inconsistent state, then some
-- references might be forgotten, which leads to reference exceptions. If
-- 'CheckRefs' is used, this will lead to failing properties, otherwise the
-- exceptions are ignored.
data CheckRefs = CheckRefs | NoCheckRefs
toggleForgottenRefChecksSession :: R.IOLike m => CheckRefs -> R.Session m -> m ()
toggleForgottenRefChecksSession flag (R.Types.Session session) =
R.Unsafe.withKeepSessionOpen session $ \seshEnv ->
case flag of
CheckRefs -> enableForgottenRefChecks (R.Unsafe.sessionRefCtx seshEnv)
NoCheckRefs -> disableForgottenRefChecks (R.Unsafe.sessionRefCtx seshEnv)