picos 0.5.0 · OCaml Package

An independent thread of execution.

A fiber corresponds to an independent thread of execution. Fibers are created by schedulers in response to Spawn effects. A fiber is associated with a computation and either forbids or permits the scheduler from propagating cancelation when the fiber performs effects. A fiber also has an associated fiber local storage.

⚠️ Many operations on fibers can only be called safely from the fiber itself, because those operations are neither concurrency nor parallelism safe. Such operations can be safely called from a handler in a scheduler when it is handling an effect performed by the fiber. In particular, a scheduler can safely check whether the fiber has_forbidden cancelation and may access the FLS of the fiber.

Interface for rescheduling

val yield : unit -> unit

yield () asks the current fiber to be rescheduled.

ℹ️ The behavior is that

on OCaml 5, yield perform the Yield effect, and
on OCaml 4, yield will call the yield operation of the current handler.

val sleep : seconds:float -> unit

sleep ~seconds suspends the current fiber for the specified number of seconds.

Interface for current fiber

type t

Represents a fiber or an independent thread of execution.

⚠️ Unlike with most other concepts of Picos, operations on fibers are typically not concurrency or parallelism safe, because the fiber is considered to be owned by a single thread of execution.

type fiber := t

Type alias for Fiber.t within this signature.

val current : unit -> t

current () returns the current fiber.

⚠️ Extra care should be taken when storing the fiber object in any shared data structure, because, aside from checking whether two fibers are equal, it is generally unsafe to perform any operations on foreign fibers.

ℹ️ The behavior is that

on OCaml 5, current performs the Current effect, and
on OCaml 4, current will call the current operation of the current handler.

⚠️ The current operation must always resume the fiber without propagating cancelation. A scheduler may, of course, decide to reschedule the current fiber to be resumed later.

Because the scheduler does not discontinue a fiber calling current, it is recommended that the caller checks the cancelation status at the next convenient moment to do so.

val has_forbidden : t -> bool

has_forbidden fiber determines whether the fiber forbids or permits the scheduler from propagating cancelation to it.

ℹ️ This is mostly useful in the effect handlers of schedulers.

⚠️ There is no "reference count" of how many times a fiber has forbidden or permitted propagation of cancelation. Calls to forbid and permit directly change a single boolean flag.

⚠️ It is only safe to call has_forbidden from the fiber itself.

