Module Capsule_expert

Capsules are a mechanism for safely having uncontended access to mutable data from multiple threads. The interface in this module ensures that only one thread can have uncontended access to that data at a time.

We consider every piece of mutable data in the program to live inside of some capsule. This might be an explicit capsule created by the user using this interface, or an implicit capsule created when a new thread is started. Whenever some thread is executing a function it has uncontended access to a single capsule and any new mutable data it creates is created within that capsule. We say that the function is "running within" the capsule.

Capsules are only ever associated with one thread at a time, which ensures there are no data races in the program. The implicit capsules created when a new thread is started are only ever associated with that thread. Explicit capsules can change which threads have uncontended access to them using synchronization primitives.

Each explicit capsule is associated with a type "brand" -- written 'k throughout this interface -- which allows us to statically reason about access to the capsule within the type system. In the documentation of this interface we will often use 'k to refer to the capsule associated with that brand.

When you create a new capsule 'k via create, the library returns a unique 'k Key.t that grants you exclusive ownership of that capsule. You can temporarily hand out a Password.t (or Password.Shared.t) to functions or threads that need to access the capsule. This ensures that mutable data is only ever accessed in accordance with the capsule's concurrency rules.

Using a 'k Key.t more than once turns it into an aliased key. Aliased global keys indicate that the corresponding capsule has been permanently shared across threads with read-only access.

This module only provides interfaces that statically rule out data races. The Await library augments capsules with various synchronization primitives that prevent races at runtime.