Inter-Process Communication

Sec treats a process boundary as a real semantic isolation boundary. Values, references, resource capabilities and shared storage therefore require explicit rules when they cross between processes. IPC is not implemented by pretending that two processes share one ordinary address space, and copying a pointer, descriptor number or native handle value never creates portable Sec ownership in another process.

Sec 0.1 defines byte-stream pipes, typed message transport, shared-memory capabilities, process-shared synchronization, safe typed shared values, process-shared atomics and type-preserving capability transfer. These facilities share one ownership and lifecycle model but remain semantically distinct.

Core rule: IPC preserves process isolation. Ordinary references, process-local addresses and native handle numbers do not acquire cross-process meaning merely because their machine representation can be copied.

Purpose

Process creation is described in Processes and Command. This chapter describes what happens after an isolation boundary exists and processes need to exchange data, authority or synchronized shared state.

The IPC model owns the semantics of:

  • anonymous byte pipes;
  • typed process-to-process messages;
  • shared backing storage and process-local mappings;
  • process-shared mutexes and semaphores;
  • safe typed shared values;
  • process-shared lock-free atomic values;
  • resource and capability transfer;
  • peer-loss and IPC lifecycle behavior;
  • IPC target capabilities;
  • IPC-specific Semantic IR, analysis, diagnostics and lowering obligations.

Ordinary in-process channels, process lifecycle, general transferability rules, ordinary atomics, network RPC and application serialization remain owned by their respective language areas.

IPC Families

Sec 0.1 defines four fundamental IPC families:

FamilyMeaning
PipeOrdered unidirectional byte stream with no portable message boundaries.
Typed IPCOrdered transport of complete typed messages.
Shared memoryOne backing-storage identity mapped independently into process address spaces.
Capability transferTransfer of authority to an existing resource while preserving its Sec type.

Process-shared synchronization and process-shared atomics are explicit facilities built on the same isolation-boundary model. A target may use different native mechanisms internally, but those mechanisms must preserve the selected Sec abstraction.

Channels Are Not IPC

Channel[T], Sender[T] and Receiver[T] are in-process concurrency abstractions. They coordinate tasks and threads inside one process address space and never automatically become IPC.

Typed process messaging uses different source-visible types:

IPCSender[T]
IPCReceiver[T]

This distinction prevents a process boundary from disappearing behind an apparently ordinary channel operation. A future adapter could be defined explicitly, but Sec 0.1 defines no implicit conversion from in-process channels to IPC.

IPC Is Not RPC

Typed IPC transports messages. It does not automatically provide remote methods, service identities, request/response correlation, request IDs, RPC deadlines, application exceptions, protocol negotiation or service discovery.

IPCSender[Request]
IPCReceiver[Request]

An RPC framework may use typed IPC as one transport, but that framework owns the higher-level request/response protocol. Core IPC deliberately stops at message and capability transport.

Semantic Properties

IPC relies on compiler-derived semantic properties rather than source interfaces that users manually implement.

ProcessTransferable

ProcessTransferable answers whether a semantic value can cross a process boundary through a defined transfer representation or capability adapter. IPC consumes that proof but does not redefine it.

SharedStorable(T)

SharedStorable(T) means that the compiler can define one fixed-size, self-contained canonical shared representation for T. Such a representation may not depend on process-local references, RawPtr meaning, resource ownership, destructor-managed ownership state or a process-local allocation graph.

Examples that are not ordinarily SharedStorable include:

string
ref T
ref mut T
RawPtr[T]
owning arrays and collections
File
Process[T]
Task[T]
PipeReader
IPCSender[T]
SharedMemory
IPCMutex

IPCAtomicValue(T)

IPCAtomicValue(T) is the conservative scalar subset that can participate in the complete lock-free process-shared atomic contract. It includes approved boolean, signed-integer, unsigned-integer, compatible enum and named scalar forms. A RawPtr[T] is explicitly excluded because a process-local address does not acquire cross-process meaning through atomic storage.

Pipes

A pipe is an ordered unidirectional byte stream:

PipeWriter -> bytes -> PipeReader

Pipe writes do not create portable message boundaries. Multiple writes form one byte stream, and a reader cannot infer where individual write calls occurred.

Pipes are therefore appropriate for stream protocols and external-process standard I/O. Use typed IPC when complete message boundaries matter.

Pipe API

@noCopy
type Pipe struct {
    Reader: PipeReader,
    Writer: PipeWriter,
}

