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

Change default MR page size behaviour #238

Merged
merged 1 commit into from
Oct 30, 2024
Merged

Commits on Oct 30, 2024

  1. Change default MR page size behaviour

    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]>
    Ivan-Velickovic committed Oct 30, 2024
    Configuration menu
    Copy the full SHA
    5b0b54a View commit details
    Browse the repository at this point in the history