On 9/7/24 18:33, Gernot Heiser via Devel wrote:

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

Are faults (which, obviously, do not require any capabilities) another way to communicate with other code? -- Sincerely, Demi Marie Obenour (she/her/hers)

Think I'm starting to understand this. My current understanding of a syscall is operations like read(), write() or mkdir() are implemented in the kernel. So they are executed at a higher execution level (e.g., Ring 0 in x64, EL1 in ARM64) and each have their own syscall numbers. Most user applications don't directly invoke them, but rather use a libc wrapper with the same syscall name. In seL4, this idea is a bit different. The kernel itself handles send+receive and yield (and also their variations) syscalls inside the kernel at a higher execution level. Object methods are implemented using those syscalls inside libsel4. Which executes at a lower execution level (e.g., Ring 4, EL0). Here I am, again, a little bit confused. Sorry. When I looked at the source and did some debugging I see that, as an example, UntypedRetype is implemented in libsel4 (sel4_client.h) Like you, and others, said it is implemented using send+receive system calls. So, everything is good so far. But, what about their syscall numbers you have mentioned that have been vectored for efficiency? I was not able to find them in the source (both after and before system call stub generation). I looked inside syscall.h after syscall_header_gen.py. I'm sure I'm missing something or my understanding of what a syscall needs more work. Thanks for the previous answers. It motivated me to debug an application (a tutorial) and see how parts of libsel4 is actually implemented. -T

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

On 11 Sep 2024, at 07:02, Hugo V.C. wrote:

Thanks T. Having this in a documentation would be nice to improve seL4 learning curve. I really appreciated reading all the explanations, but this T summary is very helpful, like the few really important things an experienced skydiver say to beginners to increase their self confidence.

I don’t think tutorials on microkernels and capabilities belong into the seL4 kernel documentation. However, the white paper could be more explicit about this, I’ll think about that. (I guess the white paper is due for an upgrade anyway, given that the Microkit is now the preferred way for building seL4-based systems.) Incidentally, I yesterday delivered my first Advanced OS lecture for the year, and I had strengthened the explanation of cap invocation, see - p16ff of https://cgi.cse.unsw.edu.au/~cs9242/24/lectures/01a-intro.pdf - p4 of https://cgi.cse.unsw.edu.au/~cs9242/24/lectures/01b-sel4.pdf Gernot

On 12 Sep 2024, at 06:41, Hugo V.C. wrote:

"I don’t think tutorials on microkernels and capabilities belong into the seL4 kernel documentation"

Sure. I have no idea how you guys can deal with this... I'm on the commercial side, just thinking about how people can "easily" become seL4 developer…

How is this affected by low-level technical details that are hidden behind libraries, especially if you use higher-level frameworks such as the Microkit? Gernot

Hello Hugo, The thing is, to fully understand how things work on a low level you can read the seL4 source, it's not that much, it's open and available to everyone. And it's really the best way to find out specific details. So the door is wide open already. People are welcome to ask questions to increase their understanding of how seL4 works, that's how this thread started. Perhaps it's nice to have a medium level description of how seL4 works on a technical level, but it will always describe someone's personal mental model, and will always be a simplification, hence slightly incorrect for some corner cases. However, the seL4 manual is not the place for such info, it's strength is exactly its terseness. Its goal is to give an overview of seL4, if there is too much detail that overview becomes lost and the manual becomes huge and not easily readable any more. The information should be limited to what the user needs to know when using sel4. Giving too much details too early only leads to confusion, people need to build a mental model of how seL4 works first and then they can adjust it when learning more. We can add more information to the website, feel free to open a pull request or open an issue to request specific documentation. I agree that there is so much more to say about seL4, but manpower is limited. Greetings, Indan On 2024-09-11 23:15, Hugo V.C. wrote:

Well, people usually like to understand how things work, moreover on a system like seL4. And, whether you like or not, there will be forks, hacks, modifications... the more info you provide, the more involved the community will be.

Frameworks are a must to speed up real life adoption, but ideally, all the low level info must be clear and the easier the better.

I used to pentest an RTOS derivative of VxWorks on top of some Marvel Armada cpus, at the beginning with public very abstract info, but the fun came when I got (legit) access to confidential low level cpu specs of the different models... then I undestood why some fault injection attacks were being successful.

Developers can do their job with just Mikrokit, but many of them, will have curiosity to understand why they need to do things the way they are forced. By being able to fully understand how things really work at low level, they get more involved, they can also contribute with improvements, and, hopefully, they will be happier than just blindly trust.

It's about letting the door open to developers and engineers to learn at deeper level, as easy as possible.

Maybe a door some people will never open, but for those who dare to open, would be nice to be sure they get engaged.

...

On 12 Sep 2024, at 06:41, Hugo V.C. wrote:

...

"I don’t think tutorials on microkernels and capabilities belong into

...

...

Sure. I have no idea how you guys can deal with this... I'm on the

commercial side, just thinking about how people can "easily" become seL4 developer…

How is this affected by low-level technical details that are hidden behind libraries, especially if you use higher-level frameworks such as

On Wednesday, September 11, 2024, Gernot Heiser via Devel wrote: the seL4 kernel documentation" the Microkit?

...

Gernot

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