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 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 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. ---