RFC-12: The seL4 Device Driver Framework

[lsf37]

Original Jira issue and discussion.

[lsf37]

Status update from 2024-07-25 TSC meeting: wait for framework to mature more, including support for further device classes.

[wom-bat]

The sDDF (available https://github.com/au-ts/sddf ) documented at https://trustworthy.systems/projects/drivers
is now significantly more mature. It's probably worth revisiting this,

[midnightveil]

I'd say it is also worth revisiting the text of the RFC, at the moment it just describes the framework, it says nowhere what the RFC is for: that is, to subsume sel4_libs (et al) and CAmkES as the 'recommended' way to use seL4.

Like, this just documents why we want the sDDF to exist, not why it should be part of the seL4 organisation/project?

[Indanz]

My main concern is that it doesn't provide a clean device class independent, generic communication framework, with the device class specific stuff build on top of that. At least I can't find it if I look in the source. I think sDDF should provide generic infrastructure that can also be used by non-devices, like servers and other inter process communication by user written code. Specifically the message passing queue mechanism used, no point in everyone re-inventing the wheel there. The device specific details are just details and extra metadata. Once you have a generic framework, you only have to proof that once for correctness.

[gernotheiser]

I don't understand this argument.
The sDDF is, as the name says, a device driver framework, that's intentionally OS-personality agnostic. We specifically don't want to impose on the design of the OS personality (and specifically removed the initial dependence on the microkit for that reason).
If you want to extend the model into the rest of the OS, you have LionsOS.

[Indanz]

All the reasons why you want a device driver framework to be OS-personality agnostic also apply to client-server communication frameworks. Furthermore, the problem that is being solved by sDDF is essentially generic client-server communication, with nothing device driver specific about it, other than perhaps cleaning caches for DMA.

That is one reason reason to make the message queue generic. The other reason is to avoid code duplication in different driver subsystems that need bulk data transfer via shared memory.

[gernotheiser]

When you say "make the message queue generic" are you arguing that the queues should be an independent piece of infrastructure and the sDDF a user of it, i.e. built on top? I.e. splitting the two?
I'd be open to this, as long as it doesn't compromise the simplicity.
It's certainly true that a lot of investment went into getting those queues right and performant, including a fair (and on-going) amount of formal verification.

[Indanz]

Implementation wise, yes. Organisation wise, I would still bundle it with sDDF to keep it all in one place for practical purposes, at least initially.