Issue #755: fix the bug in maxPhysicalDebt and invariant

The prototype had a bug in the calculation of `maxPhysicalDebt` where it was not
considering that incoming runs that are inputs to a merge can be overfull. Runs
can be overfull because we hold back runs that are underfull. However, runs
should only be overfull in the sense that they are too large for their current
level. They can't be overfull with respect to the next level too.

This same bug occurred in `invariant`, where a similar change was made to
consider overfull runs properly.

Some other minor changes to `invariant` were made to make the checked invariant
a little more precise.

Author: jorisdral

src-prototypes/ScheduledMerges.hs

@@ -353,7 +353,7 @@ invariant conf@LSMConfig{..} (LSMContent _ levels ul) = do
         -- levelling run becomes too large and is promoted, in that case
         -- initially there's no merge, but it is still represented as an
         -- 'IncomingRun', using 'Single'. Thus there are no other resident runs.
-        MergePolicyLevelling -> assertST $ null rs
+        MergePolicyLevelling -> assertST $ null rs && null ls
         -- Runs in tiering levels usually fit that size, but they can be one
         -- larger, if a run has been held back (creating a (T+1)-way merge).
         MergePolicyTiering   -> assertST $ all (\r -> runToLevelNumber MergePolicyTiering conf r `elem` [ln, ln+1]) rs
@@ -383,18 +383,19 @@ invariant conf@LSMConfig{..} (LSMContent _ levels ul) = do
             (_, CompletedMerge r) ->
               assertST $ runToLevelNumber MergePolicyLevelling conf r <= ln+1
 
-            -- An ongoing merge for levelling should have T incoming runs of
-            -- 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 T runs.
+            -- An ongoing merge for levelling should have T incoming runs of the
+            -- right size for the level below (or slightly larger due to holding
+            -- back underfull runs), and at most 1 run from this level. 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 T runs.
             (_, OngoingMerge _ rs _) -> do
               assertST $ length rs `elem` [configSizeRatio, configSizeRatio + 1]
               assertST $ all (\r -> runSize r > 0) rs  -- don't merge empty runs
               let incoming = take configSizeRatio rs
               let resident = drop configSizeRatio rs
               assertST $ all (\r -> runToLevelNumber MergePolicyTiering conf r `elem` [ln-1, ln]) incoming
+              assertST $ length resident `elem` [0, 1]
               assertST $ all (\r -> runToLevelNumber MergePolicyLevelling conf r <= ln+1) resident
 
         MergePolicyTiering ->
@@ -421,13 +422,19 @@ invariant conf@LSMConfig{..} (LSMContent _ levels ul) = do
             (_, CompletedMerge r, MergeMidLevel) ->
               assertST $ runToLevelNumber MergePolicyTiering conf r `elem` [ln-1, ln, ln+1]
 
-            -- An ongoing merge for tiering should have T 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).
+            -- An ongoing merge for tiering should have T incoming runs of the
+            -- right size for the level below (or slightly larger due to holding
+            -- back underfull runs), 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 _, _) -> do
-              assertST $ length rs == configSizeRatio || length rs == configSizeRatio + 1
-              assertST $ all (\r -> runToLevelNumber MergePolicyTiering conf r == ln-1) rs
+              assertST $ length rs `elem` [configSizeRatio, configSizeRatio + 1]
+              assertST $ all (\r -> runSize r > 0) rs  -- don't merge empty runs
+              let incoming = take configSizeRatio rs
+              let heldBack = drop configSizeRatio rs
+              assertST $ all (\r -> runToLevelNumber MergePolicyTiering conf r `elem` [ln-1, ln]) incoming
+              assertST $ length heldBack `elem` [0, 1]
+              assertST $ all (\r -> runToLevelNumber MergePolicyTiering conf r == ln-1) heldBack
 
 -- We don't make many assumptions apart from what the types already enforce.
 -- In particular, there are no invariants on the progress of the merges,
@@ -1499,15 +1506,24 @@ newLevelMerge tr conf@LSMConfig{..} level mergePolicy mergeType rs = do
     -- such that we pay off the physical and nominal debts at the same time.
     --
     -- We can bound the worst case physical debt: this is the maximum amount of
-    -- steps a merge at this level could need. Note that for levelling this is
-    -- includes the single run in the current level.
+    -- steps a merge at this level could need. See the
+    -- 'expectedMergingRunLengths' where-clause of the 'invariant' function for
+    -- the full reasoning.
     maxPhysicalDebt =
       case mergePolicy of
         MergePolicyLevelling ->
-          configSizeRatio * levelNumberToMaxRunSize MergePolicyTiering conf (level-1)
+          -- Incoming runs, which may be slightly overfull with respect to the
+          -- previous level
+          configSizeRatio * levelNumberToMaxRunSize MergePolicyTiering conf level
+              -- The single run that was already on this level
             + levelNumberToMaxRunSize MergePolicyLevelling conf level
         MergePolicyTiering   ->
-          length rs * levelNumberToMaxRunSize MergePolicyTiering conf (level-1)
+          -- Incoming runs, which may be slightly overfull with respect to the
+          -- previous level
+          configSizeRatio * levelNumberToMaxRunSize MergePolicyTiering conf level
+              -- Held back run that is underfull with respect to the current
+              -- level
+            + levelNumberToMaxRunSize MergePolicyTiering conf (level - 1)
 
 -------------------------------------------------------------------------------
 -- MergingTree abstraction