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/sel... 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