Indan Zupancic

Correct. People usually configure it via `NUM_NODES`, but that's not a good excuse to not have a help text. `KernelMaxNumNodes > 1` means SMP is enabled. The current kernel boot...

> Some kind of pre-seL4 boot loader can be coded to detect the number of cores The kernel could do this itself too. But that doesn't solve the case where...

I know what you meant. > Then, still I don´t get what's the engineering limitation for "But there is no other way to communicate the desired number of cores to...

The only ISB that are really necessary are the ones that are done when the FPU is disabled and the kernel needs to do operations that require the FPU to...

> which means that an ISB before the kernel modifying FPU registers would also work. Yes. But... > This might penalise some FPU switching (e.g. if the state is touched...

> > This might penalise some FPU switching (e.g. if the state is touched multiple times) but would be easy to confirm correct, plus it would never penalise the non-fpu-touchy...

Agreed. That's why I'm not too keen on slowing down the already slow FPU switching case. ``` TX1 test results (init-build.sh -DFASTPATH=TRUE -DHARDWARE=TRUE -DFAULT=TRUE -DAARCH64=TRUE -DPLATFORM=tx1) All mentioned changes are...

> It seems to me that Call+ReplyRecv (which is what really counts) is faster than "now" in all scenarios "seL4_Call (FPU)" is important too, as that shows the cost of...

> When switching FPU contexts, why is the second ISB needed for an out-of-order cpu? I was thinking about checking whether the FPU is enabled according to the system register....

> Configure Arm HYP to always enable the FPU for EL2 and drop all ISBs, if possible. For Aarch64 this seems possible for both non-HYP and HYP. Aarch32 is probably...