Description
A bounded FIFO channel with terminal close and drain semantics.
The channel owns no task and allocates no storage after elaboration. Multiple producers and consumers may call it concurrently. Blocking uses protected entries, preserving the same synchronous API for lightweight and native tasks.
Element assignment and finalization execute as part of channel protected operations. Element_Type operations must therefore not block, reenter the same Channel, or propagate exceptions. If a prohibited finalization raises after delivery, the dequeue remains committed and the value cannot be delivered again.
Channel_Closed
Channel_Closed : exception;
Raised when Send observes a closed channel, or Receive observes a closed and empty channel.
Element_Array
type Element_Array is array (Positive range <>) of Element_Type;
@exclude Internal fixed storage for Channel.
Element_Type
type Element_Type is private;
Definite value transferred by copy through the channel.
Empty_Value
Empty_Value : Element_Type;
Resource-empty value used to initialize storage and clear each slot immediately after delivery. Copying and finalizing this value must obey the Element_Type protected-operation requirements above.
Finish
procedure Finish (Operation : in out Receive_Operation; Value : out Element_Type)
Consume a terminal receive and copy out its value.
Parameters
- Operation
Terminal receive operation
- Value
Received value on success
Finish
procedure Finish (Operation : in out Send_Operation)
Consume a terminal send. Channel close and timeout reproduce the synchronous exceptions; cancellation raises Operation_Cancelled.
Parameters
- Operation
Terminal send operation
Operation_Cancelled
Operation_Cancelled : exception renames Flyology.Operations.Operation_Cancelled;
Raised by Finish after a scoped channel operation is cancelled.
Receive
function Receive
(Set : not null access Flyology.Operations.Completion_Set'Class;
Item : not null access Channel;
Timeout : Duration := -1.0) return Receive_Operation
Start a receive without suspending the owner task. The received value is retained by the operation and copied out only by Finish.
Parameters
- Set
Completion set that owns the operation slot
- Item
Aliased channel that outlives the operation
- Timeout
Relative operation deadline in seconds
Return value
Started limited receive operation
Receive
procedure Receive
(Item : not null access Channel; Timeout : Duration := -1.0; Operation : in out Receive_Operation)
Start or restart a receive in an established operation object.
Parameters
- Item
Aliased channel that outlives the operation
- Timeout
Relative operation deadline in seconds
- Operation
Fresh or consumed receive operation
Receive_Operation
type Receive_Operation is new Flyology.Operations.Operation with private;
First-class receive operation using the synchronous channel barrier. A completed operation owns its received value until Finish or finalization.
Send
function Send
(Set : not null access Flyology.Operations.Completion_Set'Class;
Item : not null access Channel;
Value : Element_Type;
Timeout : Duration := -1.0) return Send_Operation
Start a send without suspending the owner task. Value is copied into the operation before this call returns, so the source actual need not remain alive. Negative Timeout is unlimited and zero is an immediate attempt.
Parameters
- Set
Completion set that owns the operation slot
- Item
Aliased channel that outlives the operation
- Value
Value copied into the pending operation
- Timeout
Relative operation deadline in seconds
Return value
Started limited send operation
Send
procedure Send
(Item : not null access Channel;
Value : Element_Type;
Timeout : Duration := -1.0;
Operation : in out Send_Operation)
Start or restart a send in an established operation object.
Parameters
- Item
Aliased channel that outlives the operation
- Value
Value copied into the pending operation
- Timeout
Relative operation deadline in seconds
- Operation
Fresh or consumed send operation
Send_Operation
type Send_Operation is new Flyology.Operations.Operation with private;
First-class send operation using the synchronous channel barrier. A pending operation owns its copied value until Finish or finalization.
Snapshot
type Snapshot is record
Closed : Boolean;
Pending : Natural;
Waiting_Senders : Natural;
Waiting_Receivers : Natural;
end record;
One coherent channel-state snapshot.
Record fields
- Closed
Whether Close has been called
- Pending
Number of values currently buffered
- Waiting_Senders
Number of callers queued for capacity
- Waiting_Receivers
Number of callers queued for a value
Timed_Receive
procedure Timed_Receive (Item : in out Channel; Value : out Element_Type; Timeout : Duration)
Remove the oldest value within one relative deadline. Negative Timeout waits indefinitely; zero is an immediate attempt. Values accepted before Close remain receivable until the channel drains.
Parameters
- Item
Channel to update
- Value
Receives the oldest buffered value
- Timeout
Deadline interval in seconds
Raised exceptions
- Channel_Closed
The closed channel is fully drained
- Timeout_Error
No value is available before the deadline
Timed_Send
procedure Timed_Send (Item : in out Channel; Value : Element_Type; Timeout : Duration)
Append Value within one relative deadline. Negative Timeout waits indefinitely; zero is an immediate attempt. Once the protected Send is accepted, success wins over a simultaneous deadline.
Parameters
- Item
Channel to update
- Value
Value copied into the channel
- Timeout
Deadline interval in seconds
Raised exceptions
- Channel_Closed
Close occurs before acceptance
- Timeout_Error
No capacity is available before the deadline
Timeout_Error
Timeout_Error : exception;
Raised by a timed Send or Receive whose deadline expires first.
Try_Receive_Result
type Try_Receive_Result is (Item_Received, Channel_Empty, Receive_Closed);
Result of a nonblocking receive attempt.
Enumeration literals
- Item_Received
The oldest value was returned
- Channel_Empty
No value was available from an open channel
- Receive_Closed
The closed channel was fully drained
Try_Send
procedure Try_Send
(Object : in out Channel;
Value : Element_Type;
Accepted : not null access Boolean;
Result : out Try_Send_Result)
Attempt to append without waiting and publish abort-stable ownership evidence. Accepted is cleared before attempting to enter the protected channel, then becomes True only after the complete item and queue state have been installed. Unlike Result, the caller-aliased evidence remains authoritative if the calling task is aborted at either boundary. True means the channel owns exactly one copy of Value; False means it owns none. Once True is published, a later propagated internal notification failure does not revoke acceptance; ordinary Result copy-out may then be unavailable.
Parameters
- Object
Channel on which to attempt the send
- Value
Value to copy if capacity is available
- Accepted
Caller-owned evidence that the channel accepted Value
- Result
Item_Sent, Channel_Full, or Send_Closed
Try_Send_Result
type Try_Send_Result is (Item_Sent, Channel_Full, Send_Closed);
Result of a nonblocking send attempt.
Enumeration literals
- Item_Sent
The value was appended
- Channel_Full
No capacity was available
- Send_Closed
The channel had been closed