mirror of
https://github.com/AmbiML/sparrow-kata-full.git
synced 2025-07-14 06:24:14 +00:00
sel4-sys: documentation cleanups
Change-Id: Ic6a2440c492f2c1ca5a034cf2abfe4015ce3deaa GitOrigin-RevId: 97ede65dfb940af050cbb7e5e9a4e99703ab7931
This commit is contained in:
Sam Leffler
parent
36f2577a40
commit
164a27b601
@ -1,4 +1,5 @@
|
||||
# Copyright (c) 2015 The Robigalia Project Developers
|
||||
# TBD: Google copyright
|
||||
# Licensed under the Apache License, Version 2.0 <LICENSE-APACHE or
|
||||
# http://www.apache.org/licenses/LICENSE-2.0> or the MIT license <LICENSE-MIT
|
||||
# or http://opensource.org/licenses/MIT>, at your option. All files in the
|
||||
@ -8,10 +9,10 @@
|
||||
name = "sel4-sys"
|
||||
version = "0.1.0"
|
||||
edition = "2018"
|
||||
authors = ["Corey Richardson <corey@octayn.net>"]
|
||||
authors = ["Corey Richardson <corey@octayn.net>", "Sam Leffler <sleffler@google.com>"]
|
||||
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"
|
||||
|
||||
@ -1,52 +1,70 @@
|
||||
# sel4-sys
|
||||
|
||||
[](https://crates.io/crates/sel4-sys)
|
||||
[](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
|
||||
|
||||
Loading…
Reference in New Issue
Block a user