Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Prototype: change credit scaling, using nominal vs physical credit #571

Open
wants to merge 7 commits into
base: main
Choose a base branch
from

Conversation

dcoutts
Copy link
Collaborator

@dcoutts dcoutts commented Feb 13, 2025

Previously we've had a somewhat complex method to scale credits from
those supplied in a level (1 per update) to the credits used in merging.

The existing scheme has a number of downsides:

  • no clear distinction between scaled and unscaled credits, what does
    each one measure?
  • complex, needs scaling dependent of the merge-policy
  • always uses worst case supply of credits so often finishes early
  • rounding errors compound problem of credit over-supply
  • no satisfactory way to check we do not over-supply credits
  • contributing credits to a merge from multiple handles will cause the
    merge to finish earlier than any of the handles needs it to finish,
    thus doing work more eagerly than necessary.

The new scheme involves:

  • distinguishing physical vs nominal credits, with a clear definition
    for each measure
  • converting between nominal and physical without merge policy
  • physical debt is no longer worst case but matches actual cost
  • integer rounding errors do not compound
  • we can assert that we reach the nominal and physical debt totals at
    the same moment (when the merge is done) and thus we can assert no
    over-supply of physical credits.
  • we can avoid supplying credits too quickly to a merge that is shared
    between multiple handles, each one only pushes it as far as it needs.

Consolidate it and move it before first use (in merging run).
Change it from tracking just the unspent credits and remaining debt to
tracking the spent and unspent credits and the total debt.

This makes it more similar to the tracking we do in the real
implementation. It also makes it easier to assert things: like the
supplied credit being less than the total debt.

And finally, we will need to know the total debt for the
nominal/physical credit scaling that we want to try out.
So we split out the merge debt (which never changes) and keep it in the
MergingRun, so that it is accessible directly and purely for both
ongoing and completed merges.

Previously the merge debt was only available for the OngoingMerge, not
the CompletedMerge, and one had to read the STRef MergingRunState to get
it.

We'll want to know the total merge debt directly to help simplify how we
supply credits.
Use a dedicated type that does not contain extranious information. There
will soon be even more extranious information that makes sense only for
merges within levels, and not within merging trees, so now is a good
time to separate it before it becomes too complex.

In particular there would be no sensible way to generate the
unneccessary information for property tests.
Previously we've had a somewhat complex method to scale credits from
those supplied in a level (1 per update) to the credits used in merging.

The existing scheme has a number of downsides:
* no clear distinction between scaled and unscaled credits, what does
  each one measure?
* complex, needs scaling dependent of the merge-policy
* always uses worst case supply of credits so often finishes early
* rounding errors compound problem of credit over-supply
* no satisfactory way to check we do not over-supply credits
* contributing credits to a merge from multiple handles will cause the
  merge to finish earlier than any of the handles needs it to finish,
  thus doing work more eagerly than necessary.

The new scheme involves:
* distinguishing physical vs nominal credits, with a clear definition
  for each measure
* converting between nominal and physical without merge policy
* physical debt is no longer worst case but matches actual cost
* integer rounding errors do not compound
* we can assert that we reach the nominal and physical debt totals at
  the same moment (when the merge is done) and thus we can assert no
  over-supply of physical credits.
* we can avoid supplying credits too quickly to a merge that is shared
  between multiple handles, each one only pushes it as far as it needs.
Copy link
Collaborator

@mheinzel mheinzel left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice.

prototypes/ScheduledMerges.hs Outdated Show resolved Hide resolved
prototypes/ScheduledMergesTest.hs Outdated Show resolved Hide resolved
prototypes/ScheduledMerges.hs Outdated Show resolved Hide resolved
@dcoutts dcoutts force-pushed the dcoutts/merge-credits-scaling branch from 702031b to 0487ec5 Compare February 13, 2025 15:32
@dcoutts
Copy link
Collaborator Author

dcoutts commented Feb 13, 2025

@mheinzel PR review applied in two extra patches. If you think that's good now then I'll squash and merge.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants