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.