Re: [seL4] Try two for libsel4 not having a dependency on libc

4 Jul 2015


      Whoops, here
https://github.com/winksaville/sel4-min-sel4/tree/no-libc-dependency is
the correct link, the link in the previous message was older.


On Fri, Jul 3, 2015 at 3:39 PM Wink Saville  wrote:
...
Here
https://github.com/winksaville/sel4-min-sel4/tree/no-libc-using-libsel4_gen
is another try, there are now separate libs for printf, putchar and assert
plus some new simple apps. The app myassert shows overriding of the assert
methods, here is the commit message:
libsel4 without dependencies on libc.
There are now separate libs for benchmark, assert, printf and putchar:
libs/libsel4_benchmark
      libs/libsel4_assert
      libs/libsel4_printf
      libs/libsel4_putchar
And some simple test apps:
apps/test-newlibs -> test simple things
      apps/min-app -> Does nothing, just retuns 0
      apps/hw -> tests putchar
      apps/helloworld -> tests printf
      apps/assert -> tests seL4_Asserts ..
      apps/myassert -> tests that we can override _seL4_AssertFail ..
      apps/bootinfo -> tests that we can access seL4_BootInfo
The primary changes are introducing sel4_types.h and removing std*
types
    plus porting assert and IO code from the kernel to libsel4_assert
    and libsel4_printf, libsel4_putchar.
This means the code within libraries do not overload any typical libc
    entities. Instead the libraries use types like seL4_Uint32 ... instead
of
    uint32_t. And printf is now seL4_Printf and assert is seL4_Assert ....
Finally, the only file modified that effects kernel code is
    kernel/tools/bitfield_gen.py. It needed to be modified as it generates
    files for both kernel and user space. And for user space the generated
code
    (types_gen.h) needed to use the new types and asserts. The changes
should
    not change what is generated for the kernel and I did a comparison of
    kernel_final.{c|s} before and after my change and the only differences
    were time stamps.
On Thu, Jul 2, 2015 at 9:47 PM Adrian Danis 
wrote:
...
My main problem with this change remains bringing in all of this IO
implementation into the C library. As far as I can tell all of the putchar,
printf, varargs, halt etc is introduced just to support assertions. Why not
rely on the user system to provide the actual assertion implementation,
allowing all of the I/O code to be moved out of this library?
i.e. define assert to something like
#ifdef NDEBUG
#define libsel4_assert(x) (void)0
#else
#define libsel4_assert(x) ((void)((x) || (__assert_fail(#x, __FILE__,
__LINE__, __func__),0)))
#endif
void __assert_fail (const char *, const char *, int, const char *);
And then rely on the user code to provide an implementation of
__assert_fail, which if they are linking against the muslc library is
already provided.
Adrian
On 03/07/15 13:11, Wink Saville wrote:
@Harry,
I'll fix the comment.
Using print_string is a good idea, I'll look into how to create a
string with __FILE__, __LINE__, __func__ at compile time rather than
runtime, maybe just using paste ("#") will work.
I guess my feeling is asserts should work without the user having to do
extra steps, so there should be a default one in any case. Also, I believe
it can be overridden at link time by the user supplying their own
implementation.
On using "assert 0" to eliminate duplicate code, do you mean eliminate
"_seL4_Fail" and just have "_seL4_AssertFail"?
On Thu, Jul 2, 2015 at 7:52 PM Wink Saville  wrote:
...
Moving sel4_benchmark.h into libsel4 was something I was thinking we
might do. I'm thinking longer maybe it could significantly expand and
possibly have supporting c sources so that's why I kept it separate for now.
On using error rather than message, NP, I chose message because I didn't
want to always force people to change the configuration, but maybe that
would be error is better.
Some what related, I've chosen to always assume putchar would be
available in some configurations, so I created
sel4_debug_printf.h/sel4_debug_assert.h which uses NDEBUG to conditionally
turn off/on asserts and printf. Where as sel4_printf.h/sel4_assert.h
assumes putchar would always be available. So this a different behavior
then previously and people may not like it.
As I said, still quite a bit to discuss and of course, the main one: is
having libsel4 independent of libc something that's desirable? Which,
obviously you don't think it is, but others seem to like it, so we'll see
what happens.
 -- Wink
On Thu, Jul 2, 2015, 5:25 PM Matthew Fernandez <
matthew.fernandez@nicta.com.au> wrote:
...
Though I'm still opposed to this change overall, my two cents on the
current state:
- Should we just put the benchmarking code in libsel4bench [0]? I
realise the former is for
benchmarking the kernel and the latter is (arguably) for benchmarking
userspace, but it seems to me
a better home for it.
- You've used `#pragma message` in one instance. I would prefer
`#error` for consistency, though
I'm aware `#pragma message` is more portable. Moreover, why are we
emitting messages here in the
first place? It's a perfectly valid (in fact the default) configuration
to have the benchmarking
syscalls disabled.
[0]: https://github.com/seL4/libsel4bench
...
One other note, this isn't done. It still needs to be integrated with
muslc (libc) and at a minimum
seL4_Halt needs to be properly implemented. And I'm sure there will
be plenty of other changes
needed but I hope we're closer.
On Thu, Jul 2, 2015 at 5:11 PM Wink Saville mailto:wink@saville.com> wrote:
Here https://github.com/winksaville/sel4-min-sel4/tree/no-libc3
is try #3, I've pasted the
    commit message below as it tells the story, let me know what you
On 03/07/15 10:19, Wink Saville wrote:
think:
...
libsel4 with no libc dependency.
         The primary changes are introducing sel4_types.h and
removing std* types
...
plus porting assert and printf code from the kernel to
libsel4. All of
...
this means the code within libsel4 does not overload any
typical libc
...
entities. So now libsel4 uses types like seL4_Uint32 ...
instead of
...
uint32_t. And printf is now seL4_Printf and assert is
seL4_Assert ....
...
I'm also using sel4_ prefixes for various files as I felt it
was more
...
consistent with the names of the entities within the files.
         The only new library is libsel4_benchmark and since it
consists of just
...
sel4_benchmark.h we might want to move that back into
libsel4. I would
...
have liked to move out libsel4_assert, libsel4_printf and
libsel4_putchar
...
but since asserts are used by low level generated code I
couldn't come up
...
with a good way of doing that.
         Finally, the only file modified that effects kernel code is
         kernel/tools/bitfield_gen.py. It needed to be modified as it
generates
...
files for both kernel and user space. And for user space the
generated code
...
(types_gen.h) needed to use the new types and asserts. The
changes should
...
not change what is generated for the kernel and I did a
comparison of
...
kernel_final.{c|s} before and after my change and the only
differences
...
were time stamps
-- Wink
On Mon, Jun 29, 2015 at 7:07 PM Wink Saville 
mailto:wink@saville.com> wrote:
...
Will do.
On Mon, Jun 29, 2015, 7:05 PM Anna Lyons <
Anna.Lyons@nicta.com.au
...
mailto:Anna.Lyons@nicta.com.au> wrote:
Hi,
>
             > Currently there is at least one known problem, I
modified
...
> bitfield_gen.py so types_gen.h has no asserts since at
the moment the
...
> kernel uses assert and userspace is libsel4_assert. We
could either do
...
> something like I've done and remove them or change the
kernel to use
...
> libsel4_assert or something else.
             >
The asserts are really important to avoid horrible bugs
when using
...
functions created by the bitfield generator, so if we go
ahead with this
...
let's make sure they survive in some form.
Cheers,
            Anna.
________________________________
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
_______________________________________________
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 listDevel@sel4.systemshttps://sel4.systems/lists/listinfo/devel