search

seL4 / microkit

Microkit - A simple operating system framework for the seL4 microkernel
Other
70 stars 37 forks source link

Rust Microkit Migration Plan #28

Open podhrmic opened 1 year ago

podhrmic commented 1 year ago

Hello! Just wondering - is there a migration plan for the Rust Core platform? It looks like @nspin made some tweaks to the seL4 kernel and to the Core Platform itself, but I am not sure how easy is to merge those changes here?

The cargo and rust part should be pretty independent, it would just be nice to use the same kernel and Core Platform SDK.

Ivan-Velickovic commented 1 year ago

I believe @nspin intends to upstream his changes to add Rust support, but I don't know any more details other than that. It might be best to ask him directly.

I think the only difference between Nick's kernel and the current seL4CP kernel is that Nick's is more recent. To my knowledge the only thing that needs to change in seL4CP to use a newer kernel is that seL4_MinSchedContextBits was changed, so this line https://github.com/BreakawayConsulting/sel4cp/blob/74db455afd369f9db0442735cfdc13df52fb9163/tool/sel4coreplat/sel4.py#L157 should reflect that. I'm planning to change the kernel to instead properly export these hard-coded values so that in the future using an updated kernel is less fragile.

Nick has already made this change though and has it working, I don't see any issue with just using his version of seL4 with seL4CP until his Rust work gets mainlined.

lsf37 commented 1 year ago

Just to confirm: the plan is to converge all of this so it works together out of the box. It'll take a bit more time until it is there, but I don't think we're far off.

nspin commented 1 year ago

I've updated simple-sel4cp-demo. Now, the seL4 and sel4cp submodules point to commits which are based on current upstream trunks (as of writing), and contain only the minimal set of changes.

The seL4 commit contains only one change on top of upstream trunk (seL4/seL4:master), and that is a rebased version of the boot protocol change found at BreakawayConsulting/seL4:sel4cp-core-support. As @Ivan-Velickovic mentioned, I've been using a more up-to-date kernel.

The sel4cp commit contains only two changes on top of upstream trunk (BreakawayConsulting/sel4cp:main). One is the one seL4_MinSchedContextBits-related change that @Ivan-Velickovic mentioned. The other just adds handling for unaligned ELF segments in PDs, and could be polished and upstreamed.

Ivan-Velickovic commented 9 months ago

Now that @nspin's Rust support for seL4 (including Microkit) has been moved to the seL4 Foundation, there's just a couple more things to sort out before this issue can be resolved:

  1. Decide whether to have the microkit Rust crate live in this repository or not.
  2. Have at least one example written in Rust in this repository, a hello-world is definitely necessary given that the build process for using Rust is very different compared to the C examples.
  3. Properly integrate everything regarding documentation, if you were to solely look at the contents of this repository and the SDK manual, you would have no idea that Rust bindings exist. If the other Rust examples such as https://github.com/seL4/rust-microkit-demo and https://github.com/seL4/rust-microkit-http-server-demo continue to live in their own repositories, we need to at least have pointers to them from here.
  4. Allow the microkit crate to use the mainline Microkit SDK (there's just a couple minor patches to be upstreamed so should be trivial just a matter of time).