Module Capsule_prim.ExtendedSource

Capsules are a mechanism for safely having uncontended or shared access to mutable data from multiple threads.

We consider every piece of mutable data in the program to live inside of some capsule. This might be an explicit capsule created using this interface, or an implicit capsule created when a new task is spawned (which expects a portable closure). Whenever a 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.

Similarly, an implicit subcapsule is created when a subtask is forked (for example using Parallel.fork_join2). Unlike capsules, a subcapsule is allowed to read mutable data from its parent, as expressed by the shareable (as opposed to portable) requirement over the subtask's closure.

This module only provides interfaces that statically rule out data races. The Await and Parallel libraries augment capsules with various synchronization primitives that prevent data races dynamically.

Meaningful access to the value within a ('a, 'k) Data.t pointer requires an uncontended or shared 'k Access.t. An 'k Access.t can be synchronized using Sync.Mutex.with_lock from the Await library.

Alternatively, the three following modules Frozen, Owned and Scoped offer practical wrappers for common patterns when synchronizing capsule access.

Frozen represents a capsule whose contents have been permanently frozen: nobody may write to it, so everyone may read from it without synchronization.

Owned uses aliasing as a proxy for contention; owning a capsule uniquely is sufficient to access a capsule, since uniqueness guarantees that only one thread has access to it.

Scoped uses 'k Capsule.Password.t -- a token that is only ever available locally -- to grant permission for the current thread to have uncontended access to the capsule 'k for the duration of the current region. Locality guarantees that a password is not shared with other existing threads. Unlike Owned and the more direct Access.t, a Scoped.t crosses contention, and can hence be accessed from a different capsule.

A Scoped.Shared represents a temporary freeze: the capsule may only be read from for the duration of the local 'k Capsule.Password.Shared.t

Each wrapper offers various trade-offs; when making a choice over which kind of wrapper to use, it can be useful to observe whether a piece of data follows a common pattern:

• Does the data go through a phase where it gets initialized, after which it is only read from by multiple threads? You can create a Frozen using Frozen.create.
• Is it necessary to acquire locks for multiple capsules at the same time? A Scoped must be used.
• Are you trying to access some immutable part of your data? You do not need to acquire access to a capsule, you can use Data.get_id.

Frozen, Owned and Scoped can each be synchronized with a mutex or reader-writer lock in the Await or Parallel libraries