diff --git a/apps/system/components/kata-os-common/src/sel4-sys/Cargo.toml b/apps/system/components/kata-os-common/src/sel4-sys/Cargo.toml index 0b90be7..5f14814 100644 --- a/apps/system/components/kata-os-common/src/sel4-sys/Cargo.toml +++ b/apps/system/components/kata-os-common/src/sel4-sys/Cargo.toml @@ -1,4 +1,5 @@ # Copyright (c) 2015 The Robigalia Project Developers +# TBD: Google copyright # Licensed under the Apache License, Version 2.0 or the MIT license , at your option. All files in the @@ -8,10 +9,10 @@ name = "sel4-sys" version = "0.1.0" edition = "2018" -authors = ["Corey Richardson "] +authors = ["Corey Richardson ", "Sam Leffler "] description = "Rust interface to the seL4 kernel" -documentation = "https://doc.robigalia.org/sel4_sys" -repository = "https://gitlab.com/robigalia/sel4-sys" +documentation = "fixme" +repository = "fixme" readme = "README.md" license = "MIT/Apache-2.0" build = "build.rs" diff --git a/apps/system/components/kata-os-common/src/sel4-sys/README.md b/apps/system/components/kata-os-common/src/sel4-sys/README.md index 612436d..e0334ad 100644 --- a/apps/system/components/kata-os-common/src/sel4-sys/README.md +++ b/apps/system/components/kata-os-common/src/sel4-sys/README.md @@ -1,52 +1,70 @@ # sel4-sys -[![Crates.io](https://img.shields.io/crates/v/sel4-sys.svg?style=flat-square)](https://crates.io/crates/sel4-sys) +[![Crates.io](https://img.shields.io/crates/v/sel4-sys.svg?style=flat-square)](FIXME) -[Documentation](https://doc.robigalia.org/sel4_sys) +[Documentation](FIXME) A Rust interface to the [seL4 kernel](https://sel4.systems). Raw syscall -bindings, kernel API, and data structure declarations. Provides the same -interface that libsel4 does, with a few C-isms reduced. +bindings, kernel API, and data structure declarations. Provides the +same interface that libsel4 does, with many C-isms removed. -NOTE: be sure to `git submodule update --recursive --init` if you clone this -repository, as we pull in seL4 via a submodule. +NOTE: this module depends on the sel4-config crate to sync seL4 kernel +configuration. That crate and sel4-sys depend on the SEL4_DIR and +SEL4_OUT_DIR environment variables being set to the top of the seL4 +kernel source and build directories. -## Updating to a new version of seL4 +## Current status -Updating to a new version of seL4 isn't hard, but it can be annoying. -First, cd into the `seL4` submodule, do a `git fetch`, and checkout the new -version you want to evaluate. Then, do a `cargo build`. At that point, you can -try running `cargo build`. It probably won't succeed, due to changes in API -and the Python tools. +This is a work-in-progress. The crate has been heavily used on a riscv32 +target for Rust code developed for CAmkES and for a new rootserver that +replaces capdl-loader-app. Other architectures have not been compiled and +are likely missing code in arch/*.rs. -To fix the Python tools, I use a command like: +Similarly seL4/CAmkES feature support is lightly tested. All features have +been compiled but, for example, only dynamic object allocation has been +(heavily) tested. - diff -u seL4/tools/bitfield_gen.py tools/bitfield_gen.py | pygmentize | less -R +System calls use a Rust-friendly calling api (returning seL4_Result) +instead of return an seL4_Error. Some kernel data structures have been +re-cast for use by Rust code and to minimize dependence on the seL4 +kernel configuration. Work is ongoing to export all the seL4 data types +and definitions needed to build a complete system in Rust and to make data +types more Rust friendly (e.g. enums used for things like bitflags). Rust +code still depends on the sel4runtime library to handle getting to "main" +(or the equivalent CAmkES interface) but that can be distilled to <100 +lines of code. -I then carefully look at the diff to see if there are any meaningful -differences. One challenge when doing this is that a lot of some of the tools -has been ripped out, because it deals with topics Robigalia doesn't need to -care about (bitfield proofs, or declaration order, for example). +## Tracking seL4 -Once you have a successful `cargo build`, you're not done. It's likely that -the kernel added, removed, or otherwise changed various pieces of the ABI. In -particular, inspect `lib.rs` and update for any changes in the IPC buffer -(unlikely) or bootinfo (increasingly unlikely). Update `arch/x86_64.rs` etc -for any changes in the object types. Changes are usually easy to see by a cd -into seL4/libsel4 and a `git diff X.0.0..Y.0.0`. +Updating to a new version of seL4 should be straightforward. The scripts +in the tools directory are direct descendents of the seL4 tools scripts. +The intent is to merge the Rust support in tools/*.py into the seL4 code +base so that tracking seL4 requires limited work. -As a quick smoketest, go to the `hello-world` repository and compile and run -it with the new kernel and `sel4-sys`. +## Regression testing with sel4test -After that, it's time to update the `sel4` crate and any other impacted user -components. +This crate can be used with sel4test for regression testing. There is +a wrapper crate for sel4-sys that generates C-callable api's to the +Rust code. Using this with the sel4test framework then gives you full +coverage of the system calls used by sel4test. -## Status +## Code structure -Mostly complete, though largely untested. +Code is broadly broken into 3 pieces: +1. Static arch-independent defniitions and interfaces: lib.rs +2. Static arch-dependent definitions and interfaces: arch/*.rs +3. Dynamically-generated definitions and interfaces, created by the + tools/*.py scripts (TBD: merged into seL4 kernel) + +#3 happens via cargo using a custom build.rs and the companion sel4-config +crate that syncs an seL4 kernel configuration. Various pieces of code are +glued together with Rust include directives. Target configuration keys off +the Rust target_arch and target_pointer_width. + +TBD: dependent crates, optional features. ## TODO -- Add support iterating over the `seL4_BootInfoHeader` -- Add automated, comprehensive tests -- Formal verification that the code actually follows the implemented ABI. +- Fill in support for architectures other than riscv32 +- Test all crate features (e.g. static object allocation) +- More complete coverage of seL4 api's