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