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, tunaci...@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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
