Thanks for this. I was particularly struck by 'Time as a first class resource' and the implications for security. Side-channel attacks are a big concern for me. Well done.
On Fri, Oct 21, 2022 at 1:09 AM Gernot Heiser <ger...@unsw.edu.au> wrote: > > Hi Sid, > > I talked a bit more about IPC and why it doesn’t make sense cross-core at my > seL4 Overview at last week's Summit. The videos will hopefully go up next > week, but you can find the slides at > https://trustworthy.systems/publications/papers/Heiser_22%3Asel4s-o.abstract > > Gernot > > > On 5 Oct 2022, at 07:16, Sid Agrawal <siag...@cs.ubc.ca> wrote: > > > > Hi, > > I came across Gernot Heiser's blog post on "How to use seL4 IPC" [1]. The > > article explicitly says that doing cross-core IPC is a bad idea. This > > statement led to a series of questions for me, which I hope you guys can > > help me with. > > > > Scenario > > ------------ > > We have a system with two cores. Let's say that a physical memory server is > > running on core0, my application is on core1, and they are somehow pinned > > to those cores. The application wants some physical memory (frame > > capabilities) from the memory server. > > > > Questions > > ------------- > > Q1. Will the application be able to invoke the endpoint given that the TCB > > which will respond to it is on a separate core? If yes, will sending a > > capability back via cross-core IPC be allowed? I did not read anything in > > the manual which said otherwise. > > > > Q2. Why is a cross-core IPC a bad idea? This might be a loaded question, > > but I am not able to appreciate the badness of the idea :) > > > > Q3. What would be the right way to do it? For example, in > > Barrelfish(limited experience from a course), the application(on core1) > > would make an IPC to a monitor running on the same core1. This monitor did > > synchronization with another monitor running on the other core(core0) via a > > shared memory region (all in user space). That monitor(core0) then sent an > > IPC to the memory server running on core0. And then back again via the > > monitors. > > > > Best, > > Sid > > > > > > [1] > > https://microkerneldude.org/2019/03/07/how-to-and-how-not-to-use-sel4-ipc/ > > _______________________________________________ > > Devel mailing list -- devel@sel4.systems > > To unsubscribe send an email to devel-leave@sel4.systems > > _______________________________________________ > Devel mailing list -- devel@sel4.systems > To unsubscribe send an email to devel-leave@sel4.systems -- Bob Trower --- From Gmail webmail account. --- _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