val forbid : t -> (unit -> 'a) -> 'a

forbid fiber thunk tells the scheduler that cancelation must not be propagated to the fiber during the execution of thunk.

The main use case of forbid is the implementation of concurrent abstractions that may have to await for something, or may need to perform other effects, and must not be canceled while doing so. For example, the wait operation on a condition variable typically reacquires the associated mutex before returning, which may require awaiting for the owner of the mutex to release it.

ℹ️ forbid does not prevent the fiber or the associated computation from being canceled. It only tells the scheduler not to propagate cancelation to the fiber when it performs effects.

⚠️ It is only safe to call forbid from the fiber itself.

val permit : t -> (unit -> 'a) -> 'a

permit fiber thunk tells the scheduler that cancelation may be propagated to the fiber during the execution of thunk.

It is possible to spawn a fiber with cancelation forbidden, which means that cancelation won't be propagated to fiber unless it is explicitly permitted by the fiber at some point.

⚠️ It is only safe to call permit from the fiber itself.

val is_canceled : t -> bool

is_canceled fiber is equivalent to

not (Fiber.has_forbidden fiber) &&
let (Packed computation) =
  Fiber.get_computation fiber
in
Computation.is_canceled computation

ℹ️ This is mostly useful in the effect handlers of schedulers.

⚠️ It is only safe to call is_canceled from the fiber itself.

val canceled : t -> (exn * Stdlib.Printexc.raw_backtrace) option

canceled fiber is equivalent to:

if Fiber.has_forbidden fiber then
  None
else
  let (Packed computation) =
    Fiber.get_computation fiber
  in
  Computation.canceled computation

ℹ️ This is mostly useful in the effect handlers of schedulers.

⚠️ It is only safe to call canceled from the fiber itself.

val check : t -> unit

check fiber is equivalent to:

if not (Fiber.has_forbidden fiber) then
  let (Packed computation) =
    Fiber.get_computation fiber
  in
  Computation.check computation

ℹ️ This is mostly useful for periodically polling the cancelation status during CPU intensive work.

⚠️ It is only safe to call check from the fiber itself.

val exchange : t -> forbid:bool -> bool

exchange fiber ~forbid sets the bit that tells the scheduler whether to propagate cancelation or not and returns the previous state.

val set : t -> forbid:bool -> unit

set fiber ~forbid sets the bit that tells the scheduler whether to propagate cancelation or not.

module FLS : sig ... end

Fiber local storage

Interface for spawning

val create_packed : forbid:bool -> Computation.packed -> t

create_packed ~forbid packed creates a new fiber record.

val create : forbid:bool -> 'a Computation.t -> t

create ~forbid computation is equivalent to create_packed ~forbid (Computation.Packed computation).

val spawn : t -> (t -> unit) -> unit

spawn fiber main starts a new fiber by performing the Spawn effect.

⚠️ Fiber records must be unique and the caller of spawn must make sure that a specific fiber record is not reused. Failure to ensure that fiber records are unique will break concurrent abstractions written on top the the Picos interface.

⚠️ If the main function raises an exception it is considered a fatal error. A fatal error should effectively either directly exit the program or stop the entire scheduler, without discontinuing existing fibers, and force the invocations of the scheduler on all domains to exit. What this means is that the caller of spawn should ideally arrange for any exception to be handled by main, but, in case that is not practical, it is also possible to allow an exception to propagate out of main, which is then guaranteed to, one way or the other, to stop the entire program. It is not possible to recover from a fatal error.

ℹ️ The behavior is that

on OCaml 5, spawn performs the Spawn effect, and
on OCaml 4, spawn will call the spawn operation of the current handler.

Interface for structuring

val get_computation : t -> Computation.packed

get_computation fiber returns the computation that the fiber is currently associated with.

val set_computation : t -> Computation.packed -> unit

set_computation fiber packed associates the fiber with the specified computation.

Interface for foreign fiber

val equal : t -> t -> bool

equal fiber1 fiber2 is physical equality for fibers, i.e. it determines whether fiber1 and fiber2 are one and the same fiber.

ℹ️ One use case of equal is in the implementation of concurrent primitives like mutexes where it makes sense to check that acquire and release operations are performed by the same fiber.

module Maybe : sig ... end

An unboxed optional fiber.

Interface for schedulers

val try_suspend : 
  t ->
  Trigger.t ->
  'x ->
  'y ->
  (Trigger.t -> 'x -> 'y -> unit) ->
  bool

try_suspend fiber trigger x y resume tries to suspend the fiber to await for the trigger to be signaled. If the result is false, then the trigger is guaranteed to be in the signaled state and the fiber should be eventually resumed. If the result is true, then the fiber was suspended, meaning that the trigger will have had the resume action attached to it and the trigger has potentially been attached to the computation of the fiber.

val unsuspend : t -> Trigger.t -> bool

unsuspend fiber trigger makes sure that the trigger will not be attached to the computation of the fiber. Returns false in case the fiber has been canceled and propagation of cancelation is not forbidden. Otherwise returns true.

⚠️ The trigger must be in the signaled state!

val resume : 
  t ->
  ((exn * Stdlib.Printexc.raw_backtrace) option, 'r)
    Stdlib.Effect.Deep.continuation ->
  'r

resume fiber k is equivalent to Effect.Deep.continue k (Fiber.canceled t).

val resume_with : 
  t ->
  ((exn * Stdlib.Printexc.raw_backtrace) option, 'b)
    Stdlib.Effect.Shallow.continuation ->
  ('b, 'r) Stdlib.Effect.Shallow.handler ->
  'r

resume_with fiber k h is equivalent to Effect.Shallow.continue_with k (Fiber.canceled t) h.

val continue : t -> ('v, 'r) Stdlib.Effect.Deep.continuation -> 'v -> 'r

continue fiber k v is equivalent to:

match Fiber.canceled fiber with
| None -> Effect.Deep.continue k v
| Some (exn, bt) ->
  Effect.Deep.discontinue_with_backtrace k exn bt

val continue_with : 
  t ->
  ('v, 'b) Stdlib.Effect.Shallow.continuation ->
  'v ->
  ('b, 'r) Stdlib.Effect.Shallow.handler ->
  'r

continue_with fiber k v h is equivalent to:

match Fiber.canceled fiber with
| None -> Effect.Shallow.continue_with k v h
| Some (exn, bt) ->
  Effect.Shallow.discontinue_with_backtrace k exn bt h

type Stdlib.Effect.t += private

| Current : t Stdlib.Effect.t

Schedulers must handle the Current effect to implement the behavior of current.

⚠️ The scheduler must eventually resume the fiber without propagating cancelation. This is necessary to allow a fiber to control the propagation of cancelation through the fiber.

The scheduler is free to choose which ready fiber to resume next. However, in typical use cases of current it makes sense to give priority to the fiber performing Current, but this is not required.

type Stdlib.Effect.t += private

| Yield : unit Stdlib.Effect.t

Schedulers must handle the Yield effect to implement the behavior of yield.

In case the fiber permits propagation of cancelation and the computation associated with the fiber has been canceled the scheduler is free to discontinue the fiber immediately.

The scheduler should give priority to running other ready fibers before resuming the fiber performing Yield. A scheduler that always immediately resumes the fiber performing Yield may prevent an otherwise valid program from making progress.

type Stdlib.Effect.t += private

| Spawn : {
1. fiber : t;
2. main : t -> unit;
} -> unit Stdlib.Effect.t

Schedulers must handle the Spawn effect to implement the behavior of spawn.

In case the fiber permits propagation of cancelation and the computation associated with the fiber has been canceled the scheduler is free to discontinue the fiber immediately before spawning new fibers.

The scheduler is free to run the newly created fiber on any domain and decide which fiber to give priority to.

⚠️ The scheduler should guarantee that, when Spawn returns normally, the given main will eventually be called by the scheduler and, when Spawn raises an exception, the main will not be called. In other words, Spawn should check cancelation just once and be all or nothing. Furthermore, in case a newly spawned fiber is canceled before its main is called, the scheduler must still call the main. This allows a program to ensure, i.e. keep track of, that all fibers it spawns are terminated properly and any resources transmitted to spawned fibers will be disposed properly.

Design rationale

The idea is that fibers correspond 1-to-1 with independent threads of execution. This allows a fiber to non-atomically store state related to a thread of execution.

The status of whether propagation of cancelation is forbidden or permitted could be stored in the fiber local storage. The justification for storing it directly with the fiber is that the implementation of some key synchronization and communication mechanisms, such as condition variables, requires the capability.

No integer fiber id is provided by default. It would seem that for most intents and purposes the identity of the fiber is sufficient. Fiber local storage can be used to implement a fiber id or e.g. a fiber hash.

The fiber local storage is designed for the purpose of extending fibers and to be as fast as possible. It is not intended for application programming.

Yield is provided as a separate effect to specifically communicate the intent that the current fiber should be rescheduled. This allows all the other effect handlers more freedom in choosing which fiber to schedule next.

package picos

Interface for rescheduling

Interface for current fiber

Interface for spawning

Interface for structuring

Interface for foreign fiber

Interface for schedulers

Design rationale