Build instructions

[daniel-ac-martin]

It would be nice if some build instructions were provided in the README of this repo. For example, is it expected that this will always be built via the build system in https://github.com/seL4/seL4_tools/tree/master/cmake-tool, or is it possible to build this standalone?

When attempting a standalone build, with:

cmake -G Ninja -C config.cmake path/to/sel4runtime/

(config.cmake just sets things like KernelSel4Arch.)

I get the following error:

CMake Error at CMakeLists.txt:20 (config_string):
  Unknown CMake command "config_string".

It seems that config_string is defined over in the kernel repo: https://github.com/seL4/seL4/blob/master/tools/helpers.cmake#L322

I'm new to CMake so it's possible that I've misunderstood, but it seems to me that the build system of this repo expects this function to have already been defined for it, and so to be built via a larger build system (seL4_tools?). Including this from my config.cmake doesn't seem to have any effect.

Any help/advice on any of the above would be appreciated.

[daniel-ac-martin]

To provide some extra context, I've been trying to put together a simplified (to my eyes!) build system for building on top of seL4. The tutorials point people in the direction of pulling down many code repositories and building within a predefined build system, implemented in CMake. I don't know CMake and I'm also interested in building things in Zig or perhaps even Rust, which have their own ways of doing things. So I've been trying to find a way to:

• build only the seL4 dependencies that are necessary / helpful
• limit the seL4 build system to building seL4 dependencies
• include and link against the built seL4 dependencies from a bespoke build system (GNU Make plus whatever Zig or Rust provide)

