Channels and Select

Purpose

Message passing is often simpler and safer than shared mutable state. A channel lets one execution entity transfer ownership of a value to another without sharing the same mutable object directly.

Sec channels deliberately model ownership transfer exactly. When a send commits, ownership of the message moves into the channel or directly to a rendezvous receiver. When a receive commits, ownership moves out to the receiver. Result types always show whether ownership moved or was returned to the caller.

In-Process Channels

Ordinary Channel[T], Sender[T], Receiver[T] and MessageTicket[T] are strictly in-process capabilities. They do not automatically become IPC.

task  -> task
task  -> thread
thread -> task
thread -> thread

If communication must cross a process boundary, Sec uses the separate IPC model from chapter 66. Ordinary channels are not ProcessTransferable and are never silently lowered to process messaging.

Core Types

The compiler-known source-visible channel surface in Sec 0.1 includes:

Channel[T]
Sender[T]
Receiver[T]
MessageTicket[T]
ChannelCapability
ChannelOptions
ChannelStatistics
SenderID
ChannelSendResult[T]
ChannelTrySendResult[T]
ChannelTryReceiveResult[T]
ChannelRevocableSendResult[T]
ChannelRevokeResult[T]
MessageDisposition

The public container type is Channel[T]. It is @noCopy and exposes exactly two public fields: Tx and Rx.

@noCopy
type Channel[T] struct {
    Tx: Sender[T]
    Rx: Receiver[T]

    try init(capacity: uint) AllocationError
    try init(options: ChannelOptions) AllocationError
}

The hidden queueing and synchronization state is part of the implementation, but it is not a third public field and must not leak into the source model.

Construction and Options

Channel construction is fallible only through AllocationError when the selected profile requires dynamic allocation or cannot prove construction infallible.

let messages := try Channel[string](capacity: 16)

let jobs := try Channel[Job](options: ChannelOptions {
    Capacity: 64,
    MaxSenders: 8,
    Capabilities: { ChannelCapability.Statistics }
})

ChannelOptions contains exactly three public fields:

• Capacity: uint
• MaxSenders: uint
• Capabilities: set[ChannelCapability]

MaxSenders must be at least 1. The option fields that fix endpoint identity and optional runtime metadata must be known before lowering.

Optional Capabilities

Channels can enable a closed set of optional features through ChannelCapability.

enum ChannelCapability {
    Revocation
    Expiration
    ISRSafeSend
    Statistics
}

• Revocation enables SendRevocable(...) and message tickets.
• Expiration enables message lifetime overloads.
• ISRSafeSend allows target-validated bounded non-blocking TrySend from ISR context.
• Statistics enables statistics snapshots.

There is no general channel priority capability in Sec 0.1. Priority between competing operations is expressed through source order in select, not by a per-channel priority configuration.

Sender[T]

Sender[T] is move-only. It owns one send capability for one channel identity.

@noCopy
type Sender[T]

impl Sender[T] {
    fn Share() Option[Sender[T]]

    fn Send(message: T) ChannelSendResult[T]
    fn Send(message: T, lifetime: duration) ChannelSendResult[T]
    fn TrySend(message: T) ChannelTrySendResult[T]

    fn SendRevocable(message: T) ChannelRevocableSendResult[T]
    fn SendRevocable(
        message: T,
        lifetime: duration
    ) ChannelRevocableSendResult[T]

    fn Statistics() ChannelStatistics

    fn Close() void
}

Share() does not consume the original sender. Close() consumes the local sender capability. Blocking Send(...) is a waiting operation; TrySend(...) is the non-blocking counterpart.

Receiver[T]

Receiver[T] is also move-only. Sec 0.1 defines exactly one live receive capability for an ordinary channel.

@noCopy
type Receiver[T]

impl Receiver[T] {
    fn Receive() Option[T]
    fn TryReceive() ChannelTryReceiveResult[T]

    fn Discard() void
    fn Statistics() ChannelStatistics
    fn Close() void
}

Discard() does not consume the receiver. Close() does. A normal blocking receive returns Option[T]: Some(value) means one message was received; None means the send side is closed and the channel is drained.

Send Result Types

Sec uses exact result types so the caller can see whether ownership transferred or was returned.

Blocking send

type ChannelSendResult[T] union {
    Sent
    Closed(T)
}

Sent means the send committed. Closed(T) means the receive side closed before commit, so ownership of the unsent message returns to the caller.

Non-blocking send

type ChannelTrySendResult[T] union {
    Sent
    WouldBlock(T)
    Closed(T)
}

WouldBlock(T) is used when the channel is open but the send cannot commit immediately. It returns ownership of the unsent value. This is especially important for bounded channels and rendezvous channels with no immediately matching receiver.

Receive Result Types

Blocking Receive() returns Option[T]. Non-blocking receive has its own exact result type.

type ChannelTryReceiveResult[T] union {
    Received(T)
    Empty
    Closed
}

• Received(T) means a deliverable message was received immediately.
• Empty means the channel is open but no deliverable message is available immediately.
• Closed means the send side is closed and no deliverable queued message remains.

