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)