Indan Zupancic
Indan Zupancic
The main thing this achieves is reverting commit [3d2ae69f](https://github.com/seL4/seL4/commit/3d2ae69f9cb184c34b6b56d1365e57693e832db4) and fixing the underlaying delay problem properly. CAS can take very long to finish on ARM if the exclusive reservation granule...
Currently `c_entry_hook()` may be called without the kernel lock held and it accesses a global `ksEnter` when `CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES` or `CONFIG_BENCHMARK_TRACK_UTILISATION` is set. `c_exit_hook()` is usually called without lock held, but...
The code using ksCurTime assumes that ksCurTime is up-to-date, but this assumption is wrong for ksCurTime of other CPU cores. Those can be quite some time in the past. The...
updateTimestamp before taking kernel lock The intention of the MCS design is that updateTimestamp is performed as early in the kernel operation instruction stream as possible. Acquiring the lock can...
System calls are initiated by the currently running task, so charging them makes sense. The same is not true for interrupts, especially not the scheduling timer interrupt causing a context...
Replace `NODE_STATE_ON_CORE(ksCurTime)` calls with `NODE_STATE(ksCurTime)`. The code using ksCurTime assumes that `ksCurTime` is up-to-date, but this assumption is wrong for `ksCurTime` of other CPU cores. refill_new(), refill_ready(), refill_update() and refill_unblock_check()...
include/smp/ipi.h not only declares data, but also defines all IPI related global variables, while the file is included in multiple places. It works because all kernel code is combined into...
Notifications should influence scheduling as little as possible. Tasks woken up by notifications should not be put at the head of the release queue. Enqueue is used to optimise the...
Lazy FPU loading seems to work badly in combination with SMP and passive threads that use the FPU, as TCB migration should be fast. - Merge `Arch_migrateTCB` with `migrateTCB` and...
To limit WCET, `preemptionPoint()` is called to check if there is anything else to do. It returns `EXCEPTION_PREEMPTED` when IRQs are pending or when the current task runs out of...