Picos.Trigger
Ability to await for a signal.
To suspend and later resume the current thread of execution, one can create
a trigger, arrange signal
to be called on it, and await
for the call.
Here is a simple example:
run begin fun () ->
Flock.join_after @@ fun () ->
let trigger = Trigger.create () in
Flock.fork begin fun () ->
Trigger.signal trigger
end;
match Trigger.await trigger with
| None ->
(* We were resumed normally. *)
()
| Some (exn, bt) ->
(* We were canceled. *)
Printexc.raise_with_backtrace exn bt
end
⚠️ Typically we need to cleanup after await
, but in the above example we didn't insert the trigger into any data structure nor did we attach the trigger to any computation.
All operations on triggers are wait-free, with the obvious exception of await
. The signal
operation inherits the properties of the action attached with on_signal
to the trigger.
Represents a trigger. A trigger can be in one of three states: initial, awaiting, or signaled.
ℹ️ Once a trigger becomes signaled it no longer changes state.
🏎️ A trigger in the initial and signaled states is a tiny object that does not hold onto any other objects.
val create : unit -> t
create ()
allocates a new trigger in the initial state.
val is_signaled : t -> bool
is_signaled trigger
determines whether the trigger is in the signaled state.
This can be useful, for example, when a trigger
is being inserted to multiple locations and might be signaled concurrently while doing so. In such a case one can periodically check with is_signaled trigger
whether it makes sense to continue.
ℹ️ Computation.try_attach
already checks that the trigger being inserted has not been signaled so when attaching a trigger to multiple computations there is no need to separately check with is_signaled
.
val await : t -> (exn * Stdlib.Printexc.raw_backtrace) option
await trigger
waits for the trigger to be signal
ed.
The return value is None
in case the trigger has been signaled and the fiber was resumed normally. Otherwise the return value is Some (exn, bt)
, which indicates that the fiber has been canceled and the caller should raise the exception. In either case the caller is responsible for cleaning up. Usually this means making sure that no references to the trigger remain to avoid space leaks.
⚠️ As a rule of thumb, if you inserted the trigger to some data structure or attached it to some computation, then you are responsible for removing and detaching the trigger after await
.
ℹ️ A trigger in the signaled state only takes a small constant amount of memory. Make sure that it is not possible for a program to accumulate unbounded numbers of signaled triggers under any circumstance.
⚠️ Only the owner or creator of a trigger may call await
. It is considered an error to make multiple calls to await
.
ℹ️ The behavior is that, unless await
can return immediately,
await
will perform the Await
effect, andawait
will call the await
operation of the current handler.val signal : t -> unit
signal trigger
puts the trigger
into the signaled state and calls the resume action, if any, attached using on_signal
.
The intention is that calling signal trigger
guarantees that any fiber awaiting the trigger
will be resumed. However, when and whether a fiber having called await
will be resumed normally or as canceled is determined by the scheduler that handles the Await
effect.
ℹ️ Note that under normal circumstances, signal
should never raise an exception. If an exception is raised by signal
, it means that the handler of Await
has a bug or some catastrophic failure has occurred.
⚠️ Do not call signal
from an effect handler in a scheduler.
val is_initial : t -> bool
is_initial trigger
determines whether the trigger is in the initial or in the signaled state.
ℹ️ Consider using is_signaled
instead of is_initial
as in some contexts a trigger might reasonably be either in the initial or the awaiting state depending on the order in which things are being done.
on_signal trigger x y resume
attempts to attach the resume
action to the trigger
and transition the trigger to the awaiting state.
The return value is true
in case the action was attached successfully. Otherwise the return value is false
, which means that the trigger was already in the signaled state.
⚠️ The action that you attach to a trigger must be safe to call from any context that might end up signaling the trigger directly or indirectly through propagation. Unless you know, then you should assume that the resume
action might be called from a different domain running in parallel with neither effect nor exception handlers and that if the attached action doesn't return the system may deadlock or if the action doesn't return quickly it may cause performance issues.
⚠️ It is considered an error to make multiple calls to on_signal
with a specific trigger
.
from_action x y resume
is equivalent to let t = create () in assert (on_signal t x y resume); t
.
⚠️ The action that you attach to a trigger must be safe to call from any context that might end up signaling the trigger directly or indirectly through propagation. Unless you know, then you should assume that the resume
action might be called from a different domain running in parallel with neither effect nor exception handlers and that if the attached action doesn't return the system may deadlock or if the action doesn't return quickly it may cause performance issues.
⚠️ The returned trigger will be in the awaiting state, which means that it is an error to call await
, on_signal
, or dispose
on it.
val dispose : t -> unit
type Stdlib.Effect.t += private
| Await : t -> (exn * Stdlib.Printexc.raw_backtrace) option Stdlib.Effect.t
Schedulers must handle the Await
effect to implement the behavior of await
.
In case the fiber permits propagation of cancelation, the trigger must be attached to the computation of the fiber for the duration of suspending the fiber by the scheduler.
Typically the scheduler calls try_suspend
, which in turn calls on_signal
, to attach a scheduler specific resume
action to the trigger
. The scheduler must guarantee that the fiber will be resumed after signal
has been called on the trigger
.
Whether being resumed due to cancelation or not, the trigger must be either signaled outside of the effect handler, or disposed by the effect handler, before resuming the fiber.
In case the fiber permits propagation of cancelation and the computation associated with the fiber has been canceled the scheduler is free to continue the fiber immediately with the cancelation exception after disposing the trigger.
⚠️ A scheduler must not discontinue, i.e. raise an exception to, the fiber as a response to Await
.
The scheduler is free to choose which ready fiber to resume next.
A key idea behind this design is that the handler for Await
does not need to run arbitrary user defined code while suspending a fiber: the handler calls on_signal
by itself. This should make it easier to get both the handler and the user code correct.
Another key idea is that the signal
operation provides no feedback as to the outcome regarding cancelation. Calling signal
merely guarantees that the caller of await
will return. This means that the point at which cancelation must be determined can be as late as possible. A scheduler can check the cancelation status just before calling continue
and it is, of course, possible to check the cancelation status earlier. This allows maximal flexibility for the handler of Await
.
The consequence of this is that the only place to handle cancelation is at the point of await
. This makes the design simpler and should make it easier for the user to get the handling of cancelation right. A minor detail is that await
returns an option instead of raising an exception. The reason for this is that matching against an option is slightly faster than setting up an exception handler. Returning an option also clearly communicates the two different cases to handle.
On the other hand, the trigger mechanism does not have a way to specify a user-defined callback to perform cancelation immediately before the fiber is resumed. Such an immediately called callback could be useful for e.g. canceling an underlying IO request. One justification for not having such a callback is that cancelation is allowed to take place from outside of the scheduler, i.e. from another system level thread, and, in such a case, the callback could not be called immediately. Instead, the scheduler is free to choose how to schedule canceled and continued fibers and, assuming that fibers can be trusted, a scheduler may give priority to canceled fibers.
This design also separates the allocation of the atomic state for the trigger, or create
, from await
, and allows the state to be polled using is_signaled
before calling await
. This is particularly useful when the trigger might need to be inserted to multiple places and be signal
ed in parallel before the call of await
.
No mechanism is provided to communicate any result with the signal. That can be done outside of the mechanism and is often not needed. This simplifies the design.
Once signal
has been called, a trigger no longer refers to any other object and takes just two words of memory. This e.g. allows lazy removal of triggers, assuming the number of attached triggers can be bounded, because nothing except the trigger itself would be leaked.
To further understand the problem domain, in this design, in a suspend-resume scenario, there are three distinct pieces of state:
The trigger and cancelation status are both updated independently and atomically through code in this interface. The key requirement left for the user is to make sure that the state of the shared data structure is updated correctly independently of what await
returns. So, for example, a mutex implementation must check, after getting Some (exn, bt)
, what the state of the mutex is and how it should be updated.