@noCopy
type PipeReader

@noCopy
type PipeWriter

fn CreatePipe() Result[Pipe, IOError]

impl PipeReader {
    property IsClosed: bool {
        get
    }

    fn Read(buffer: ref mut byte[]) Result[uint, IOError]
    fn ReadExact(buffer: ref mut byte[]) Result[uint, IOError]
    fn Duplicate() Result[PipeReader, IOError]
    fn Close() Result[void, IOError]

    free {
        // Best-effort close of an open endpoint.
    }
}

impl PipeWriter {
    property IsClosed: bool {
        get
    }

    fn Write(data: ref byte[]) Result[uint, IOError]
    fn WriteAll(data: ref byte[]) Result[uint, IOError]
    fn Duplicate() Result[PipeWriter, IOError]
    fn Close() Result[void, IOError]

    free {
        // Best-effort close of an open endpoint.
    }
}

Pipe is an ordinary owning aggregate. Its reader and writer fields are independently tracked, so ordinary partial-move rules apply:

let pipe := try CreatePipe()
let reader :<- pipe.Reader
let writer :<- pipe.Writer

Pipe Semantics

Read may return a short successful read. For a non-empty buffer, Ok(0) means end-of-stream. For an empty buffer, Ok(0) is immediate and does not establish EOF.

EOF occurs only after every write capability for the logical pipe is gone and all previously accepted buffered bytes have been consumed. Closing one duplicated writer does not create EOF while another writer capability remains alive.

ReadExact fills the requested buffer or returns IOError.UnexpectedEndOfFile if EOF arrives after only a prefix has been read.

Write may commit only a prefix. WriteAll keeps writing until the complete sequence commits or an error occurs. It is not transactional with respect to bytes already written: an error after a committed prefix does not retract that prefix.

When no read capability remains, later writes that cannot be delivered return IOError.BrokenPipe.

Pipe buffering is implementation-defined but bounded. Sec exposes no portable capacity property in 0.1, and hidden unbounded buffering is forbidden.

Read and Write are primitive selectable operations. ReadExact and WriteAll are composed operations and are not primitive select branches in Sec 0.1.

Typed IPC

Typed IPC transports complete semantic values across process boundaries:

IPCSender[T] -> complete T messages -> IPCReceiver[T]

Every successful Send commits exactly one complete T. The receiver never observes message fragments, a partially materialized value or bytes from several messages merged into one value.

Typed IPC is not limited to parent and child processes. Any processes that validly establish or receive matching capabilities may communicate.

Typed IPC API

@noCopy
type IPCPair[T] struct {
    Sender: IPCSender[T],
    Receiver: IPCReceiver[T],
}

@noCopy
type IPCSender[T]

@noCopy
type IPCReceiver[T]

fn CreateIPC[T]() Result[IPCPair[T], IPCError]

enum IPCError error {
    Closed
    PeerClosed
    TransferFailed
    MaterializationFailed
    OutOfMemory
    ResourceLimit
    ProtocolFailure
    NativeFailure
}

impl IPCSender[T] {
    property IsClosed: bool {
        get
    }

    fn Send(message: T) Result[void, IPCError]
    fn Duplicate() Result[IPCSender[T], IPCError]
    fn Close() void

    free {
        // Cleanly releases this local sender capability if still open.
    }
}

impl IPCReceiver[T] {
    property IsClosed: bool {
        get
    }

    fn Receive() Result[Option[T], IPCError]
    fn Duplicate() Result[IPCReceiver[T], IPCError]
    fn Close() void

    free {
        // Cleanly releases this local receiver capability if still open.
    }
}

CreateIPC[T]() requires ProcessTransferable(T) and target support for IPCTypedMessages plus a complete transfer plan for T. A statically non-transferable type is rejected at compile time.

Send and Ownership

Sending follows ordinary Sec ownership rules. A named existing move-only value that is consumed uses the explicit move marker:

try sender.Send(<-message)

A consuming send is transactional with respect to source ownership.

ResultOwnership meaning
Ok()The complete message transfer committed; the consumed source binding becomes unavailable.
Err(...) before commitThe complete source value remains owned locally; no partial field transfer becomes visible.

A message containing several resource-owning fields still commits as one semantic operation. Runtime preparation may have substeps, but pre-commit failure must roll back every temporary destination resource.

Successful Send means the message has committed to the IPC transport. It does not mean that the receiver has already called Receive, processed the request or sent a reply.

