Hello T, "Object methods" are just system calls in the technical sense, they are fully executed in kernel mode. You can find the (generated) syscall numbers in your build directory: build/libsel4/include/sel4/syscall.h It's generated from libsel4/include/api/syscall.xml by a script. The start will look something like: typedef enum { seL4_SysCall = -1, seL4_SysReplyRecv = -2, seL4_SysSend = -3, seL4_SysNBSend = -4, seL4_SysRecv = -5, seL4_SysReply = -6, seL4_SysYield = -7, seL4_SysNBRecv = -8, (The rest is either debug-only or platform dependent.) The "object methods" are a seL4_SysCall on a cap of a specific type. ("Call" in the seL4 sense of doing a send + wait for reply, not to be confused with "syscall".) The call will be decoded depending on the cap's type, and that object's handling code will check the invocation number to see what you want to do. To avoid doing the wrong thing when passing a cap of the wrong type, all invocations have a unique number: build/libsel4/include/sel4/invocation.h This two-tiered numbering system makes it easier to quickly handle IPC seL4_SysCalls. Capabilities in seL4 are a bit like file descriptors in other OSes: A generic interface to do things with specific "objects", via a few standardised system calls (read, write versus recv and send). In the end it's all semantics. If you are confused how the kernel knows whether you are calling a method on the endpoint object or sending a message to another task: That's solved by endpoints not having any methods to call. Same trick is used for notifications. I hope that clears things up. Greetings, Indan On 2024-09-09 13:19, tunacici7@gmail.com wrote:
Think I'm starting to understand this. My current understanding of a syscall is operations like read(), write() or mkdir() are implemented in the kernel. So they are executed at a higher execution level (e.g., Ring 0 in x64, EL1 in ARM64) and each have their own syscall numbers. Most user applications don't directly invoke them, but rather use a libc wrapper with the same syscall name.
In seL4, this idea is a bit different. The kernel itself handles send+receive and yield (and also their variations) syscalls inside the kernel at a higher execution level. Object methods are implemented using those syscalls inside libsel4. Which executes at a lower execution level (e.g., Ring 4, EL0).
Here I am, again, a little bit confused. Sorry. When I looked at the source and did some debugging I see that, as an example, UntypedRetype is implemented in libsel4 (sel4_client.h) Like you, and others, said it is implemented using send+receive system calls. So, everything is good so far. But, what about their syscall numbers you have mentioned that have been vectored for efficiency? I was not able to find them in the source (both after and before system call stub generation). I looked inside syscall.h after syscall_header_gen.py.
I'm sure I'm missing something or my understanding of what a syscall needs more work.
Thanks for the previous answers. It motivated me to debug an application (a tutorial) and see how parts of libsel4 is actually implemented. -T