Closed carries no payload because there is no message to transfer.

Sender Sharing and Limits

The initial Tx capability counts toward MaxSenders. Additional senders are created explicitly through Share().

let work := try Channel[Job](options: ChannelOptions {
    Capacity: 32,
    MaxSenders: 2,
    Capabilities: { }
})

match work.Tx.Share() {
    Some(other) => {
        StartProducer(<-other)
    }

    None => {
        HandleSenderLimit()
    }
}

None means the configured sender limit is already reached. It does not consume or invalidate the original sender.

Revocable Messages

If a channel enables ChannelCapability.Revocation, the sender may use SendRevocable(...). A successful revocable send returns a MessageTicket[T] that owns the right to attempt later revocation.

type ChannelRevocableSendResult[T] union {
    Accepted(MessageTicket[T])
    Closed(T)
}

type ChannelRevokeResult[T] union {
    Revoked(T)
    Unavailable(MessageDisposition)
}

MessageTicket[T] is move-only and Revoke() consumes it. Revocation is ticket-owned, not sender-owned.

match ticket.Revoke() {
    Revoked(message) => {
        Recover(<-message)
    }

    Unavailable(disposition) => {
        HandleDisposition(disposition)
    }
}

If revocation loses the race, the result reports a terminal MessageDisposition: Received, Expired or Discarded.

Expiration and Statistics

If ChannelCapability.Expiration is enabled, send and revocable-send overloads may attach a message lifetime using duration. Expiration is a message property, not a select timeout.

If ChannelCapability.Statistics is enabled, sender and receiver expose a statistics snapshot. The public type is:

type ChannelStatistics struct {
    Sent: uint64
    Received: uint64
    Revoked: uint64
    Expired: uint64
    Discarded: uint64
}

The counters are saturating snapshots. They are useful for instrumentation and observability, not as a synchronization substitute for actual program logic.

Close, Discard and Lifecycle

Closing sender capabilities eventually closes the send side. Closing the receiver closes the receive side immediately. Discarding drops queued deliverable messages from the receive side without consuming the receiver itself.

• Sender[T].Close() consumes that sender capability.
• Receiver[T].Close() consumes the receiver capability.
• Receiver[T].Discard() preserves the receiver capability.

A blocking receive returns None only when the send side is closed and the channel is drained. A non-blocking receive returns Closed under the same fully drained closed condition.

FIFO Ordering and Rendezvous

Ordinary Sec channels are FIFO by successful message commit order. One sender preserves its own successful commit order, while concurrent senders are ordered by the actual global channel commit order.

A channel may be buffered or rendezvous-style depending on capacity and runtime realization. The source-level rules stay the same: send and receive commit at a definite point, and the exact result type reports success, closure or immediate inability to proceed.

Revoked, expired and discarded messages are skipped without reordering the remaining deliverable committed messages.

Cancellation and Waiting

Waiting channel operations are current-execution cancellation points. That includes blocking Send(...), blocking Receive() and blocking select. The non-waiting Try... operations are not cancellation points.

Sec 0.1 does not define SendTimed, ReceiveTimed or ref Context overloads on ordinary channels. Timeouts are composed through select and after branches instead.

Select Basics

select waits on multiple concurrent operations and executes exactly one branch.

select {
    message := rx.Receive() => {
        Process(message)
    }

    after 100ms => {
        HandleTimeout()
    }
}

A single execution of select chooses at most one branch. After the chosen branch body completes, control continues after the statement.

Selectable Branches

For channels, the most common select branches are receives, sends, revocable sends, timeout branches and a final optional default branch.

Receive branch

select {
    result := rx.Receive() => {
        match result {
            Some(message) => Process(<-message)
            None => HandleClosed()
        }
    }
}

Send branch

select {
    result := tx.Send(<-message) => {
        match result {
            Sent => HandleSent()
            Closed(returned) => Recover(<-returned)
        }
    }
}

Revocable send branch

select {
    result := tx.SendRevocable(<-message) => {
        match result {
            Accepted(ticket) => Store(<-ticket)
            Closed(returned) => Recover(<-returned)
        }
    }

    after 20ms => {
        HandleTimeout(message)
    }
}

When the send or receive branch is not selected, it must not consume ownership or mutate observable channel state.

Readiness and Commit

Every selectable operation has two conceptual phases:

readiness
commit

Readiness answers whether an operation could proceed. Commit performs the operation, transfers ownership and publishes the branch result. Only the selected branch commits. Non-selected branches remain unconsumed and must not change observable state.

Source-Order Priority

Branches are considered in source order. If multiple branches are ready at the same selection point, the first ready branch wins. This is an intentional source-visible priority rule, not an implementation accident.

select {
    critical := criticalRx.Receive() => {
        HandleCritical(critical)
    }

    normal := normalRx.Receive() => {
        HandleNormal(normal)
    }
}

If both receives are ready, the critical branch is selected. Sec 0.1 does not inject hidden fairness that overrides source order. A later branch may starve if an earlier branch is continuously ready.

