libsel4/riscv: avoid gcc 14.2 miscompilation

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>
This commit is contained in:
Gerwin Klein 2026-05-07 12:57:48 +02:00
parent 506f20d696
commit b62417a292

View file

@ -687,8 +687,8 @@ LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWaitWithMRs(seL4_CPtr dest, se
LIBSEL4_INLINE_FUNC void seL4_Yield(void)
{
register seL4_Word scno asm("a7") = seL4_SysYield;
asm volatile("ecall" :: "r"(scno));
riscv_sys_null(seL4_SysYield);
asm volatile("" ::: "memory");
}
#ifdef CONFIG_KERNEL_MCS