Gerwin Klein

Nice find. Do you have a test case that fails before and passes after?

Ignore my ramblings. We do want the scheduler to always be called on unicore, so this is fine -- it already is being called, I just misread the diff.

> Agree with @jearc. This might not currently break anything, however, IMO it is assumed that the scheduler is called under the protection of the BKL. We should make this...

The proof test fails, which means this will need a (hopefully trivial) proof update before it can get merged.

This sounds like a fairly big change, so it would need funding to verify. In particular changes like a new object binding sound expensive. Notification binding was one of the...

Maybe slightly pedantic, but the distinction between object and cap to object is not only theoretical, it's more than hat. In a mental model where you invoke the object, not...

> > if you think of the delete operation as being invoked on an object, that would have to mean that the object immediately disappears and the memory can be...

> Right now I don't think there is actually any restriction on building an SMP kernel for a platform, even if there is only one CPU defined in the DTS....

The same is present in [gicv2.c](https://github.com/seL4/seL4/blob/49f4ddfc8c20249b7a114a4cc3baa42f5f9eaa6c/src/arch/arm/machine/gic_v2.c#L37)

This one I have slightly less hope for -- it's likely that we'd have to go deep into the guts of `simp` to prevent it from instantiating schematics and changing...