[seL4] Re: sel4cp and device driver API's

Hi Eric,

On 1 Sep 2022, at 13:07, Eric Jacobs wrote:

I was looking into sel4cp (https://github.com/BreakawayConsulting/sel4cp) for some ideas about designing high-performance, high-security systems with seL4 and I had some questions about how it interfaces with devices.

I saw that there's an ethernet driver (example/tqma8xqp1gb/ethernet/eth.c) which is structured as a PD with two shared memory ring buffers (TX and RX) and associated notifications, without using IPC/ppcall at all in the API.

Insofar as IPC/ppcall is the cornerstone of performance in seL4, I wonder if there could be or should be a role for IPC/ppcall. Does using IPC in place of notifications here violate the "don't use IPC for synchronization" rule? I guess I'm not too clear on what the advantage of notifications is over IPC for things like shared memory buffers.

You certainly should not use IPC just for synchronisation, but if you have a two-way control flow then it becomes a question of one IPC vs two Signals.

I think my ideal goal would be something like a IPC-based API where one can pass in a (limited) number of scatter-gather vectors, plus some metadata (offloading parameters, priority, etc.), and could benefit from the fastpath. This would enable a high-performance stack that could take advantage of things like zero-copy buffering where applicable.

More generally, I also wonder how IPC fits in with bidirectional devices if we follow the strict priority-based call restrictions (recommended in seL4; required in sel4cp). If the device can both send and receive data, then it seems it has to be both a high-priority PD (to be called) and a low-priority PD (to call in to the stack), assuming that we are avoiding the use of blocking-style turnaround API's (such as read, recv, etc. - I feel those are best left at the application layers.)

You identify some of the relevant issues ;-) We have been looking at some of this in detail for our high-performance driver framework (see https://trustworthy.systems/projects/TS/drivers/, although that page is presently devoid of technical detail). We are preparing a release which is scheduled to happen at the time of the seL4 Summit in 5 weeks’ time. There will be an extensive report describing design and implementation. While the basic framework is in place and performs well (it outperforms Linux without even trying too hard…) there are a number of questions that still need further research, and are unlikely to be resolved by the time of the initial release. One of them is whether drivers should be active (synchronising with notifications only) or passive PDs (using PPCs). There are a bunch of tradeoffs to consider, and we need a fair amount of experimental work to settle it. The good news is that the effect the choice has on driver as well as client implementation is minimal (a few lines changed, possibly zero on the client side). Gernot