Change default MR page size behaviour #238
Merged
Conversation
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
Before this patch, we would default to the platform's smallest page size if it is not explicitly set on a memory region. However, I have noticed that users of Microkit (including myself) often forget that you can specify the page size of memory region yourself and so if you have a very large memory region, it is much more efficient to use say, 2MB pages, instead of 4K pages. From this experience, I believe that it is worthwhile to change the default behaviour to select the larget possible page size for the memory region that does not lead to any memory waste. For example, if you have a 4MB sized MR, 2MB page sizes would be used. If you have a 4.1MB sized MR, 4K page sizes would be used. I cannot think of any reasonable use-case with Microkit currently where people would be relying on this implicit default behaviour. Signed-off-by: Ivan-Velickovic <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Before this patch, we would default to the platform's smallest page size if it is not explicitly set on a memory region.
However, I have noticed that users of Microkit (including myself) often forget that you can specify the page size of memory region yourself and so if you have a very large memory region, it is much more efficient to use say, 2MB pages, instead of 4K pages.
From this experience, I believe that it is worthwhile to change the default behaviour to select the larget possible page size for the memory region that does not lead to any memory waste. For example, if you have a 4MB sized MR, 2MB page sizes would be used. If you have a 4.1MB sized MR, 4K page sizes would be used.
I cannot think of any reasonable use-case with Microkit currently where people would be relying on this implicit default behaviour.