Matt, I've guarded the definitions with conditionals to try to avoid that, but maybe a better option might be to use different names completely. Also, we could test for compatibility at compile time and generate errors. My rational for wanting this is that libc doesn't seem to be providing that much value as very few of its vsyscalls are implemented anyway. Thus its utility is actually small, IMHO. Also, I happen to be interested in minimal systems so unused and extraneous code is an anathema. Here, in libsel4, by adding these few LOC's we are removing "thousands" of LOC brought in by the need of a libc. Anyway, I'd certainly like to keep the discussion going to revisit the the earlier decision, I just feel strongly the less code the better. On Tue, Jun 23, 2015, 12:02 AM Matthew Fernandez < matthew.fernandez@nicta.com.au> wrote:

Hi Wink,

As you've observed in that commit, removing the libc dependency leads you to re-implement pieces of it inline. We used to do something similar to this, but replaced this with an explicit dependency on libc to avoid complications with multiple definitions of typedefs and such. In the case of programmer error, these typedefs may not match and if the conflicting typedefs are never seen within the same translation unit your compiler will not notice either. The end result was subtle bugs arising from ABI incompatibility.

When we made the change, out rationale was that anyone using the syscall stubs would have libc available anyway. This certainly introduces a circular dependency, but it's not easy to remove without repeating parts of one library in the other or playing tricks with externs and weak symbols. In my experience, all of this is more fragile and less preferable than living with the circular dependency. However, my opinion may not be universally shared as we haven't had a discussion about this for some time.

Cheers, Matt

...

I noticed that seL4/libsel4 was dependent upon libc and so I created a

On 23/06/15 11:16, Wink Saville wrote: patch

...

( https://github.com/winksaville/seL4/commit/fc91a1f68c054fdb41aaa42a7b56a80f4...) which removes the dependency. If there is interest I can submit a pull request, and of course will make any changes deemed necessary to make it suitable for acceptance.

Please advise,

Wink

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

________________________________

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.

Thanks for the comments, I'll fix assert and create a pull request so additional discussions can be in the github project. On Tue, Jun 23, 2015, 5:08 AM Matthew Fernandez < matthew.fernandez@nicta.com.au> wrote:

Hi Wink,

The guards you've used look sufficient (though it's mildly concerning that any poor user who received your libsel4's assert.h before libc's has their asserts unconditionally become no-ops). We also previously explored the option of using different typedef names, but felt it led to unnecessary confusion when reading the stubs. I'm not debating whether these things can be checked for at compile time, but IMHO the necessary checks in a large build system are more complex than one might initially imagine.

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. I'm not opposed to the idea behind this proposal, of removing the libsel4->libc dependency, but since I am unlikely to be the one maintaining it, I'll leave it to others to make a call on whether to go in this direction.

Cheers, Matt

...

Matt,

I've guarded the definitions with conditionals to try to avoid that, but maybe a better option might be to use different names completely. Also, we could test for compatibility at compile time and generate errors.

My rational for wanting this is that libc doesn't seem to be providing

...

implemented anyway. Thus its utility is actually small, IMHO. Also, I happen to be interested in minimal systems so unused and extraneous code is an anathema. Here, in libsel4, by adding

...

LOC brought in by the need of a libc.

Anyway, I'd certainly like to keep the discussion going to revisit the

On 23/06/15 21:03, Wink Saville wrote: that much value as very few of its vsyscalls are these few LOC's we are removing "thousands" of the earlier decision, I just feel strongly the

...

less code the better.

On Tue, Jun 23, 2015, 12:02 AM Matthew Fernandez < matthew.fernandez@nicta.com.au mailto:matthew.fernandez@nicta.com.au> wrote:

Hi Wink,

As you've observed in that commit, removing the libc dependency leads you to re-implement pieces of it inline. We used to do something similar to this, but replaced this with an explicit dependency on libc to avoid complications with multiple definitions of typedefs and such. In the case of programmer error, these typedefs may not match and if the conflicting typedefs are never seen within the same translation unit your compiler will not notice either. The end result was subtle bugs arising from ABI incompatibility.

When we made the change, out rationale was that anyone using the syscall stubs would have libc available anyway. This certainly introduces a circular dependency, but it's not easy to remove without repeating parts of one library in the other or playing tricks with externs and weak symbols. In my experience, all of this is more fragile and less preferable than living with the circular dependency. However, my opinion may not be universally shared as we haven't had a discussion about this for some time.

Cheers, Matt

