Add a crate for embeded_hal (etc.) driver adapters #25

protoben · 2023-10-03T18:13:55Z

This PR adds a sel4-hal-adapters crate to provide generic adapters that handle IPC for HW drivers, using existing HAL traits. Currently, it only contains an adapter for the smoltcp::phy::Device trait, but additional adapters could be added using the same pattern.

I've also modified the http-server example to use the smoltcp::phy adapter, as an example of how this could be used. The smoltcp::phy::Driver implementation has been moved into this crate, since this is (maybe) a better place for it to live.

protoben · 2023-10-03T20:23:23Z

Currently trying to figure out why CI is failing. I previously tested on the standalone http demo.

Also, I keep getting the following error when I make various changes. (I most recently got it when trying to add a debug_print to crates/examples/microkit/http-server/pds/virtio-net-driver/src/main.rs.)

    Checking sel4-microkit v0.1.0 (/nix/store/7kvxif22s3y7wbwsy1fps7k820xbjchp-workspace/src/sel4-microkit)
error[E0412]: cannot find type `Reply` in crate `sel4`
  --> src/sel4-microkit/src/cspace.rs:12:35
   |
12 | pub(crate) const REPLY_CAP: sel4::Reply = slot_to_local_cptr(4);
   |                                   ^^^^^ not found in `sel4`

error[E0599]: no method named `nb_send_recv` found for struct `LocalCPtr` in the current scope
  --> src/sel4-microkit/src/handler.rs:60:51
   |
