On 8 Sep 2024, at 01:33, tunacici7@gmail.com wrote:
However, I have one fundamental question: Are the object methods system calls?
It is said that seL4 only has 3 logical system calls: Send, Recv and Yield. (In all the slides, videos and other documents I have seen) And the rest is just variations of those ones. But what about object methods? Are they system calls? Are they executed in kernel space?
If they are system calls, then wouldn't all the resources out there be misleading? Since there are way more than just Send, Recv and Yield. If they are not, then how are they handled? Does 'libsel4' have anything to do with it? I can't imagine 'seL4_Untype_Retype' executing in user space.
In a pure capability system, the only operation is invoking an object (though its cap). In seL4, objects are invoked by sending and receiving from them. In fact, they are really invoked by call() (i.e. send+receive). In addition there’s yield(), which is a (arguably unprincipled) special case. Everything (other than yield) is a method invocation on an object. That’s why my slides say that *logically* there are only 3 syscalls. The implementation vectors them onto separate (per-object) syscall numbers for efficiency. Gernot