Module Capsule_expert.Password

'k t is the type of "passwords" representing permission for the current thread to have uncontended access to the capsule 'k. They are only ever available locally, so cannot move between threads.

Obtaining a 'k t requires exclusive access to 'k, either through a 'k Key.t @ unique or indirectly through acquiring a mutex or rw-lock associated with 'k. The mode system prevents retaining the 'k t after releasing access to the capsule. This guarantees that uncontended access to the capsule is only granted to one thread at a time.

A boxed version of Password.t for places where you need a type with layout value.

Shared passwords represent permission to get shared access to a capsule.

shared t downgrades a 'k password to a 'k shared password.

with_current k f calls f with a password for the current capsule k.

Note f cannot return the unforkable password, as the result is forkable.