On Tue, Jun 16, 2015 at 5:42 PM, Adrian Danis wrote:

The seL4 kernel itself does not need anything for running C++ support.

However, ......

give you a bit of insight into what is required for a proper C++ port.

Recall that the important part is application binary application calling conventions. Once an ABI is understood a lot can be done. The micro kernel has calling conventions and services. Applications need to live on top of this. For students the easy trick is to write in the high level language but save the assembly output file and inspect how the function is passed data and how it returns results. When mixing compilers this is a challenge. With gcc there is a common set of ABI services. Mixed vendor compilers are more complex. One issue is the set of choices that the language specification gives to compiler authors. In FORTRAN there are a couple famous vendors and they encode and test for True & False differently. The result is shared library trouble. Much can be sorted with cautious test cases. -- T o m M i t c h e l l

While we have 'ported' muslc it is worth pointing out that this does not mean the entire C library is usable. This is because all of the underlying unix syscalls are not implemented in any of our existing environments. For example, if you tried to call pthread_create, this would eventually result in attempting to call the clone syscall, which is not implemented and would fail. A C++ standard library does not necessarily depend upon a C library, it just so happens that GCCs C++ library does. There are no good and maintained standalone C++ libraries that I am aware of. There use to be one by apache (http://stdcxx.apache.org/), but it has been discontinued. 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. Adrian On 18/06/15 01:58, Yuxin Ren wrote:

Hi Adrian,

Thank you for your explanation. But I am still a little confused. If a C++ program uses standard library, then both standard library C++ library and C library are needed, right? And in sel4, you have ported a standard library C library (muslc), but you do not port any standard library C++ library to sel4. Is this correct? I know some standard library C library, such as glibc or muslc, but I do not know any standard library C++ library. Could you give me suggestion which C++ library may easy to port?

In additon, you said that you had some success with using your native gcc C++ libraries for compilation. Do you mean you link C++ program with Linux native C++ library first, and then link it to C library in sel4?

Thanks a lot!. Yuxin

On Tue, Jun 16, 2015 at 8:42 PM, Adrian Danis mailto:Adrian.Danis@nicta.com.au> wrote:

The seL4 kernel itself does not need anything for running C++ support. However, a version of the C++ standard library would need to be ported / implemented to a particular seL4 environment. If you would like to compile C++ code that does not use the standard library then this relatively easy and there is a trivial example in sel4test (see https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/src/tests/d... and https://github.com/seL4/sel4test/blob/master/apps/sel4test-tests/Makefile)

I had some success with using my native gcc C++ libraries for compilation, although it was a little fiddly to make work. The idea there is that since the C++ standard libraries depend upon the syscalls and other symbols defined in the C library you can just link against your native C++ libraries, and rely on the ported C library (in our case muslc) to implement the syscalls and make everything work. I am not promoting this as a good idea or a way to build a reliable system, but might give you a bit of insight into what is required for a proper C++ port.

Adrian

On 17/06/15 08:32, Yuxin Ren wrote:

...

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

_______________________________________________ Devel mailing list Devel@sel4.systems mailto: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.

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 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