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 private protected entries, preserving synchronous calls for lightweight and native tasks. Mutating wrapper calls must not be made from an enclosing protected action: the wrapper may signal a scoped waiter after its private lock exits, while the caller's outer lock would still be held. GNARL's blocking check rejects detectable cases before the channel changes state, but native builds without Detect_Blocking may not maintain that counter. External selective delay calls on Send and Receive migrate to Timed_Send and Timed_Receive; other selective alternatives need caller-side redesign. The wrapper changes Channel's ABI; rebuild callers.
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.
Await_Drained
procedure Await_Drained (Item : in out Channel)
Wait until Close has occurred and the buffer is empty.
Parameters
- Item
Channel to observe
Channel
type Channel (Capacity : Positive) is tagged limited private;
Fixed-capacity MPMC FIFO wrapper. Close is terminal. Values accepted before Close remain available in FIFO order; blocked and later senders are rejected, while receivers finish draining the buffer.
Record fields
- Capacity
Maximum buffered value count
Channel_Closed
Channel_Closed : exception;
Raised when Send observes a closed channel, or Receive observes a closed and empty channel.
Close
procedure Close (Item : in out Channel)
Idempotently reject new sends and let accepted values drain.
Parameters
- Item
Channel to close
Current
function Current (Item : Channel) return Snapshot
Read channel state under its protected lock.
Parameters
- Item
Channel to inspect
Return value
Current close, buffer, and waiter counts
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'Class;
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 : in out Channel; Value : out Element_Type)
Remove the oldest value, waiting while the open channel is empty.
Parameters
- Item
Source channel
- Value
Receives the oldest buffered value
Raised exceptions
- Channel_Closed
The closed channel has been fully drained
Receive
procedure Receive
(Item : not null access Channel'Class; 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'Class;
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 : in out Channel; Value : Element_Type)
Append Value, waiting while the open channel is full.
Parameters
- Item
Destination channel
- Value
Value copied into the channel
Raised exceptions
- Channel_Closed
Close occurs before the value is accepted
Send
procedure Send
(Item : not null access Channel'Class;
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
procedure Try_Receive
(Item : in out Channel; Value : in out Element_Type; Result : out Try_Receive_Result)
Attempt to remove the oldest value without waiting. Value is assigned only when Result is Item_Received.
Parameters
- Item
Source channel
- Value
Receives the oldest buffered value on success
- Result
Item_Received, Channel_Empty, or Receive_Closed
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 (Item : in out Channel; Value : Element_Type; Result : out Try_Send_Result)
Attempt to append without waiting.
Parameters
- Item
Destination channel
- Value
Value to copy if capacity is available
- Result
Item_Sent, Channel_Full, or Send_Closed
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_After_Clear
procedure Try_Send_After_Clear
(Item : in out Channel;
Value : Element_Type;
Accepted : not null access Boolean;
Result : out Try_Send_Result)
@exclude Internal half of the abort-stable package-level Try_Send. Accepted must already be False. On success it becomes True only after the complete item and queue state have been installed.
Parameters
- Item
Destination channel
- 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