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.
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.
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_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