Braid-inspired seL4-native distribution architecture

[schonfinkel]

Summary

Design and implement a braid-inspired distributed Erlang architecture where multiple beam_server PDs form a user-defined topology (ring, mesh, hypercube) over a shared-memory distribution carrier instead of TCP. The topology is statically defined in tools/sdf/system.zig at build time, no EPMD, no dynamic discovery. This is the seL4-native path, it coexists with the baseline TCP distribution path in #22.

Braid Investigation

What Braid Is

Braid (Peer Stritzinger / GRiSP) is an Erlang/OTP ecosystem for orchestrating distributed Erlang clusters at arbitrary scale. It has four components:

Component	Role	Applicable to seL4?
braid.erl	Local library: creates clusters of nodes with arbitrary topologies (ring, mesh, hypercube) using hidden-node connections. Works without any external infrastructure.	Yes, loads as an OTP application. Defines the connection graph.
braidnet	Cloud orchestrator: spawns Docker containers, routes Erlang Distribution through itself. Fly.io-only.	No container orchestration doesn't map to seL4's static PD model.
braidnode	Per-node library: runs inside containers, routes dist connections through braidnet, delegates SSL signing. Uses a patched OTP build.	Partially, the routing concept maps to shmem_dist, mTLS delegation maps to a cert PD, but the patched-OTP approach doesn't fit seL4.
braidcert	Internal PKI: issues certificates for mTLS between nodes.	Yes (future), a dedicated cert PD that stores private keys and signs on behalf of beam_server PDs.

Key

Braid replaces EPMD's dynamic discovery and the fully-connected mesh with a pre-defined topology connected over a trusted transport. On seL4, the topology can be static (defined in the SDF at build time), and the transport can be a shared-memory ring buffer instead of TCP: lower latency, no network stack, and naturally aligned with Microkit's capability-based IPC model.

• braid.erl is directly usable. It is a pure-Erlang library (single module) that connects pre-existing nodes over user-defined topologies.
• For this project, we adapt it to connect pre-running beam_server PDs over the shmem_dist carrier instead of spawning new OS processes via some sort of passive server.

Architecture

Layer 1: Shared-Memory Distribution Carrier (shmem_dist)

A custom Erlang distribution carrier that replaces TCP sockets with shared-memory ring buffers and Microkit channel notifications.

graph LR
    %% Node Definitions & Hierarchy
    subgraph Cluster ["BEAM Inter-Process Communication"]
        
        subgraph BS0 ["beam_server_0"]
            E0["shmem_dist.erl<br>(Erlang module)"] 
            E0 --> N0["shmem_dist_nif<br>(C NIF or linked driver)"]
        end

        subgraph BS1 ["beam_server_1"]
            E1["shmem_dist.erl<br>(Erlang module)"] 
            E1 --> N1["shmem_dist_nif<br>(C NIF or linked driver)"]
        end

        %% Cross-server NIF communication
        N0 <--> |ring buffer| N1

        %% Shared Memory Region
        subgraph SMR ["Shared Memory Region"]
            direction LR
            TX["TX ring buffer<br>(0 → 1)"]
            RX["RX ring buffer<br>(1 → 0)"]
            MC["Microkit Channel (notification)"]
        end

        %% Connections to Shared Memory
        N0 ---> SMR
        N1 ---> SMR
    end

    %% Styling
    style Cluster fill:#f9f9f9,stroke:#333,stroke-width:2px
    style SMR fill:#e1f5fe,stroke:#0288d1,stroke-width:2px
    style BS0 fill:#fff,stroke:#333
    style BS1 fill:#fff,stroke:#333

Loading

Design points:

