While working on formal verification of cache coloring and page coloring mechanisms in Bao, we discovered two possible optimizations in function pp_alloc_clr. Here is the first optimization.
The outer loop (currently line 123 in commit 7448c66 in file src/core/mmu/mem.c) performs two search iterations:
- the first one starting from
pool->last until the end of the pool, and
- the second one starting from the beginning of the pool until the end of the pool.
A proposed optimization would be to stop the second search iteration if the required set of pages does not start before pool->last. Indeed, since a required set of pages starting at or after pool->last was not found during the first iteration, it cannot be found in that part of the pool during the second iteration.
We will propose a pull request with this optimization.
We were able to prove a (slightly simplified) corrected version of cache coloring and page coloring mechanisms in Bao with our optimizations. Many thanks to Axel Amestoy who performed the verification of the optimized version.
While working on formal verification of cache coloring and page coloring mechanisms in Bao, we discovered two possible optimizations in function
pp_alloc_clr. Here is the first optimization.The outer loop (currently line 123 in commit 7448c66 in file src/core/mmu/mem.c) performs two search iterations:
pool->lastuntil the end of the pool, andA proposed optimization would be to stop the second search iteration if the required set of pages does not start before
pool->last. Indeed, since a required set of pages starting at or afterpool->lastwas not found during the first iteration, it cannot be found in that part of the pool during the second iteration.We will propose a pull request with this optimization.
We were able to prove a (slightly simplified) corrected version of cache coloring and page coloring mechanisms in Bao with our optimizations. Many thanks to Axel Amestoy who performed the verification of the optimized version.