Urgh, sorry about the formatting. Repeating below...
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?
_______________________________________________
Devel mailing list -- [email protected]
To unsubscribe send an email to [email protected]
