Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Streamline kernel/libsel4 and remove its libc dependencies #15

Closed
winksaville opened this issue Jul 9, 2015 · 1 comment
Closed

Streamline kernel/libsel4 and remove its libc dependencies #15

winksaville opened this issue Jul 9, 2015 · 1 comment

Comments

@winksaville
Copy link
Contributor

Currently libsel4 has support for more than just interfacing to the kernel, it should be simplified and also it would be desirable to not require libc to use libsel4. The current libc (musl) contains support for many system calls not provided by seL4, one example is thread creation and there are other features, such as capabilities which musl will not likely ever support.

Therefore not having libsel4 depend upon libc can significantly reduce the amount of code needed for some uses of seL4. See this thread (http://sel4.systems/pipermail/devel/2015-June/000391.html) for some additional discussion.
@winksaville winksaville changed the title Streamline kernel/libsel4 and remove libc dependencies Streamline kernel/libsel4 and remove its libc dependencies Jul 9, 2015
winksaville added a commit to winksaville/seL4 that referenced this issue Jul 9, 2015
@winksaville
Streamline libsel4 and remove its libc dependencies.
9eb6b58 
There are now separate libs for benchmark, assert, printf, putchar
start/stop:

      libs/libsel4benchmark
      libs/libsel4assert
      libs/libsel4printf
      libs/libsel4putchar
      libs/libsel4startstop

The primary changes are introducing sel4/sel4.h and removing std* types
plus porting assert and IO code from the kernel to libsel4assert,
libsel4printf, libsel4putchar.

This means the code within libsel4 and the newlibs 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.

Bug: seL4#15 Streamline kernel/libsel4 and remove its libc dependencies
winksaville added a commit to winksaville/seL4 that referenced this issue Jul 10, 2015
@winksaville
Streamline libsel4 and remove its libc dependencies.
e653f8f 
There are now separate libs for benchmark, assert, printf, putchar
start/stop:

      libs/libsel4benchmark
      libs/libsel4assert
      libs/libsel4printf
      libs/libsel4putchar
      libs/libsel4startstop

The primary changes are introducing sel4/sel4.h and removing std* types
plus porting assert and IO code from the kernel to libsel4assert,
libsel4printf, libsel4putchar.

This means the code within libsel4 and the newlibs 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.

Bug: seL4#15 Streamline kernel/libsel4 and remove its libc dependencies
@winksaville winksaville mentioned this issue Jul 10, 2015
Merged
@winksaville
Copy link
Contributor Author

Superseded by #16

pingerino pushed a commit that referenced this issue Jan 11, 2016
@AdrianDanis
Merge pull request #15 in SEL4/sel4 from ~ADANIS/sel4:libsel4 to master
dc3e0d4 
* commit '5271925ba54639b849261e652e73ab56ee243fb2':
  libsel4: Always usage IPC buffer for invocations (SELFOUR-381)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@winksaville