I know that Core Platform is trying to address some of these things, but that doesn't seem ready for use and doesn't appear to support x86_64 at this time. (It also seems to introduce it's own set of tools, which makes me wonder if something simpler is possible.)

Apologies if I've said something silly; I'm fairly new to this.

[daniel-ac-martin]

Oh, I should add that, so far, I've been able to build a standalone kernel (based on the information provided on the website) and I'm now trying to run something on top of it. Hence why sel4runtime seems useful to add at this point.

[Ivan-Velickovic]

Hi Daniel, while I unfortunately can't help you with the CMake issues, I was curious if anything in particular about the Core Platform makes it seem not ready for use? Hopefully I can try to address them/get the issues resolved. Regarding x86_64 support, there is someone working on that and so in the future seL4CP will have support for x86_64.

[Ivan-Velickovic]

Regarding Rust support, you may be interested in looking at https://gitlab.com/coliasgroup/rust-seL4. I haven't tried to get Zig working on raw seL4, but have gotten in working with seL4CP fairly trivially. Zig (at least last time I checked) can't fully translate libsel4 because of the use of inline GCC assembly so that's the main point of friction when using Zig with seL4 in my experience.

[daniel-ac-martin]

Hi @Ivan-Velickovic. Thanks for the response.

Build instructions

In the end, I was able to get a minimal C program running but I did need to make use of the build system in seL4_tools. I suspect that is the only way to do it. I suspect that any build instructions for this repo would go something like the following:

• Make sure you have also pulled down the seL4 (kernel) and seL4_tools repos.
• Create a CMakeLists.txt and within it:
  • Append the following directories to your CMAKE_MODULE_PATH:
  • path/to/seL4/
  • path/to/seL4_tools/cmake_tool/helpers/
  • path/to/seL4_runtime/
  • Add the lines:

    find_package(seL4 REQUIRED)
    find_package(seL4runtime REQUIRED)
    sel4_import_kernel()
    sel4runtime_import_project()
    sel4_import_libsel4()

• Run cmake -G ninja
• Run ninja libsel4runtime.a

Usage instructions would be something like:

• Write and compile a normal C program (with a main() function)
• Link into an ELF executable linking your object files with libsel4runtime.a and libsel4.a and using the linker script provided in seL4_tools. e.g:

  gcc -Wl,-u_sel4_start -Wl,-e_sel4_start -Wl,-T path/to/seL4_tools/cmake-tool/helpers/tls_rootserver.lds -o roottask.elf path/to/libsel4.a path/to/libsel4runtime.a $(OBJS)

  Note: When linking ensure you provide an implementation of strcpy(). (An implementation of libc such as the muslibc repo will provide this.)

• Provide the resulting ELF as an initrd to seL4.

Of course, someone with more knowledge would be able to write that up in a better way.

I was thinking of uploading my work on this, but I'm not sure whether it has any value.

Regarding seL4CP / Core Platform

(Remember, I've not delved to deeply into Core Platform yet.)

I suppose we'd have to split out a few things:

1. Things that make seL4CP seems like it's not ready for use at all
2. Things that make seL4CP seem like it's not ready for my purposes
3. The reservations that I had about the approach (not necessarily well thought out, mainly gut instincts / prejudices)

Regarding number 1, I suppose the following things jump out at me:

• There doesn't seem to be much user documentation / tutorials / how-to guides (there are references to a user manual, but I've not found anything beyond: https://github.com/BreakawayConsulting/sel4cp/blob/main/docs/manual.md )
• The README tells my to use a pre-built SDK but doesn't tell me where to get one
• It looks like I need a special compiler (not just a cross-compiler, but a specific version)
• I need a special (unverified?) version of the kernel (could the changes by merged into the main repo?)
• One 1 'board' is listed as being supported (I don't know anything about ARM development so I don't know how significant this is)

Number 2 (my purposes) is mainly around x86_64 support, but it also seems to be implied that Core Platform is just for embedded development, so I don't know how suitable it might be for more general purpose operating systems. (But I'm really just tickering around as a hobbiest, so my opinions could be nonsense.)

Number 3 (general reservations) is probably around the need to use the 'tool'. Once special build tools are introduced I start to worry about having a brittle build system that is hard to get set up. i.e. Will other developers be able to easily get the tool installed and working for them? I also worry about losing control over my project and having to conform to another project's way of building things. (Similar to the CMake build system for seL4.) But these are mainly my knee jerk reactions that are coming from a place of ignorance with regards to this type of work (although they have been built up from experience in other areas).

I like the general approach in Core Platform. The abstractions seem to be fairly simple to understand. Providing the roottask and a library to link custom tasks / PDs against makes sense.

I can also see the value in having the tool. Especially the static analysis to ensure the system is configured in a way that prevents deadlocks. But I wonder if that could be done in a different way, perhaps by having the debug builds of the roottask reject such misconfigurations. On the other hand, maybe I'd be more comfortable with the tool it was demystified, and I understood what it was doing.

I hope that is of some use to you. Apologies if I've said anything silly, as I say, I'm coming at this as a novice.

BTW, I'm really interested in the work to add x86_64 support to seL4CP. Do you have a link?

[daniel-ac-martin]

Regarding Rust support, you may be interested in looking at https://gitlab.com/coliasgroup/rust-seL4. I haven't tried to get Zig working on raw seL4, but have gotten in working with seL4CP fairly trivially. Zig (at least last time I checked) can't fully translate libsel4 because of the use of inline GCC assembly so that's the main point of friction when using Zig with seL4 in my experience.

Thanks for that link. Yes, I also ran into that issue with Zig, which makes me think that a better approach would be to avoid seL4runtime and libsel4, and instead reverse engineer them into zig code, and make syscalls directly. It would be nice if the seL4 documentation was a bit clearer on how to do this, but it seems to assume that everyone will use the ecosystem that they provide. i.e. The documentation refers to the libsel4 API rather than the seL4 ABI and opcodes etc. (Again, apologies if I'm missing something.)

[Ivan-Velickovic]

Thank you very much for the feedback, I really appreciate it. I will address the seL4CP points first.

There doesn't seem to be much user documentation / tutorials / how-to guides (there are references to a user manual, but I've not found anything beyond: https://github.com/BreakawayConsulting/sel4cp/blob/main/docs/manual.md )

You are right, currently there is nothing official other than the manual. For the seL4 Summit last year I made a basic tutorial for the seL4CP, you can view it here: https://summit.ivanvelickovic.com/. I have plans to improve it and eventually upstream it so that people like yourself will have an easier time getting into seL4CP. There are plans for more documentation and well documented non-trivial example system, but it will be some time before those are ready.

The README tells my to use a pre-built SDK but doesn't tell me where to get one

You are correct, I have noticed this before and it should be fixed.

It looks like I need a special compiler (not just a cross-compiler, but a specific version)

This is done intentionally in order to make the SDK as reproducible as possible. While any cross-compiler should work, that is not the reality I have personally found with C code and hence having a specific toolchain is (in my opinion) necessary.

I need a special (unverified?) version of the kernel (could the changes by merged into the main repo?)

There is a single patch to seL4 required for seL4CP to currently work, I am working to resolve this now by either removing the patch and changing seL4CP or to upstream the patch. The patch is to the unverified boot code of seL4 and should not have an affect on the verification of it.

One 1 'board' is listed as being supported (I don't know anything about ARM development so I don't know how significant this is)

There are now multiple boards supported but the README has not been updated, will fix this. Thanks for pointing it out.

Number 2 (my purposes) is mainly around x86_64 support, but it also seems to be implied that Core Platform is just for embedded development, so I don't know how suitable it might be for more general purpose operating systems.

The Core Platform is targeted to embedded development for simplicity. One of the main (intentional) restrictions of seL4CP systems is a static architecture, meaning that you will always know how many PDs, MRs etcs will exist for the life of the system. There are dynamic features being introduced (e.g. starting/stopping/late-loading of PDs) and plans for more in the future. However, a general purpose OS usually requires levels of dynamicism that seL4CP does not plan to provide.

Number 3 (general reservations) is probably around the need to use the 'tool'. Once special build tools are introduced I start to worry about having a brittle build system that is hard to get set up.

This is definitely a valid concern to be had. The tool is basically responsible for taking the system description, PD ELFs, etc and producing the final binary that the board will load to start your system. Here's a hello world example that shows invoking the tool, https://github.com/BreakawayConsulting/sel4cp/blob/9eb051f9d74549039a309499671bc440cc86bc7f/example/zcu102/hello/Makefile#L54. As you can see, it's not invasive. In fact, one of the goals of seL4CP is to not have any users have to conform to any specific build system.

Again, thanks for the feedback. It's always really useful to have perspective from the community.

[Ivan-Velickovic]

Of course, someone with more knowledge would be able to write that up in a better way.

Having someone push for it would definitely make it more likely to happen.

I was thinking of uploading my work on this, but I'm not sure whether it has any value.

I think it most definitely well, it's more about finding the right place for it so that is visible. Perhaps @lsf37 or @kent-mcleod can comment.

[Ivan-Velickovic]

Thanks for that link. Yes, I also ran into that issue with Zig, which makes me think that a better approach would be to avoid seL4runtime and libsel4, and instead reverse engineer them into zig code, and make syscalls directly.

That is another way of doing things yes, it depends on what your goal is. For systems built on top of frameworks like seL4CP then having the seL4 API being written in the language of the user-code matters less so, as you are not really interacting with it directly. If say you wanted to write an OS directly on top of seL4 solely in Zig, it would be nicer to have language-specific bindings. If that suits you, following what Nick is doing with his Rust support for seL4 might be the way to go.

[lsf37]

I was thinking of uploading my work on this, but I'm not sure whether it has any value.

I think it most definitely well, it's more about finding the right place for it so that is visible. Perhaps @lsf37 or @kent-mcleod can comment.

@kent-mcleod is expert on the build system, but I think that would be useful, yes. Can we find a good place for it on the doc site somewhere? It should be reasonably easy for people to improve it from there if somebody has made a start.

[Ivan-Velickovic]

BTW, I'm really interested in the work to add x86_64 support to seL4CP. Do you have a link?

Forgot to address this part. Will ask the person working on it if it's in a shareable state yet and get back to you.

[maaaat]

BTW, I'm really interested in the work to add x86_64 support to seL4CP. Do you have a link?

Forgot to address this part. Will ask the person working on it if it's in a shareable state yet and get back to you.

@Ivan-Velickovic kindly asked if I could share the x86_64 port of sel4cp that I've been working on in the past months. I'm happy to do so, but keep in mind that what I have at this point is really just an early proof-of-concept and I will be force-pushing the branch in the coming months as I do more testing on real hardware and clean up the code. Until then feel free to have a look of course, the branch is here.

It also requires a small modification of the seL4 kernel here which does some trickery with the multiboot2 specs to mark some regions of memory as device untyped. This is good enough for a proof of concept but I might want do try another approach at some point, one that does not require abusing the multiboot2 specs and ideally that does not touch the kernel at all.

So there is some code, I'm actively working on it, but it's a long way from being production ready.