From a414034763e6346fcd5ea5ce6780ecb2c8c841bf Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Thu, 25 Jul 2024 11:22:09 +0200 Subject: [PATCH 01/10] refactor prototype --- prototypes/ScheduledMerges.hs | 77 ++++++++++++++++++++--------------- 1 file changed, 44 insertions(+), 33 deletions(-) diff --git a/prototypes/ScheduledMerges.hs b/prototypes/ScheduledMerges.hs index 56cb319d2..720439003 100644 --- a/prototypes/ScheduledMerges.hs +++ b/prototypes/ScheduledMerges.hs @@ -1,7 +1,3 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE EmptyCase #-} -{-# LANGUAGE ScopedTypeVariables #-} - -- | A prototype of an LSM with explicitly scheduled incremental merges. -- -- The scheduled incremental merges is about ensuring that the merging @@ -118,6 +114,12 @@ type Debt = Int type Run = Map Key Op type Buffer = Map Key Op +runSize :: Run -> Int +runSize = Map.size + +bufferSize :: Buffer -> Int +bufferSize = Map.size + type Op = Update Value Blob type Key = Int @@ -138,18 +140,18 @@ levellingRunSize n = 4^(n+1) tieringRunSizeToLevel :: Run -> Int tieringRunSizeToLevel r - | s <= bufferSize = 1 -- level numbers start at 1 + | s <= maxBufferSize = 1 -- level numbers start at 1 | otherwise = 1 + (finiteBitSize s - countLeadingZeros (s-1) - 1) `div` 2 where - s = Map.size r + s = runSize r levellingRunSizeToLevel :: Run -> Int levellingRunSizeToLevel r = max 1 (tieringRunSizeToLevel r - 1) -- level numbers start at 1 -bufferSize :: Int -bufferSize = tieringRunSize 1 -- 4 +maxBufferSize :: Int +maxBufferSize = tieringRunSize 1 -- 4 mergePolicyForLevel :: Int -> [Level s] -> MergePolicy mergePolicyForLevel 1 [] = MergePolicyTiering @@ -274,20 +276,22 @@ newMerge tr level mergepolicy mergelast rs = do mergeLast = mergelast, mergeDebt = debt, mergeCost = cost, - mergeRunsSize = map Map.size rs + mergeRunsSize = map runSize rs } assert (let l = length rs in l >= 2 && l <= 5) $ MergingRun mergepolicy mergelast <$> newSTRef (OngoingMerge debt rs r) where - cost = sum (map Map.size rs) + cost = sum (map runSize rs) -- How much we need to discharge before the merge can be guaranteed - -- complete. + -- complete. More precisely, this is the maximum amount a merge at this + -- level could need. This overestimation means that merges will only + -- complete at the last possible moment. -- Note that for levelling this is includes the single run in the current -- level. - debt = case mergepolicy of - MergePolicyLevelling -> newMergeDebt (4 * tieringRunSize (level-1) - + levellingRunSize level) - MergePolicyTiering -> newMergeDebt (4 * tieringRunSize (level-1)) + debt = newMergeDebt $ case mergepolicy of + MergePolicyLevelling -> 4 * tieringRunSize (level-1) + + levellingRunSize level + MergePolicyTiering -> 4 * tieringRunSize (level-1) -- deliberately lazy: r = case mergelast of MergeMidLevel -> (mergek rs) @@ -313,7 +317,7 @@ expectCompletedMerge tr (MergingRun mergepolicy mergelast ref) = do traceWith tr MergeCompletedEvent { mergePolicy = mergepolicy, mergeLast = mergelast, - mergeSize = Map.size r + mergeSize = runSize r } return r OngoingMerge d _ _ -> @@ -413,7 +417,7 @@ update tr (LSMHandle scr lsmr) k op = do modifySTRef' scr (+1) supplyCredits 1 ls let wb' = Map.insert k op wb - if Map.size wb' >= bufferSize + if bufferSize wb' >= maxBufferSize then do ls' <- increment tr sc (bufferToRun wb') ls writeSTRef lsmr (LSMContent Map.empty ls') @@ -500,49 +504,50 @@ increment tr sc = \r ls -> do assert ok (return ls') where go :: Int -> [Run] -> Levels s -> ST s (Levels s) - go !ln rs [] = do + go !ln incoming [] = do let mergepolicy = mergePolicyForLevel ln [] traceWith tr' AddLevelEvent - mr <- newMerge tr' ln mergepolicy MergeLastLevel rs + mr <- newMerge tr' ln mergepolicy MergeLastLevel incoming return (Level mr [] : []) where tr' = contramap (EventAt sc ln) tr - go !ln rs' (Level mr rs : ls) = do + go !ln incoming (Level mr rs : ls) = do r <- expectCompletedMerge tr' mr + let resident = r:rs case mergePolicyForLevel ln ls of -- If r is still too small for this level then keep it and merge again -- with the incoming runs. MergePolicyTiering | tieringRunSizeToLevel r < ln -> do let mergelast = mergeLastForLevel ls - mr' <- newMerge tr' ln MergePolicyTiering mergelast (rs' ++ [r]) + mr' <- newMerge tr' ln MergePolicyTiering mergelast (incoming ++ [r]) return (Level mr' rs : ls) -- This tiering level is now full. We take the completed merged run -- (the previous incoming runs), plus all the other runs on this level -- as a bundle and move them down to the level below. We start a merge -- for the new incoming runs. This level is otherwise empty. - MergePolicyTiering | levelIsFull rs -> do - mr' <- newMerge tr' ln MergePolicyTiering MergeMidLevel rs' - ls' <- go (ln+1) (r:rs) ls + MergePolicyTiering | tieringLevelIsFull ln incoming resident -> do + mr' <- newMerge tr' ln MergePolicyTiering MergeMidLevel incoming + ls' <- go (ln+1) resident ls return (Level mr' [] : ls') -- This tiering level is not yet full. We move the completed merged run -- into the level proper, and start the new merge for the incoming runs. MergePolicyTiering -> do let mergelast = mergeLastForLevel ls - mr' <- newMerge tr' ln MergePolicyTiering mergelast rs' - traceWith tr' (AddRunEvent (length (r:rs))) - return (Level mr' (r:rs) : ls) + mr' <- newMerge tr' ln MergePolicyTiering mergelast incoming + traceWith tr' (AddRunEvent (length resident)) + return (Level mr' resident : ls) -- The final level is using levelling. If the existing completed merge -- run is too large for this level, we promote the run to the next -- level and start merging the incoming runs into this (otherwise -- empty) level . - MergePolicyLevelling | levellingRunSizeToLevel r > ln -> do + MergePolicyLevelling | levellingLevelIsFull ln incoming r -> do assert (null rs && null ls) $ return () - mr' <- newMerge tr' ln MergePolicyTiering MergeMidLevel rs' + mr' <- newMerge tr' ln MergePolicyTiering MergeMidLevel incoming ls' <- go (ln+1) [r] [] return (Level mr' [] : ls') @@ -550,14 +555,20 @@ increment tr sc = \r ls -> do MergePolicyLevelling -> do assert (null rs && null ls) $ return () mr' <- newMerge tr' ln MergePolicyLevelling MergeLastLevel - (rs' ++ [r]) + (incoming ++ [r]) return (Level mr' [] : []) where tr' = contramap (EventAt sc ln) tr -levelIsFull :: [Run] -> Bool -levelIsFull rs = length rs + 1 >= 4 +-- | Only based on run count, not their sizes. +tieringLevelIsFull :: Int -> [Run] -> [Run] -> Bool +tieringLevelIsFull _ln _incoming resident = length resident >= 4 + +-- | The level is only considered full once the resident run is /too large/ for +-- the level. +levellingLevelIsFull :: Int -> [Run] -> Run -> Bool +levellingLevelIsFull ln _incoming resident = levellingRunSizeToLevel resident > ln duplicate :: LSM s -> ST s (LSM s) duplicate (LSMHandle _scr lsmr) = do @@ -619,7 +630,7 @@ representationShape = ( fmap (\(mp, ml, mrs) -> (mp, ml, summaryMRS mrs)) mmr , map summaryRun rs) where - summaryRun = Map.size + summaryRun = runSize summaryMRS (CompletedMerge r) = Left (summaryRun r) summaryMRS (OngoingMerge _ rs _) = Right (map summaryRun rs) From ab10233c77b715293729ae8e158172f87ef6a954 Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Wed, 24 Jul 2024 12:42:15 +0200 Subject: [PATCH 02/10] unify style of invariant This way we always know the exact assertion that failed. --- prototypes/ScheduledMerges.hs | 73 ++++++++++++++++++----------------- 1 file changed, 37 insertions(+), 36 deletions(-) diff --git a/prototypes/ScheduledMerges.hs b/prototypes/ScheduledMerges.hs index 720439003..b85aca27e 100644 --- a/prototypes/ScheduledMerges.hs +++ b/prototypes/ScheduledMerges.hs @@ -49,7 +49,7 @@ import Data.STRef import Control.Exception (assert) import Control.Monad.ST import Control.Tracer (Tracer, contramap, traceWith) -import GHC.Stack (HasCallStack) +import GHC.Stack (HasCallStack, callStack) import Database.LSMTree.Normal (LookupResult (..), Update (..)) @@ -165,11 +165,11 @@ mergeLastForLevel _ = MergeMidLevel -- | Note that the invariants rely on the fact that levelling is only used on -- the last level. -- -invariant :: forall s. Levels s -> ST s Bool +invariant :: forall s. Levels s -> ST s () invariant = go 1 where - go :: Int -> [Level s] -> ST s Bool - go !_ [] = return True + go :: Int -> [Level s] -> ST s () + go !_ [] = return () go !ln (Level mr rs : ls) = do @@ -177,20 +177,19 @@ invariant = go 1 SingleRun r -> return (CompletedMerge r) MergingRun _ _ ref -> readSTRef ref - assert (case mr of - SingleRun{} -> True - MergingRun mp ml _ -> mergePolicyForLevel ln ls == mp - && mergeLastForLevel ls == ml) - assert (length rs <= 3) $ - assert (expectedRunLengths ln rs ls) $ - assert (expectedMergingRunLengths ln mr mrs ls) $ - return () + assertST $ case mr of + SingleRun{} -> True + MergingRun mp ml _ -> mergePolicyForLevel ln ls == mp + && mergeLastForLevel ls == ml + assertST $ length rs <= 3 + expectedRunLengths ln rs ls + expectedMergingRunLengths ln mr mrs ls go (ln+1) ls -- All runs within a level "proper" (as opposed to the incoming runs -- being merged) should be of the correct size for the level. - expectedRunLengths :: Int -> [Run] -> [Level s] -> Bool + expectedRunLengths :: Int -> [Run] -> [Level s] -> ST s () expectedRunLengths ln rs ls = case mergePolicyForLevel ln ls of -- Levels using levelling have only one run, and that single run is @@ -198,13 +197,13 @@ invariant = go 1 -- other "normal" runs. The exception is when a levelling run becomes -- too large and is promoted, in that case initially there's no merge, -- but it is still represented as a 'MergingRun', using 'SingleRun'. - MergePolicyLevelling -> null rs - MergePolicyTiering -> all (\r -> tieringRunSizeToLevel r == ln) rs + MergePolicyLevelling -> assertST $ null rs + MergePolicyTiering -> assertST $ all (\r -> tieringRunSizeToLevel r == ln) rs -- Incoming runs being merged also need to be of the right size, but the -- conditions are more complicated. expectedMergingRunLengths :: Int -> MergingRun s -> MergingRunState - -> [Level s] -> Bool + -> [Level s] -> ST s () expectedMergingRunLengths ln mr mrs ls = case mergePolicyForLevel ln ls of MergePolicyLevelling -> @@ -212,54 +211,57 @@ invariant = go 1 -- A single incoming run (which thus didn't need merging) must be -- of the expected size range already (SingleRun r, CompletedMerge{}) -> - assert (levellingRunSizeToLevel r == ln) True + assertST $ levellingRunSizeToLevel r == ln -- A completed merge for levelling can be of almost any size at all! -- It can be smaller, due to deletions in the last level. But it -- can't be bigger than would fit into the next level. (_, CompletedMerge r) -> - assert (levellingRunSizeToLevel r <= ln+1) True + assertST $ levellingRunSizeToLevel r <= ln+1 -- An ongoing merge for levelling should have 4 incoming runs of -- the right size for the level below, and 1 run from this level, -- but the run from this level can be of almost any size for the -- same reasons as above. Although if this is the first merge for -- a new level, it'll have only 4 runs. - (_, OngoingMerge _ rs _) -> - assert (length rs == 4 || length rs == 5) True - && assert (all (\r -> tieringRunSizeToLevel r == ln-1) (take 4 rs)) True - && assert (all (\r -> levellingRunSizeToLevel r <= ln+1) (drop 4 rs)) True + (_, OngoingMerge _ rs _) -> do + assertST $ length rs == 4 || length rs == 5 + assertST $ all (\r -> tieringRunSizeToLevel r == ln-1) (take 4 rs) + assertST $ all (\r -> levellingRunSizeToLevel r <= ln+1) (drop 4 rs) MergePolicyTiering -> case (mr, mrs, mergeLastForLevel ls) of -- A single incoming run (which thus didn't need merging) must be -- of the expected size already (SingleRun r, CompletedMerge{}, _) -> - tieringRunSizeToLevel r == ln + assertST $ tieringRunSizeToLevel r == ln -- A completed last level run can be of almost any smaller size due -- to deletions, but it can't be bigger than the next level down. -- Note that tiering on the last level only occurs when there is -- a single level only. - (_, CompletedMerge r, MergeLastLevel) -> - ln == 1 - && tieringRunSizeToLevel r <= ln+1 + (_, CompletedMerge r, MergeLastLevel) -> do + assertST $ ln == 1 + assertST $ tieringRunSizeToLevel r <= ln+1 -- A completed mid level run is usually of the size for the -- level it is entering, but can also be one smaller (in which case -- it'll be held back and merged again). (_, CompletedMerge r, MergeMidLevel) -> - rln == ln || rln == ln+1 - where - rln = tieringRunSizeToLevel r + assertST $ tieringRunSizeToLevel r `elem` [ln, ln+1] -- An ongoing merge for tiering should have 4 incoming runs of -- the right size for the level below, and at most 1 run held back -- due to being too small (which would thus also be of the size of -- the level below). - (_, OngoingMerge _ rs _, _) -> - (length rs == 4 || length rs == 5) - && all (\r -> tieringRunSizeToLevel r == ln-1) rs + (_, OngoingMerge _ rs _, _) -> do + assertST $ length rs == 4 || length rs == 5 + assertST $ all (\r -> tieringRunSizeToLevel r == ln-1) rs + +-- 'callStack' just ensures that the 'HasCallStack' constraint is not redundant +-- when compiling with debug assertions disabled. +assertST :: HasCallStack => Bool -> ST s () +assertST p = assert p $ return (const () callStack) ------------------------------------------------------------------------------- @@ -429,8 +431,7 @@ supply (LSMHandle scr lsmr) credits = do LSMContent _ ls <- readSTRef lsmr modifySTRef' scr (+1) supplyCredits credits ls - ok <- invariant ls - assert ok $ return () + invariant ls lookups :: LSM s -> [Key] -> ST s [(Key, LookupResult Value Blob)] lookups lsm = mapM (\k -> (k,) <$> lookup lsm k) @@ -500,8 +501,8 @@ increment :: forall s. Tracer (ST s) Event -> Counter -> Run -> Levels s -> ST s (Levels s) increment tr sc = \r ls -> do ls' <- go 1 [r] ls - ok <- invariant ls' - assert ok (return ls') + invariant ls' + return ls' where go :: Int -> [Run] -> Levels s -> ST s (Levels s) go !ln incoming [] = do From 6fa93c46035a98d8abb775323e6523f9a61f01bc Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Tue, 23 Jul 2024 21:46:12 +0200 Subject: [PATCH 03/10] add test for merging underfull run again with incoming ones --- prototypes/ScheduledMergesTestQLS.hs | 55 ++++++++++++++++++++++++---- 1 file changed, 47 insertions(+), 8 deletions(-) diff --git a/prototypes/ScheduledMergesTestQLS.hs b/prototypes/ScheduledMergesTestQLS.hs index 22250f59b..98e39f96a 100644 --- a/prototypes/ScheduledMergesTestQLS.hs +++ b/prototypes/ScheduledMergesTestQLS.hs @@ -1,11 +1,4 @@ -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilies #-} module ScheduledMergesTestQLS (tests) where @@ -15,10 +8,12 @@ import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Constraint (Dict (..)) +import Data.Foldable (traverse_) import Data.Proxy import Data.STRef import Control.Exception +import Control.Monad (replicateM_) import Control.Monad.ST import Control.Tracer (Tracer (Tracer), nullTracer) import qualified Control.Tracer as Tracer @@ -43,6 +38,8 @@ tests :: TestTree tests = testGroup "ScheduledMerges" [ testProperty "ScheduledMerges vs model" prop_LSM , testCase "regression_empty_run" test_regression_empty_run + , testCase "merge_again_with_incoming" test_merge_again_with_incoming + , testCase "merge_again_with_incoming'" test_merge_again_with_incoming' ] prop_LSM :: Actions (Lockstep Model) -> Property @@ -84,6 +81,48 @@ test_regression_empty_run = -- finish merge LSM.supply lsm 16 +-- | Covers the case where a run ends up too small for a level, so it gets +-- merged again with the next incoming runs. +-- That merge gets completed by supplying credits. +test_merge_again_with_incoming :: IO () +test_merge_again_with_incoming = + runWithTracer $ \tracer -> do + stToIO $ do + lsm <- LSM.new + let ins k = LSM.insert tracer lsm k 0 + -- get something to 3rd level (so 2nd level is not levelling) + -- (needs 5 runs to go to level 2 so the resulting run becomes too big) + traverse_ ins [101..100+(5*16)] + -- get a very small run (4 elements) to 2nd level + replicateM_ 4 $ + traverse_ ins [201..200+4] + -- get another run to 2nd level, which the small run can be merged with + traverse_ ins [301..300+16] + -- complete the merge + LSM.supply lsm 32 + +-- | Covers the case where a run ends up too small for a level, so it gets +-- merged again with the next incoming runs. +-- That merge gets completed and becomes part of another merge. +test_merge_again_with_incoming' :: IO () +test_merge_again_with_incoming' = + runWithTracer $ \tracer -> do + stToIO $ do + lsm <- LSM.new + let ins k = LSM.insert tracer lsm k 0 + -- get something to 3rd level (so 2nd level is not levelling) + -- (needs 5 runs to go to level 2 so the resulting run becomes too big) + traverse_ ins [101..100+(5*16)] + -- get a very small run (4 elements) to 2nd level + replicateM_ 4 $ + traverse_ ins [201..200+4] + -- get another run to 2nd level, which the small run can be merged with + traverse_ ins [301..300+16] + -- get 3 more to 2nd level, so the merge above is expected to complete + -- (actually more, as runs only move once a fifth run arrives...) + traverse_ ins [401..400+(6*16)] + + -- | Provides a tracer and will add the log of traced events to the reported -- failure. runWithTracer :: (Tracer (ST RealWorld) Event -> IO a) -> IO a From 22f88b4e0bd74acbffc2482eae23d97de4221605 Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Thu, 25 Jul 2024 11:55:48 +0200 Subject: [PATCH 04/10] increase size for prototype lockstep test --- prototypes/ScheduledMergesTestQLS.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prototypes/ScheduledMergesTestQLS.hs b/prototypes/ScheduledMergesTestQLS.hs index 98e39f96a..6fca07d4d 100644 --- a/prototypes/ScheduledMergesTestQLS.hs +++ b/prototypes/ScheduledMergesTestQLS.hs @@ -36,7 +36,7 @@ import Test.Tasty.QuickCheck (testProperty) tests :: TestTree tests = testGroup "ScheduledMerges" [ - testProperty "ScheduledMerges vs model" prop_LSM + testProperty "ScheduledMerges vs model" $ mapSize (*10) prop_LSM -- still <10s , testCase "regression_empty_run" test_regression_empty_run , testCase "merge_again_with_incoming" test_merge_again_with_incoming , testCase "merge_again_with_incoming'" test_merge_again_with_incoming' From c76b0a930bb40e350e04ebffc00552a290c6291a Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Wed, 24 Jul 2024 12:50:14 +0200 Subject: [PATCH 05/10] fix run size invariants that were too tight --- prototypes/ScheduledMerges.hs | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/prototypes/ScheduledMerges.hs b/prototypes/ScheduledMerges.hs index b85aca27e..53a1f0794 100644 --- a/prototypes/ScheduledMerges.hs +++ b/prototypes/ScheduledMerges.hs @@ -198,7 +198,13 @@ invariant = go 1 -- too large and is promoted, in that case initially there's no merge, -- but it is still represented as a 'MergingRun', using 'SingleRun'. MergePolicyLevelling -> assertST $ null rs - MergePolicyTiering -> assertST $ all (\r -> tieringRunSizeToLevel r == ln) rs + -- Runs in tiering levels usually fit that size, but they can be one + -- larger, if a run has been held back (creating a 5-way merge). + MergePolicyTiering -> assertST $ all (\r -> tieringRunSizeToLevel r `elem` [ln, ln+1]) rs + -- (This is actually still not really true, but will hold in practice. + -- In the pathological case, all runs passed to the next level can be + -- factor (5/4) too large, and there the same holding back can lead to + -- factor (6/4) etc., until at level 12 a run is two levels too large. -- Incoming runs being merged also need to be of the right size, but the -- conditions are more complicated. @@ -220,13 +226,14 @@ invariant = go 1 assertST $ levellingRunSizeToLevel r <= ln+1 -- An ongoing merge for levelling should have 4 incoming runs of - -- the right size for the level below, and 1 run from this level, + -- the right size for the level below (or slightly larger due to + -- holding back underfull runs), and 1 run from this level, -- but the run from this level can be of almost any size for the -- same reasons as above. Although if this is the first merge for -- a new level, it'll have only 4 runs. (_, OngoingMerge _ rs _) -> do assertST $ length rs == 4 || length rs == 5 - assertST $ all (\r -> tieringRunSizeToLevel r == ln-1) (take 4 rs) + assertST $ all (\r -> tieringRunSizeToLevel r `elem` [ln-1, ln]) (take 4 rs) assertST $ all (\r -> levellingRunSizeToLevel r <= ln+1) (drop 4 rs) MergePolicyTiering -> @@ -246,9 +253,10 @@ invariant = go 1 -- A completed mid level run is usually of the size for the -- level it is entering, but can also be one smaller (in which case - -- it'll be held back and merged again). + -- it'll be held back and merged again) or one larger (because it + -- includes a run that has been held back before). (_, CompletedMerge r, MergeMidLevel) -> - assertST $ tieringRunSizeToLevel r `elem` [ln, ln+1] + assertST $ tieringRunSizeToLevel r `elem` [ln-1, ln, ln+1] -- An ongoing merge for tiering should have 4 incoming runs of -- the right size for the level below, and at most 1 run held back From 8071d62cbc6491c4b008156f823df7ea66f1ce2b Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Thu, 25 Jul 2024 11:41:13 +0200 Subject: [PATCH 06/10] tighten invariants --- prototypes/ScheduledMerges.hs | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/prototypes/ScheduledMerges.hs b/prototypes/ScheduledMerges.hs index 53a1f0794..1e6006ad5 100644 --- a/prototypes/ScheduledMerges.hs +++ b/prototypes/ScheduledMerges.hs @@ -213,10 +213,13 @@ invariant = go 1 expectedMergingRunLengths ln mr mrs ls = case mergePolicyForLevel ln ls of MergePolicyLevelling -> + assert (mergeLastForLevel ls == MergeLastLevel) $ case (mr, mrs) of -- A single incoming run (which thus didn't need merging) must be -- of the expected size range already - (SingleRun r, CompletedMerge{}) -> + (SingleRun r, m) -> do + assertST $ case m of CompletedMerge{} -> True + OngoingMerge{} -> False assertST $ levellingRunSizeToLevel r == ln -- A completed merge for levelling can be of almost any size at all! @@ -232,15 +235,19 @@ invariant = go 1 -- same reasons as above. Although if this is the first merge for -- a new level, it'll have only 4 runs. (_, OngoingMerge _ rs _) -> do - assertST $ length rs == 4 || length rs == 5 - assertST $ all (\r -> tieringRunSizeToLevel r `elem` [ln-1, ln]) (take 4 rs) - assertST $ all (\r -> levellingRunSizeToLevel r <= ln+1) (drop 4 rs) + assertST $ length rs `elem` [4, 5] + let incoming = take 4 rs + let resident = drop 4 rs + assertST $ all (\r -> tieringRunSizeToLevel r `elem` [ln-1, ln]) incoming + assertST $ all (\r -> levellingRunSizeToLevel r <= ln+1) resident MergePolicyTiering -> case (mr, mrs, mergeLastForLevel ls) of -- A single incoming run (which thus didn't need merging) must be -- of the expected size already - (SingleRun r, CompletedMerge{}, _) -> + (SingleRun r, m, _) -> do + assertST $ case m of CompletedMerge{} -> True + OngoingMerge{} -> False assertST $ tieringRunSizeToLevel r == ln -- A completed last level run can be of almost any smaller size due @@ -288,7 +295,7 @@ newMerge tr level mergepolicy mergelast rs = do mergeCost = cost, mergeRunsSize = map runSize rs } - assert (let l = length rs in l >= 2 && l <= 5) $ + assert (length rs `elem` [4, 5]) $ MergingRun mergepolicy mergelast <$> newSTRef (OngoingMerge debt rs r) where cost = sum (map runSize rs) From ef61d4fa7c0bae6569119491106d80e25cd997ee Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Tue, 23 Jul 2024 21:49:09 +0200 Subject: [PATCH 07/10] fix calculation of merge debt The adjustment of the calculation is necessary to avoid assertion failures for the new assertion. --- prototypes/ScheduledMerges.hs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/prototypes/ScheduledMerges.hs b/prototypes/ScheduledMerges.hs index 1e6006ad5..583cd4faa 100644 --- a/prototypes/ScheduledMerges.hs +++ b/prototypes/ScheduledMerges.hs @@ -296,19 +296,21 @@ newMerge tr level mergepolicy mergelast rs = do mergeRunsSize = map runSize rs } assert (length rs `elem` [4, 5]) $ - MergingRun mergepolicy mergelast <$> newSTRef (OngoingMerge debt rs r) + assert (mergeDebtLeft debt >= cost) $ + MergingRun mergepolicy mergelast <$> newSTRef (OngoingMerge debt rs r) where cost = sum (map runSize rs) -- How much we need to discharge before the merge can be guaranteed -- complete. More precisely, this is the maximum amount a merge at this - -- level could need. This overestimation means that merges will only - -- complete at the last possible moment. + -- level could need. While the real @cost@ of a merge would lead to merges + -- finishing early, the overestimation @debt@ means that in this prototype + -- merges will only complete at the last possible moment. -- Note that for levelling this is includes the single run in the current -- level. debt = newMergeDebt $ case mergepolicy of MergePolicyLevelling -> 4 * tieringRunSize (level-1) + levellingRunSize level - MergePolicyTiering -> 4 * tieringRunSize (level-1) + MergePolicyTiering -> length rs * tieringRunSize (level-1) -- deliberately lazy: r = case mergelast of MergeMidLevel -> (mergek rs) @@ -373,6 +375,10 @@ data MergeDebt = newMergeDebt :: Debt -> MergeDebt newMergeDebt d = MergeDebt 0 d +mergeDebtLeft :: MergeDebt -> Int +mergeDebtLeft (MergeDebt c d) = + assert (c < d) $ d - c + -- | As credits are paid, debt is reduced in batches when sufficient credits have accumulated. data MergeDebtPaydown = -- | This remaining merge debt is fully paid off with credits. From 6f15601f7fcdcf1de399a73786c97a6112308dbb Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Thu, 25 Jul 2024 12:45:19 +0200 Subject: [PATCH 08/10] prototype: supply 1.25 credits for 5-way tiering merges This is necessary when holding back runs that are too small. --- prototypes/ScheduledMerges.hs | 34 ++++++++++++++++++++++------------ 1 file changed, 22 insertions(+), 12 deletions(-) diff --git a/prototypes/ScheduledMerges.hs b/prototypes/ScheduledMerges.hs index 583cd4faa..1903c847d 100644 --- a/prototypes/ScheduledMerges.hs +++ b/prototypes/ScheduledMerges.hs @@ -42,6 +42,7 @@ module ScheduledMerges ( import Prelude hiding (lookup) import Data.Bits +import Data.Foldable (traverse_) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.STRef @@ -474,22 +475,31 @@ bufferToRun :: Buffer -> Run bufferToRun = id supplyCredits :: Credit -> Levels s -> ST s () -supplyCredits n ls = - sequence_ - [ supplyMergeCredits (n * creditsForMerge mr) mr | Level mr _rs <- ls ] +supplyCredits n = + traverse_ $ \(Level mr _rs) -> do + cr <- creditsForMerge mr + supplyMergeCredits (ceiling (fromIntegral n * cr)) mr -- | The general case (and thus worst case) of how many merge credits we need -- for a level. This is based on the merging policy at the level. -- -creditsForMerge :: MergingRun s -> Credit -creditsForMerge SingleRun{} = 0 - --- A levelling merge is 5x the cost of a tiering merge. --- That's because for levelling one of the runs as an input to the merge --- is the one levelling run which is (up to) 4x bigger than the others put --- together, so it's 1 + 4. -creditsForMerge (MergingRun MergePolicyLevelling _ _) = 5 -creditsForMerge (MergingRun MergePolicyTiering _ _) = 1 +creditsForMerge :: MergingRun s -> ST s Rational +creditsForMerge SingleRun{} = return 0 + +-- A levelling merge has 1 input run and one resident run, which is (up to) 4x +-- bigger than the others. +-- It needs to be completed before another run comes in. +creditsForMerge (MergingRun MergePolicyLevelling _ _) = return $ (1 + 4) / 1 + +-- A tiering merge has 5 runs at most (once could be held back to merged again) +-- and must be completed before the level is full (once 4 more runs come in). +creditsForMerge (MergingRun MergePolicyTiering _ ref) = do + readSTRef ref >>= \case + CompletedMerge _ -> return 0 + OngoingMerge _ rs _ -> do + let numRuns = length rs + assertST $ numRuns `elem` [4, 5] + return $ fromIntegral numRuns / 4 type Event = EventAt EventDetail data EventAt e = EventAt { From 77c4bb4bb87640a6a3ec9fdded4eaa9d598fcb82 Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Tue, 30 Jul 2024 12:33:57 +0200 Subject: [PATCH 09/10] check invariant after supplying credits --- prototypes/ScheduledMerges.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/prototypes/ScheduledMerges.hs b/prototypes/ScheduledMerges.hs index 1903c847d..4c12b41b9 100644 --- a/prototypes/ScheduledMerges.hs +++ b/prototypes/ScheduledMerges.hs @@ -440,10 +440,12 @@ update tr (LSMHandle scr lsmr) k op = do LSMContent wb ls <- readSTRef lsmr modifySTRef' scr (+1) supplyCredits 1 ls + invariant ls let wb' = Map.insert k op wb if bufferSize wb' >= maxBufferSize then do ls' <- increment tr sc (bufferToRun wb') ls + invariant ls' writeSTRef lsmr (LSMContent Map.empty ls') else writeSTRef lsmr (LSMContent wb' ls) @@ -531,9 +533,7 @@ data EventDetail = increment :: forall s. Tracer (ST s) Event -> Counter -> Run -> Levels s -> ST s (Levels s) increment tr sc = \r ls -> do - ls' <- go 1 [r] ls - invariant ls' - return ls' + go 1 [r] ls where go :: Int -> [Run] -> Levels s -> ST s (Levels s) go !ln incoming [] = do From 44a8cd4f491f4ed4cb10ff6e47803e3cd974cbf1 Mon Sep 17 00:00:00 2001 From: Matthias Heinzel Date: Tue, 20 Aug 2024 09:41:12 +0200 Subject: [PATCH 10/10] make assertions on LSM shape in prototype tests --- prototypes/ScheduledMerges.hs | 16 +++-- prototypes/ScheduledMergesTestQLS.hs | 104 ++++++++++++++++++++------- 2 files changed, 88 insertions(+), 32 deletions(-) diff --git a/prototypes/ScheduledMerges.hs b/prototypes/ScheduledMerges.hs index 4c12b41b9..a8ff2d435 100644 --- a/prototypes/ScheduledMerges.hs +++ b/prototypes/ScheduledMerges.hs @@ -655,14 +655,18 @@ dumpLevel (Level (MergingRun mp ml mr) rs) = do mrs <- readSTRef mr return (Just (mp, ml, mrs), rs) +-- For each level: +-- 1. the runs involved in an ongoing merge +-- 2. the other runs (including completed merge) representationShape :: [(Maybe (MergePolicy, MergeLastLevel, MergingRunState), [Run])] - -> [(Maybe (MergePolicy, MergeLastLevel, Either Int [Int]), [Int])] + -> [([Int], [Int])] representationShape = map $ \(mmr, rs) -> - ( fmap (\(mp, ml, mrs) -> (mp, ml, summaryMRS mrs)) mmr - , map summaryRun rs) + let (ongoing, complete) = summaryMR mmr + in (ongoing, complete <> map summaryRun rs) where summaryRun = runSize - summaryMRS (CompletedMerge r) = Left (summaryRun r) - summaryMRS (OngoingMerge _ rs _) = Right (map summaryRun rs) - + summaryMR = \case + Nothing -> ([], []) + Just (_, _, CompletedMerge r) -> ([], [summaryRun r]) + Just (_, _, OngoingMerge _ rs _) -> (map summaryRun rs, []) diff --git a/prototypes/ScheduledMergesTestQLS.hs b/prototypes/ScheduledMergesTestQLS.hs index 6fca07d4d..f1f1708d2 100644 --- a/prototypes/ScheduledMergesTestQLS.hs +++ b/prototypes/ScheduledMergesTestQLS.hs @@ -13,7 +13,7 @@ import Data.Proxy import Data.STRef import Control.Exception -import Control.Monad (replicateM_) +import Control.Monad (replicateM_, when) import Control.Monad.ST import Control.Tracer (Tracer (Tracer), nullTracer) import qualified Control.Tracer as Tracer @@ -26,7 +26,7 @@ import Test.QuickCheck.StateModel.Lockstep hiding (ModelOp) import qualified Test.QuickCheck.StateModel.Lockstep.Defaults as Lockstep import qualified Test.QuickCheck.StateModel.Lockstep.Run as Lockstep import Test.Tasty -import Test.Tasty.HUnit (testCase) +import Test.Tasty.HUnit (HasCallStack, testCase) import Test.Tasty.QuickCheck (testProperty) @@ -39,7 +39,6 @@ tests = testGroup "ScheduledMerges" [ testProperty "ScheduledMerges vs model" $ mapSize (*10) prop_LSM -- still <10s , testCase "regression_empty_run" test_regression_empty_run , testCase "merge_again_with_incoming" test_merge_again_with_incoming - , testCase "merge_again_with_incoming'" test_merge_again_with_incoming' ] prop_LSM :: Actions (Lockstep Model) -> Property @@ -73,17 +72,34 @@ test_regression_empty_run = del 1 del 2 del 3 + + expectShape lsm + [ ([], [4,4,4,4]) + ] + -- run 5, results in last level merge of run 1-4 ins 0 ins 1 ins 2 ins 3 + + expectShape lsm + [ ([], [4]) + , ([4,4,4,4], []) + ] + -- finish merge LSM.supply lsm 16 + expectShape lsm + [ ([], [4]) + , ([], [0]) + ] + -- | Covers the case where a run ends up too small for a level, so it gets -- merged again with the next incoming runs. --- That merge gets completed by supplying credits. +-- That 5-way merge gets completed by supplying credits That merge gets +-- completed by supplying credits and then becomes part of another merge. test_merge_again_with_incoming :: IO () test_merge_again_with_incoming = runWithTracer $ \tracer -> do @@ -93,35 +109,62 @@ test_merge_again_with_incoming = -- get something to 3rd level (so 2nd level is not levelling) -- (needs 5 runs to go to level 2 so the resulting run becomes too big) traverse_ ins [101..100+(5*16)] - -- get a very small run (4 elements) to 2nd level - replicateM_ 4 $ - traverse_ ins [201..200+4] - -- get another run to 2nd level, which the small run can be merged with - traverse_ ins [301..300+16] - -- complete the merge - LSM.supply lsm 32 --- | Covers the case where a run ends up too small for a level, so it gets --- merged again with the next incoming runs. --- That merge gets completed and becomes part of another merge. -test_merge_again_with_incoming' :: IO () -test_merge_again_with_incoming' = - runWithTracer $ \tracer -> do - stToIO $ do - lsm <- LSM.new - let ins k = LSM.insert tracer lsm k 0 - -- get something to 3rd level (so 2nd level is not levelling) - -- (needs 5 runs to go to level 2 so the resulting run becomes too big) - traverse_ ins [101..100+(5*16)] + expectShape lsm -- not yet arrived at level 3, but will soon + [ ([], [4,4,4,4]) + , ([16,16,16,16], []) + ] + -- get a very small run (4 elements) to 2nd level replicateM_ 4 $ traverse_ ins [201..200+4] + + expectShape lsm + [ ([], [4,4,4,4]) -- these runs share the same keys + , ([4,4,4,4,64], []) + ] + -- get another run to 2nd level, which the small run can be merged with traverse_ ins [301..300+16] - -- get 3 more to 2nd level, so the merge above is expected to complete - -- (actually more, as runs only move once a fifth run arrives...) - traverse_ ins [401..400+(6*16)] + expectShape lsm + [ ([], [4,4,4,4]) + , ([4,4,4,4], []) + , ([], [80]) + ] + + -- add just one more run so the 5-way merge on 2nd level gets created + traverse_ ins [401..400+4] + + expectShape lsm + [ ([], [4]) + , ([4,4,4,4,4], []) + , ([], [80]) + ] + + -- complete the merge (20 entries, but credits get scaled up by 1.25) + LSM.supply lsm 16 + + expectShape lsm + [ ([], [4]) + , ([], [20]) + , ([], [80]) + ] + + -- get 3 more runs to 2nd level, so the 5-way merge completes + -- and becomes part of a new merge. + -- (actually 4, as runs only move once a fifth run arrives...) + traverse_ ins [501..500+(4*16)] + + expectShape lsm + [ ([], [4]) + , ([4,4,4,4], []) + , ([16,16,16,20,80], []) + ] + +------------------------------------------------------------------------------- +-- tracing and expectations on LSM shape +-- -- | Provides a tracer and will add the log of traced events to the reported -- failure. @@ -140,6 +183,15 @@ instance Exception TracedException where displayException (Traced e ev) = displayException e <> "\ntrace:\n" <> unlines (map show ev) +expectShape :: HasCallStack => LSM s -> [([Int], [Int])] -> ST s () +expectShape lsm expected = do + shape <- representationShape <$> dumpRepresentation lsm + when (shape == expected) $ + error $ unlines + [ "expected shape: " <> show expected + , "actual shape: " <> show shape + ] + ------------------------------------------------------------------------------- -- QLS infrastructure --