Receive and Completion

Receive() has three result classes:

Ok(Some(message))
    one complete T was received and is now owned locally

Ok(None)
    the sender side ended cleanly and no committed messages remain

Err(error)
    transport or materialization failed

An empty but still-open transport waits. None never means temporary emptiness, cancellation, timeout or abnormal peer loss.

Clean receive-side completion occurs only after all sender capabilities have ended cleanly and all committed messages have been resolved. Buffered messages are delivered before Ok(None).

Abrupt sender process death is not clean closure. If abnormal disappearance makes the sender side terminal, the receiver observes a stable terminal transport error, normally IPCError.NativeFailure unless a more specific portable error applies.

Duplication and MPMC

Duplicating a sender or receiver creates another independently owned capability to the same logical transport. It does not create a second queue.

Typed IPC therefore supports multi-producer/multi-consumer arrangements:

  • each committed message is delivered exactly once;
  • one receiving capability receives a message;
  • duplicated receivers do not broadcast;
  • successful commit order is preserved per sender;
  • cross-sender fairness or ordering is not portable-guaranteed;
  • which waiting receiver receives a message is not portable-guaranteed.

Typed IPC buffering is bounded and may legally be zero-capacity rendezvous. A program must therefore not assume that Send merely appends to a queue without waiting.

select and Commit

Send and Receive are primitive selectable operations. Select separates non-destructive readiness from commit.

select {
    sender.Send(<-message) => {
        // Ownership commits only if the selected Send returns Ok().
    }

    after 1s => {
        // message remains available here
    }
}

A non-selected send commits no message and transfers no ownership. A non-selected receive dequeues nothing and materializes no value. Backends must not speculatively perform all candidate operations and attempt to undo the losing branches afterward.

Shared Memory

Sec separates authority to a shared backing object from each process-local mapping.

SharedMemory
SharedReadMapping
SharedWriteMapping

SharedMemory identifies one logical shared backing object. A mapping is one process's view of that backing object in its own virtual address space. Different processes may map the same bytes at different addresses.

Rule: A process transfers or duplicates the backing capability, not a process-local mapping address.

Shared Memory API

enum SharedMemoryError error {
    Closed
    InvalidSize
    PermissionDenied
    OutOfMemory
    ResourceLimit
    MappingFailed
    DuplicationFailed
    NativeFailure
}

@noCopy
type SharedMemory

fn CreateSharedMemory(size: uint) Result[SharedMemory, SharedMemoryError]

impl SharedMemory {
    property Size: uint {
        get
    }

    property IsClosed: bool {
        get
    }

    fn MapRead() Result[SharedReadMapping, SharedMemoryError]
    fn MapWrite() Result[SharedWriteMapping, SharedMemoryError]
    fn Duplicate() Result[SharedMemory, SharedMemoryError]
    fn Close() Result[void, SharedMemoryError]

    free {
        // Best-effort release of this local backing capability.
    }
}

@noCopy
type SharedReadMapping

impl SharedReadMapping {
    property Size: uint {
        get
    }

    property IsClosed: bool {
        get
    }

    unsafe fn View() ref byte[]
    fn Close() Result[void, SharedMemoryError]

    free {
        // Best-effort unmap if still mapped.
    }
}

@noCopy
type SharedWriteMapping

impl SharedWriteMapping {
    property Size: uint {
        get
    }

    property IsClosed: bool {
        get
    }

    unsafe fn View() ref mut byte[]
    fn Close() Result[void, SharedMemoryError]

    free {
        // Best-effort unmap if still mapped.
    }
}

Shared memory creation requires size > 0. The new logical region is zero-initialized before any mapping may observe it. Native page rounding may allocate more storage internally, but bytes beyond the logical Size are not portable accessible storage through this contract.

Mappings and unsafe Views

SharedReadMapping and SharedWriteMapping are process-local and are not process-transferable. Transfer the SharedMemory capability and create a new mapping in the destination process.

A mapping carries enough backing-lifetime authority to remain valid even if the local SharedMemory capability that created it is later closed. The backing object stays alive while any owning capability or mapping still requires it.

View() is unsafe because ordinary process-local borrow checking cannot prove exclusivity against mappings in other processes. The returned reference must not outlive the mapping.

Important: Shared memory by itself provides no mutual exclusion, atomicity, acquire/release ordering or race prevention. unsafe does not waive the data-race rules.

Process-Shared Synchronization

