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.

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.

For these reasons, we deliberately exclude a libc from low-level Genode
components. While doing that, we observed that we did, in fact, *not*
re-implement most of the libc functionality. For meaningful components
like our GUI server, user-level networking components, device drivers,
or our root task, 99% of the libc would remain unused anyway. The
"re-implementation" of the desired libc features turned out to be a
non-issue really. These are a few string functions and memory
management. Because we use C++, our "re-implementation" is able to
benefit from a decent type system and templates. In fact, the entire
Genode API is self-sustaining (no dependency from either libc or the
standard C++ library) and its implementation comprises only about 15,000
lines of C++ code. A mandatory dependency from a libc would spoil that
figure. ;-)

I do not question the value of a libc (or the standard C++ library) in
general. Many applications greatly benefit from it. But I think that
programs that don't benefit from it should be able to live without it.

For my work on bringing Genode to seL4, I encountered the very issue
that Wink is addressing with his patch. I had to "emulate" the few parts
of the libc that are expected by the seL4 bindings:


https://github.com/genodelabs/genode/tree/master/repos/base-sel4/include/sel4

I would have preferred bindings that use headers and types that are
differently named than those of a libc. By using disjoint names, the
seL4 bindings could be used in a free-standing way. But they could also
be combined with a real libc without the need for shadowing header
files. Instead of creating stubs for libc headers as done by Wink's
patch, I would avoid the inclusion of any libc header. The bindings
could include a single "bindings ABI" header that supplies the few types
and definitions that are expected by the bindings but are specific for
the used tool chain or user-level environment. Each environment (RefOS,
Genode, ...) could then supply a different version of this single header
file.

Cheers
Norman

-- 
Dr.-Ing. Norman Feske
Genode Labs

http://www.genode-labs.com · http://genode.org

Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth

_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to