Channel Declarations

ChannelDecl       ::= SyncChannelDecl | AsyncChannelDecl

SyncChannelDecl   ::= 'Sync' 'Chan' ident '=' ident '-->' ident ';'?

AsyncChannelDecl  ::= 'Async'? 'Chan' ident '=' ident ('<->' | '-->') ident ViaClause? ';'?

ViaClause         ::= 'via' ident ('<' Type '>')?

A channel declaration introduces one named communication endpoint between two protection domains. Channels carry the events that show up inside a process expression — c?x (receive) and c!e (send). They live in .fis system files; the .fi files reference channels by name only.

Channel kinds

The Async keyword may be omitted — a Chan without a leading Sync is asynchronous by default. The default arrow is <->. Only Sync channels require the unidirectional --> form.

Fields

• Name — snake_case identifier. The same name appears in process expressions on the LHS of ? / !.

• Endpoints — two protection-domain names. Both must be declared in the same .fis file.

• Buffer (optional, after via) — the MemoryRegion that backs the channel’s payload buffer, optionally annotated with a typed slot: via packet_buffer_outer<int> or a declared data-layer struct (via eth_outer_output<Slot>). Without via, the channel is treated as a pure synchronisation point with no shared payload buffer. A struct payload is the channel’s communication type: it must be a system (.fis) struct — never a program-local struct — and the C backend types receive binders from it (o2d?pkt declares static struct Slot pkt;).

  A buffer region is implicitly mapped into both endpoint PDs (rw, cached) at compiler-allocated vaddrs — it must not also appear in an explicit Mapping, and it may back only one channel. Each endpoint’s generated unit declares the loader-patched symbols <region>_vaddr / <region>_size (and driver code may declare <region>_paddr on demand), named after the region, not a mapping.

The optional trailing semicolon is accepted but not required.

Examples

// Synchronous unidirectional — outer PD calls into the diode.
Sync Chan o2d = eth_outer --> dd;

// Asynchronous bidirectional — `Async` is the default, can be omitted.
Chan d2i = dd <-> eth_inner;
Async Chan s2o = simulate <-> eth_outer;

// Buffer-backed channel, typed slot.
Chan packet = eth_outer <-> eth_inner via packet_buffer_outer<int>;

// Buffer-backed, untyped (slot type defaults later).
Chan ring = eth_outer --> eth_inner via ring_buffer_outer;

Channel events in process bodies

Inside a process, channel events are written chan_name '?' ident (receive) and chan_name '!' ident (send). The names must match exactly; the validator resolves each event back to the declared ChannelDecl to check direction and payload type.

See Event Declarations → Channel events for the inline event grammar and Process Definitions for how channel events sit in a process expression.

Limitations

• A struct payload types the receive binder in the generated C, but the payload transport (the ring copy through the backing region) is not generated yet — it is an explicit follow-up under the data-diode case study (#201). The generated code marks the pending copy with a comment.
• Send-site type checking (c!e against the declared payload) needs expression typing and is tracked under the type-system work (#117).
• The Sync modifier rejects bidirectional <-> syntactically; sync bidirectional channels would require a richer call/reply protocol than the current implementation supports.