Sec 0.1 defines two fundamental blocking process-shared synchronization types:

IPCMutex
IPCSemaphore

These are distinct from ordinary in-process synchronization types. The implementation may use kernel objects, shared storage or another native mechanism as long as the full process-shared Sec contract is preserved.

enum IPCSyncError error {
    Closed
    InvalidCount
    LimitExceeded
    OwnerDied
    PermissionDenied
    OutOfMemory
    ResourceLimit
    NativeFailure
}

IPCMutex

@noCopy
type IPCMutex

@noCopy
type IPCMutexGuard

fn CreateIPCMutex() Result[IPCMutex, IPCSyncError]

impl IPCMutex {
    property IsClosed: bool {
        get
    }

    fn Lock() Result[IPCMutexGuard, IPCSyncError]
    fn TryLock() Result[Option[IPCMutexGuard], IPCSyncError]
    fn Duplicate() Result[IPCMutex, IPCSyncError]
    fn Close() Result[void, IPCSyncError]

    free {
        // Best-effort release of this local mutex capability.
    }
}

impl IPCMutexGuard {
    free {
        // Releases the acquired logical IPC mutex.
    }
}

IPCMutex is non-recursive. A successful Lock() returns one guard, and that guard is the unlock capability. There is no separate public Unlock() method in Sec 0.1.

The mutex capability may cross a process boundary when the target provides the required adapter. The guard is execution-local and never process-transferable.

If the owning execution or process dies while holding the guard, the logical mutex is permanently poisoned and later acquisition returns IPCSyncError.OwnerDied. Sec 0.1 does not silently pretend that the abandoned critical section is consistent.

IPCSemaphore

@noCopy
type IPCSemaphore

fn CreateIPCSemaphore(
    Initial: uint,
    Maximum: uint
) Result[IPCSemaphore, IPCSyncError]

impl IPCSemaphore {
    property Maximum: uint {
        get
    }

    property IsClosed: bool {
        get
    }

    fn Acquire() Result[void, IPCSyncError]
    fn TryAcquire() Result[bool, IPCSyncError]
    fn Release() Result[void, IPCSyncError]
    fn Duplicate() Result[IPCSemaphore, IPCSyncError]
    fn Close() Result[void, IPCSyncError]

    free {
        // Best-effort release of this local semaphore capability.
    }
}

Construction requires:

Maximum > 0
Initial <= Maximum

The current permit count is intentionally not a portable property. Acquire may wait; TryAcquire is immediate. A permit acquired by a process is not automatically restored merely because that process later dies.

SharedValue[T]

Raw shared memory exposes bytes and therefore requires an application-defined unsafe representation and synchronization protocol. SharedValue[T] is the safe typed alternative for values that satisfy SharedStorable(T).

enum IPCSharedError error {
    Closed
    LayoutMismatch
    OwnerDied
    PermissionDenied
    OutOfMemory
    ResourceLimit
    MappingFailed
    DuplicationFailed
    NativeFailure
}

@noCopy
type SharedValue[T]

@noCopy
type SharedValueGuard[T]

fn CreateSharedValue[T](
    initial: T
) Result[SharedValue[T], IPCSharedError]

impl SharedValue[T] {
    property IsClosed: bool {
        get
    }

    fn Lock() Result[SharedValueGuard[T], IPCSharedError]
    fn TryLock() Result[Option[SharedValueGuard[T]], IPCSharedError]
    fn Duplicate() Result[SharedValue[T], IPCSharedError]
    fn Close() Result[void, IPCSharedError]

    free {
        // Best-effort release of this local SharedValue capability.
    }
}

impl SharedValueGuard[T] {
    fn Read() T
    fn Write(value: T) void

    free {
        // Publishes required release ordering and releases the guard.
    }
}

The safe API deliberately does not expose ref T or ref mut T into process-shared storage. Read() materializes a process-local snapshot; Write(value) replaces the canonical shared representation while the guard owns the critical section.

A guard is execution-local and may not remain live across a potentially waiting or suspending operation. If an execution dies while holding the guard, the shared value becomes permanently poisoned and later locks return IPCSharedError.OwnerDied.

IPCAtomic[T]

IPCAtomic[T] represents one process-shared atomic storage identity. It is a resource capability, not an arbitrary inline field in a raw shared-memory layout.

@noCopy
type IPCAtomic[T]

