From 70a1657762cbfe3e60ad7754391d81876ea11c70 Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Mon, 10 Mar 2025 19:07:46 +0100 Subject: [PATCH 01/12] QLS: misc improvements --- test/Test/Database/LSMTree/StateMachine.hs | 88 +++++++--------------- 1 file changed, 28 insertions(+), 60 deletions(-) diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index ef3d9149d..98af970ea 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -1,37 +1,15 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE EmptyDataDeriving #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE InstanceSigs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE MultiWayIf #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE StandaloneKindSignatures #-} -{-# LANGUAGE TypeApplications #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} #if MIN_VERSION_GLASGOW_HASKELL(9,8,1,0) -{-# LANGUAGE TypeAbstractions #-} +{-# LANGUAGE TypeAbstractions #-} #endif {-# OPTIONS_GHC -Wno-orphans #-} -{- HLINT ignore "Evaluate" -} -{- HLINT ignore "Use camelCase" -} -{- HLINT ignore "Redundant fmap" -} -{- HLINT ignore "Short-circuited list comprehension" -} -- TODO: remove once table union is implemented - {- TODO: improve generation and shrinking of dependencies. See https://github.com/IntersectMBO/lsm-tree/pull/4#discussion_r1334295154. @@ -1822,8 +1800,11 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = Map.member (Model.tableID t) (Model.tables st) ] - genUnionDescendantTableVars = QC.elements unionDescendantTableVars - genNotUnionDescendantTableVars = QC.elements notUnionDescendantTableVars + -- We already want to enable unions, but some operations on tables don't + -- support unions yet. Therefore, we want to only run them on tables that + -- don't descend from a union. + genUnionDescendantTableVar = QC.elements unionDescendantTableVars + genNotUnionDescendantTableVar = QC.elements notUnionDescendantTableVars unionDescendantTableVars, notUnionDescendantTableVars :: [Var h (WrapTable h IO k v b)] (unionDescendantTableVars, notUnionDescendantTableVars) = partitionEithers $ @@ -1970,8 +1951,14 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = -- implemented , isJust (eqT @h @ModelIO.Table) ] - ++ [ (2, fmap Some $ (Action <$> genErrors <*>) $ - Unions <$> gen2or3TableVars) + ++ [ (2, fmap Some $ (Action <$> genErrors <*>) $ do + -- Generate at least a 2-way union, and at most a 3-way union. + -- + -- Tests for 0-way and 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 -- TODO: this is currently only enabled for the reference @@ -1986,7 +1973,6 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = -- implementation. Enable this unconditionally once table union is -- implemented , isJust (eqT @h @ModelIO.Table) - ] ++ [ (8, fmap Some $ (Action <$> genErrors <*>) $ SupplyUnionCredits <$> genUnionTableVar <*> genUnionCredits) @@ -2005,35 +1991,17 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = , isJust (eqT @h @ModelIO.Table) ] where - -- Generate at least a 2-way union, and at most a 3-way union. + -- For querying the union debt or supplying union credits, the + -- interesting cases to test for are when tables are union tables. For + -- non-union tables, these operations should just be no-ops, so we + -- generate them only rarely. -- - -- Unit tests for 0-way and 1-way unions are included in the UnitTests - -- module. n-way unions for n>3 lead to larger unions, which are less likely - -- to be finished before the end of an action sequence. - gen2or3TableVars :: Gen (NonEmpty (Var h (WrapTable h IO k v b))) - gen2or3TableVars = do - tableVar1 <- genTableVar - tableVar2 <- genTableVar - mtableVar3 <- QC.oneof [pure Nothing, Just <$> genTableVar] - pure $ NE.fromList $ catMaybes [ - Just tableVar1, Just tableVar2, mtableVar3 - ] - -- TODO: tweak distribution once table unions are implemented - genUnionTableVar = QC.frequency $ - -- The interesting cases to test for are when tables are union - -- tables. - [ (9, genUnionDescendantTableVars) - | not (null unionDescendantTableVars) - ] - -- For non-union tables, querying the union debt or supplying union - -- credits are no-ops, so we generate such tables only rarely. - -- - -- TODO: replace union actions on non-union tables with a few unit - -- tests? - ++ [ (1, genNotUnionDescendantTableVars) - | not (null notUnionDescendantTableVars) - ] + -- TODO: replace union actions on non-union tables with unit tests? + genUnionTableVar = QC.frequency [ + (9 * length unionDescendantTableVars, genUnionDescendantTableVar) + , (1 * length notUnionDescendantTableVars, genNotUnionDescendantTableVar) + ] -- TODO: tweak distribution once table unions are implemented genUnionCredits = QC.frequency [ From 008852b52b30efdc10d11ace690ac45d8c65f3d1 Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Mon, 10 Mar 2025 19:10:16 +0100 Subject: [PATCH 02/12] QLS: enable unions, conditionally disable cursor and range query --- .../LSMTree/Internal/MergeSchedule.hs | 5 +--- test/Test/Database/LSMTree/StateMachine.hs | 26 ++++++++----------- 2 files changed, 12 insertions(+), 19 deletions(-) diff --git a/src/Database/LSMTree/Internal/MergeSchedule.hs b/src/Database/LSMTree/Internal/MergeSchedule.hs index b69f03cd2..e37957866 100644 --- a/src/Database/LSMTree/Internal/MergeSchedule.hs +++ b/src/Database/LSMTree/Internal/MergeSchedule.hs @@ -358,10 +358,7 @@ iforLevelM_ lvls k = V.iforM_ lvls $ \i lvl -> k (LevelNo (i + 1)) lvl -- of multiple runs, but a nested tree of merges. -- -- TODO: So far, this is --- * never created --- * not stored in snapshots --- * not loaded from snapshots --- * ignored in lookups +-- * not considered when creating cursors (also used for range lookups) -- * never made merge progress on (by supplying credits to it) -- * never merged into the regular levels data UnionLevel m h = diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index 98af970ea..2cf1b7602 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -1755,7 +1755,7 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = concat [ genActionsSession , genActionsTables - , genUnionActions + , genActionsUnion , genActionsCursor , genActionsBlobRef ] @@ -1896,8 +1896,10 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = | let genErrors = pure Nothing -- TODO: generate errors ] ++ [ (5, fmap Some $ (Action <$> genErrors <*>) $ - RangeLookup <$> genRange <*> genTableVar) + RangeLookup <$> genRange <*> genNotUnionDescendantTableVar) + -- TODO: enable range lookups on tables with unions | let genErrors = pure Nothing -- TODO: generate errors + , not (null notUnionDescendantTableVars) -- TODO: enable range lookups on tables with unions ] ++ [ (10, fmap Some $ (Action <$> genErrors <*>) $ Updates <$> genUpdates <*> genTableVar) @@ -1916,9 +1918,11 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = | let genErrors = pure Nothing -- TODO: generate errors ] ++ [ (3, fmap Some $ (Action <$> genErrors <*>) $ - NewCursor <$> QC.arbitrary <*> genTableVar) + NewCursor <$> QC.arbitrary <*> genNotUnionDescendantTableVar) + -- TODO: cursors for tables with unions | length cursorVars <= 5 -- no more than 5 cursors at once , let genErrors = pure Nothing -- TODO: generate errors + , not (null notUnionDescendantTableVars) -- TODO: cursors for tables with unions ] ++ [ (2, fmap Some $ (Action <$> genErrors <*>) $ CreateSnapshot <$> genCorruption <*> pure label <*> genUnusedSnapshotName <*> genTableVar) @@ -1938,33 +1942,25 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = ] -- | Generate table actions that have to do with unions. - genUnionActions :: [(Int, Gen (Any (LockstepAction (ModelState h))))] - genUnionActions + genActionsUnion :: [(Int, Gen (Any (LockstepAction (ModelState 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 - -- TODO: this is currently only enabled for the reference - -- implementation. Enable this unconditionally once table union is - -- implemented - , isJust (eqT @h @ModelIO.Table) ] ++ [ (2, fmap Some $ (Action <$> genErrors <*>) $ do -- Generate at least a 2-way union, and at most a 3-way union. -- - -- Tests for 0-way and 1-way unions are included in the UnitTests - -- module. n-way unions for n>3 lead to large unions, which are less + -- 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 - -- TODO: this is currently only enabled for the reference - -- implementation. Enable this unconditionally once table union is - -- implemented - , isJust (eqT @h @ModelIO.Table) ] ++ [ (2, fmap Some $ (Action <$> genErrors <*>) $ RemainingUnionDebt <$> genUnionTableVar) From cfca7fb32af3bda5ef12a5cdd4a821261e50d609 Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Tue, 11 Mar 2025 10:59:49 +0000 Subject: [PATCH 03/12] Extend the StateMachine Stats parentTable tracking to cover unions The parentTable in the Stats tracks the ultimate parent for each table. This is used along with the action log to measure coverage of operations on table duplicates. With unions, a table can now have multiple ultimate parents. A union table's ultimate parents are the ultimate parents of each of its input tables. Also deal with the consequences of multiple parent tables for the dupTableActionLog tracking: we extend the action log for _each_ ultimate parent table separately. --- test/Test/Database/LSMTree/StateMachine.hs | 70 ++++++++++++---------- 1 file changed, 38 insertions(+), 32 deletions(-) diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index 2cf1b7602..b47ee7941 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -68,6 +68,12 @@ import Data.Bifunctor (Bifunctor (..)) import Data.Constraint (Dict (..)) import Data.Either (partitionEithers) import Data.Kind (Type) +#if MIN_VERSION_base(4,20,0) +import Data.List (nub) +#else +import Data.List (foldl', nub) + -- foldl' is included in the Prelude from base 4.20 onwards +#endif import Data.List.NonEmpty (NonEmpty (..)) import qualified Data.List.NonEmpty as NE import Data.Map.Strict (Map) @@ -2249,10 +2255,10 @@ data Stats = Stats { , closedTableSizes :: !(Map Model.TableID Int) -- | The ultimate parent for each table. This is the 'TableId' of a table -- created using 'new' or 'open'. - , parentTable :: Map Model.TableID Model.TableID + , parentTable :: Map Model.TableID [Model.TableID] -- | Track the interleavings of operations via different but related tables. - -- This is a map from the ultimate parent table to a summary log of which - -- tables (derived from that parent table via duplicate) have had + -- 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] @@ -2449,15 +2455,11 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result (OpenSnapshot{}, MEither (Right (MTable tbl))) -> insertParentTableNew tbl stats (Duplicate ptblVar, MEither (Right (MTable tbl))) -> - insertParentTableDerived ptblVar tbl stats - (Union ptblVar _ptblVar2, MEither (Right (MTable tbl))) -> - insertParentTableDerived ptblVar tbl stats - (Unions (ptblVar :| _ptblVars), MEither (Right (MTable tbl))) -> - insertParentTableDerived ptblVar tbl stats - -- TODO: we're abitrarily picking the first parent as the parent (and - -- ignoring ptblVar2 and ptblVars above). Tables should be able to have - -- *multiple* ultimate parent tables, which is currently not possible: - --parentTable only stores a single ultimate parent table per table. + 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 @@ -2465,22 +2467,25 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result insertParentTableNew tbl stats = stats { parentTable = Map.insert (Model.tableID tbl) - (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 IO k v b) + [GVar Op (WrapTable h IO k v b)] -> Model.Table k v b -> Stats -> Stats - insertParentTableDerived ptblVar tbl stats = - let -- immediate and ultimate parent table ids - iptblId, uptblId :: Model.TableID - iptblId = getTableId (lookUp ptblVar) - uptblId = parentTable stats Map.! iptblId + insertParentTableDerived ptblVars tbl stats = + let uptblIds :: [Model.TableID] -- the set of ultimate parent table ids + uptblIds = 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) - uptblId + uptblIds (parentTable stats) } @@ -2526,18 +2531,19 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result -- not the latest one already updateLastActionLog :: GVar Op (WrapTable h IO k v b) -> Stats updateLastActionLog tableVar = - case Map.lookup pthid (dupTableActionLog stats) of - Just (thid' : _) - | thid == thid' -> stats -- the most recent action was via this table - malog -> - let alog = thid : fromMaybe [] malog - in stats { - dupTableActionLog = Map.insert pthid alog - (dupTableActionLog stats) - } + stats { + dupTableActionLog = foldl' (flip (Map.alter extendLog)) + (dupTableActionLog stats) + (parentTable stats Map.! thid) + } where - thid = getTableId (lookUp tableVar) - pthid = parentTable stats Map.! thid + 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 @@ -2755,7 +2761,7 @@ tagFinalState' (getModel -> ModelState finalState finalStats) = concat [ ] tagDupTableActionLog = - [ ("Interleaved actions on table duplicates", + [ ("Interleaved actions on table duplicates or unions", [DupTableActionLog (showPowersOf 2 n)]) | (_, alog) <- Map.toList (dupTableActionLog finalStats) , let n = length alog From b23fe4351042bed65574e643cca98601ae644355 Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Mon, 17 Mar 2025 11:42:01 +0000 Subject: [PATCH 04/12] Update test/Test/Database/LSMTree/StateMachine.hs Co-authored-by: Joris Dral --- test/Test/Database/LSMTree/StateMachine.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index b47ee7941..e6a2e90e4 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -2253,7 +2253,7 @@ data Stats = Stats { -- sizes from the final model state (which of course has only tables still -- open in the final state). , closedTableSizes :: !(Map Model.TableID Int) - -- | The ultimate parent for each table. This is the 'TableId' of a table + -- | 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. From 0ecab4e7a5233511af2d96d00726af4a13ffc57c Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Tue, 11 Mar 2025 14:16:04 +0000 Subject: [PATCH 05/12] Generalise the StateMachine Stats closed table tracking Track the whole closed table, not just the table size. This will let us reuse the same tracking for additional purposes. --- test/Test/Database/LSMTree/StateMachine.hs | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index e6a2e90e4..9c27cd15b 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -2249,10 +2249,10 @@ data Stats = Stats { -- === Final tags (per action sequence, per table) -- | Number of actions per table (succesful or failing) , numActionsPerTable :: !(Map Model.TableID Int) - -- | The size of tables that were closed. This is used to augment the table - -- sizes from the final model state (which of course has only tables still - -- open in the final state). - , closedTableSizes :: !(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] @@ -2275,7 +2275,7 @@ initStats = Stats { , successActions = [] , failActions = [] , numActionsPerTable = Map.empty - , closedTableSizes = Map.empty + , closedTables = Map.empty , parentTable = Map.empty , dupTableActionLog = Map.empty } @@ -2302,7 +2302,7 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result . updSuccessActions . updFailActions . updNumActionsPerTable - . updClosedTableSizes + . updClosedTables . updDupTableActionLog . updParentTable where @@ -2437,15 +2437,14 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result (numActionsPerTable stats) } - updClosedTableSizes stats = case (action', result) of + updClosedTables stats = case (action', result) of (Close 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) - , let tsize = Model.withSomeTable Model.size table -> stats { - closedTableSizes = Map.insert tid tsize (closedTableSizes stats) + closedTables = Map.insert tid table (closedTables stats) } _ -> stats @@ -2756,7 +2755,8 @@ tagFinalState' (getModel -> ModelState finalState finalStats) = concat [ | let openSizes, closedSizes :: Map Model.TableID Int openSizes = Model.withSomeTable Model.size . snd <$> Model.tables finalState - closedSizes = closedTableSizes finalStats + closedSizes = Model.withSomeTable Model.size <$> + closedTables finalStats , size <- Map.elems (openSizes `Map.union` closedSizes) ] From ac6e4d535ca2feb4452c9bdcaf08c0fa481f0b19 Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Wed, 12 Mar 2025 10:39:44 +0000 Subject: [PATCH 06/12] Label state machine results involving unions Label the number of tables with trivial and non-trivial unions. Label the number of actions on tables from non-trivial unions. --- test/Test/Database/LSMTree/StateMachine.hs | 47 ++++++++++++++++++++-- 1 file changed, 44 insertions(+), 3 deletions(-) diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index 9c27cd15b..44fca9328 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -2229,8 +2229,6 @@ instance InterpretOp Op (ModelValue (ModelState h)) where Statistics, labelling/tagging -------------------------------------------------------------------------------} --- TODO: add tagging of interesting cases for union-related actions. - data Stats = Stats { -- === Tags -- | Names for which snapshots exist @@ -2262,6 +2260,12 @@ data Stats = Stats { -- \"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 @@ -2278,6 +2282,7 @@ initStats = Stats { , closedTables = Map.empty , parentTable = Map.empty , dupTableActionLog = Map.empty + , unionTables = Map.empty } updateStats :: @@ -2293,7 +2298,7 @@ updateStats :: -> Val h a -> Stats -> Stats -updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result = +updateStats action@(Action _merrs action') lookUp modelBefore modelAfter result = -- === Tags updSnapshotted -- === Final tags @@ -2305,6 +2310,7 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result . updClosedTables . updDupTableActionLog . updParentTable + . updUnionTables where -- === Tags @@ -2549,6 +2555,22 @@ updateStats action@(Action _merrs action') lookUp modelBefore _modelAfter result 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 h) (WrapTable h IO k v b) -> Model.TableID getTableId (MTable t) = Model.tableID t @@ -2705,6 +2727,8 @@ tagFinalState' (getModel -> ModelState finalState finalStats) = concat [ , tagNumTableActions , tagTableSizes , tagDupTableActionLog + , tagNumUnionTables + , tagNumUnionTableActions ] where tagNumLookupsResults = [ @@ -2767,6 +2791,23 @@ tagFinalState' (getModel -> ModelState finalState finalStats) = concat [ , 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 -------------------------------------------------------------------------------} From 3a7d4e3aee119a1eca751841d72c3335918b8d00 Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Wed, 12 Mar 2025 10:41:01 +0000 Subject: [PATCH 07/12] Label state machine tests involving opening a snapshot of a union table --- test/Test/Database/LSMTree/StateMachine.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index 44fca9328..da3849758 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -2600,6 +2600,8 @@ data Tag = -- | A snapshot failed to open because we detected that the snapshot was -- corrupt | OpenSnapshotDetectsCorruption R.SnapshotName + -- | Opened a snapshot (successfully) for a table involving a union + | OpenSnapshotUnion deriving stock (Show, Eq, Ord) -- | This is run for after every action @@ -2620,6 +2622,7 @@ tagStep' (ModelState _stateBefore statsBefore, , tagDeleteMissingSnapshot , tagCreateSnapshotCorruptedOrUncorrupted , tagOpenSnapshotDetectsCorruption + , tagOpenSnapshotUnion ] where tagSnapshotTwice @@ -2673,6 +2676,14 @@ tagStep' (ModelState _stateBefore statsBefore, | otherwise = Nothing + tagOpenSnapshotUnion + | OpenSnapshot{} <- action' + , MEither (Right (MTable t)) <- result + , Model.isUnionDescendant t == Model.IsUnionDescendant + = Just OpenSnapshotUnion + | otherwise + = Nothing + -- | Tags for the final state data FinalTag = -- | Total number of lookup results that were 'SUT.NotFound' From c41a1b6006bc04dbd18d45ec70b5a3b77495b0c9 Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Fri, 14 Mar 2025 19:11:49 +0000 Subject: [PATCH 08/12] Enable existing unit test for unions of one input table Can be enabled now that unions are implemented. And of course, because the test was not being run, there was a previously undetected bug in the unit test. Now fixed. --- test/Test/Database/LSMTree/UnitTests.hs | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/test/Test/Database/LSMTree/UnitTests.hs b/test/Test/Database/LSMTree/UnitTests.hs index 8d4878df1..b4764979e 100644 --- a/test/Test/Database/LSMTree/UnitTests.hs +++ b/test/Test/Database/LSMTree/UnitTests.hs @@ -18,10 +18,10 @@ import Database.LSMTree as R import Control.Exception (Exception, bracket, try) import Database.LSMTree.Extras.Generators (KeyForIndexCompact) -import qualified Test.QuickCheck as QC +import qualified Test.QuickCheck.Arbitrary as QC +import qualified Test.QuickCheck.Gen as QC import Test.Tasty (TestTree, testGroup) import Test.Tasty.HUnit -import Test.Tasty.QuickCheck (Property, testProperty) import Test.Util.FS (withTempIOHasBlockIO) @@ -33,12 +33,7 @@ tests = , testCase "unit_closed_cursor" unit_closed_cursor , testCase "unit_twoTableTypes" unit_twoTableTypes , testCase "unit_snapshots" unit_snapshots - - -- Properties - - , testProperty "prop_unions_1" $ - -- TODO: enable once unions are implemented - QC.expectFailure prop_unions_1 + , testCase "unit_unions_1" unit_unions_1 ] unit_blobs :: (String -> IO ()) -> Assertion @@ -155,9 +150,8 @@ unit_snapshots = snap2 = "table2" -- | Unions of 1 table are equivalent to duplicate -prop_unions_1 :: Property -prop_unions_1 = - QC.once $ QC.ioProperty $ +unit_unions_1 :: Assertion +unit_unions_1 = withTempIOHasBlockIO "test" $ \hfs hbio -> withSession nullTracer hfs hbio (FS.mkFsPath []) $ \sess -> withTable @_ @Key1 @Value1 @Blob1 sess defaultTableConfig $ \table -> do @@ -165,8 +159,8 @@ prop_unions_1 = bracket (unions $ table :| []) close $ \table' -> bracket (duplicate table) close $ \table'' -> do - inserts table [(Key1 17, Value1 43, Nothing)] - inserts table [(Key1 17, Value1 44, Nothing)] + inserts table' [(Key1 17, Value1 43, Nothing)] + inserts table'' [(Key1 17, Value1 44, Nothing)] -- The original table is unmodified r <- lookups table [Key1 17] From 98fad1f2f00815f7f741a3d5437e2788d4e40f18 Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Fri, 14 Mar 2025 19:31:24 +0000 Subject: [PATCH 09/12] Add unit tests for the trivial case of querying and supplying union credits The trivial case is when the table has no union level, as then there is no union debt, and supplying credits returns them all as leftovers. And implement these trivial cases. --- src/Database/LSMTree/Internal.hs | 12 ++++++++---- test/Database/LSMTree/Model/Session.hs | 4 +++- test/Test/Database/LSMTree/UnitTests.hs | 16 ++++++++++++++++ 3 files changed, 27 insertions(+), 5 deletions(-) diff --git a/src/Database/LSMTree/Internal.hs b/src/Database/LSMTree/Internal.hs index e2fe4ef42..338dd2bfe 100644 --- a/src/Database/LSMTree/Internal.hs +++ b/src/Database/LSMTree/Internal.hs @@ -1630,8 +1630,10 @@ remainingUnionDebt :: (MonadSTM m, MonadThrow m) => Table m h -> m UnionDebt remainingUnionDebt t = do traceWith (tableTracer t) TraceRemainingUnionDebt withOpenTable t $ \tEnv -> do - RW.withReadAccess (tableContent tEnv) $ \_tableContent -> do - error "remainingUnionDebt: not yet implemented" + RW.withReadAccess (tableContent tEnv) $ \tableContent -> + case tableUnionLevel tableContent of + NoUnion -> pure (UnionDebt 0) + Union{} -> error "remainingUnionDebt: not yet implemented" -- | See 'Database.LSMTree.Normal.UnionCredits'. newtype UnionCredits = UnionCredits Int @@ -1644,5 +1646,7 @@ supplyUnionCredits t credits = do traceWith (tableTracer t) $ TraceSupplyUnionCredits credits withOpenTable t $ \tEnv -> do -- TODO: should this be acquiring read or write access? - RW.withWriteAccess (tableContent tEnv) $ \_tableContent -> do - error "supplyUnionCredits: not yet implemented" + RW.withWriteAccess (tableContent tEnv) $ \tableContent -> + case tableUnionLevel tableContent of + NoUnion -> pure (tableContent, credits) -- all leftovers + Union{} -> error "supplyUnionCredits: not yet implemented" diff --git a/test/Database/LSMTree/Model/Session.hs b/test/Database/LSMTree/Model/Session.hs index 34e9e872a..7da2c8c89 100644 --- a/test/Database/LSMTree/Model/Session.hs +++ b/test/Database/LSMTree/Model/Session.hs @@ -844,7 +844,9 @@ supplyUnionCredits :: -> UnionCredits -> m UnionCredits supplyUnionCredits t@Table{..} c@(UnionCredits credits) - | credits <= 0 = pure c + | credits <= 0 = do + _ <- guardTableIsOpen t + pure c | otherwise = do (updc, table) <- guardTableIsOpen t when (isUnionDescendant == IsUnionDescendant) $ diff --git a/test/Test/Database/LSMTree/UnitTests.hs b/test/Test/Database/LSMTree/UnitTests.hs index b4764979e..c211be5ca 100644 --- a/test/Test/Database/LSMTree/UnitTests.hs +++ b/test/Test/Database/LSMTree/UnitTests.hs @@ -34,6 +34,7 @@ tests = , testCase "unit_twoTableTypes" unit_twoTableTypes , testCase "unit_snapshots" unit_snapshots , testCase "unit_unions_1" unit_unions_1 + , testCase "unit_union_credits" unit_union_credits ] unit_blobs :: (String -> IO ()) -> Assertion @@ -174,6 +175,21 @@ unit_unions_1 = r'' <- lookups table'' [Key1 17] V.map ignoreBlobRef r'' @?= [Found (Value1 44)] +-- | Querying or supplying union credits to non-union tables is trivial. +unit_union_credits :: Assertion +unit_union_credits = + withTempIOHasBlockIO "test" $ \hfs hbio -> + withSession nullTracer hfs hbio (FS.mkFsPath []) $ \sess -> + withTable @_ @Key1 @Value1 @Blob1 sess defaultTableConfig $ \table -> do + inserts table [(Key1 17, Value1 42, Nothing)] + + -- The table is not the result of a union, so the debt is always 0, + UnionDebt debt <- remainingUnionDebt table + debt @?= 0 + + -- and supplying credits returns them all as leftovers. + UnionCredits leftover <- supplyUnionCredits table (UnionCredits 42) + leftover @?= 42 ignoreBlobRef :: Functor f => f (BlobRef m b) -> f () ignoreBlobRef = fmap (const ()) From 0a0de7f5f5554400f9027728266c3e5308730229 Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Fri, 14 Mar 2025 19:57:47 +0000 Subject: [PATCH 10/12] Don't cover querying or supplying credits to non-union tables in QLS We cover the trivial case of querying or supplying credits to tables that are not derived from a union operation in the unit tests, so we do not need to spend coverage space in the QLS tests on the trivial cases. So only gnerate RemainingUnionDebt, SupplyUnionCredits for tables that are derived from union operations. --- test/Test/Database/LSMTree/StateMachine.hs | 30 +++++++++------------- 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index da3849758..81afaa870 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -1969,42 +1969,36 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = , let genErrors = pure Nothing -- TODO: generate errors ] ++ [ (2, fmap Some $ (Action <$> genErrors <*>) $ - RemainingUnionDebt <$> genUnionTableVar) - | let genErrors = pure Nothing -- TODO: generate errors + RemainingUnionDebt <$> genUnionDescendantTableVar) + -- Tables not derived from unions are covered in UnitTests. + | not (null unionDescendantTableVars) + , let genErrors = pure Nothing -- TODO: generate errors -- TODO: this is currently only enabled for the reference -- implementation. Enable this unconditionally once table union is -- implemented , isJust (eqT @h @ModelIO.Table) ] ++ [ (8, fmap Some $ (Action <$> genErrors <*>) $ - SupplyUnionCredits <$> genUnionTableVar <*> genUnionCredits) - | let genErrors = pure Nothing -- TODO: generate errors + SupplyUnionCredits <$> genUnionDescendantTableVar <*> genUnionCredits) + -- Tables not derived from unions are covered in UnitTests. + | not (null unionDescendantTableVars) + , let genErrors = pure Nothing -- TODO: generate errors -- TODO: this is currently only enabled for the reference -- implementation. Enable this unconditionally once table union is -- implemented , isJust (eqT @h @ModelIO.Table) ] ++ [ (2, fmap Some $ (Action <$> genErrors <*>) $ - SupplyPortionOfDebt <$> genUnionTableVar <*> genPortion) - | let genErrors = pure Nothing -- TODO: generate errors + SupplyPortionOfDebt <$> genUnionDescendantTableVar <*> genPortion) + -- Tables not derived from unions are covered in UnitTests. + | not (null unionDescendantTableVars) + , let genErrors = pure Nothing -- TODO: generate errors -- TODO: this is currently only enabled for the reference -- implementation. Enable this unconditionally once table union is -- implemented , isJust (eqT @h @ModelIO.Table) ] where - -- For querying the union debt or supplying union credits, the - -- interesting cases to test for are when tables are union tables. For - -- non-union tables, these operations should just be no-ops, so we - -- generate them only rarely. - -- - -- TODO: tweak distribution once table unions are implemented - -- TODO: replace union actions on non-union tables with unit tests? - genUnionTableVar = QC.frequency [ - (9 * length unionDescendantTableVars, genUnionDescendantTableVar) - , (1 * length notUnionDescendantTableVars, genNotUnionDescendantTableVar) - ] - -- TODO: tweak distribution once table unions are implemented genUnionCredits = QC.frequency [ -- The typical, interesting case is to supply a positive number of From a3c5cd05dc7e3fe235800e96436559124012462c Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Fri, 14 Mar 2025 20:08:20 +0000 Subject: [PATCH 11/12] Cover supplying 0 union credits as a unit test and remove QLS coverage Same principle as previous patches. Keep the precious coverage space in the QLS tests for the non-trivial cases, and cover the trivial case in a unit test. --- src/Database/LSMTree/Internal.hs | 7 ++++++- test/Database/LSMTree/Model/Session.hs | 2 +- test/Test/Database/LSMTree/StateMachine.hs | 13 ++++--------- test/Test/Database/LSMTree/UnitTests.hs | 22 ++++++++++++++++++++++ 4 files changed, 33 insertions(+), 11 deletions(-) diff --git a/src/Database/LSMTree/Internal.hs b/src/Database/LSMTree/Internal.hs index 338dd2bfe..d331d8543 100644 --- a/src/Database/LSMTree/Internal.hs +++ b/src/Database/LSMTree/Internal.hs @@ -1649,4 +1649,9 @@ supplyUnionCredits t credits = do RW.withWriteAccess (tableContent tEnv) $ \tableContent -> case tableUnionLevel tableContent of NoUnion -> pure (tableContent, credits) -- all leftovers - Union{} -> error "supplyUnionCredits: not yet implemented" + Union{} + | credits <= UnionCredits 0 -> pure (tableContent, UnionCredits 0) + --TODO: remove this 0 special case once the general case covers it. + -- We do not need to optimise the 0 case. It is just here to + -- simplify test coverage. + | otherwise -> error "supplyUnionCredits: not yet implemented" diff --git a/test/Database/LSMTree/Model/Session.hs b/test/Database/LSMTree/Model/Session.hs index 7da2c8c89..6d9233cd0 100644 --- a/test/Database/LSMTree/Model/Session.hs +++ b/test/Database/LSMTree/Model/Session.hs @@ -846,7 +846,7 @@ supplyUnionCredits :: supplyUnionCredits t@Table{..} c@(UnionCredits credits) | credits <= 0 = do _ <- guardTableIsOpen t - pure c + pure (UnionCredits 0) -- always 0, not negative | otherwise = do (updc, table) <- guardTableIsOpen t when (isUnionDescendant == IsUnionDescendant) $ diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index 81afaa870..cc4af96cd 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -1999,15 +1999,10 @@ arbitraryActionWithVars _ label ctx (ModelState st _stats) = , isJust (eqT @h @ModelIO.Table) ] where - -- TODO: tweak distribution once table unions are implemented - genUnionCredits = QC.frequency [ - -- The typical, interesting case is to supply a positive number of - -- union credits. - (9, R.UnionCredits . QC.getPositive <$> QC.arbitrary) - -- Supplying 0 or less credits is a no-op, so we generate it only - -- rarely. - , (1, R.UnionCredits <$> QC.arbitrary) - ] + -- 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] diff --git a/test/Test/Database/LSMTree/UnitTests.hs b/test/Test/Database/LSMTree/UnitTests.hs index c211be5ca..ec51cea24 100644 --- a/test/Test/Database/LSMTree/UnitTests.hs +++ b/test/Test/Database/LSMTree/UnitTests.hs @@ -35,6 +35,7 @@ tests = , testCase "unit_snapshots" unit_snapshots , testCase "unit_unions_1" unit_unions_1 , testCase "unit_union_credits" unit_union_credits + , testCase "unit_union_credit_0" unit_union_credit_0 ] unit_blobs :: (String -> IO ()) -> Assertion @@ -191,6 +192,27 @@ unit_union_credits = UnionCredits leftover <- supplyUnionCredits table (UnionCredits 42) leftover @?= 42 +-- | Supplying zero or negative credits to union tables works, but does nothing. +unit_union_credit_0 :: Assertion +unit_union_credit_0 = + withTempIOHasBlockIO "test" $ \hfs hbio -> + withSession nullTracer hfs hbio (FS.mkFsPath []) $ \sess -> + withTable @_ @Key1 @Value1 @Blob1 sess defaultTableConfig $ \table -> do + inserts table [(Key1 17, Value1 42, Nothing)] + + bracket (table `union` table) close $ \table' -> do + -- Supplying 0 credits works and returns 0 leftovers. + UnionCredits leftover <- supplyUnionCredits table' (UnionCredits 0) + leftover @?= 0 + + -- Supplying negative credits also works and returns 0 leftovers. + UnionCredits leftover' <- supplyUnionCredits table' (UnionCredits (-42)) + leftover' @?= 0 + + -- And the table is still vaguely cromulent + r <- lookups table' [Key1 17] + V.map ignoreBlobRef r @?= [Found (Value1 42)] + ignoreBlobRef :: Functor f => f (BlobRef m b) -> f () ignoreBlobRef = fmap (const ()) From 0acc119e120850e8f0d3ab867e74446aa3d8429a Mon Sep 17 00:00:00 2001 From: Duncan Coutts Date: Mon, 17 Mar 2025 16:31:44 +0000 Subject: [PATCH 12/12] Make more QLS Stats members properly strict Slightly better memory use in the tests. --- test/Test/Database/LSMTree/StateMachine.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/Test/Database/LSMTree/StateMachine.hs b/test/Test/Database/LSMTree/StateMachine.hs index cc4af96cd..a7b9e39d2 100644 --- a/test/Test/Database/LSMTree/StateMachine.hs +++ b/test/Test/Database/LSMTree/StateMachine.hs @@ -2221,7 +2221,7 @@ instance InterpretOp Op (ModelValue (ModelState h)) where data Stats = Stats { -- === Tags -- | Names for which snapshots exist - snapshotted :: Set R.SnapshotName + snapshotted :: !(Set R.SnapshotName) -- === Final tags (per action sequence, across all tables) -- | Number of succesful lookups and their results , numLookupsResults :: {-# UNPACK #-} !(Int, Int, Int) @@ -2242,13 +2242,13 @@ data Stats = Stats { , 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] + , 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] + , 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.