How to edit RefOS libs c file
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@sel4.systems>; Date: Sun, Jun 21, 2015 10:00 AM To: "devel"<devel@sel4.systems>; Subject: Devel Digest, Vol 13, Issue 11 Send Devel mailing list submissions to devel@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@sel4.systems You can reach the person managing the list at devel-owner@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@gmail.com> To: devel@sel4.systems Subject: Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC Message-ID: <CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig@mail.gmail.com> Content-Type: text/plain; charset="utf-8"
Hi Yuxin,
From my reading of the Genode documents and source code, I would expect
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. 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@gwmail.gwu.edu> To: Norman Feske <norman.feske@genode-labs.com> Cc: "devel@sel4.systems" <devel@sel4.systems> Subject: Re: [seL4] Does sel4 support c++ Message-ID: <CAAKbDrcbyh0YV+nHzhziiiXavn-= P_tW5bS2LUfPzHcBF-iMKg@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@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@sel4.systems https://sel4.systems/lists/listinfo/devel
-------------- next part -------------- An HTML attachment was scrubbed... URL: < http://sel4.systems/pipermail/devel/attachments/20150619/5b4ce704/attachment...
------------------------------
Subject: Digest Footer
_______________________________________________ Devel mailing list Devel@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/attachment-0001.html> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 13, Issue 11 *************************************
Refos was a student project, and as typical of student projects, the documentation patchy. The student is no longer with us. I think your best bet is to learn how it works. The advantage of most student projects, is that they don’t have time to make anything too big or complex :) - Kevin From: Devel [mailto:devel-bounces@sel4.systems] On Behalf Of ??????? Sent: Monday, 22 June 2015 2:52 PM To: devel-request Subject: [seL4] How to edit RefOS libs c file 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@sel4.systems<mailto:devel-request@sel4.systems>>; Date: Sun, Jun 21, 2015 10:00 AM To: "devel"<devel@sel4.systems<mailto:devel@sel4.systems>>; Subject: Devel Digest, Vol 13, Issue 11 Send Devel mailing list submissions to devel@sel4.systems<mailto:devel@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@sel4.systems<mailto:devel-request@sel4.systems> You can reach the person managing the list at devel-owner@sel4.systems<mailto:devel-owner@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@gmail.com<mailto:cyberfonic@gmail.com>> To: devel@sel4.systems<mailto:devel@sel4.systems> Subject: Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC Message-ID: <CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig@mail.gmail.com<mailto:CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig@mail.gmail.com>> Content-Type: text/plain; charset="utf-8"
Hi Yuxin,
From my reading of the Genode documents and source code, I would expect
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. 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@gwmail.gwu.edu<mailto:ryx@gwmail.gwu.edu>> To: Norman Feske <norman.feske@genode-labs.com<mailto:norman.feske@genode-labs.com>> Cc: "devel@sel4.systems<mailto:devel@sel4.systems>" <devel@sel4.systems<mailto:devel@sel4.systems>> Subject: Re: [seL4] Does sel4 support c++ Message-ID: <CAAKbDrcbyh0YV+nHzhziiiXavn-= P_tW5bS2LUfPzHcBF-iMKg@mail.gmail.com<mailto:P_tW5bS2LUfPzHcBF-iMKg@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@genode-labs.com<mailto:norman.feske@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@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel
-------------- next part -------------- An HTML attachment was scrubbed... URL: < http://sel4.systems/pipermail/devel/attachments/20150619/5b4ce704/attachment...
------------------------------
Subject: Digest Footer
_______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@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/attachment-0001.html> ------------------------------ Subject: Digest Footer _______________________________________________ Devel mailing list Devel@sel4.systems<mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel ------------------------------ End of Devel Digest, Vol 13, Issue 11 ************************************* ________________________________ 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.
Hi ぷ风过无痕, CIDL is an in-house language and compiler. As Kevin said, it was built by a student who has moved on to other things. Below I've reproduced some internal documentation on it. However, I suspect the best way to understand it is to dive into the source code. Matt -- CIDL -- CIDL is a quick straightforward IDL compiler which generates stubs from a simple XML format IDL. CIDL aims to have processes in seL4 talking to each other with minimal work involved. CIDL expects a backing interface underneath, and one using pure seL4 IPC buffers has been supplied. The idea is that the user may simply switch their backing interface over to use shared buffers / passing pages around / whatever when they have the infrastructure to support it, and everything hopefully just works. Features: - Integers, C strings, generic types & structs, arrays - Distinguishes between input / output arguments - Return values - Cap transfer - Save-and-reply-later supported (useful for async) IDL Language: CIDL uses a simple XML-based IDL language, based somewhat loosely on seL4's syscall XML IDL. XSD spec for the IDL language: <xs:schema attributeFormDefault="unqualified" elementFormDefault="qualified" xmlns:xs="http://www.w3.org/2001/XMLSchema"> <xs:element name="interface"> <xs:complexType> <xs:sequence> <xs:element type="xs:string" name="include" maxOccurs="unbounded" minOccurs="0"/> <xs:element name="function" maxOccurs="unbounded" minOccurs="0"> <xs:complexType mixed="true"> <xs:sequence> <xs:element name="param" maxOccurs="unbounded" minOccurs="0"> <xs:complexType> <xs:simpleContent> <xs:extension base="xs:string"> <xs:attribute type="xs:string" name="type" use="required"/> <xs:attribute type="xs:string" name="name" use="required"/> <xs:attribute name="mode" use="optional"> <xs:simpleType> <xs:restriction base="xs:string"> <xs:pattern value="(array|length|connect_ep)"/> </xs:restriction> </xs:simpleType> </xs:attribute> <xs:attribute name="dir" use="optional" default="in"> <xs:simpleType> <xs:restriction base="xs:string"> <xs:pattern value="(in|out)"/> </xs:restriction> </xs:simpleType> </xs:attribute> <xs:attribute type="xs:string" name="lenvar" use="optional"/> </xs:extension> </xs:simpleContent> </xs:complexType> </xs:element> </xs:sequence> <xs:attribute type="xs:string" name="name" use="required"/> <xs:attribute type="xs:string" name="return" use="required"/> </xs:complexType> </xs:element> </xs:sequence> <xs:attribute type="xs:string" name="label_min" use="required"/> <xs:attribute type="xs:string" name="connect_ep" use="optional" default=""/> </xs:complexType> </xs:element> </xs:schema> Example XML conforming to this spec: <?xml version="1.0" ?> <interface label_min='0x5000' connect_ep=''> <include>stdio.h</include> <include>test_types.h</include> <function name="test_function1" return='seL4_CPtr'> TEST FUNCTION 1 </function> <function name="test_function2" return='int'> TEST FUNCTION 2 <param type="seL4_CPtr" name="session" mode="connect_ep"/> <param type="uintptr_t" name="a"/> <param type="uintptr_t*" name="b" dir="out"/> <param type="err_t*" name = "f" /> <param type="int*" name="c" mode="array" lenvar="lenv"/> <param type="int" name="lenv" mode="length" /> </function> </interface> -- end -- On 22/06/15 15:37, Kevin Elphinstone wrote:
Refos was a student project, and as typical of student projects, the documentation patchy. The student is no longer with us.
I think your best bet is to learn how it works. The advantage of most student projects, is that they don’t have time to make anything too big or complex J
-Kevin
*From:*Devel [mailto:devel-bounces@sel4.systems] *On Behalf Of *??????? *Sent:* Monday, 22 June 2015 2:52 PM *To:* devel-request *Subject:* [seL4] How to edit RefOS libs c file
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@sel4.systems <mailto:devel-request@sel4.systems>>;
*Date: * Sun, Jun 21, 2015 10:00 AM
*To: * "devel"<devel@sel4.systems <mailto:devel@sel4.systems>>;
*Subject: * Devel Digest, Vol 13, Issue 11
Send Devel mailing list submissions to devel@sel4.systems <mailto:devel@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@sel4.systems <mailto:devel-request@sel4.systems>
You can reach the person managing the list at devel-owner@sel4.systems <mailto:devel-owner@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@gmail.com <mailto:cyberfonic@gmail.com>> To: devel@sel4.systems <mailto:devel@sel4.systems> Subject: Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC Message-ID: <CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig@mail.gmail.com <mailto:CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig@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@gwmail.gwu.edu <mailto:ryx@gwmail.gwu.edu>> To: Norman Feske <norman.feske@genode-labs.com <mailto:norman.feske@genode-labs.com>> Cc: "devel@sel4.systems <mailto:devel@sel4.systems>" <devel@sel4.systems <mailto:devel@sel4.systems>> Subject: Re: [seL4] Does sel4 support c++ Message-ID: <CAAKbDrcbyh0YV+nHzhziiiXavn-= P_tW5bS2LUfPzHcBF-iMKg@mail.gmail.com <mailto:P_tW5bS2LUfPzHcBF-iMKg@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@genode-labs.com <mailto:norman.feske@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@sel4.systems <mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel
+devel on my reply; for any future references Hi, CIDL is a 200-line single-file minimalistic IDL compiler. It is really simple and you can just read the code directly. https://github.com/seL4/refos/blob/master/impl/cidl_compile The IDL files are here: https://github.com/seL4/refos/tree/master/impl/libs/librefos/interface And the client / server templates: https://github.com/seL4/refos/tree/master/impl/cidl_templates A minimal custom IDL compiler was chosen because others were too complex / assumed infrastructure different to low lvl seL4 environment and/or designed to work over network rather than kernel IPC. - Xi On 21 June 2015 at 23:51, Matthew Fernandez <matthew.fernandez@nicta.com.au> wrote:
Hi ぷ风过无痕,
CIDL is an in-house language and compiler. As Kevin said, it was built by a student who has moved on to other things. Below I've reproduced some internal documentation on it. However, I suspect the best way to understand it is to dive into the source code.
Matt
-- CIDL --
CIDL is a quick straightforward IDL compiler which generates stubs from a simple XML format IDL. CIDL aims to have processes in seL4 talking to each other with minimal work involved. CIDL expects a backing interface underneath, and one using pure seL4 IPC buffers has been supplied. The idea is that the user may simply switch their backing interface over to use shared buffers / passing pages around / whatever when they have the infrastructure to support it, and everything hopefully just works.
Features: - Integers, C strings, generic types & structs, arrays - Distinguishes between input / output arguments - Return values - Cap transfer - Save-and-reply-later supported (useful for async)
IDL Language:
CIDL uses a simple XML-based IDL language, based somewhat loosely on seL4's syscall XML IDL.
XSD spec for the IDL language:
<xs:schema attributeFormDefault="unqualified" elementFormDefault="qualified" xmlns:xs="http://www.w3.org/2001/XMLSchema"> <xs:element name="interface"> <xs:complexType>
<xs:sequence> <xs:element type="xs:string" name="include" maxOccurs="unbounded" minOccurs="0"/> <xs:element name="function" maxOccurs="unbounded" minOccurs="0"> <xs:complexType mixed="true"> <xs:sequence> <xs:element name="param" maxOccurs="unbounded" minOccurs="0"> <xs:complexType> <xs:simpleContent>
<xs:extension base="xs:string">
<xs:attribute type="xs:string" name="type" use="required"/> <xs:attribute type="xs:string" name="name" use="required"/>
<xs:attribute name="mode" use="optional"> <xs:simpleType> <xs:restriction base="xs:string"> <xs:pattern value="(array|length|connect_ep)"/> </xs:restriction> </xs:simpleType> </xs:attribute>
<xs:attribute name="dir" use="optional" default="in"> <xs:simpleType> <xs:restriction base="xs:string"> <xs:pattern value="(in|out)"/> </xs:restriction> </xs:simpleType> </xs:attribute>
<xs:attribute type="xs:string" name="lenvar" use="optional"/>
</xs:extension>
</xs:simpleContent> </xs:complexType> </xs:element> </xs:sequence> <xs:attribute type="xs:string" name="name" use="required"/> <xs:attribute type="xs:string" name="return" use="required"/> </xs:complexType> </xs:element> </xs:sequence> <xs:attribute type="xs:string" name="label_min" use="required"/> <xs:attribute type="xs:string" name="connect_ep" use="optional" default=""/> </xs:complexType> </xs:element> </xs:schema>
Example XML conforming to this spec: <?xml version="1.0" ?> <interface label_min='0x5000' connect_ep=''> <include>stdio.h</include> <include>test_types.h</include> <function name="test_function1" return='seL4_CPtr'> TEST FUNCTION 1 </function> <function name="test_function2" return='int'> TEST FUNCTION 2 <param type="seL4_CPtr" name="session" mode="connect_ep"/> <param type="uintptr_t" name="a"/> <param type="uintptr_t*" name="b" dir="out"/> <param type="err_t*" name = "f" /> <param type="int*" name="c" mode="array" lenvar="lenv"/> <param type="int" name="lenv" mode="length" /> </function> </interface>
-- end --
On 22/06/15 15:37, Kevin Elphinstone wrote:
Refos was a student project, and as typical of student projects, the documentation patchy. The student is no longer with us.
I think your best bet is to learn how it works. The advantage of most student projects, is that they don’t have time to make anything too big or complex J
-Kevin
*From:*Devel [mailto:devel-bounces@sel4.systems] *On Behalf Of *??????? *Sent:* Monday, 22 June 2015 2:52 PM *To:* devel-request *Subject:* [seL4] How to edit RefOS libs c file
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@sel4.systems <mailto:devel-request@sel4.systems>>;
*Date: * Sun, Jun 21, 2015 10:00 AM
*To: * "devel"<devel@sel4.systems <mailto:devel@sel4.systems>>;
*Subject: * Devel Digest, Vol 13, Issue 11
Send Devel mailing list submissions to devel@sel4.systems <mailto:devel@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@sel4.systems <mailto:devel-request@sel4.systems>
You can reach the person managing the list at devel-owner@sel4.systems <mailto:devel-owner@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@gmail.com <mailto:cyberfonic@gmail.com>> To: devel@sel4.systems <mailto:devel@sel4.systems> Subject: Re: [seL4] Devel Digest, Vol 13, Issue 10_Bare Metal support for GCC Message-ID: <CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig@mail.gmail.com
<mailto:CALj3Nd3+CFFQF41BOwW+-bwFNOEZS9HyVLHDwVssTyMAcsU3ig@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@gwmail.gwu.edu <mailto:ryx@gwmail.gwu.edu>> To: Norman Feske <norman.feske@genode-labs.com <mailto:norman.feske@genode-labs.com>> Cc: "devel@sel4.systems <mailto:devel@sel4.systems>" <devel@sel4.systems <mailto:devel@sel4.systems>> Subject: Re: [seL4] Does sel4 support c++ Message-ID: <CAAKbDrcbyh0YV+nHzhziiiXavn-= P_tW5bS2LUfPzHcBF-iMKg@mail.gmail.com <mailto:P_tW5bS2LUfPzHcBF-iMKg@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@genode-labs.com <mailto:norman.feske@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@sel4.systems <mailto:Devel@sel4.systems> https://sel4.systems/lists/listinfo/devel
participants (4)
-
HyperNewbie -
Kevin Elphinstone -
Matthew Fernandez -
ぷ风过无痕??