enum IPCAtomicError error {
    PermissionDenied
    OutOfMemory
    ResourceLimit
    DuplicationFailed
    NativeFailure
}

fn CreateIPCAtomic[T](
    initial: T
) Result[IPCAtomic[T], IPCAtomicError]

impl IPCAtomic[T] {
    fn Load() T
    fn Load(order: MemoryOrder) T

    fn Store(value: T) void
    fn Store(value: T, order: MemoryOrder) void

    fn Swap(value: T) T
    fn Swap(value: T, order: MemoryOrder) T

    fn CompareExchange(
        expected: T,
        desired: T
    ) CompareExchangeResult[T]

    fn CompareExchange(
        expected: T,
        desired: T,
        successOrder: MemoryOrder,
        failureOrder: MemoryOrder
    ) CompareExchangeResult[T]

    fn Duplicate() Result[IPCAtomic[T], IPCAtomicError]

    free {
        // Releases this local IPC atomic capability.
    }
}

The selected target must provide the complete lock-free process-shared operation set for the concrete T. There is no hidden mutex fallback. Unsupported type, width or profile combinations are compile-time errors.

IPC atomics reuse the ordinary MemoryOrder and CompareExchangeResult[T] vocabulary. Omitted orders default to SeqCst. Explicit orders must be compile-time-known so target support and process-shared synchronization semantics can be validated statically.

Process death does not poison an IPCAtomic[T]. Each operation has one linearization point and is either committed or not committed.

Capability Transfer

Sec does not define one untyped portable IPCHandle. A transferable resource keeps its concrete semantic type across the process boundary:

File           -> File
PipeReader     -> PipeReader
PipeWriter     -> PipeWriter
SharedMemory   -> SharedMemory
IPCMutex       -> IPCMutex
IPCSemaphore   -> IPCSemaphore
IPCAtomic[T]   -> IPCAtomic[T]
SharedValue[T] -> SharedValue[T]

The destination's native descriptor, handle, port or mapping token may differ from the source representation. The semantic resource identity and authority are what matter.

Duplication creates another Sec owner of the same logical resource. Transfer moves authority according to ordinary ownership rules. Neither operation may increase authority or accidentally expose unrelated parent-process resources.

A typed IPC message may contain resource capabilities:

type WorkerRequest struct {
    Input: File,
    Output: PipeWriter,
}

try sender.Send(<-request)

The complete composite value commits atomically from source semantics. Pre-commit failure preserves the complete source value and rolls back all temporary destination capabilities.

Command Resource Binding

The process chapter owns Command and process lifecycle. IPC owns the capability-transfer semantics that let an existing File, PipeReader or PipeWriter become child standard I/O.

The portable Sec 0.1 direct resource set is:

stdin:
    File
    PipeReader

stdout:
    File
    PipeWriter

stderr:
    File
    PipeWriter

Existing named move-only resources use explicit <- when consumed by command configuration. Configuration is transactional: on failure, the previous command configuration and caller ownership both remain unchanged.

Authority and Rendezvous

Core IPC is capability-based. Resources are created, duplicated, transferred during process startup, transferred through typed IPC or established through another explicit authority path.

Sec 0.1 deliberately defines no universal core:

CreateNamedIPC
OpenIPC
IPCAddress
IPCListener

Two independently started processes may use a platform service, local socket path, service manager or another bootstrap mechanism to find each other. That rendezvous layer owns naming, authentication, permissions and cleanup. Once authority is established, it may expose canonical Sec IPC capabilities.

A ProcessID, native PID, descriptor number, native handle value or string name is not itself IPC authority. Knowing an identifier does not grant arbitrary access to another process's resources.

Typed Transfer Compatibility

Typed IPC endpoints are monomorphic. An IPCSender[T] and its logical receiver are typed to exactly T for their lifetime. Sec 0.1 defines no dynamic any typed endpoint.

Compatibility is nominal, not structural. Two different nominal types remain different even if their fields happen to have the same machine layout.

Typed IPC transfer is semantic rather than a portable memcpy of one process's storage. For example, a transferable string is materialized in destination-owned storage; the destination does not receive the source heap pointer. Capability-bearing fields use capability transfer rather than serialized native handle integers.

The compiler/runtime associates an internal transfer identity with nominal type, generic specialization, transfer plan, representation revision and capability-bearing components. This identity is not exposed as a public source-level IPCTypeID.

The internal representation is not a public stable file, network or cross-language wire format. Persistent or independently versioned protocols use explicit serialization.

