sel4 and compilation with/without optimisation

[Alexander Boettcher]

Hello,

On 02.01.22 21:01, Alexander Tormasov via users wrote:
> Gcc with any optimisation level do drop this code because original function which
> call x86_flush_rsb (c_handle_vmexit) does not used at all and being removed
> during optimisation.
> 
> So, if you during debug add something like CFLAGS= as an env or make variable with -O0 - you are doomed!
> 
> this is true for current 10.3 and previous 9 gcc compilers…
> This is not a part of genode code while problem happens in port sources [2]. I am not even sure how I can post an issue.
> 
> [1] https://gcc.gnu.org/onlinedocs/gcc/Simple-Constraints.html#Simple-Constraints
> [2] contrib/sel4-9ab19376285d865052c2b5021560306306bf19a8/src/kernel/sel4/include/arch/x86/arch/machine.h
> [3] https://lists.genode.org/pipermail/users/2020-August/007193.html

on Genode you can steer resp. override the optimization level using CC_OLEVEL as whole by defining it in build/<arch>/etc/tools.conf or within
your component specifically. For OKL4 and NOVA, e.g., we force the optimization level to the known working ones, just grep to find the places in the sources.

For seL4 we don't do that, maybe it is worth to force here also the optimization level to the "good" ones. I would
suggest to look into [0][1][2], depending on your architecture.

[0] repos/base-sel4/lib/mk/spec/arm/kernel-sel4.inc
[1] repos/base-sel4/lib/mk/spec/x86_32/kernel-sel4-pc.mk
[2] repos/base-sel4/lib/mk/spec/x86_64/kernel-sel4-pc.mk

Beside that, you would/will need to discuss and patch seL4 sources and get them upstream. Once we update to a newer seL4 version, we would get your changes automatically.

Cheers,

-- 
Alexander Boettcher
Genode Labs

https://www.genodians.org - https://www.genode.org