60 |             (None, Some(action)) => action.cptr().nb_send_recv(
   |                                     --------------^^^^^^^^^^^^ method not found in `LocalCPtr<Unspecified>`

Some errors have detailed explanations: E0412, E0599.
For more information about an error, try `rustc --explain E0412`.
error: could not compile `sel4-microkit` (lib) due to 2 previous errors

Any idea what might be going on there?

nspin · 2023-10-03T22:19:26Z

Thank you, @protoben! This is an exciting direction.

Also, I keep getting the following error when I make various changes. (I most recently got it when trying to add a debug_print to crates/examples/microkit/http-server/pds/virtio-net-driver/src/main.rs.)

It looks like the sel4-microkit crate is being compiled against a seL4 configuration without MCS. What is your development environment like? Are you building it in the context of a project like rust-microkit-http-server-demo, or are you using Nix shell in the context of this repository?

The Build docs job is failing because the meta crate unconditionally depends on the new sel4-hal-adapters crate, which in turn depends on sel4-microkit, which does not support non-MCS kernel configurations. The meta crate is build and documented for a range of kernel configurations, some of which do not include MCS. The solution would be to make sel4-hal-adapaters an optional dependency of meta, active only when the sel4-microkit feature is enabled. You could use the way sel4-microkit-message is handled in meta as an example.

The Run other tests job initially failed due to a transient build-time networking failure, but I re-ran it, and now everything builds but the HTTP server test fails with an HTTP timeout.

The Check dependencies job that failed should actually be called Check source (fixed in #26). It's failing because the Nix code that checks (and, in some cases, generates) this project's Cargo.toml files doesn't know about the Cargo.toml file that you've added. I'll put some thought into how to make this approach I've taken less intrusive. A good fix for now would be adding the entry "sel4-hal-adapters" = "crates/sel4-hal-adapters"; to the attribute set externalCratePathAttrs at

rust-sel4/hacking/nix/scope/generated-cargo-manifests/default.nix

Line 45 in 2c3720d

externalCratePathAttrs = {

protoben · 2023-10-04T17:07:05Z

Thanks! Making sel4-hal-adapters depend on sel4-microkit like you describe fixed the build error I was getting.

Still trying to figure out the timeout issue.

nspin · 2023-10-04T22:10:39Z

Still trying to figure out the timeout issue.

Turns out the HTTP server pexpect script for testing wasn't logging all of QEMU's output. I've fixed that in #29.

Apparently this line is being executed: https://github.com/protoben/rust-seL4/blob/ed936b3749b7db329ff9a2805fd1030074b2f155/crates/sel4-hal-adapters/src/smoltcp/phy/handler.rs#L153

crates/examples/microkit/http-server/pds/virtio-net-driver/src/main.rs

nspin · 2023-10-04T22:59:17Z

By the way, I'm still working out to best lay out information about the Nix code for testing and CI for contributors who wish to use it. It might be useful for debugging in this case. So, in the meantime, here are some useful Nix invocations:

Build and run the HTTP server demo:

nix-build -A worlds.aarch64.qemu-arm-virt.microkit.instances.microkit.examples.http-server.links && ./result/simulate

Build and run the automated HTTP server demo test just like CI:

nix-build -A worlds.aarch64.qemu-arm-virt.microkit.instances.microkit.examples.http-server.automate && ./result

Drop into a Nix shell with an environment suitable for hacking on the HTTP server demo crates:

nix-shell -A worlds.aarch64.qemu-arm-virt.microkit.shell

From inside the Nix shell, build a relevant crate:

cargo b $h --target aarch64-sel4-microkit -p microkit-http-server-example-virtio-net-driver

($h combines a few Cargo flags for convenience.)

crates/examples/microkit/http-server/helpers/smoltcp-phy-impl/src/lib.rs

crates/examples/microkit/http-server/pds/virtio-net-driver/Cargo.toml

crates/sel4-hal-adapters/Cargo.toml

protoben · 2023-10-09T22:12:24Z

@nspin Any idea why the "Check source" job is still failing? Running nix-build -A generatedSources.check --no-out-link succeeds locally.

In the CI, the error seems to be Cargo.toml differs from /nix/store/lar2w5hryj1xr76i17w52xzqcp190ivl-x.toml, which I'm not sure how to rectify.

nspin · 2023-10-10T04:57:03Z

@nspin Any idea why the "Check source" job is still failing? Running nix-build -A generatedSources.check --no-out-link succeeds locally.

The Makefile target check-source (which is what the Check source job invokes) uses nix-build -A generatedSources.check --no-out-link to generate a script that actually does the checking:

rust-sel4/Makefile

Line 45 in 8e90b88

script=$$($(nix_build) -A generatedSources.check --no-out-link) && $$script

So, while that nix-build invocation may be succeeding, the Make invocation make check-source is failing.

In the CI, the error seems to be Cargo.toml differs from /nix/store/lar2w5hryj1xr76i17w52xzqcp190ivl-x.toml, which I'm not sure how to rectify.

The stderr output right above that message is actually a diff, where /nix/store/lar2w5hryj1xr76i17w52xzqcp190ivl-x.toml is the expected value of Cargo.toml, modulo formatting. I should make that output more clear with a better derivation name.

--- Cargo.toml
+++ /nix/store/lar2w5hryj1xr76i17w52xzqcp190ivl-x.toml
@@ -12,7 +12,6 @@
       "crates/examples/microkit/banscii/pds/pl011-driver/interface-types",
       "crates/examples/microkit/hello/pds/hello",
       "crates/examples/microkit/http-server/helpers/virtio-hal-impl",
-      "crates/examples/microkit/http-server/helpers/smoltcp-phy-impl",
       "crates/examples/microkit/http-server/pds/server",
       "crates/examples/microkit/http-server/pds/server/core",
       "crates/examples/microkit/http-server/pds/sp804-driver",
@@ -21,6 +20,7 @@
       "crates/examples/microkit/http-server/pds/virtio-blk-driver",
       "crates/examples/microkit/http-server/pds/virtio-blk-driver/interface-types",
       "crates/examples/microkit/http-server/pds/virtio-net-driver",
+      "crates/examples/microkit/http-server/pds/virtio-net-driver/interface-types",
       "crates/examples/root-task/example-root-task",
       "crates/examples/root-task/example-root-task-without-runtime",
       "crates/examples/root-task/hello",

Quick fix for the failure

The code checking Cargo.toml doesn't know about the crate at "crates/examples/microkit/http-server/helpers/smoltcp-phy-impl". This can be resolved by adding another entry to externalCratePathAttrs. Specifically, "microkit-http-server-example-smoltcp-phy-impl" = "crates/examples/microkit/http-server/helpers/smoltcp-phy-impl";.

https://github.com/protoben/rust-seL4/blob/33fbde82f5653a6401d21e039284971de990a27c/hacking/nix/scope/generated-cargo-manifests/default.nix#L45-L52

You removed the crate at "crates/examples/microkit/http-server/pds/virtio-net-driver/interface-types", but the checking script still thinks it exists. That's because this file exists: https://github.com/protoben/rust-seL4/blob/33fbde82f5653a6401d21e039284971de990a27c/hacking/cargo-manifest-sources/crates/examples/microkit/http-server/pds/virtio-net-driver/interface-types/crate.nix. Deleting that file would resolve this difference.

Actual solution

Managing Cargo manifests for this many crates is tedious and error-prone: keeping all of the relative paths correct; using the same versions of dependencies throughout the project; keeping metadata up to date; etc. To make things easier and more robust, I've been managing these files using some Nix expressions.

The Cargo.toml files which are not explicitly declared to be outside of the domain of this automation are generated from the Nix expressions in ./hacking/cargo-manifest-sources/crates. make update-generated-sources does the generating, and make check-generated-sources (a prerequisite of make check-sources) makes sure they're up to date.

The Cargo manifest generation process is very intentionally disentangled from the rest of the project's build + test code. However, as this PR has shown, developers who add new crates or otherwise change the dependency graph still need to interact with this automation. So, I'll spend the next few days improving it and documenting it (including how to bypass it) to make things easier for future contributors. Sorry for the trouble this time around!

In the meantime, here's a suggestion to complete this PR:

https://github.com/nspin/rust-sel4/tree/nspin/wip/hal-adapter-pr-suggestion

nspin · 2023-10-10T04:58:52Z

By the way, the commit history for the protoben:hamlinb/hal-adapters branch isn't quite right. It appears that some upstream commits have been appended rather than prepended to the PR.

nspin · 2023-10-10T12:24:45Z

Also, I have an idea about moving some of the code in this PR around a bit. Perhaps we should discuss this idea before you go to the effort of putting the finishing touches on the PR as it exists now.

I noticed that you moved the contents of what was the sel4-shared-ring-buffer-smoltcp crate into the new sel4-hal-adapters crate. I think there is value in leaving sel4-shared-ring-buffer-smoltcp decoupled from the sel4-hal-adapters. In particular, sel4-hal-adapters is Microkit-specific, whereas sel4-shared-ring-buffer-smoltcp can be used in contexts outside of Mircokit. sel4-hal-adapters could re-export or wrap some of sel4-shared-ring-buffer-smoltcp's API for convenience, though, for the best of both worlds.

What do you think about that?

protoben · 2023-10-11T16:41:19Z

That makes sense. I mentioned above that I had moved the phy::Driver implementation out of that crate. My motivation was that it would be easier to maintain the IPC if all the code that relied on its implementation details were kept in a single place.

You make a good point, though. I didn't consider that it might be useful outside of microkit.

I can re-work the PR to do as you suggest. I'll go ahead and mark it as a draft, for now.

protoben · 2023-10-11T16:43:05Z

By the way, the commit history for the protoben:hamlinb/hal-adapters branch isn't quite right. It appears that some upstream commits have been appended rather than prepended to the PR.

Hmm... I'm not sure how I managed that, since I've just been rebasing. Thanks for pointing it out. I'll try to fix it.

nspin · 2023-10-12T20:26:55Z

That makes sense. I mentioned above that I had moved the phy::Driver implementation out of that crate. My motivation was that it would be easier to maintain the IPC if all the code that relied on its implementation details were kept in a single place.

I'm under the impression that the behavior of the sel4-shared-ring-buffer-smoltcp crate, along with the behavior it expects from the other side of the shared ring buffer, is (informally) specified by the sDDF. Are there details related to that crate's behavior or interface that should be internal?

For IPC that we ourselves have define, like the sel4_hal_adapters::smoltcp::phy::Request type, I think that definitely makes sense to keep internal to the sel4-hal-adapters crate.

The scope of my suggestion is just the sel4-shared-ring-buffer-smoltcp. Concretely, I'm suggesting that we leave it as it is, and perhaps re-export or wrap its export in sel4-hal-adapters for the convenience of sel4-hal-adapters users.

nspin · 2023-10-14T09:57:38Z

By the way, I'm improving the sel4-shared-ring-buffer-related crates to be robust against misbehaved or malicious peers. The API of the sel4-shared-ring-buffer crate won't change drastically, and I haven't started working on the sel4-shared-ring-buffer-smoltcp crate yet, but I figured, for the sake of synchronization, I should ask: do you know yet whether you are planning on making any substantial changes to the sel4-shared-ring-buffer-smoltcp (or wherever that code ends up)?

protoben · 2023-10-19T23:28:24Z

No, I think my stuff should be pretty much contained in hal-adapters.

nspin · 2023-10-20T01:19:36Z

Here is the PR: #32

nspin · 2023-10-24T04:07:57Z

Some work towards getting the Cargo manifest management tools into a more appropriate state for collaboration: #36

nspin · 2023-10-26T00:11:55Z

. So, I'll spend the next few days improving it and documenting it (including how to bypass it) to make things easier for future contributors. Sorry for the trouble this time around!

Here is the new Cargo management manifest tool documentation:

https://github.com/seL4/rust-sel4/tree/main/hacking/cargo-manifest-management

protoben · 2023-11-06T16:28:19Z

Sorry I haven't been keeping up on this. I got busy with other projects at work.

I'm going to try and fix this up (with the changes you suggested above) this week. I'll probably start fresh on a new branch so the rebase is cleaner.

nspin · 2023-11-06T22:37:10Z

No problem. Let me know how I can help! If the related changes that have happened underneath this PR (mentioned in this thread) get in your way, feel free to reach out here or on https://mattermost.trustworthy.systems/.

nspin · 2023-12-12T02:07:21Z

@protoben Is this PR ready for review?

protoben · 2023-12-14T17:34:07Z

Yes! Sorry, should have pinged you.

…

-------- Original Message --------

On Dec 11, 2023, 6:07 PM, Nick Spinale wrote: Is this PR ready for review? — Reply to this email directly, [view it on GitHub](#25 (comment)), or [unsubscribe](https://github.com/notifications/unsubscribe-auth/ABDLJ523YX2WLZHJSGLSB73YI636LAVCNFSM6AAAAAA5RMQMJWVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTQNJRGE4DSMBXGI). You are receiving this because you were mentioned.Message ID: ***@***.***>

nspin · 2023-12-20T08:25:26Z

Could you add copyright + license headers to the files mentioned in https://github.com/seL4/rust-sel4/actions/runs/6910861641/job/18804620813?pr=25?

The following files have no copyright and licensing information:
* crates/sel4-hal-adapters/Cargo.nix
* crates/sel4-hal-adapters/src/embedded_hal/mod.rs
* crates/sel4-hal-adapters/src/lib.rs
* crates/sel4-hal-adapters/src/smoltcp/mod.rs
* crates/sel4-hal-adapters/src/smoltcp/phy/device.rs
* crates/sel4-hal-adapters/src/smoltcp/phy/handler.rs
* crates/sel4-hal-adapters/src/smoltcp/phy/mod.rs

nspin · 2023-12-20T08:32:09Z

Otherwise, code looks great.

I noticed you dropped the use of this new crate in the HTTP server demo. Was that intentional? It would be cool to have a demo showing off this crate (could be separate from the HTTP serve demo), but we can add that later.

protoben · 2023-12-22T19:21:27Z

I noticed you dropped the use of this new crate in the HTTP server demo. Was that intentional? It would be cool to have a demo showing off this crate (could be separate from the HTTP serve demo), but we can add that later.

Intentional, yes, but just because I was having trouble finding time to update that part. I suspect it won't be hard, but I haven't had time to look at it. I figured I would make that into a separate PR, if that sounds reasonable.

I'd be fine with modifying the existing HTTP example or forking it off into a separate one, whichever seems best to you.

protoben · 2023-12-23T00:49:32Z

Could you add copyright + license headers to the files mentioned in https://github.com/seL4/rust-sel4/actions/runs/6910861641/job/18804620813?pr=25?

Oops. Fixed.

Also, looks like make check-dependencies was failing due to a vulnerability found in zerocopy 0.7.6. I bumped it to 0.7.32 and made a separate PR (#48).

nspin · 2023-12-23T03:47:27Z

I figured I would make that into a separate PR, if that sounds reasonable.

Sounds good to me.

Also, looks like make check-dependencies was failing due to a vulnerability found in zerocopy 0.7.6. I bumped it to 0.7.32 and made a separate PR (#48).

Merged! Thanks.

nspin · 2023-12-23T05:50:59Z

crates/sel4-hal-adapters/Cargo.nix

+{ mk, versions, localCrates, smoltcpWith, serdeWith, authors }:
+
+mk {


If you replace these lines with

{ mk, mkDefaultFrontmatterWithReuseArgs, defaultReuseFrontmatterArgs, versions, localCrates, smoltcpWith, serdeWith, authors }: mk { nix.frontmatter = mkDefaultFrontmatterWithReuseArgs (defaultReuseFrontmatterArgs // { copyrightLines = defaultReuseFrontmatterArgs.copyrightLines ++ [ "Copyright 2023, Galois, Inc." ]; });

then the copyright lines in the adjacent generated Cargo.toml file will match those in this file.

Not sure if anyone cares about the copyright lines in the generated Cargo.toml files, though.

Or, after rebasing on top of #49,

{ mk, overrideDefaultFrontmatter, versions, localCrates, smoltcpWith, serdeWith, authors }: mk { nix.frontmatter = overrideDefaultFrontmatter { extraCopyrightLines = [ "Copyright 2023, Galois, Inc." ]; };

Again, only if you care about copyright info in the generated Cargo.toml file.

nspin · 2023-12-23T06:39:44Z

After rebasing on top of main (specifically, #48), this is ready to be merged!

Signed-off-by: Ben Hamlin <hamlinb@galois.com>

protoben requested a review from nspin as a code owner October 3, 2023 18:13

nspin reviewed Oct 4, 2023

View reviewed changes

crates/examples/microkit/http-server/pds/virtio-net-driver/src/main.rs Outdated Show resolved Hide resolved

nspin reviewed Oct 4, 2023

View reviewed changes

protoben marked this pull request as draft October 11, 2023 16:41

protoben force-pushed the hamlinb/hal-adapters branch from 33fbde8 to afc95f0 Compare November 18, 2023 01:18

nspin marked this pull request as ready for review December 20, 2023 08:22

protoben force-pushed the hamlinb/hal-adapters branch from 26c71c8 to 603e408 Compare December 23, 2023 00:52

protoben requested a review from nspin December 23, 2023 00:54

nspin reviewed Dec 23, 2023

View reviewed changes

protoben added 2 commits December 25, 2023 11:18

Add HAL-adapters crate

d4c0961

Signed-off-by: Ben Hamlin <hamlinb@galois.com>

Add licensing info to hal-adapters crate

e5a2707

Signed-off-by: Ben Hamlin <hamlinb@galois.com>

nspin force-pushed the hamlinb/hal-adapters branch from 603e408 to e5a2707 Compare December 25, 2023 16:18

nspin approved these changes Dec 25, 2023

View reviewed changes

nspin merged commit 3318293 into seL4:main Dec 25, 2023
15 checks passed

nspin mentioned this pull request Jun 19, 2024

Introduce more driver abstractions #152

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add a crate for embeded_hal (etc.) driver adapters #25

Add a crate for embeded_hal (etc.) driver adapters #25

protoben commented Oct 3, 2023

protoben commented Oct 3, 2023

nspin commented Oct 3, 2023 •

edited

Loading

protoben commented Oct 4, 2023

nspin commented Oct 4, 2023

nspin commented Oct 4, 2023

protoben commented Oct 9, 2023

nspin commented Oct 10, 2023

nspin commented Oct 10, 2023

nspin commented Oct 10, 2023

protoben commented Oct 11, 2023

protoben commented Oct 11, 2023

nspin commented Oct 12, 2023 •

edited

Loading

nspin commented Oct 14, 2023

protoben commented Oct 19, 2023

nspin commented Oct 20, 2023

nspin commented Oct 24, 2023 •

edited

Loading

nspin commented Oct 26, 2023 •

edited

Loading

protoben commented Nov 6, 2023

nspin commented Nov 6, 2023

nspin commented Dec 12, 2023 •

edited

Loading

protoben commented Dec 14, 2023 via email

nspin commented Dec 20, 2023

nspin commented Dec 20, 2023

protoben commented Dec 22, 2023

protoben commented Dec 23, 2023

nspin commented Dec 23, 2023

nspin Dec 23, 2023

nspin Dec 23, 2023

nspin Dec 23, 2023

nspin commented Dec 23, 2023 •

edited

Loading

		{ mk, versions, localCrates, smoltcpWith, serdeWith, authors }:

		mk {

Add a crate for embeded_hal (etc.) driver adapters #25

Add a crate for embeded_hal (etc.) driver adapters #25

Conversation

protoben commented Oct 3, 2023

protoben commented Oct 3, 2023

nspin commented Oct 3, 2023 • edited Loading

protoben commented Oct 4, 2023

nspin commented Oct 4, 2023

nspin commented Oct 4, 2023

protoben commented Oct 9, 2023

nspin commented Oct 10, 2023

Quick fix for the failure

Actual solution

nspin commented Oct 10, 2023

nspin commented Oct 10, 2023

protoben commented Oct 11, 2023

protoben commented Oct 11, 2023

nspin commented Oct 12, 2023 • edited Loading

nspin commented Oct 14, 2023

protoben commented Oct 19, 2023

nspin commented Oct 20, 2023

nspin commented Oct 24, 2023 • edited Loading

nspin commented Oct 26, 2023 • edited Loading

protoben commented Nov 6, 2023

nspin commented Nov 6, 2023

nspin commented Dec 12, 2023 • edited Loading

protoben commented Dec 14, 2023 via email

nspin commented Dec 20, 2023

nspin commented Dec 20, 2023

protoben commented Dec 22, 2023

protoben commented Dec 23, 2023

nspin commented Dec 23, 2023

nspin Dec 23, 2023

Choose a reason for hiding this comment

nspin Dec 23, 2023

Choose a reason for hiding this comment

nspin Dec 23, 2023

Choose a reason for hiding this comment

nspin commented Dec 23, 2023 • edited Loading

nspin commented Oct 3, 2023 •

edited

Loading

nspin commented Oct 12, 2023 •

edited

Loading

nspin commented Oct 24, 2023 •

edited

Loading

nspin commented Oct 26, 2023 •

edited

Loading

nspin commented Dec 12, 2023 •

edited

Loading

nspin commented Dec 23, 2023 •

edited

Loading