Hello,

I am working on a lock system using templates (based on what is found here: https://github.com/seL4/camkes/tree/master/apps/mutex). This system can work, but there are some issues with the components just going back and forth when calling the locks. I believe this is an issue with multiple components using the same endpoint to communicate with the “lock server” and the calls getting pre-empted by other threads.

Here are the system calls that are used to hit the endpoint with the (un)lock request.

    seL4_Send(/*? ep ?*/, info);

    info = seL4_Recv(/*? ep ?*/, NULL);

And in the lock server:

    seL4_MessageInfo_t info = seL4_Recv(/*? ep ?*/, &sender);

    …do locking things

    seL4_Send(/*? ep ?*/, info);

So in order to prevent preempting by other threads, I went and changed the (un)lock request system call to

info = seL4_Call(/*? ep ?*/, info);

Using print statements, I was able to determine that the lock server receives the proper message on the endpoint and performs the locking operations. However, when it reaches the seL4_Send operation, the system locks up. This shouldn’t be the case, because one component is waiting on the endpoint with the seL4_Call, and the other is sending information on the same endpoint, especially when having separate Send & Recv statements works.

Am I doing something incorrect?

Thanks for your help,

Chris Guikema