On 30 Sep 2022, at 15:53, mincheol@vt.edu wrote:

Hi,

I am trying to benchmark seL4's cross core IPC. I was able to run the IPC tutorial program and am now trying to run the server and the client on different VCPU. I found seL4_TCB_SetAffinity() but need to know the entry point of user program.

Please note that IPC makes little sense cross-core. seL4 IPC should be viewed as a way to execute a function in a different protection domain, which should not require forcing synchronisation of cores. The only reason cross-core IPC is supported at all is that it would take extra effort to prevent, but do not rely on the functionality being supported in the future. Synchronise cores with Notifications. For more detail see https://microkerneldude.org/2019/03/07/how-to-and-how-not-to-use-sel4-ipc/ Gernot