• Two unidirectional ring buffers per PD pair (TX + RX), matching the sDDF queue pattern already used for serial I/O (see main.c's serial_rx_queue_handle / serial_dequeue()).
• Microkit channels for wakeups:
  • When PD A writes a message, it notifies PD B via a Microkit channel.
  • PD B's notification handler routes to the correct carrier instance.
  • Same pattern as the notification-driven event loop from Make the BEAM PD block on notifications instead of busy-yielding at ~100% CPU #14.
• Depends on the native port driver primitives:
  • Shared-memory region + Microkit channel between two PDs.
  • See Let BEAM talk to a native PD over shared memory + a Microkit channel #21.
• The dist_proto handshake is unchanged:
  • Node name negotiation, cookie Challenge, and message framing happen at the Erlang level.
  • Only the transport layer changes.
• Carrier implementation:
  • Either a linked-in C driver (erl_driver) or a dirty NIF (erl_nif with ERL_NIF_DIRTY_IO). A linked-in driver integrates more naturally with ERTS's dist_util module
  • A NIF is simpler but must not block the scheduler.

Layer 2: Topology Definition (braid.erl)

• braid.erl is loaded as an OTP application.
• One designated PD (the manager_server) runs braid:create/1 to establish the cluster:

%% Topology config (generated from SDF at build time)
Nodes = #{
    n0 => #{
        args => [{connect_all, false}],
        connections => [n1, n3]
    },
    n1 => #{
        args => [{connect_all, false}],
        connections => [n0, n2]
    },
    n2 => #{
        args => [{connect_all, false}],
        connections => [n1, n3]
    },
    n3 => #{
        args => [{connect_all, false}],
        connections => [n2, n0]
    }
}.
Cluster = braid:create(Nodes).
%% braid:multicall(Cluster, erlang, nodes, []) =>
%%   #{n0 => ['n1@node','n3@node'],
%%     n1 => ['n0@node','n2@node'], ...}

On seL4, nodes are not spawned by our passive server:

• They are separate beam_server PDs that have already booted.
• Braid's manager connects to each as a hidden node over the shared-memory carrier, establishes the peer-to-peer connections, then steps back.
  our passive server- If the manager PD faults, the cluster continues (peers are directly connected).

Layer 3: PD Topology (SDF)

All PDs, memory regions, and channels are declared in tools/sdf/system.zig at build time. The SDF generator also emits the Erlang topology config so braid:create/1 receives the correct connection graph.

// Ring of N beam_server PDs + 1 manager PD
const n_nodes = 4;
var beam_pds: [n_nodes]PdPrototype = undefined;
for (0..n_nodes) |i| {
    beam_pds[i] = pd("beam_server_" ++ i, beam_server_elf).init();
}

const manager = pd("manager_server", beam_server_elf).init();

// Shared-memory regions for each ring edge
for (0..n_nodes) |i| {
    const next = (i + 1) % n_nodes;
    const region = shmem_region(
        alloc_name("shmem", i, next),
        shmem_size  // e.g., 2 MiB for dual ring buffers
    );
    map(beam_pds[i], region);
    map(beam_pds[next], region);

    const ch = channel();
    connect(beam_pds[i].notify, ch);
    connect(beam_pds[next].notify, ch);
}

• For a ring of 4 PDs, this yields 4 shared-memory regions (one per edge) vs 6 for a full mesh.
• For 8 PDs: 8 vs 28. The topology's resource cost scales with the chosen graph, not O(n²).

Layer 4: Cert PD for mTLS Key Isolation

Following braidcert's model, a dedicated cert_pd holds distribution TLS private keys and signs handshakes on behalf of beam_server PDs. The private key is mapped only into cert_pd's VSpace, if a beam_server PD is compromised, the distribution keys cannot be exfiltrated.

sequenceDiagram
    participant beam_server_0
    participant cert_pd as cert_pd (holds private key)

    beam_server_0->>cert_pd: signing request
    cert_pd-->>beam_server_0: signed blob

Loading

This is the natural seL4 expression of braidnode's "delegated signing" property: PD isolation replaces the patched-OTP approach.

Alternatives Considered

• Full braidnet/braidnode port: Too much work and not really worth the effort.
• Custom message-passing protocol (not dist_proto): Would lose compatibility with the Erlang ecosystem: rpc, global, pg, mnesia all expect standard dist_proto. The carrier is just the transport, the protocol stays standard.

Acceptance Criteria

• braid.erl loads as an OTP application inside beam_server PDs
• shmem_dist carrier passes the ERTS distribution handshake over shared memory (node name + cookie challenge)
• A ring of 2+ beam_server PDs established via braid:create/1 with topology defined in tools/sdf/system.zig
• net_adm:ping(n1@node) returns pong across PDs over shared memory
• A spawn/message round-trip works node-to-node (e.g., rpc:call) over shared memory
• braid:multicall(Cluster, erlang, nodes, []) shows correct topology
• Manager PD disconnection (e.g., fault) leaves the cluster intact, peer connections survive braid's hidden-node cleanup
• A dist-smoke harness boots N beam_server PDs + 1 manager PD, establishes the braid topology, and validates connectivity
• boot-smoke + shell-smoke remain green with the additional PDs in the image