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
_______________________________________________
Genode users mailing list
[email protected]
https://lists.genode.org/listinfo/users
