Gerwin Klein

I actually like the solution here, because it makes IRQ enabling and notification setting atomic and gets us nice semantics. I have the feeling we probably would have done this...

Good to see the old domain tests failing -- that means we're actually doing something :). This should disappear once we've updated sel4test accordingly.

> * [ ] Rename `DomainSetSet` to `DomainSet`? Given that the change is only breaking if you are using the kernel API directly, we should at least have a deprecation...

I was wondering why the RPi5 was suddenly so clean compared to the other ones.. If you leave them out now, we definitely need prominent pointers to what is missing...

The only problem can I see is that the compiler no longer warns you if you are using an invocation label that the current config does not support. If we're...

> Normally the solution for that would be to use an anonymous union. That would mean changing `seL4_UserContext`, wrap all existing fields in an unnamed union and add an union...

> Surely that's a long-term project that will take years. That doesn't mean we should let the code diverge from the verification subset. We've just spent extra work last year...

Agreed, this whole thing will need an overhaul when there is a RISC-V hardware platform that does support more than one ASID and we want to run seL4 on it....

(Planning this for after the release, I need to concentrate on fixing the proof first)

No, SGI is fine and enabled by default. The problem is that the prover sees different code when different config options are set and the preprocess test must check all...