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)
My mistake, I double checked and the convention is actually the same, just r15 is an additional register for mr3:
sys, dst,info, mr0, mr1, mr2, mr3 syscall x86_64_seL4: rdi, rsi, rdx, r10, r8, r9, r15
As sys is usually a constant, I shifted the registers when inspecting the codegen. So all is good, my apologize for the noise. Happy new year! ________________________________ From: Devel devel-bounces@sel4.systems on behalf of Alexandre Mutel alexandre_mutel@live.com Sent: Sunday, December 29, 2019 12:14 To: devel@sel4.systems devel@sel4.systems Subject: [seL4] Understand seL4 x86_64 Kernel ABI calling convention
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)
-
Alexandre Mutel