The way I think about this is that many of the things that you might traditionally consider “system calls” are just special cases of sending a message to a kernel object using a capability. For example, the “system call” for changing the priority of a thread is actually implemented by sending a simple message (that includes the new priority) through a capability for the target thread (or rather, for the associated TCB object). Even sending a message to another thread by IPC is just a special case in which the capability you specify references an endpoint object (or a notification object, depending on which kind of IPC you are using). Libsel4 makes it easier to write user-level code that accesses these functions, but the implementations (including for things like seL4_Untype_Retype) are running in kernel space. One interesting detail is that, unless the user-level code has a hand in creating its own capability space, there is no general way for it to determine the types of the objects that it can access. For example, you might have code that you think is sending a “SetPriority” message to a thread, when in fact the object that it references is an endpoint whose messages are received and handled by another thread. So long as the latter provides a convincing simulation of a TCB object, the caller won’t notice a difference. This provides an interesting way to wrap additional functionality or restrictions around built-in kernel objects. I hope that helps! Best wishes, Mark [*] I used SetPriority as a simple example, but perhaps should mention that the real SetPriority message also requires a second TCB capability that provides the authority to change the first thread's priority.
On Sep 7, 2024, at 8:33 AM, tunacici7@gmail.com wrote:
I've recently started to learn seL4 by following the Tutorials, which have been great so far. I've been also reading the Manual & API reference to understand and gain insight into different mechanisms.
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.
Unfortunately, I couldn't find any answers to this question online. So that's why I'm asking it here. Maybe there are others who wonders the same thing.
NOTE The API Reference page confuses me even more. It lists Object Methods in its own category (instead of being under System Calls). Does this means Object Methods are NOT system calls? Or the term System Call is just not what I think it is(basically an endpoint to kernel)?. END NOTE
Thanks for the answers in advance. -T _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems