Gerwin Klein

Turns out this is a bit more complex in the proofs. We specifically introduced this case 6 years ago in ba78e3b (and forgot to update the manual), because we were...

>> But if we're doing such big breaking changes, the whole init functions could be cleared up. Currently there is way too much overlap between seL4_TCB_Configure, seL4_TCB_SetSpace and seL4_TCB_SetSchedParams. The...

This is in the merge queue after #1435

Reopening this, but removing it from the release. The situation is now safe from the kernel perspective, but we should still check for stale mapping info in all configs --...

> 1. I am under the impression that seL4 should not have nested exceptions (in normal operation). Yes, that is correct. There should be no faults at all generated while...

> Is there a more up to date version of https://sel4.systems/Info/Docs/seL4-spec.pdf anywhere? (even just a single platform is useful, because there is arch-independent things). There currently isn't but there probably...

Squashed the commits as discussed on MM. Have a look if you're happy with the commit message.

Interesting, the not-excessive assert fails on x64. Can you have a look if x64 is wasting memory or if it actually needs the larger size?

> I'm going to be annoying and say that `intStateIRQNode` doesn't need to be power-of-two. It absolutely does have to be. > Yes, it's kind of a CNode, and yes,...

> That might affect the proofs (one would hope) but I can't see the equivalent proof code for x86 as there is for arm/riscv. Yes, it will affect them, hopefully...