On 23/06/15 11:16, Wink Saville wrote: > I noticed that seL4/libsel4 was dependent upon libc and so I created a patch > ( https://github.com/winksaville/seL4/commit/fc91a1f68c054fdb41aaa42a7b56a80f4...) which removes the dependency. If > there is interest I can submit a pull request, and of course will make any changes deemed necessary to make it suitable > for acceptance. > > Please advise, > > Wink > > > _______________________________________________ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel >

________________________________

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.

libc support is important and desirable in many contexts, but simplicity is important too. if libsel4 can be made to not depend upon libc I believe that is an advantage. Anyway, I've created a pull request (https://github.com/seL4/seL4/pull/14) which allows seL4test on the qemu x86 pc99 simulation (make simulate-ia32) to continue to pass. Please review and add comments there if you're interested. On Tue, Jun 23, 2015 at 6:27 PM Tom Mitchell wrote:

One important aspect of the C library is that it covers and bridges two universes. One is the system call interface to the kernel. A micro kernel needs more bridging. Second are features and functions for common programming activities and manipulation of common data structures.

http://www.gnu.org/software/libc/manual/pdf/libc.pdf

The common things like math libraries and more string handling... pattern matching. Things like users and groups are possibly a do not care on a sensor but math and binary to character conversions have value. Users, groups and permissions are the framework for security.... Filesystem code in the kernel enforcers access as well as maintaining data to blocks on disk mappings but could be done in user space.

One working model to inspect this is the Cygwin project that builds on a Windows foundation and gives the programer a Unix like API. https://www.cygwin.com/ Look to see how differences in the Windows model and Unix (posix) model are managed and errors handled.

A key part is error handling.

On Tue, Jun 23, 2015 at 8:18 AM, Wink Saville wrote:

...

Thanks for the comments, I'll fix assert and create a pull request so additional discussions can be in the github project.

On Tue, Jun 23, 2015, 5:08 AM Matthew Fernandez < matthew.fernandez@nicta.com.au> wrote:

...

Hi Wink,

The guards you've used look sufficient (though it's mildly concerning that any poor user who received your libsel4's assert.h before libc's has their asserts unconditionally become no-ops). We also previously explored the option of using different typedef names, but felt it led to unnecessary confusion when reading the stubs. I'm not debating whether these things can be checked for at compile time, but IMHO the necessary checks in a large build system are more complex than one might initially imagine.

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. I'm not opposed to the idea behind this proposal, of removing the libsel4->libc dependency, but since I am unlikely to be the one maintaining it, I'll leave it to others to make a call on whether to go in this direction.

Cheers, Matt

...

Matt,

I've guarded the definitions with conditionals to try to avoid that, but maybe a better option might be to use different names completely. Also, we could test for compatibility at compile time and generate errors.

My rational for wanting this is that libc doesn't seem to be providing

...

implemented anyway. Thus its utility is actually small, IMHO. Also, I happen to be interested in minimal systems so unused and extraneous code is an anathema. Here, in libsel4, by adding

...

LOC brought in by the need of a libc.

Anyway, I'd certainly like to keep the discussion going to revisit the

...

less code the better.

On Tue, Jun 23, 2015, 12:02 AM Matthew Fernandez < matthew.fernandez@nicta.com.au mailto:matthew.fernandez@nicta.com.au> wrote:

Hi Wink,

As you've observed in that commit, removing the libc dependency leads you to re-implement pieces of it inline. We used to do something similar to this, but replaced this with an explicit dependency on libc to avoid complications with multiple definitions of typedefs and such. In the case of

On 23/06/15 21:03, Wink Saville wrote: that much value as very few of its vsyscalls are these few LOC's we are removing "thousands" of the earlier decision, I just feel strongly the programmer error, these typedefs may not match and if the

...

conflicting typedefs are never seen within the same translation

unit your compiler will not notice either. The end

...

result was subtle bugs arising from ABI incompatibility.

When we made the change, out rationale was that anyone using the

syscall stubs would have libc available anyway. This

...

certainly introduces a circular dependency, but it's not easy to

remove without repeating parts of one library in the

...

other or playing tricks with externs and weak symbols. In my

experience, all of this is more fragile and less preferable

...

than living with the circular dependency. However, my opinion may

not be universally shared as we haven't had a

...

discussion about this for some time.

Cheers, Matt

On 23/06/15 11:16, Wink Saville wrote: > I noticed that seL4/libsel4 was dependent upon libc and so I

created a patch

...

> (

https://github.com/winksaville/seL4/commit/fc91a1f68c054fdb41aaa42a7b56a80f4...) which removes the

...

dependency. If > there is interest I can submit a pull request, and of course

will make any changes deemed necessary to make it

...

suitable > for acceptance. > > Please advise, > > Wink > > > _______________________________________________ > Devel mailing list > Devel@sel4.systems > https://sel4.systems/lists/listinfo/devel >

________________________________

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 Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

-- T o m M i t c h e l l _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

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

On 23 June 2015 at 08:02, Matthew Fernandez wrote:

When we made the change, out rationale was that anyone using the syscall stubs would have libc available anyway. This certainly introduces a circular dependency, but it's not easy to remove without repeating parts of one library in the other or playing tricks with externs and weak symbols. In my experience, all of this is more fragile and less preferable than living with the circular dependency. However, my opinion may not be universally shared as we haven't had a discussion about this for some time.

There are many cases where you may want syscalls and not libc, for example several programming languages use direct bindings not bindings via libc (eg Go). I am interested in porting a different libc, and while the bits needed may well be ABI compatible it is hard to tell. So I would much rather the syscall stubs could be used standalone without a libc. Justin