Initial CI support to compile the demo

[podhrmic]

• This PR enables github actions and compiles the demo loader.img
• Small changes in how docker image is built (no UID), so it is easier to use in the CI runner
• The docker image is ideally built and pushed automatically (on change) as well, ideally to seL4 dockerhub (and not my private one)
• Proper testing would need to be added, perhaps by utilizing Qemu Avocado framework

[podhrmic]

Here is the actual CI run: https://github.com/GaloisInc/rust-seL4-sel4cp-demo/actions/runs/5481298393/jobs/9985421029

[nspin]

I've only just now finished setting up a first take on CI for coliasgroup/rust-seL4, and we haven't yet decided what CI should look like for these demo repositories. Let's revisit this PR once that has been decided.

The code from this demo is developed in coliasgroup/rust-seL4 and then manually copied into this repository (see update.sh) , so that this repository can clearly demonstrate a simple build system. For the meantime, I've added a test for this code in the main repository that runs in CI: coliasgroup/rust-sel4@e5af5f3

[podhrmic]

Right on! If you want help with more complex CI setup, I can ask folks here at Galois who deal with CI for our large code bases like Cryptol and Saw. IMHO it would be cool to add at least docker as a target (not everyone uses nix), and perhaps a couple of the most common operating systems for people who want to install/use rust-sel4 directly (Ubuntu/Debian).

The code from this demo is developed in coliasgroup/rust-seL4 and then manually copied into this repository (see update.sh)

Interesting - does this mean that any changes/addition in the banscii crates should be done in rust-sel4 rather than here? I am wondering what would be the best way to handle coverage - making sure that each crate/component is tested, and avoid having dead components that were plaguing Camkes. Perhaps having a .system file associated with each crate would be a good start?
Probably with QEMU as a target board for now, because the Xilinx QEMU that supports ZCU102 is export controlled.

What do you think?

[nspin]

I consider this demo to have three purposes:

• To exercise and inform the design choices made in the rust-seL4 project, especially the sel4cp crate
• To demonstrate how to use the sel4cp crate at the source level
• To suggest one way to structure a build system for a Rust-based sel4cp system

From this perspective, the purpose of any testing and CI in this repository would be to demonstrate or suggest one way to set up testing and CI for a Rust-based sel4cp system.

IMHO it would be cool to add at least docker as a target (not everyone uses nix), and perhaps a couple of the most common operating systems for people who want to install/use rust-sel4 directly (Ubuntu/Debian).

Yes, definitely. The Nix stuff is really just meant for hacking on and testing the rust-seL4 project itself, and shouldn't leak into the requirements for using the rust-seL4 project. So the intended usage modes for the rust-seL4 project, including the one demonstrated in this demo, shouldn't require Nix and should fit into a wide range of environments including Docker and native Ubuntu/Debian.

Could you clarify what you mean by adding Docker or other environments as targets?

I've hacked up some ideas for GitHub actions-based CI for this demo which doesn't require uploading a Docker image that is specific to this repository to the GitHub Packages Container Registry, and allows us to keep the UID/GID convenience. What do you think of these ideas?

main...nspin:rust-seL4-sel4cp-demo:nspin/wip/ci-ideas

Also, in response to your suggestion about publishing a Docker image, I've drafted a Docker image which contains dependencies and pre-build artifacts for the rust-seL4 project:

https://github.com/coliasgroup/rust-seL4-docker-images

Interesting - does this mean that any changes/addition in the banscii crates should be done in rust-sel4 rather than here?

I've been primarily developing the code of this demo in the rust-seL4 project repo and copying it over using the ./update.sh script. That has made it easier to hack on both the demo and the sel4cp crates in parallel, but this silly and redundant arrangement makes collaboration harder and muddies the demo a bit. I think a better solution would be to remove the code from the rust-seL4 project repo and just work on it here, especially now that the sel4cp crate API has settled.

I am wondering what would be the best way to handle coverage - making sure that each crate/component is tested, and avoid having dead components that were plaguing Camkes. Perhaps having a .system file associated with each crate would be a good start?

