sel4bench
sel4bench copied to clipboard
Improved page mapping benchmarks
The existing page mapping benchmarks only appear to be implemented for x86 platforms. In this PR, I have extended the benchmarks to work on AARCH64 and fixed a bug with the protect benchmark, which would result in the same page being protected repeatedly instead of protection being applied to all of the pages in the range. I have also modified the CMake to be more explicit that this benchmark is currently only supported on x86 and AARCH64.
Because of the changes to vspace mapping in https://github.com/seL4/seL4/pull/801, the logic for preparing the page tables is quite different on AARCH64 compared to x86_64, which retains the design of unique kernel objects for each level of the page table. Because it is not obvious if a page table mapping succeeding means that the lowest level page table required for mapping a small page exists, I repeatedly map page tables for an address until the mapping operation fails with seL4_DeleteFirst
, indicating that the page table has already been completely filled in for this address. Not sure if this is the ideal way of doing this and I can change it to do something else if not.