mirror of
https://github.com/seL4/seL4.git
synced 2026-05-12 17:16:20 +00:00
b62417a292
a7 is not changed by seL4_Yield, so the original declaration is correct. However, in some loops GCC 14.2 may drop the load to a7 if a7 or memory are not declared as clobbered in the assembly block. This is a problem if *other* code does write to a7. For some reason GCC 14.2 does not recognise those other loads. GCC 14.3 and GCC 15 both work as expected. The problem manifests in SCHED0011 in sel4test. This change works around the GCC 14.2 problem because GCC 14.2 is the standard Debian trixie compiler and it is likely that people will hit the problem even if we say that GCC 14.2 should not be used. The workaround uses the same implementation of seL4_Yield as the Arm and x86/x64 versions do: inline call to sys_null with an empty asm volatile declaring memory as clobbered. The memory clobber declaration eliminates the miscompilation, and overall the implementations are now consistent. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>