Do you mean coverage for the code in the rust-seL4 project? If so, then I think this would probably be the best place for those tests. Or do you mean the components in this demo? I think that any components from this demo that might be reused should be hosted as part of the rust-seL4 project proper, and tested there.

[podhrmic]

Hi @nspin !

Could you clarify what you mean by adding Docker or other environments as targets?

I meant building and publishing a dedicated docker image as a part of the CI. If you wanted to go beyond that, you could precompile the SDK for various platforms (like Mac, Linux), but that is probably rather excessive at this point.

I've hacked up some ideas for GitHub actions-based CI for this demo which doesn't require uploading a Docker image that is specific to this repository to the GitHub Packages Container Registry, and allows us to keep the UID/GID convenience. What do you think of these ideas?

Very cool! I opened an MR with some suggestions here. Basically, you keep a base image that doesn't have the UID/GID set up, and publish that image. Users then can quickly(!) locally build an image with the UID/GID overlay, so you keep both the convenience of the permissions, and the prebuild image that is easy to download.

Also, in response to your suggestion about publishing a Docker image, I've drafted a Docker image which contains dependencies and pre-build artifacts for the rust-seL4 project:

Excellent! I wonder if @TrustworthySystems wouldn't mind adopting such image for convenience? That way you avoid having a separate repo for a single dockerfile.

Or do you mean the components in this demo? I think that any components from this demo that might be reused should be hosted as part of the rust-seL4 project proper, and tested there.

I meant exactly that. Ideally each component is used in at least one demo that is reproducible and build/run as a part of a CI job. I don't have a strong opinion about where the components should be hosted, but I would really like to avoid the Camkes situation, where you have a plethora of components in various repositories, without any indication whether they work or not, and which versions of various libraries (kernel, camkes tool, etc) they require. And no, writing it in a README is not enough:-)

[podhrmic]

@nspin I am looking at your http-server example (very cool btw!). I see you have a nix build script for it - maybe link to it in the crate docs and show that the crate is indeed build and tested in the CI?

[nspin]

I meant building and publishing a dedicated docker image as a part of the CI. If you wanted to go beyond that, you could precompile the SDK for various platforms (like Mac, Linux), but that is probably rather excessive at this point.

I agree that we should provide whatever we can to shorten the distance to a working project for users of this work, and I think publishing Docker images as part of CI is a good idea.

However, I think that the scope of any such published artifacts should be the entire rust-seL4 project, not just this demo. The rust-seL4 project-wide Docker image I've drafted is meant to serve this purpose. That repo's CI could publish images, and projects like the one in this repo could depend on those images. How does that line up with what you have in mind?

I meant exactly that. Ideally each component is used in at least one demo that is reproducible and build/run as a part of a CI job. I don't have a strong opinion about where the components should be hosted, but I would really like to avoid the Camkes situation, where you have a plethora of components in various repositories, without any indication whether they work or not, and which versions of various libraries (kernel, camkes tool, etc) they require. And no, writing it in a README is not enough:-)

Providing re-usable sel4cp components isn't really in scope for the rust-seL4 project at the moment. I definitely think that providing re-usable components would be useful (provided that it's done with proper testing and documentation as you noted!), but, for the moment, we're still working on solidifying more foundational aspects of the project. I think that, until the lower level APIs get more eyes and approval and this project is integrated into the foundation's governance+maintenance domain, it will be tough to find the resources or confidence to provide re-usable components in a robust and responsible way.

But I totally hear you. When providing re-usable sel4cp components comes into scope, it will certainly be important to test and document them in a rigorous way, which includes CI with user-visible reporting.

[nspin]

@nspin I am looking at your http-server example (very cool btw!). I see you have a nix build script for it - maybe link to it in the crate docs and show that the crate is indeed build and tested in the CI?

For posterity's sake:

https://github.com/coliasgroup/rust-seL4-sel4cp-http-server-demo