Module Picos

The architecture of Picos

The core concepts of Picos are

• Trigger — ability to await for a signal,
• Computation — a cancelable computation, and
• Fiber — an independent thread of execution,

that are implemented in terms of the effects

• Trigger.Await — to suspend and resume a fiber,
• Computation.Cancel_after — to cancel a computation after given period of time,
• Fiber.Current — to obtain the unique handle of the current fiber,
• Fiber.Yield — to cooperatively request rescheduling the current fiber, and
• Fiber.Spawn — to start new fibers,

that can be used to implement many kinds of higher level concurrent programming facilities.

Understanding cancelation

A central idea of Picos is to provide a collection of building blocks for parallelism safe cancelation.

Consider the following motivating example:

Mutex.protect mutex begin fun () ->
  while true do
    Condition.wait condition mutex
  done
end

Assume that the fiber executing the above computation might be canceled, at any point, by another fiber running in parallel. How could that be done ensuring both safety and liveness?

• For safety, cancelation should not leave the program in an invalid state or cause the program to leak memory. In this case, the ownership of the mutex must be transferred to the next fiber or be left unlocked and no references to unused objects must be left in the mutex or the condition variable.

• For liveness, cancelation should take effect as soon as possible. In this case, cancelation should take effect even during the Mutex.lock inside Mutex.protect and the Condition.wait operations when the fiber might be in a suspended state awaiting for a signal to continue.

Here is another motivating example:

(* ... allocate resources ... *)
Fun.protect ~finally begin fun () ->
  Flock.join_after begin fun () ->
    (* ... *)
    Flock.fork begin fun () ->
      (* ... may use resources ... *)
    end;
    (* ... *)
  end;
  (* ... resources no longer used ... *)
end

The idea is that the main or parent fiber allocates some resources, which are then used by child fibers running in parallel. What should happen when the main fiber gets canceled? We again have both safety and liveness concerns:

• For safety, to ensure that resources are not finalized prematurely, the Flock.join_after call must not return or raise before all of the child fibers have terminated.

• For liveness, when the parent fiber gets canceled, we'd like all the child fibers to also get canceled.

Picos is designed to allow the above motivating examples and more to be implemented correctly addressing both safety and liveness.

Cancelation in Picos

The Fiber concept in Picos corresponds to an independent thread of execution. A fiber may explicitly forbid or permit the scheduler from propagating cancelation to it. This is important for the implementation of some key concurrent abstractions such as condition variables, where it is necessary to forbid cancelation when the associated mutex is reacquired.

Each fiber has an associated Computation at all times. A computation is something that needs to be completed either by returning a value through it or by canceling it with an exception. To cancel a fiber one cancels the computation associated with the fiber or any computation whose cancelation is propagated to the computation associated with the fiber.

Before a computation has been completed, it is also possible to attach a Trigger to the computation and also to later detach the trigger from the computation. A trigger attached to a computation is signaled as the computation is completed.

The Trigger concept in Picos is what allows a fiber to be suspended and later resumed. A fiber can create a trigger, add it to any shared data structure(s), and await for the trigger to be signaled. The await operation, which is implemented by the scheduler, also, in case the fiber permits cancelation, attaches the trigger to the computation of the fiber when it suspends the fiber. This is what allows a fiber to be resumed via cancelation of the computation.

The return value of await tells whether the fiber was resumed normally or due to being canceled and the caller then needs to properly handle either case. After being canceled, depending on the concurrent abstraction being implemented, the caller might need to e.g. remove references to the trigger from the shared data structures, cancel asynchronous IO operations, or transfer ownership of a mutex to the next fiber in the queue of the mutex.

Modules reference

For the examples in this document, we first open the Picos module

open Picos

as well as the Picos_std_structured library,

open Picos_std_structured

which we will be using for managing fibers in some of the examples, and define a simple scheduler on OCaml 4

let run main = Picos_mux_thread.run main

using the basic thread based scheduler and on OCaml 5

let run main = Picos_mux_random.run_on ~n_domains:2 main

using the randomized effects based scheduler that come with Picos as samples.

Core modules