Devel

devel@sel4.systems

9 participants
1390 discussions

Streamline seL4/libsel4 and make it not depend on libc
by Wink Saville 10 Jul '15

10 Jul '15

I've got sel4test running with libsel4 not having a dependency on libc. I've pulled out libsel4assert, libsel4benchmark, libsel4printf and libsel4putchar from libsel4 and they are separate libraries The biggest change is to seL4/libsel4 and sel4/tools/bitfield_gen.py. The changes to bitfield_gen.py allow it to generate the same code as before for the kernel but uses the new names for entities in user space. Please let me know what you think. -- Wink https://github.com/winksaville/seL4/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4test/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4allocman/tree/libsel4-no-libc-depende… https://github.com/winksaville/libsel4utils/tree/libsel4-no-libc-dependency https://github.com/winksaville/sel4test/tree/libsel4-no-libc-dependency https://github.com/winksaville/libsel4assert https://github.com/winksaville/libsel4benchmark https://github.com/winksaville/libsel4printf https://github.com/winksaville/libsel4putchar

4 11

can IPC be concurrent running?
by Pei.XiLong(裴喜龙) 07 Jul '15

07 Jul '15

Hi, We can get the definition of IPCBuffer from here https://github.com/seL4/seL4/blob/master/libsel4/arch_include/arm/sel4/arch… enum { seL4_GlobalsFrame = 0xffffc000, }; It is fixed in one virtual space, that means the IPC in seL4's thread cann't be concurrent, we can't prepare more than 1 IPC request at the same time, for we call these function: seL4_SetTag, seL4_SetMR, seL4_SetUserData wil use this buffer, but there is no locker to protect the buffer. Is my understanding correct? Xilong Pei Tongji University 2015/7/6

1 0

Where is the definition of seL4_TCB_BindAEP and seL4_TCB_UnbindAEP?
by XilongPei(裴喜龙) 07 Jul '15

07 Jul '15

Hi, In test program binding.c https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/b inding.c , there are two functions, seL4_TCB_BindAEP and seL4_TCB_UnbindAEP, where can I get their definitions? Xilong Pei Tongji University 2015/7/6

2 1

Try two for libsel4 not having a dependency on libc
by Wink Saville 04 Jul '15

04 Jul '15

Here <https://github.com/winksaville/sel4-min-sel4/tree/new-libs> is a different approach for removing the libc dependency, it seemed like people thought libsel4 was to big and that as part of the effort of breaking the dependency it should be made smaller. Basically libsel4 does nothing expect satisfy dependency needed for the kernel for some xml files. And I've broken libsel4 into basically 8 other libraries. see here <https://github.com/winksaville/sel4-min-sel4/tree/new-libs/libs>. This maybe taking things to far, but it does mean people can use only what they need, which I like. The smallest example is app/min-hw which only uses libsel4_gen, libsel4_startup. libsel4_bootinfo and libsel4_putchar. At the other extreme apps/test-newlibs uses everything. Anyway other organizations are certainly possible. 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. Anyway, before creating a pull request I'd like to know what people think. -- Wink

4 12

Who can give me a sample program using sel4platsupport_new_io_ops
by XilongPei(裴喜龙) 01 Jul '15

01 Jul '15

Hi, sel4platsupport_new_io_ops is defined in libsel4platsupport/include/sel4platsupport/io.h , it creates a new implementation of the platsupport io_ops interface using a provided simple, vspace and vka, Here is its protocol: /* * @param simple Simple interface for getting the physical frames * @param vspace VSpace interface to use for mapping * @param vka VKA interface for allocating any extra objects or cslots * @param io_ops Interface to fill in * * @return returns 0 on success */ int sel4platsupport_new_io_ops(simple_t simple, vspace_t vspace, vka_t vka, ps_io_ops_t *io_ops); Who can give me a sample program using this function? I guess it will be used in I/O DMA program, but I don't know much about DMA program. Xilong Pei Tongji University 2015/7/1

1 0

Make seL4/libsel4 not depend upon libc
by Wink Saville 29 Jun '15

29 Jun '15

