On 8 Sep 2024, at 01:33, tunaci...@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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems

Reply via email to