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 <[email protected]
<mailto:[email protected]>> 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
<[email protected]
<mailto:[email protected]>> 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
On 03/07/15 10:19, Wink Saville wrote:
> 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
<[email protected] <mailto:[email protected]>
<mailto:[email protected] <mailto:[email protected]>>> 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 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
<[email protected] <mailto:[email protected]>
<mailto:[email protected] <mailto:[email protected]>>> wrote:
>
> Will do.
>
>
> On Mon, Jun 29, 2015, 7:05 PM Anna Lyons
<[email protected] <mailto:[email protected]>
> <mailto:[email protected]
<mailto:[email protected]>>> 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
> [email protected]
> https://sel4.systems/lists/listinfo/devel
>
>
>
> _______________________________________________
> Devel mailing list
> [email protected]
> 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
[email protected]
https://sel4.systems/lists/listinfo/devel
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