Lifecycle and Peer Loss

Process death releases capabilities owned solely by that process according to native and runtime cleanup, but it does not destroy a logical IPC resource still owned elsewhere.

  • shared memory remains alive while another capability or mapping exists;
  • an IPC atomic retains the latest committed value while another capability exists;
  • consumed semaphore permits are not restored merely because the acquiring process dies;
  • a mutex held at death becomes poisoned;
  • typed endpoint abnormal disappearance remains distinct from clean closure.

Lifecycle transitions that make a waiting result decidable wake the affected operation. For example, the last pipe writer disappearing may make a read return EOF, and the last IPC receiver disappearing makes a future send return PeerClosed.

Cancellation and Commit

IPC uses the general Sec cancellation model. IPC error enums do not gain extra Cancelled variants.

A waiting IPC operation may be interrupted only before semantic commit. Before commit, cancellation leaves the source-visible state unchanged:

Send       - message ownership remains local
Receive    - no message is dequeued
Mutex Lock - no guard is acquired
Semaphore  - no permit is consumed

Once an operation commits, commit wins. Cancellation, timeout or competing readiness cannot revoke the effect. This prevents states such as “message removed but result discarded” or “mutex acquired but guard lost”.

Cancellation does not invent unrelated resource actions. It does not implicitly close endpoints, terminate a process, destroy shared memory, poison an unlocked mutex or reset a semaphore.

Target Capabilities

There is no single universal IPCSupported flag. The active CompilationPlan uses granular semantic capabilities:

IPCPipes
IPCTypedMessages
IPCSharedMemory
IPCMutex
IPCSemaphore
IPCAtomicRepresentation(width)

These capabilities mean that the target/runtime can provide the complete Sec semantics for that family, not merely that a similarly named native API exists.

Route-specific adapters include at least:

CapabilityDuplicate(T)
ProcessStartupTransfer(T)
IPCTypedTransfer(T)
ProcessStandardIOResourceBinding(T, role)

Semantic transfer eligibility and concrete target route support are separate proofs. A resource may be process-transferable in principle while one selected target lacks a particular transfer route.

Missing statically known family, width or route support is a compile-time error. Sec does not replace compile-time target validation with runtime if IPCSupported checks.

Semantic IR and Analysis

IPC remains semantic until ownership, lifecycle, synchronization and target obligations are resolved. It must not be erased prematurely into opaque native calls.

Semantic IR preserves, where relevant:

  • IPC operation kind;
  • logical IPC resource identity;
  • Sec capability owner identity;
  • resource/capability relationships;
  • message and transfer type identity;
  • memory order;
  • process-shared synchronization scope;
  • source provenance.

Owner identity, logical resource identity, shared-storage identity, synchronization identity and native descriptor/handle identity are separate concepts. Duplication changes the owner identity while preserving the logical resource identity.

Conditional operations preserve prepare/commit/rollback semantics. This applies to process startup transfer, consuming Send, resource transfer, command resource binding, SharedValue duplication, composite materialization and selected branch commit.

Cross-process deadlock analysis may include tasks, threads, processes, IPC mutexes, semaphore waits, typed sends/receives, pipe backpressure and process join edges. A zero-capacity typed transport is a real rendezvous wait edge.

Data-race analysis includes shared-backing identity, shared-value protection identity, process-shared synchronization and IPC atomic memory order. Entering unsafe around a mapping view does not disable those analyses.

Defensive Materialization

IPC peers are not inherently trusted. A peer may be buggy, compromised, built separately or terminate during transfer. Typed transfer state is validated before it becomes source-visible typed state.

Validation may include:

  • framing and lengths;
  • overflow-safe size arithmetic;
  • variant discriminants;
  • allocation bounds;
  • capability counts and capability types;
  • schema/transfer identity;
  • representation-specific integer bounds.

Partial materialization is destroyed on failure. Temporary native/runtime state created during transfer, duplication, process bootstrap or rollback must have exactly one cleanup path.

Core IPC permits bounded limits for message size, queue storage, capability counts, materialization work and temporary transfer resources. Exceeding such a limit returns the appropriate ResourceLimit error rather than forcing hidden unbounded allocation.

Type safety does not provide application authentication or authorization. Whether a peer is allowed to perform an application operation remains the responsibility of the application protocol or rendezvous layer.

Diagnostics

