-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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
Switch the default allocation policy to best-fit. #10188
Merged
Merged
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -108,7 +108,7 @@ type control = | |
percentage of the memory used for live data. | ||
The GC will work more (use more CPU time and collect | ||
blocks more eagerly) if [space_overhead] is smaller. | ||
Default: 80. *) | ||
Default: 100. *) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Should this also be changed from 100 to 120? @damiendoligez? |
||
|
||
mutable verbose : int; | ||
[@ocaml.deprecated_mutable "Use {(Gc.get()) with Gc.verbose = ...}"] | ||
|
@@ -164,30 +164,23 @@ type control = | |
memory than both next-fit and first-fit. | ||
(since OCaml 4.10) | ||
|
||
The current default is next-fit, as the best-fit policy is new | ||
and not yet widely tested. We expect best-fit to become the | ||
default in the future. | ||
The default is best-fit. | ||
|
||
On one example that was known to be bad for next-fit and first-fit, | ||
next-fit takes 28s using 855Mio of memory, | ||
first-fit takes 47s using 566Mio of memory, | ||
best-fit takes 27s using 545Mio of memory. | ||
|
||
Note: When changing to a low-fragmentation policy, you may | ||
need to augment the [space_overhead] setting, for example | ||
using [100] instead of the default [80] which is tuned for | ||
next-fit. Indeed, the difference in fragmentation behavior | ||
means that different policies will have different proportion | ||
of "wasted space" for a given program. Less fragmentation | ||
means a smaller heap so, for the same amount of wasted space, | ||
a higher proportion of wasted space. This makes the GC work | ||
harder, unless you relax it by increasing [space_overhead]. | ||
Note: If you change to next-fit, you may need to reduce | ||
the [space_overhead] setting, for example using [80] instead | ||
of the default [100] which is tuned for best-fit. Otherwise, | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. And this |
||
your program will need more memory. | ||
|
||
Note: changing the allocation policy at run-time forces | ||
a heap compaction, which is a lengthy operation unless the | ||
heap is small (e.g. at the start of the program). | ||
|
||
Default: 0. | ||
Default: 2. | ||
|
||
@since 3.11.0 *) | ||
|
||
|
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Just as a data point, in the systems I have tested, 120 has been notably faster without a measurably significant increase in memory usage.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
To concur, Coq sets 200 with the best-fit, and when I asked they seemed happy with it, so 120 is not shocking.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
At 200, memory use can increase significantly, but 120 seems like a good trade-off.
According to some measurements of the two (see https://blog.janestreet.com/memory-allocator-showdown/), best-fit at 100 has similar performance to next-fit at 80 while using less memory. This means that the gains from switching to best-fit are entirely allocated to reducing memory use, while at 120 the gains are split between reducing memory use and reducing time spent.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(Personally I think that the setting of 200 for Coq was a bit too aggressive. It is a very memory-hungry program, and while everyone is able to wait 10% longer to get their proof to complete, your machine may not necessarily be able to give 10% more memory to the process. I think this hard-limit behavior of memory would suggest a more conservative default, but I guess heavy Coq-users don't have the same perspective as they bought large-memory machines anyway.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree with @gasche: let's have default values that don't waste too much memory, because running out of memory and starting to swap is very costly indeed.