Hello!

While looking at the code base and checking generated code, I'm not sure about the pertinence of having a different ABI from user System V ABI for kernel calls, as it is implying a bit more unnecessary register shuffling, and I was wondering why this choice was made to have r10, r8, r9, r15? instead of keeping System V ABI and just replace rcx by r10 as it is discarded by syscall:

SystemVABI_x86_64_user: rdi, rsi, rdx, rcx, r8, r9

SystemVABI_x86_64_Linux_kernel: rdi, rsi, rdx, r10, r8, r9

SystemVABI_x86_64_seL4: rdi, rsi, r10, r8, r9, r15

So on a Linux Kernel, only the register rcx will be transferred to r10 (when transitioning from user to syscall), but in seL4, it has to reshuffle arguments rdx to r9.

(Note for context: I'm working on a project where I don't use a standard C compiler to interface with the seL4 Kernel API, and where the register allocator of the compiler might not be as efficient as GCC/CLang after everything is inlined, that's why I'm looking into these details)