Gerwin Klein

The numbers are encouraging. I think we still need to run it in the JFlex context (i.e. a full scanner loop) to make sure, because it might influence cache-locality etc,...

Happy to put this at the top of the list, although I don't think makes sense as a standard setting. Going from 4.0 to 4.6 is significant slowdown for one...

Good point, we should definitely add this to the benchmark suite and see what it does in context. If it's provided as an option, I'm less worried about the performance...

> The code changes seem like a big improvement overall. Could this be also done for other architectures and have a unified page table API for all supported architectures? In...

> I'm terribly sorry, I confused "page mapping" with "page table mapping". I thought you also unified page caps with page table caps. > > So everywhere I said page...

[RFC-10] is now approved, so this PR can go out of draft mode and be reviewed for merge. [RFC-10]: https://sel4.atlassian.net/browse/RFC-10?atlOrigin=eyJpIjoiNWRkNTljNzYxNjVmNDY3MDlhMDU5Y2ZhYzA5YTRkZjUiLCJwIjoiZ2l0aHViLWNvbS1KU1cifQ

To be honest, that condition would be very handy to have in verification. If there are no performance impacts from it, I'd be all for it.

@kent-mcleod and @pingerino do you see any potential problems with that?

This is one of these things where the philosophy of seL4 clashes with mainstream PC use. You can't gain actual security without knowing what hardware your are running on precisely,...

Hotplug of memory and CPU is definitely out of scope for seL4 at this time. We started with speculative execution mitigations -- ultimately these are just performance optimisations: you can...