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 Wednesday, September 11, 2024, Gernot Heiser via Devel
<devel@sel4.systems> wrote:
On 12 Sep 2024, at 06:41, Hugo V.C. <skydive...@gmail.com> 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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
