Skip to content

Commit 1bb5aac

Browse files
committed
tighten invariants
1 parent 15f5ee3 commit 1bb5aac

File tree

1 file changed

+16
-7
lines changed

1 file changed

+16
-7
lines changed

prototypes/ScheduledMerges.hs

Lines changed: 16 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -203,10 +203,13 @@ invariant = go 1
203203
expectedMergingRunLengths ln mr mrs ls =
204204
case mergePolicyForLevel ln ls of
205205
MergePolicyLevelling ->
206+
assert (mergeLastForLevel ls == MergeLastLevel) $
206207
case (mr, mrs) of
207208
-- A single incoming run (which thus didn't need merging) must be
208209
-- of the expected size range already
209-
(SingleRun r, CompletedMerge{}) ->
210+
(SingleRun r, m) -> do
211+
assertST $ case m of CompletedMerge{} -> True
212+
OngoingMerge{} -> False
210213
assertST $ levellingRunSizeToLevel r == ln
211214

212215
-- A completed merge for levelling can be of almost any size at all!
@@ -216,20 +219,26 @@ invariant = go 1
216219
assertST $ levellingRunSizeToLevel r <= ln+1
217220

218221
-- An ongoing merge for levelling should have 4 incoming runs of
219-
-- the right size for the level below, and 1 run from this level,
222+
-- the right size for the level below (since we know that that level
223+
-- must use tiering), and 1 run from this level,
220224
-- but the run from this level can be of almost any size for the
221225
-- same reasons as above. Although if this is the first merge for
222226
-- a new level, it'll have only 4 runs.
223227
(_, OngoingMerge _ rs _) -> do
224-
assertST $ length rs == 4 || length rs == 5
225-
assertST $ all (\r -> tieringRunSizeToLevel r == ln-1) (take 4 rs)
226-
assertST $ all (\r -> levellingRunSizeToLevel r <= ln+1) (drop 4 rs)
228+
let incomingRuns = take 4 rs
229+
let residentRuns = drop 4 rs
230+
assertST $ length incomingRuns == 4
231+
assertST $ length residentRuns <= 1
232+
assertST $ all (\r -> tieringRunSizeToLevel r == ln-1) incomingRuns
233+
assertST $ all (\r -> levellingRunSizeToLevel r <= ln+1) residentRuns
227234

228235
MergePolicyTiering ->
229236
case (mr, mrs, mergeLastForLevel ls) of
230237
-- A single incoming run (which thus didn't need merging) must be
231238
-- of the expected size already
232-
(SingleRun r, CompletedMerge{}, _) ->
239+
(SingleRun r, m, _) -> do
240+
assertST $ case m of CompletedMerge{} -> True
241+
OngoingMerge{} -> False
233242
assertST $ tieringRunSizeToLevel r == ln
234243

235244
-- A completed last level run can be of almost any smaller size due
@@ -277,7 +286,7 @@ newMerge tr level mergepolicy mergelast rs = do
277286
mergeCost = cost,
278287
mergeRunsSize = map Map.size rs
279288
}
280-
assert (let l = length rs in l >= 2 && l <= 5) $
289+
assert (length rs `elem` [4, 5]) $
281290
MergingRun mergepolicy mergelast <$> newSTRef (OngoingMerge debt rs r)
282291
where
283292
cost = sum (map Map.size rs)

0 commit comments

Comments
 (0)