jon.recoil.org

Module Capsule_primSource

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.

Sourcemodule Access : sig ... end

An Access.t allows wrapping and unwrapping Data.t values from the current capsule.

Sourceval current : unit -> Access.packed @@ portable

Obtain an Access.t for the current capsule. Since we do not know the brand for the current capsule, we receive a fresh one.

Sourcetype initial

The brand for the initial capsule.

Sourceval initial : initial Access.t

An Access.t for the initial capsule

Sourceval is_initial_thread : unit -> bool @@ portable

Returns whether the current thread is the initial thread. Does *not* guarantee that the current capsule is the initial capsule.

  • alert maybe_still_concurrent Being on the initial thread does not provide any guarantees about thread-safety. This fact should only be used to avoid contention.
Sourceval is_initial_domain : unit -> bool @@ portable

Returns whether the current domain is the initial domain. Does *not* guarantee that the current capsule is the initial capsule.

  • alert maybe_still_concurrent Being on the initial domain does not provide any guarantees about thread-safety. This fact should only be used to avoid contention.
Sourcemodule Password : sig ... end

Passwords represent permission to get access to a capsule.

Sourcemodule Key : sig ... end

Keys represent the ownership of the capsule.

Sourceval create : unit -> Key.packed @ unique @@ portable

create () creates a new capsule with an associated key.

Sourceval access : ('a : value_or_null) 'k. password:'k Password.t @ local -> f:('k Access.t -> 'a @ unique once portable contended) @ local once portable -> 'a @ unique once portable contended @@ portable

access ~password ~f runs f within the capsule 'k, providing it with an Access.t for 'k. The result is within 'k so it must be portable and it is marked contended.

Sourceval access_local : ('a : value_or_null) 'k. password:'k Password.t @ local -> f:('k Access.t -> 'a @ local unique portable contended) @ local once portable -> 'a @ local unique portable contended @@ portable

As access, but returns a local value.

Sourceval access_shared : ('a : value_or_null) 'k. password:'k Password.Shared.t @ local -> f:('k Access.t @ shared -> 'a @ portable contended) @ local once portable -> 'a @ portable contended @@ portable

shared_access ~password ~f runs f within the capsule 'k, providing it with a shared Access.t for 'k. The result is within 'k so it must be portable and it is marked contended.

Sourceval access_shared_local : ('a : value_or_null) 'k. password:'k Password.Shared.t @ local -> f: ('k Access.t @ shared -> 'a @ local portable contended) @ local once portable -> 'a @ local portable contended @@ portable

As access_shared, but returns a local value.

Sourcemodule Data : sig ... end

Pointers to data within a capsule.

Sourcemodule Extended : sig ... end

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