I noticed that seL4/libsel4 was dependent upon libc and so I created a patch ( https://github.com/winksaville/seL4/commit/fc91a1f68c054fdb41aaa42a7b56a80f…) 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

6 11

How to edit RefOS libs c file
by ぷ风过无痕?? 22 Jun '15

22 Jun '15

Hi, I am using RefOS to develop a small applicaiton(interprocess comunicaion).I need to edit some c files in RefOS/libs/librefos directory,But comments say that do not edit these files,these files were generated by CIDL.CIDL is a simple C IDL compiler which is made to save the trouble of manually implementing RPC interface stubs to marshal C style arguments and return value. It uses a simple XML-based IDL language. I search on the google，but just got some introduction. So where can I got some useful infomation about CIDL? Can you recommend some books or websites? ------------------ Original ------------------ From: "devel-request";<devel-request(a)sel4.systems>; Date: Sun, Jun 21, 2015 10:00 AM To: "devel"<devel(a)sel4.systems>; Subject: Devel Digest, Vol 13, Issue 11 Send Devel mailing list submissions to devel(a)sel4.systems To subscribe or unsubscribe via the World Wide Web, visit https://sel4.systems/lists/listinfo/devel or, via email, send a message with subject or body 'help' to devel-request(a)sel4.systems You can reach the person managing the list at devel-owner(a)sel4.systems When replying, please edit your Subject line so it is more specific than "Re: Contents of Devel digest..." Today's Topics: 1. Re: Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC (da Tyga) ---------------------------------------------------------------------- Message: 1 Date: Sat, 20 Jun 2015 16:26:46 +1000 From: da Tyga <cyberfonic(a)gmail.com> To: devel(a)sel4.systems Subject: Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC Message-ID: <CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig(a)mail.gmail.com> Content-Type: text/plain; charset="utf-8" > > > Hi Yuxin, I don't think you need to modify GCC, it is the compiler that you can use to generate required executables. Making changes to it is a massive undertaking. Instead of trying to reinvent stuff that has already been done, you really should read the Genode documentation and download and read the source code referenced by Norman Feske's suggestions. >From my reading of the Genode documents and source code, I would expect that you would find a considerable amount of code that you could you re-purpose for your specific requirements. Cheers, Tyga > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Jun 2015 22:46:40 +0800 > From: Yuxin Ren <ryx(a)gwmail.gwu.edu> > To: Norman Feske <norman.feske(a)genode-labs.com> > Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] Does sel4 support c++ > Message-ID: > <CAAKbDrcbyh0YV+nHzhziiiXavn-= > P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Thank you all! > > If modifying the tool chain is the easiest way, I want to try it. > But I definitely want to avoid creating the tool chain from "bare metal". > I still prefer to reuse the existing tool chain like gcc > with minimal modification. > > Could you give me some guidance how to create a custom tool chain, which > part I need to modify? > I am not familiar with gcc. So if I have to modify gcc, where can I get > more information or documentation? > > Thanks a lot!! > Yuxin > > On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske < > norman.feske(a)genode-labs.com> > wrote: > > > Hello, > > > > > The easiest approach is possibly to create a custom tool chain, and > port > > > the GCC C++ library that way. I know the people behind Genode did some > > > of this (http://genode.org/download/tool-chain), although I'm not sure > > > how much of the C++ standard library they actually support. > > > > more in-depth information about Genode's tool chain are provided by > > Section 7.2 of the documentation [1]. In short, the tool chain is a > > "bare metal" tool chain that does not depend on a C library, yet it > > still supports C++ (including exceptions and runtime type information). > > > > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas > > the STL depends on the libc. The libc is based on FreeBSD's libc. The > > STL is GCC's version. Both libraries are available via Genode's ports > > mechanism. > > > > That said, as both the libc and stdcxx are shared libraries, they cannot > > be used on the seL4 version of Genode as of now. Shared libraries don't > > work on seL4 (at least on x86_32) because the system-call bindings > > cannot be compiled with -fPIC. > > > > [1] http://genode.org/documentation/genode-foundations-15-05.pdf > > > > Best regards > > 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 > > > > _______________________________________________ > > Devel mailing list > > Devel(a)sel4.systems > > https://sel4.systems/lists/listinfo/devel > > > -------------- next part -------------- > An HTML attachment was scrubbed... > URL: < > http://sel4.systems/pipermail/devel/attachments/20150619/5b4ce704/attachmen… > > > > ------------------------------ > > Subject: Digest Footer > > _______________________________________________ > Devel mailing list > Devel(a)sel4.systems > https://sel4.systems/lists/listinfo/devel > > > ------------------------------ > > End of Devel Digest, Vol 13, Issue 10 > ************************************* > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://sel4.systems/pipermail/devel/attachments/20150620/c72cfc07/attachmen…> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel(a)sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 13, Issue 11 *************************************

4 3

Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC
by da Tyga 22 Jun '15

22 Jun '15

> > > Hi Yuxin, I don't think you need to modify GCC, it is the compiler that you can use to generate required executables. Making changes to it is a massive undertaking. Instead of trying to reinvent stuff that has already been done, you really should read the Genode documentation and download and read the source code referenced by Norman Feske's suggestions. >From my reading of the Genode documents and source code, I would expect that you would find a considerable amount of code that you could you re-purpose for your specific requirements. Cheers, Tyga > ---------------------------------------------------------------------- > > Message: 1 > Date: Fri, 19 Jun 2015 22:46:40 +0800 > From: Yuxin Ren <ryx(a)gwmail.gwu.edu> > To: Norman Feske <norman.feske(a)genode-labs.com> > Cc: "devel(a)sel4.systems" <devel(a)sel4.systems> > Subject: Re: [seL4] Does sel4 support c++ > Message-ID: > <CAAKbDrcbyh0YV+nHzhziiiXavn-= > P_tW5bS2LUfPzHcBF-iMKg(a)mail.gmail.com> > Content-Type: text/plain; charset="utf-8" > > Thank you all! > > If modifying the tool chain is the easiest way, I want to try it. > But I definitely want to avoid creating the tool chain from "bare metal". > I still prefer to reuse the existing tool chain like gcc > with minimal modification. > > Could you give me some guidance how to create a custom tool chain, which > part I need to modify? > I am not familiar with gcc. So if I have to modify gcc, where can I get > more information or documentation? > > Thanks a lot!! > Yuxin > > On Thu, Jun 18, 2015 at 9:50 PM, Norman Feske < > norman.feske(a)genode-labs.com> > wrote: > > > Hello, > > > > > The easiest approach is possibly to create a custom tool chain, and > port > > > the GCC C++ library that way. I know the people behind Genode did some > > > of this (http://genode.org/download/tool-chain), although I'm not sure > > > how much of the C++ standard library they actually support. > > > > more in-depth information about Genode's tool chain are provided by > > Section 7.2 of the documentation [1]. In short, the tool chain is a > > "bare metal" tool chain that does not depend on a C library, yet it > > still supports C++ (including exceptions and runtime type information). > > > > On Genode, the libc and STL (aka stdcxx) can be used optionally whereas > > the STL depends on the libc. The libc is based on FreeBSD's libc. The > > STL is GCC's version. Both libraries are available via Genode's ports > > mechanism. > > > > That said, as both the libc and stdcxx are shared libraries, they cannot > > be used on the seL4 version of Genode as of now. Shared libraries don't > > work on seL4 (at least on x86_32) because the system-call bindings > > cannot be compiled with -fPIC. > > > > [1] http://genode.org/documentation/genode-foundations-15-05.pdf > > > > Best regards > > 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 > > > > _______________________________________________ > > Devel mailing list > > Devel(a)sel4.systems > > https://sel4.systems/lists/listinfo/devel > > >

2 1

Does sel4 support c++
by Yuxin Ren 20 Jun '15

20 Jun '15

Hi, Can I run C++ programs on sel4? I am not familiar with programming language. I do not know the relationship between the OS and the C++ language. In order to run C++, does the OS need to provide some support or what user level library are needed? Thanks a lot. Yuxin

4 6

Virtualization extensions
by Nick Betteridge 16 Jun '15

16 Jun '15

Hi I'm very interested in working with the virtualization extensions on sel4 - is there any rough timeline for when these will be available. Thanks Nick

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

Devel