Default and Timeout

A timeout branch uses after duration => {{ ... }}. The timeout begins when execution enters the select. It uses a monotonic time source.

select {
    message := rx.Receive() => {
        Process(message)
    }

    after 100ms => {
        HandleTimeout()
    }
}

A default branch is optional and executes only when no preceding selectable branch is ready. If present, it must be the final branch and the select does not wait.

select {
    message := rx.Receive() => {
        Process(message)
    }

    default => {
        DoOtherWork()
    }
}

A positive timeout branch together with a final default branch is normally a static error because the timeout can never be selected when no earlier branch is ready.

Ownership in Select

select must preserve ownership exactly. If a branch commits, it may transfer ownership according to that operation's ordinary result type. If a branch is not selected, the original values and handles remain available according to normal ownership rules.

This matters especially for message sends, revocable sends and move-only messages. The runtime must not partially consume a message on a branch that loses the select.

Memory Semantics

A committed send/receive pair establishes the channel's required synchronization edge. The receiver observes memory effects published by the sender according to the concurrency memory model. Polling statistics or merely observing cancellation state is not equivalent to successful channel synchronization.

select must preserve the same synchronization semantics as direct send or receive operations. Only the committed branch contributes the synchronization edge.

Target and Runtime Requirements

The selected immutable CompilationPlan determines whether channels, select, timeouts and optional capabilities are supported. A target may implement them through scheduler wait sets, event loops, RTOS primitives, OS polling facilities or compiler-generated cooperative state machines.

Whatever mechanism is used, the target must preserve the Sec source semantics:

• exact result types;
• in-process channel identity;
• source-order priority in select;
• exactly-one branch commit;
• ownership rollback for non-selected branches;
• cancellation-point behavior for waiting operations;
• timeout and synchronization rules.

A target that cannot support a required branch combination or capability must reject the program instead of approximating the semantics.

Tooling and Diagnostics

Hover, completion and navigation should expose the canonical channel surface rather than legacy names. Tooling should prefer Tx, Rx, Share, Send, TrySend, Receive, TryReceive, SendRevocable, Revoke, Discard and Close.

Common diagnostics include:

• use of consumed sender or receiver capability;
• attempting to share beyond MaxSenders;
• using revocation APIs without the Revocation capability;
• using statistics without the Statistics capability;
• placing default before the final branch in select;
• combining a positive timeout with a final default that makes the timeout unreachable;
• using timeouts on a target without a valid timer source.

Implementation Status

The channels rulebook is normative and the governance status for the integrated channel surface is partial.

Already present or partly present:

• compiler-known intrinsic identities for Channel[T], Sender[T], Receiver[T] and MessageTicket[T];
• initial compiler-known support for several related result/configuration identities.

Still incomplete or planned:

• the full exact source API and all capability-gated operations;
• complete lifecycle semantics for close/discard/revocation/expiration;
• select integration with exact readiness/commit rollback behavior;
• cancellation-point commit races and target/runtime lowering;
• complete Semantic IR and LSP/tooling support.

Best Practices

• Use channels for explicit ownership transfer between concurrent entities.
• Model sender fan-out explicitly with Share() and a deliberate MaxSenders.
• Use blocking operations when waiting is acceptable and Try... operations when it is not.
• Handle returned ownership explicitly on Closed(T) and WouldBlock(T).
• Use revocable sends only when you truly need post-send recovery behavior.
• Use timeout composition through select and after; do not invent timed wrappers in user code.
• Treat source order in select as a real priority policy.
• Do not assume fairness for later select branches.
• Keep ordinary channels in-process; use the IPC APIs for cross-process messaging.
• Remember that a statistics snapshot is observability, not program synchronization.

Summary

• Channel[T] is the canonical typed in-process message channel in Sec 0.1.
• Channel[T] is @noCopy and exposes exactly Tx and Rx.
• Sender[T], Receiver[T] and MessageTicket[T] are move-only capabilities.
• Construction is fallible only through AllocationError when needed.
• ChannelOptions fixes capacity, sender limit and capability set.
• The optional capabilities are exactly Revocation, Expiration, ISRSafeSend and Statistics.
• Blocking Send(...) uses ChannelSendResult[T]; non-blocking TrySend(...) uses ChannelTrySendResult[T].
• Blocking Receive() returns Option[T]; non-blocking TryReceive() uses ChannelTryReceiveResult[T].
• Share() returns Option[Sender[T]] and respects MaxSenders.
• Revocable sends use MessageTicket[T] and ChannelRevokeResult[T].
• Ordinary channels are FIFO by committed message order and strictly in-process.
• Waiting channel operations are cancellation points; Try... operations are not.
• Ordinary channels define no timed APIs and no ref Context overloads.
• select waits on multiple concurrent operations and commits exactly one branch.
• Source order is the explicit priority rule in select.
• default is optional, must be final, and makes the select non-waiting.
• after provides timeout composition using a monotonic time source.
• Non-selected select branches must not consume ownership or mutate observable state.
• The normative model is complete, but current implementation support remains partial.