Hi,

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 {

                              Composition{

                                             …

                                             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.

Sincerely,

Jeff Brandon

Associate Staff

MIT Lincoln Laboratory

Secure Resilient Systems and Technology

Ph:   +1 781.981.9233