5 Dec
2017
5 Dec
'17
12:24 a.m.
Hi everyone, I have built a very simple application that loads another process, which is very similar to the tutorials. For testing I wanted to send from the second process to the first one using seL4_Send and observe that the second process never continues after the seL4_Send blocked, despite the receiver called seL4_Recv and got the message. If I call seL4_Call and the receiver does seL4_Recv + seL4_ReplyRecv it works without any other changes to the code. I am wondering if I am understanding something fundamentally wrong and/or what the best strategy to debug this behavior is. Thanks for your help! Cheers, Stefan