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
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
