This looks really interesting. I don't feel qualified to offer any feedback but I do have a question...
I'm particularly curious about the "single producer, single consumer, lockless bounded queues implemented as ring buffers" mentioned for the cross-address-space communications. Is this taken from any existing seL4 library/util (e.g. is it similar at all to shared memory communication in CAMkES?) or is it something novel developed specifically for the driver framework? In my research into the Pony language on seL4 I have run into the problem of all Pony's actor communication being single-address-space-assuming datastructures. There are some interesting lock-free SPMC and MPSC queues under the hood that only use C atomics, which I've been able to port over to the seL4 environment, but they're ultimately implemented as single-address-space linked lists, so something like this could be a useful tool for looking at communication between actors in different address spaces. (although Pony's message-passing is also built around an assumption the queues are unbounded... which might just not be workable at all between confined components. This is a discussion point for my thesis though :) ) Cheers, Stewart Webb _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
