I’ve been taking a look at mutex implementations in the camkes-app example and I had a question.


In the mutex example here https://github.com/seL4/camkes/tree/master/apps/mutex suppose I wanted to extend to add a third component C


I need to add the corresponding camkes, source, Kbuild, and Kconfig files and then I need to add connections to the master mutex.camkes file correct?

My first intuition was to add a connector:

               Assembly {



                                             Connection seL4MyConnector connection(from c.lock, to b.lock);





But this yields and error saying something to the effect “seL4MyConnector expects one from endpoint and two are specified”

To remedy this I added another lock component to B, and made a connection between C and this new lock B provides. The new lock being implemented by the same template.


My Questions:

In this scenario do A B and C still have access to the same mutex?

If A has a lock on the mutex, then C requests a lock, will this cause A to be unable to release the lock?

In my mental model I have three threads of control, one each for A B and C, if A has a lock and then C requests a lock, does this block B (when it receives a message from C and is now blocked on requesting the mutex)? Then when A tries to release, B is blocked and cannot release the mutex on A’s behalf. To put it another way, does this mutex example rely on B having direct access to the templated code and there only being two components?


Secondarily, in the lockserver example https://github.com/seL4/camkes/tree/master/apps/lockserver a situation is presented where three clients access a single mutex through a single server. Would there be an issue if one of the clients also acted as the server? So for instance if A implemented the three pairs of lock unlock functions instead of the server and then B and C used seL4RPCCall connections to A in order to access them, would there be any synchronization issues?


I’m relatively new to this and am trying to build a system with the help of camkes and I want to make sure I understand this before I get too far. I don’t want to be working under incorrect assumptions.


Thanks for taking the time to read this.




Jeff Brandon

Associate Staff

MIT Lincoln Laboratory

Secure Resilient Systems and Technology

Ph:   +1 781.981.9233