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.
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.)
Thoughts?
Thanks, -Eric