Mutexes on L4Ka::Pistachio?

Hi everybody,

what's the canonical way to implement locking of critical
sections (so that only one thread can enter at a time, i.e.
mutexes) with Pistachio?

On OKL4, there's a kernel-supported mutex_t object in
their lib, but I see nothing similar in L4Ka::Pistachio; neither
in the spec, nor in the source of kernel and user.

If the kernel doesn't provide mutexes, they have to be
implemented in user space, right? I'm thinking of something
like a dedicated 'mutex' manager thread per task, that other
threads would [L]IPC to lock and unlock mutexes. Does that
make sense, or am I completely lost here?

Thanks.
-Farid.