Hello T, Great to hear it clicked! Now that you understand this, I'd like to mention that seL4 kernel "objects" are not as clear-cut as they seem. This is currently not very well explained in the manual and only something you will run into when actually using seL4, mostly manifesting as peculiar limitations. The straightforward kernel objects are the ones that need to be allocated with seL4_Untyped_Retype(): Those store their state in the allocated memory and you get access to it via a cap. You usually can do anything you would expect with caps to such objects, like moving and copying them around. There is a clear distinction between the object and the cap that grants access to it. However, some "objects" don't require any state, so they don't need any memory. For these having a cap is enough. Caps to such "objects" are always passed on to the rootserver. Examples are IRQControl, ASIDControl and Domain caps. If they are used to create other "objects" (e.g. IRQHandles, ASIDPools), then usually it's not allowed to copy the caps, as they are needed to keep track of the created derived caps. Here the line between objects and caps gets fuzzy, in a sense there are no objects as such, just caps that grant the right to perform certain system actions. Other objects have very little state and store that state in their cap. Examples are SchedControl and IRQhandler. If that state is read-only, like core or IRQ number, then there are no limitations on what you can do with those caps. If it is writeable state, then you usually can't copy the cap. Lastly, there are the tricky objects: Those that require both memory and also keep state in their cap. Examples are Untyped, VSpace, PageTable and Page. Because of this caps to these objects have peculiar properties and restrictions: Untyped caps can be copied, but only if it is empty and no derived object have been created yet, because the state can only be kept up-to-date in one place. VSpace related caps can be copied and need a copy per mapping, because the mapping information is stored in the cap and there is only enough space to store one mapping. I'd like to improve the manual to make the above clearer, but not sure how to approach it. Call everything an object, even if it doesn't require state? Does that make things clearer or more confusing? The manual sidesteps the issue by not really mentioning it at all currently. Or call everything a resource and only resources that require storage objects? Or call the stateless ones kernel services and make an explicit list of them? But in a sense it's an implementation detail whether something needs state and whether that fits in the cap or not, so why call it differently? Greetings, Indan On 2024-09-10 19:17, tunacici7@gmail.com wrote:
Hey Indan,
After reading your (and others) words, it finally clicked for me! Like you (and others) have said in seL4 all interaction are done by invoke objects via capabilities.
It sounds obvious at first (many resources talk about this), but understanding is another story:)
In case there are others like me that are still having a problem understanding system calls and object methods in seL4, I have collected my thoughts below.
System call is, in a more "traditional" sense, in other OSes is like this: - execute 'syscall' with a specific system call number from the user space - there are many syscall numbers defined in those OSes (e.g., read, write, mkdir)
In seL4, however, it's a bit different: - still execute 'syscall' from the user space - but this time only Send, Recv, Yield (and other variations) have their syscall numbers defined - those are the only "system calls" that we can directly compare to other "traditional" OSes - now, in handling of the system calls (e.g., Send()) there is a decoder (see 'decodeInvocation(...)') - those decoders determine which specific capability to invoke (see 'libsel4/include/interfaces/sel4.xml' for all invocations) - each of the invocations have their own numbers (similar to system call numbers) - so (like Indan have said) we have a two-tiered system (first is architecture/CPU 'syscall' and second is seL4 'invocations') - because of this we have a separation in API reference between System Calls and Object Methods - and since object methods (like UntypedRetype) are handled inside the seL4 they are executed at higher privilege level
Again, thanks everyone for the help & replies.
-T