"Yuxin" == Yuxin Ren ryx@gwmail.gwu.edu writes:
Yuxin> Thank you all for your replies. But those Yuxin> replies are confusing to me. My understanding is, IPC provided Yuxin> by current sel4 kernel does not support communication between Yuxin> two process on different cores. Is this true?
Yes. The released verified seL4 kernel is single-core only.