James Archer

> Can the kernel check what prio is running on the destination core? It would be good to only interrupt if the migrating thread should actually preempt what's currently running...

> The problem I have with this solution is that conceptually it doesn't make sense: `ksCurThread` should always be running on the current core. This fix relies on `SCHED_ENQUEUE_CURRENT_TCB`/`SCHED_APPEND_CURRENT_TCB` being...

> I believe that schedule should only be concerned with scheduling on the current core, and should not be involved with cross-core scheduling at all, neither directly or indirectly. I...

I could be wrong about this but I don't think there is a problem. On non-MCS, if `NODE_STATE(ksSchedulerAction) == SchedulerAction_ResumeCurrentThread` then `schedule()` and `activateThread()` won't do anything. The scheduler action...

What is the rationale for vendoring liburing instead of adding it as a submodule? (I'm not sure we have a rationale for why we do this for lwip.)

>It's really only our dependencies that should be submodules, since they update so often. Anything that in the long-term doesn't change much such as lwIP, MicroPython or liburing can just...

One issue is that while inputting ^C will kill executions that wait for IO, it won't do anything for executions that don't. Example: Inputting ^C will kill ``` async def...

> Since this will make simulation and hardware tests fail, could you make corresponding PR in `sel4test` (which we won't merge) that removes the `const` qualifier from the test schedule...