← All compilation units

Flyology.Operations

Description

Provides bounded completion sets for scoped operations. An initiating I/O overload associates a limited operation object with one set and returns without waiting. The owning task can then wait for heterogeneous terminal batches without creating helper tasks or per-operation stacks. Waiting for a batch is a potentially blocking operation: a lightweight task that would suspend inside a protected action raises Program_Error before suspending, as for Flyology.IO.Wait.

Cancel

procedure Cancel (Item : in out Operation'Class)

Request terminal cancellation. Readiness and timer operations cancel immediately. Providers with kernel-owned input may retain Cancelling state in later extensions until the kernel relinquishes that input.

Parameters
Item

Operation to cancel

Capacity_Error

Capacity_Error      : exception;

Raised when a completion set has no reusable slot.

Cleanup_After_Consume

procedure Cleanup_After_Consume (Item : in out Operation)

@exclude Discharge provider state retained past terminal publication. Consume and controlled finalization call this only after the operation no longer owns a pending or terminal slot. Implementations must not raise or wait for another operation to make progress.

Parameters
Item

Operation whose retained provider state is discarded

Completion_Batch

type Completion_Batch (Capacity : Positive) is record
   Count : Natural := 0;
   Ids   : Operation_Id_Array (1 .. Capacity) := (others => Operation_Id'First);
end record;

Every previously unreported terminal identity published by one wait. Only Ids (1 .. Count) are defined.

Record fields
Capacity

Maximum number of identities in the batch

Count

Number of defined entries in Ids

Ids

Terminal operation identities in ascending slot order

Completion_Set

type Completion_Set (Capacity : Operation_Capacity) is tagged limited private;

Bounded caller-owned group used to wait for heterogeneous operations. One task must serialize initiation, waiting, cancellation, and Finish.

Record fields
Capacity

Maximum number of associated operations

Consume

procedure Consume (Item : in out Operation'Class)

Release one terminal result and make its bounded slot reusable by the same operation object. Slot release and provider cleanup form one abort-deferred transition.

Parameters
Item

Terminal operation whose slot becomes reusable

Continue_After

procedure Continue_After (Parent : in out Operation'Class; Child : in out Operation'Class)

Suspend Parent on one Child operation in the same completion set. Child becomes an internal implementation detail: waits drive its sources but do not publish its identity in user completion batches. When Child is terminal, Parent is driven with Dependency_Changed on the owner task's stack. Parent must call Child's provider-specific Finish and Release from that drive before continuing. If Child is already terminal, this procedure may drive Parent before returning.

Parameters
Parent

Pending outer provider operation

Child

Newly pending or terminal child with no other dependents

Drive

procedure Drive (Item : in out Operation; Event : Driver_Event)

Advance one provider state machine on the owning task's stack. The implementation must rearm a source or publish a terminal outcome before returning. It must retain provider errors for Finish instead of raising.

Parameters
Item

Operation whose state machine advances

Event

Source event that caused the drive

Driver_Event

type Driver_Event is
  (Start_Operation, Source_Ready, Deadline_Reached, Dependency_Changed, Continue_Operation);

Reason the owner task resumes a provider state machine.

Enumeration literals
Start_Operation

Initiation requests the first immediate step

Source_Ready

The provider's current descriptor became ready

Deadline_Reached

The provider's monotonic deadline expired

Dependency_Changed

A member operation changed terminal state

Continue_Operation

A bounded progress step asked to run again

Finalize

procedure Finalize (Item : in out Operation)

@exclude

Parameters
Item

Operation whose slot must be released

Finish

procedure Finish (Item : in out Gate_Operation; Matched : out Completion_Batch)

Consume a terminal gate and return every member outcome observed at the gate's scheduler snapshot. Inspect Outcome before Finish to distinguish a satisfied gate from an impossible success threshold. Cancellation raises Operation_Cancelled after consuming the gate; Matched is then undefined because Ada does not copy out on exceptional return.

Parameters
Item

Terminal gate operation

Matched

Member identities observed terminal by the gate

Gate_Operation

type Gate_Operation is new Operation with private;

First-class operation whose terminal result is derived from a fixed snapshot of other operations in the same completion set. Gates may depend on provider operations or earlier gates. Member outcomes remain retained until every dependent gate terminalizes.

Id

function Id (Item : Operation'Class) return Natural

Return the operation's stable set index, or zero before its first start and after finalization.

Parameters
Item

Operation to inspect

Return value

Stable set index, or zero before first start

Is_Active

function Is_Active (Item : Operation'Class) return Boolean

Report whether an operation is waiting for terminal completion.

Parameters
Item

Operation to inspect

Return value

True only while the provider remains pending

Is_Terminal

function Is_Terminal (Item : Operation'Class) return Boolean

Report whether an operation retains a terminal result.

Parameters
Item

Operation to inspect

Return value

True until Finish consumes the terminal result

Max_Operations

Max_Operations                      : constant := 32;

Maximum number of operations in one completion set.

Max_Readiness_Sources_Per_Operation

Max_Readiness_Sources_Per_Operation : constant := 6;

Maximum descriptor interests armed by one operation. This covers a primary transport, protocol and source wakeups, and bounded lifecycle and cancellation sources.

Operation

type Operation (Set : not null access Completion_Set'Class) is abstract
  new Ada.Finalization.Limited_Controlled with private;

Limited base for one scoped provider operation. Set must outlive the operation. Concrete provider packages declare derived types.

Operation_Cancelled

Operation_Cancelled : exception renames Flyology.Cancellation.Operation_Cancelled;

Raised by a provider-specific Finish after terminal cancellation.

Operation_Capacity

subtype Operation_Capacity is Positive range 1 .. Max_Operations;

Valid caller-selected completion-set capacity.

Operation_Error

Operation_Error     : exception;

Raised when an operation has an invalid or stale lifecycle state.

Operation_Id

subtype Operation_Id is Positive range 1 .. Max_Operations;

Stable one-based identity for a slot in one completion set.

Operation_Id_Array

type Operation_Id_Array is array (Positive range <>) of Operation_Id;

Bounded storage for completion identities.

Operation_Reference

type Operation_Reference is private;

Generation-stamped value identifying one operation outcome for gate composition. It contains no access value and does not extend the operation's lifetime. A reference must not outlive its completion set.

Operation_Reference_Array

type Operation_Reference_Array is array (Positive range <>) of Operation_Reference;

Definite arrays used to construct heterogeneous gates.

Outcome

function Outcome (Item : Operation'Class) return Terminal_Outcome

Return a terminal operation's retained outcome.

Parameters
Item

Terminal operation to inspect

Return value

Provider terminal outcome

Pending_Count

function Pending_Count (Set : Completion_Set) return Natural

Count operations that remain pending.

Parameters
Set

Completion set to inspect

Return value

Number of pending operations

Reference

function Reference (Item : Operation'Class) return Operation_Reference

Snapshot one operation's set identity, slot, and generation.

Parameters
Item

Active or terminal operation to reference

Return value

Value reference accepted by gate constructors

Release

procedure Release (Item : in out Operation'Class)

Release a consumed operation's slot for reuse by a different operation object. Composite providers call this after the child's typed Finish; ordinary reusable operations normally retain their idle slot instead.

Parameters
Item

Consumed, idle operation to detach from its set slot

Request_Cancellation

procedure Request_Cancellation (Item : in out Operation)

Request cancellation from a provider. The implementation must publish Cancelled only after the runtime or kernel has released every borrowed actual parameter. This primitive must not raise.

Parameters
Item

Operation to cancel or drain

Terminal_Count

function Terminal_Count (Set : Completion_Set) return Natural

Count operations that retain terminal outcomes.

Parameters
Set

Completion set to inspect

Return value

Number of terminal operations

Terminal_Outcome

type Terminal_Outcome is (Succeeded, Failed, Cancelled);

Terminal result retained until provider-specific Finish consumes it.

Enumeration literals
Succeeded

The provider completed its operation successfully

Failed

The provider completed with an operation error

Cancelled

Cancellation terminalized the operation

Wait_All

function Wait_All
  (Set : not null access Completion_Set'Class; Members : Operation_Reference_Array) return Gate_Operation

Construct a gate that succeeds when every member is terminal. Member failures and cancellations count as terminal outcomes.

Parameters
Set

Completion set shared by the gate and every member

Members

Nonempty fixed member snapshot

Return value

Started gate operation

Wait_All

procedure Wait_All (Set : in out Completion_Set)

Wait until no operation in Set remains pending. Terminal operations are retained until their provider-specific Finish operation consumes them.

Parameters
Set

Completion set to wait on

Wait_At_Least

procedure Wait_At_Least
  (Set : in out Completion_Set; Required : Positive; Completed : out Completion_Batch)

Wait until at least Required previously unreported operations are terminal, then return the complete terminal batch observed at that point. If fewer than Required operations can remain pending, return the remaining batch when the set becomes quiescent instead of deadlocking.

Parameters
Set

Completion set to wait on

Required

Minimum number of newly terminal operations

Completed

Newly published terminal identities

Wait_For_Success

function Wait_For_Success
  (Set : not null access Completion_Set'Class; Members : Operation_Reference_Array) return Gate_Operation

Construct a gate that succeeds when one member succeeds and fails when every member is terminal without a success.

Parameters
Set

Completion set shared by the gate and every member

Members

Nonempty fixed member snapshot

Return value

Started gate operation

Wait_For_Success

procedure Wait_For_Success (Set : in out Completion_Set; Completed : out Completion_Batch)

Wait for one previously unreported successful operation. Failed and cancelled operations are returned but do not satisfy the gate.

Parameters
Set

Completion set to wait on

Completed

Newly published identities of every outcome

Wait_For_Successes

function Wait_For_Successes
  (Set : not null access Completion_Set'Class; Members : Operation_Reference_Array; Required : Positive)
   return Gate_Operation

Construct a gate that succeeds after Required member successes and fails as soon as that threshold becomes impossible.

Parameters
Set

Completion set shared by the gate and every member

Members

Nonempty fixed member snapshot

Required

Required number of successful members

Return value

Started gate operation

Wait_For_Successes

procedure Wait_For_Successes
  (Set : in out Completion_Set; Required : Positive; Completed : out Completion_Batch)

Wait for Required previously unreported successful operations. Failed and cancelled operations do not count toward the threshold. Return all unreported terminal outcomes when the threshold is reached or when it becomes impossible because too few operations remain pending.

Parameters
Set

Completion set to wait on

Required

Minimum number of newly successful operations

Completed

Newly published terminal identities of every outcome

Wait_Some

function Wait_Some
  (Set      : not null access Completion_Set'Class;
   Members  : Operation_Reference_Array;
   Required : Positive := 1) return Gate_Operation

Construct a gate that succeeds after Required member operations become terminal, regardless of their individual outcomes. Remaining members continue independently. The gate consumes one completion-set slot.

Parameters
Set

Completion set shared by the gate and every member

Members

Nonempty fixed member snapshot

Required

Required number of terminal members

Return value

Started gate operation

Wait_Some

procedure Wait_Some (Set : in out Completion_Set; Completed : out Completion_Batch)

Return every unreported terminal operation. If none is terminal, wait until descriptor readiness or a monotonic deadline terminalizes at least one operation. When readiness and that operation's deadline are both observable in one zero-time poll, readiness drives one bounded provider step first; unrelated expired operations still terminalize in the same snapshot. The set and its operations are single-owner and must be used by one task.

Parameters
Set

Completion set to wait on

Completed

Newly published terminal identities

Wait_Some

procedure Wait_Some (Set : in out Completion_Set; Required : Positive; Completed : out Completion_Batch)

Counted spelling of Wait_At_Least. Wait for Required newly terminal operations, or return the remaining batch when the set becomes quiescent before that threshold can be reached.

Parameters
Set

Completion set to wait on

Required

Minimum number of newly terminal operations

Completed

Newly published terminal identities