Hi Norman,
On 24/06/15 19:33, Norman Feske wrote:
Hello Matthew,
I don't have any objection to minimal systems and probably no one who
works on microkernels does. Personally I think implementing a C
application without including libc is signing yourself up to
re-implement libc, but if you're OK with that than fair enough.
this is exactly the case for Genode. For the same reasons the seL4
kernel is not linked against a libc, it makes sense to avoid the
dependency of certain other system components from a libc. I.e.,
components that are in a similarly critical position as the kernel such
as the root task or multi-level components. From my point of view, the
following considerations come into play:
First, TCB complexity. The inclusion of a libc taints the respective
component with hundreds of thousand lines of additional code. For a
critical component, this code needs to undergo a thorough evaluation.
Granted, most of the libc code remains practically unused but the
assessment of the portions of the used code is not simple either. If not
using the libc in the first place, it can be simply left out of the
evaluation.
I don't disagree with these points, but a more preferable structure for me is
to factor this out into a minimal, trusted
libc*. We did this for a previous project involving a separation kernel
architecture. There was some doubt in my mind at
the time about this approach, but in retrospect this felt like the right way.
It gave us a complete C library (Musl)
during development and debugging and then a completely pared down TCB for
release. This means that, e.g., you never end
up re-implementing things like assert and printf that you don't need for
release.
* Maybe even a verified one ;) http://ssrg.nicta.com.au/students/summer.pml
Second, in my opinion, the libc interface is not well aligned with
modern microkernels but ridden with legacy. File handles, file
permissions, POSIX signals, anonymous memory allocations, side effects
come in mind. The libc thereby imposes many notions on the runtime
environment that are not desired for all components. E.g., the
expectation of re-entrant mutexes, pthread TLS, or POSIX priorities. By
making the libc mandatory for all user-level components, those quirky
semantics must be carried along at the lowest level to avoid breaking
the expectations of the API users.
Yes, I can't argue with those points. However, for better or worse libc and
POSIX have become common things C
programmers know and come to expect. This is more an argument for their utility
during development though, rather than
their use in the syscall stubs.
Cheers,
Matt
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