IPC diagnostics should explain the semantic reason for rejection and the boundary being crossed. Useful diagnostics identify:

  • the exact value, field or type that cannot cross the process boundary;
  • whether the failure is semantic transfer eligibility or missing target support;
  • the missing route adapter;
  • a missing explicit <- move marker;
  • a live IPC guard that crosses a potentially waiting operation;
  • an invalid atomic memory-order combination;
  • why SharedStorable(T) or IPCAtomicValue(T) failed;
  • an actionable safer alternative when one exists.

Compiler, LSP and sec analyse should agree on the same canonical semantic facts rather than reproducing IPC rules independently.

Specification and Implementation Status

The Sec 0.1 IPC rulebook is normative and complete as a language-design document. Revision 1.0 was created and synchronized on 2026-09-15.

Toolchain implementation is not yet complete. The IPC governance integration remains planned and currently records no implemented IPC items. The required work includes compiler-known public types, parser/Sema integration, transferability proofs, target planning, Semantic IR, runtime/lowering support, diagnostics and the full conformance test matrix.

Manual status: The source semantics on this page describe the normative Sec 0.1 IPC model. Availability in the current compiler must be checked separately from the language specification.

Best Practices

  • Use ordinary Channel[T] inside one process; use IPCSender[T]/IPCReceiver[T] across process boundaries.
  • Use pipes when you want a byte stream and typed IPC when you want semantic message boundaries.
  • Do not build an application protocol on assumptions about native pipe write boundaries.
  • Use explicit <- for named move-only values consumed by process transfer or typed send.
  • Remember that failed pre-commit transfer preserves source ownership.
  • Treat Ok(None) as clean typed-stream completion, never as temporary emptiness.
  • Use SharedValue[T] for common safe shared-state cases instead of inventing a raw shared-memory layout.
  • When using raw shared memory, pair it with an explicit synchronization and representation protocol.
  • Never assume that unsafe removes cross-process race or lifetime requirements.
  • Release IPCMutexGuard and SharedValueGuard before operations that may wait or suspend.
  • Use IPCAtomic[T] only where the selected target provides the complete lock-free process-shared contract.
  • Do not serialize native handles, descriptors or pointers and treat them as capabilities.
  • Do not use ProcessID or a PID as authority to arbitrary IPC resources.
  • Design for bounded backpressure; a valid implementation may use zero-capacity rendezvous.
  • Keep application authentication, authorization and protocol versioning above the core IPC layer.

Summary

  • A process boundary is a semantic isolation boundary.
  • Sec 0.1 defines pipes, typed IPC, shared memory and capability transfer as distinct IPC families.
  • Ordinary Channel[T] never automatically becomes IPC.
  • Typed IPC is transport, not implicit RPC.
  • ProcessTransferable, SharedStorable(T) and IPCAtomicValue(T) are compiler-derived semantic facts.
  • Pipes are ordered byte streams with bounded implementation-defined buffering and no portable write boundaries.
  • Typed Send commits exactly one complete semantic value or leaves source ownership intact on pre-commit failure.
  • Receive() distinguishes message delivery, clean end-of-stream and abnormal transport failure.
  • Duplicated typed receivers are MPMC consumers, not broadcast subscribers.
  • Select uses non-destructive readiness followed by one branch commit.
  • SharedMemory represents backing authority; mappings are process-local.
  • Raw shared-memory views are unsafe and provide no implicit synchronization.
  • IPCMutex is non-recursive and guard-released; owner death permanently poisons it.
  • IPCSemaphore has explicit initial/maximum bounds and process-shared permit semantics.
  • SharedValue[T] provides safe synchronized typed shared state without leaking safe shared references.
  • IPCAtomic[T] requires a complete lock-free process-shared target implementation and never silently falls back to a mutex.
  • Capability transfer preserves concrete Sec resource types and never relies on copied native handle numbers.
  • Composite transfer is all-or-nothing from source semantics.
  • Core IPC is capability-based and defines no universal global named IPC registry in Sec 0.1.
  • Typed transfer compatibility is nominal and semantic, not ordinary ABI-layout identity.
  • Cancellation may interrupt only before semantic commit; committed effects are never revoked.
  • Target support is granular through IPCPipes, IPCTypedMessages, IPCSharedMemory, IPCMutex, IPCSemaphore and IPCAtomicRepresentation(width).
  • IPC remains explicit in Semantic IR until ownership, synchronization, lifecycle and target obligations are safely lowered.
  • The IPC specification is normative; current implementation remains planned.