Skip to content

Commit 037d203

Browse files
jorisdraljorisdral
committed
QLS: add prop_noSwallowedExceptions
This property runs a sequence of state machine actions where the last action definitely injects errors, at which point we can check if no errors are swallowed. See the documentation of `prop_noSwallowedExceptions` for more information. The property is currently expected to fail.
1 parent e539628 commit 037d203

File tree

2 files changed

+215
-2
lines changed

2 files changed

+215
-2
lines changed

‎lsm-tree.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -447,6 +447,7 @@ test-suite lsm-tree-test
447447
, quickcheck-instances
448448
, quickcheck-lockstep
449449
, random
450+
, safe-wild-cards
450451
, semialign
451452
, split
452453
, stm

‎test/Test/Database/LSMTree/StateMachine/DL.hs‎

Lines changed: 214 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,43 @@
1+
{-# LANGUAGE TemplateHaskell #-}
2+
13
{-# OPTIONS_GHC -Wno-unused-do-bind #-}
24
{-# OPTIONS_GHC -Wno-orphans #-}
35

46
module Test.Database.LSMTree.StateMachine.DL (
57
tests
68
) where
79

10+
import Control.Monad (void)
11+
import Control.RefCount
812
import Control.Tracer
913
import qualified Data.Map.Strict as Map
1014
import qualified Data.Vector as V
1115
import Database.LSMTree as R
1216
import qualified Database.LSMTree.Model.Session as Model (fromSomeTable, tables)
1317
import qualified Database.LSMTree.Model.Table as Model (values)
1418
import Prelude
19+
import SafeWildCards
20+
import System.FS.API.Types
21+
import System.FS.Sim.Error hiding (Blob)
22+
import qualified System.FS.Sim.Stream as Stream
23+
import System.FS.Sim.Stream (Stream)
1524
import Test.Database.LSMTree.StateMachine hiding (tests)
1625
import Test.Database.LSMTree.StateMachine.Op
17-
import Test.QuickCheck as QC
26+
import Test.QuickCheck as QC hiding (label)
1827
import Test.QuickCheck.DynamicLogic
1928
import qualified Test.QuickCheck.Gen as QC
2029
import qualified Test.QuickCheck.Random as QC
2130
import Test.QuickCheck.StateModel.Lockstep
22-
import Test.Tasty (TestTree, testGroup)
31+
import qualified Test.QuickCheck.StateModel.Lockstep.Defaults as QLS
32+
import Test.QuickCheck.StateModel.Variables
33+
import Test.Tasty (TestTree, testGroup, withResource)
2334
import qualified Test.Tasty.QuickCheck as QC
2435
import Test.Util.PrettyProxy
2536

2637
tests :: TestTree
2738
tests = testGroup "Test.Database.LSMTree.StateMachine.DL" [
2839
QC.testProperty "prop_example" prop_example
40+
, test_noSwallowedExceptions
2941
]
3042

3143
instance DynLogicModel (Lockstep (ModelState R.Table))
@@ -80,3 +92,203 @@ dl_example = do
8092
| Just tbl <- (Model.fromSomeTable @Key @Value @Blob smTbl)
8193
-> Map.size (Model.values tbl) == Map.size kvs
8294
_ -> False
95+
96+
{-------------------------------------------------------------------------------
97+
Swallowed exceptions
98+
-------------------------------------------------------------------------------}
99+
100+
-- | See 'prop_noSwallowedExceptions'.
101+
--
102+
-- Forgotten reference checks are disabled completely, because we allow bugs
103+
-- (like forgotten references) in exception unsafe code where we inject disk
104+
-- faults.
105+
test_noSwallowedExceptions :: TestTree
106+
test_noSwallowedExceptions =
107+
withResource
108+
(checkForgottenRefs >> disableForgottenRefChecks)
109+
(\_ -> enableForgottenRefChecks) $ \ !_ ->
110+
QC.testProperty "prop_noSwallowedExceptions" prop_noSwallowedExceptions
111+
112+
-- | Test that the @lsm-tree@ library does not swallow exceptions.
113+
--
114+
-- A functional requirement for the @lsm-tree@ library is that all exceptions
115+
-- are properly communicated to the user. An alternative way of stating this
116+
-- requirement is that no exceptions should be /swallowed/ by the library. We
117+
-- test this requirement by running the state machine test with injected disk
118+
-- errors using @fs-sim@, and asserting that no exceptions are swallowed.
119+
--
120+
-- The state machine test compares the SUT against a model by checking that
121+
-- their responses to @lsm-tree@ actions are the same. As of writing this
122+
-- property, not all of these actions on the SUT are guaranteed to be fully
123+
-- exception safe. As a result, an exception might leave the database (i.e.,
124+
-- session, tables, cursors) in an inconsistent state. The results of subsequent
125+
-- operations on the inconsistent database should be considered undefined. As
126+
-- such, it is highly likely that the SUT and model will thereafter disagree,
127+
-- leading to a failing property.
128+
--
129+
-- Still, we want to run the swallowed error assertion on /all/ operations,
130+
-- regardless of whether they are exception safe. We overcome this problem by
131+
-- /definitely/ injecting errors (and running a swallowed error assertion) for
132+
-- the last action in a sequence of actions. This may leave the final database
133+
-- state inconsistent, but that is okay. However, we'll also have to disable
134+
-- sanity checks like 'NoCheckCleanup', 'NoCheckFS', and 'NoCheckRefs', because
135+
-- they are likely to fail if the database is an inconsistent state.
136+
--
137+
-- TODO: running only one swallowed exception assertion per action sequence is
138+
-- restrictive, but this automatically improves as we make more actions
139+
-- exceptions safe. When we generate injected errors for these errors by default
140+
-- (in @arbitraryWithVars@), the swallowed exception assertion automatically
141+
-- runs for those actions as well.
142+
prop_noSwallowedExceptions :: Property
143+
prop_noSwallowedExceptions = forAllDL dl_noSwallowExceptions runner
144+
where
145+
-- disable all file system and reference checks
146+
runner = propLockstep_RealImpl_MockFS_IO tr NoCheckCleanup NoCheckFS NoCheckRefs
147+
tr = nullTracer
148+
149+
-- | Run any number of actions using the default actions generator, and finally
150+
-- run a single action with errors *definitely* enabled.
151+
dl_noSwallowExceptions :: DL (Lockstep (ModelState R.Table)) ()
152+
dl_noSwallowExceptions = do
153+
-- Run any number of actions as normal
154+
anyActions_
155+
156+
-- Generate a single action as normal
157+
varCtx <- getVarContextDL
158+
st <- getModelStateDL
159+
let
160+
gen = QLS.arbitraryAction varCtx st
161+
predicate (Some a) = QLS.precondition st a
162+
shr (Some a) = QLS.shrinkAction varCtx st a
163+
Some a <- forAllQ $ withGenQ gen predicate shr
164+
165+
-- Overwrite the maybe errors of the generated action with *definitely* just
166+
-- errors.
167+
case a of
168+
Action _merrs a' -> do
169+
HasNoVariables errs <-
170+
forAllQ $ hasNoVariablesQ $ withGenQ arbitraryErrors (\_ -> True) shrinkErrors
171+
-- Run the modified action
172+
void $ action $ Action (Just errs) a'
173+
174+
-- | Generate an 'Errors' with arbitrary probabilities of exceptions.
175+
--
176+
-- The default 'genErrors' from @fs-sim@ generates streams of 'Maybe' exceptions
177+
-- with a fixed probability for a 'Just' or 'Nothing'. The version here
178+
-- generates an arbitrary probability for each stream, which should generate a
179+
-- larger variety of 'Errors' structures.
180+
--
181+
-- TODO: upstream to @fs-sim@ to replase the default 'genErrors'?
182+
arbitraryErrors :: Gen Errors
183+
arbitraryErrors = do
184+
dumpStateE <- genStream arbitrary
185+
hCloseE <- genStream arbitrary
186+
hTruncateE <- genStream arbitrary
187+
doesDirectoryExistE <- genStream arbitrary
188+
doesFileExistE <- genStream arbitrary
189+
hOpenE <- genStream arbitrary
190+
hSeekE <- genStream arbitrary
191+
hGetSomeE <- genErrorStreamGetSome
192+
hGetSomeAtE <- genErrorStreamGetSome
193+
hPutSomeE <- genErrorStreamPutSome
194+
hGetSizeE <- genStream arbitrary
195+
createDirectoryE <- genStream arbitrary
196+
createDirectoryIfMissingE <- genStream arbitrary
197+
listDirectoryE <- genStream arbitrary
198+
removeDirectoryRecursiveE <- genStream arbitrary
199+
removeFileE <- genStream arbitrary
200+
renameFileE <- genStream arbitrary
201+
hGetBufSomeE <- genErrorStreamGetSome
202+
hGetBufSomeAtE <- genErrorStreamGetSome
203+
hPutBufSomeE <- genErrorStreamPutSome
204+
hPutBufSomeAtE <- genErrorStreamPutSome
205+
return $ filterErrors Errors {..}
206+
where
207+
-- Generate a stream using 'genLikelihoods' for its 'Maybe' elements.
208+
genStream :: forall a. Gen a -> Gen (Stream a)
209+
genStream genA = do
210+
(pNothing, pJust) <- genLikelihoods
211+
Stream.genInfinite $ Stream.genMaybe pNothing pJust genA
212+
213+
-- Generate two integer likelihoods for 'Nothing' and 'Just' constructors.
214+
genLikelihoods :: Gen (Int, Int)
215+
genLikelihoods = do
216+
NonNegative pNothing <- arbitrary
217+
NonNegative pJust <- arbitrary
218+
if pNothing == 0 then
219+
pure (0, 1)
220+
else if pJust == 0 then
221+
pure (1, 0)
222+
else
223+
pure (pNothing, pJust)
224+
225+
genErrorStreamGetSome :: Gen ErrorStreamGetSome
226+
genErrorStreamGetSome = genStream $ liftArbitrary2 arbitrary arbitrary
227+
228+
genErrorStreamPutSome :: Gen ErrorStreamPutSome
229+
genErrorStreamPutSome = genStream $ flip liftArbitrary2 arbitrary $ do
230+
errorType <- arbitrary
231+
maybePutCorruption <- liftArbitrary genPutCorruption
232+
pure (errorType, maybePutCorruption)
233+
234+
genPutCorruption :: Gen PutCorruption
235+
genPutCorruption = oneof [
236+
PartialWrite <$> arbitrary
237+
, SubstituteWithJunk <$> arbitrary
238+
]
239+
where
240+
_coveredAllCases x = case x of
241+
PartialWrite{} -> pure ()
242+
SubstituteWithJunk{} -> pure ()
243+
244+
-- TODO: there is one case where an 'FsReachEOF' error is swallowed. Is that
245+
-- valid behaviour, or should we change it?
246+
filterErrors errs = errs {
247+
hGetBufSomeE = Stream.filter (not . isFsReachedEOF) (hGetBufSomeE errs)
248+
}
249+
250+
isFsReachedEOF Nothing = False
251+
isFsReachedEOF (Just (Left e)) = case e of
252+
FsReachedEOF -> True
253+
_ -> False
254+
isFsReachedEOF (Just (Right _)) = False
255+
256+
-- | Shrink each error stream and all error stream elements.
257+
--
258+
-- The default 'shrink' from @fs-sim@ shrinks only the stream structure, but not
259+
-- the elements contained in those streams.
260+
--
261+
-- TODO: upstream to @fs-sim@ to replace the default 'shrink'?
262+
shrinkErrors :: Errors -> [Errors]
263+
shrinkErrors err@($(fields 'Errors))
264+
| allNull err = []
265+
| otherwise = emptyErrors : concatMap (filter (not . allNull))
266+
[ (\s' -> err { dumpStateE = s' }) <$> Stream.liftShrinkStream shrink dumpStateE
267+
, (\s' -> err { hOpenE = s' }) <$> Stream.liftShrinkStream shrink hOpenE
268+
, (\s' -> err { hCloseE = s' }) <$> Stream.liftShrinkStream shrink hCloseE
269+
, (\s' -> err { hSeekE = s' }) <$> Stream.liftShrinkStream shrink hSeekE
270+
, (\s' -> err { hGetSomeE = s' }) <$> Stream.liftShrinkStream shrink hGetSomeE
271+
, (\s' -> err { hGetSomeAtE = s' }) <$> Stream.liftShrinkStream shrink hGetSomeAtE
272+
, (\s' -> err { hPutSomeE = s' }) <$> Stream.liftShrinkStream shrink hPutSomeE
273+
, (\s' -> err { hTruncateE = s' }) <$> Stream.liftShrinkStream shrink hTruncateE
274+
, (\s' -> err { hGetSizeE = s' }) <$> Stream.liftShrinkStream shrink hGetSizeE
275+
, (\s' -> err { createDirectoryE = s' }) <$> Stream.liftShrinkStream shrink createDirectoryE
276+
, (\s' -> err { createDirectoryIfMissingE = s' }) <$> Stream.liftShrinkStream shrink createDirectoryIfMissingE
277+
, (\s' -> err { listDirectoryE = s' }) <$> Stream.liftShrinkStream shrink listDirectoryE
278+
, (\s' -> err { doesDirectoryExistE = s' }) <$> Stream.liftShrinkStream shrink doesDirectoryExistE
279+
, (\s' -> err { doesFileExistE = s' }) <$> Stream.liftShrinkStream shrink doesFileExistE
280+
, (\s' -> err { removeDirectoryRecursiveE = s' }) <$> Stream.liftShrinkStream shrink removeDirectoryRecursiveE
281+
, (\s' -> err { removeFileE = s' }) <$> Stream.liftShrinkStream shrink removeFileE
282+
, (\s' -> err { renameFileE = s' }) <$> Stream.liftShrinkStream shrink renameFileE
283+
, (\s' -> err { hGetBufSomeE = s' }) <$> Stream.liftShrinkStream shrink hGetBufSomeE
284+
, (\s' -> err { hGetBufSomeAtE = s' }) <$> Stream.liftShrinkStream shrink hGetBufSomeAtE
285+
, (\s' -> err { hPutBufSomeE = s' }) <$> Stream.liftShrinkStream shrink hPutBufSomeE
286+
, (\s' -> err { hPutBufSomeAtE = s' }) <$> Stream.liftShrinkStream shrink hPutBufSomeAtE
287+
]
288+
289+
deriving stock instance Enum FsErrorType
290+
deriving stock instance Bounded FsErrorType
291+
292+
instance Arbitrary FsErrorType where
293+
arbitrary = arbitraryBoundedEnum
294+
shrink = shrinkBoundedEnum

0 commit comments

Comments
 (0)