seL4 / microkit

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

delay during PD initialization and execution #39

Open podhrmic opened 10 months ago

podhrmic commented 10 months ago

Hello!

I am porting an existing network driver code to sel4cp, and the driver has a couple of vTaskDelay() calls (it is for FreeRTOS).

Is there a recommended way of handling such case - e.g. I need my PD to suspend for a short time before continuing in execution?

I can think of the following options:

  1. refactor the code so it fits the event driven paradigm of sel4cp (effectively a state machine) - not practical, the state machine size could get out of hand rather quickly
  2. use pp_call to a timer to get current system time, and busy wait until the desired time elapses - rather inefficient
  3. something else?

@Ivan-Velickovic @nspin

Ivan-Velickovic commented 10 months ago

Ideally it would be the first option. From our experience at TS, we have been able to design and implement drivers without any use of blocking. I haven't looked closely at that FreeRTOS ethernet driver, but given that we've been able to go without any use of sleep() or equivalent functionality, I'm guessing that the vTaskDelay() is not necessary.

However, while network drivers can fit into the event driven model, I understand that there will exist systems where it is genuinely not possible. Internally at TS we have started to run into these cases, and are looking at making a small co-routine library for seL4CP. I will keep you updated on this and hopefully we have something to show soon.

Nick has been using Rust's support for async operations, so may want to comment on that, assuming you're writing the driver in Rust.

nspin commented 10 months ago

I am indeed having success using Rust's async features for this kind of thing. Here is an implementation of sleep():

https://github.com/coliasgroup/rust-seL4/blob/748ec222e67f00fa849d8ded4d8bc4c3a1840f37/crates/sel4-async/timers/src/lib.rs#L51

Here is an impl sel4cp::Handler that runs futures:

https://github.com/coliasgroup/rust-seL4/blob/748ec222e67f00fa849d8ded4d8bc4c3a1840f37/crates/examples/sel4cp/http-server/components/http-server/src/reactor.rs#L153

podhrmic commented 10 months ago

@nspin very cool! I will give it a try!

podhrmic commented 10 months ago

@nspin how do you think the reactor would change if you had to break out the individual components to separate PDs? Looks like now_with_timer_driver() would become a pp_call to a timer component, smoltcp/server would be the main component (so basically no change), and the virtio driver would have to be factored out (similar to what we were trying to do here). Does that match your expectation?

If so, I would be happy to refactor your example in such a way, but I could not get the server to build outside of nix - do you have a CI job or an example for that?

nspin commented 10 months ago

@nspin how do you think the reactor would change if you had to break out the individual components to separate PDs? Looks like now_with_timer_driver() would become a pp_call to a timer component, smoltcp/server would be the main component (so basically no change), and the virtio driver would have to be factored out (similar to what we were trying to do here). Does that match your expectation?

I've just finished doing exactly that:

https://github.com/coliasgroup/rust-seL4/tree/d9777945ff261a40dbe35d8902377c073ad76e18/crates/examples/sel4cp/http-server

Note that the virtio-net-driver component does more copying than it needs to, because the virtio-drivers crate I'm using does not have a sufficiently low-level interface. When I move to a physical device on which we can benchmark, I'll of course strive for a performant implementation of the network driver PD, but, for now, I've just left it clunky and slow in order to be able to leverage that third party crate instead of writing my own virtio-net driver code.

If so, I would be happy to refactor your example in such a way, but I could not get the server to build outside of nix - do you have a CI job or an example for that?

I will work on a standalone demo for this code like https://github.com/GaloisInc/rust-seL4-sel4cp-demo.

nspin commented 10 months ago

I've just finished doing exactly that:

https://github.com/coliasgroup/rust-seL4/tree/d9777945ff261a40dbe35d8902377c073ad76e18/crates/examples/sel4cp/http-server

I've cleaned this up and created a new repo:

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