[seL4] Re: General Question On Object Methods

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

...

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,

...

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 Wednesday, September 11, 2024, Gernot Heiser via Devel wrote:

...

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

Hi Indan, yes source code is available, but people is not reading source code of a "standard" system, so just reading it, even if the most accurate way to know what's going on (this is how anyone will do it for Linux Kernel, in example) in the specific case of seL4, can be a bit frustrating, as most things we know about OS here do not apply. To be more clear, for anyone comming from Linux Kernel, seL4 is an alien... :-) And yes, door is open to read the code, that's why is open source. Sure. But I talk about another kind of door, the one of understanding how things work, maybe, with that medium level description you mention, really I don't know. Please don't misunderstand me 🙏, I'm not telling seL4 is opaque, it's Open Source, that's wonderful! I'm just telling that maybe having access to source code and the technical manual, is not enougth to the average seL4 newbie engineer. You guys do an amazing job. Manpower is probably the "problem". I know. I really know. Ok, step by step. On Thursday, September 12, 2024, Indan Zupancic wrote: the they the

...

Microkit?

...

Gernot