Cohesix Architecture

Cohesix is a seL4-based control-plane operating system for edge GPU nodes. A Queen admits and supervises bounded Worker tasks; host executors perform GPU and ecosystem operations through explicit, ticketed interfaces. Physical drivers run in isolated target runtimes, and the authenticated console is the only target TCP listener.

This document owns the system-level view of Cohesix: trust boundaries, runtime components, principal control and data flows, and the selected direction for seL4 task and temporal isolation. Exact namespace contracts belong in INTERFACES.md, Secure9P invariants in SECURE9P.md, role policy in ROLES_AND_SCHEDULING.md, and physical-driver rules in DRIVERS.md.

Readers new to Queen, Worker, NineDoor, and other Cohesix terms can start with the Glossary.

Architecture state is explicit throughout this document:

• Current means implemented by the selected checked-in profile and source. A current target claim still requires evidence for that exact target and artifact set.
• Accepted means the required immutable evidence exists for the exact profile, target, image, and proof class. Configuration, implementation, target acceptance, runtime-release acceptance, and production-use-case acceptance are different states.

1. Authority and evidence boundary

Cohesix is built from the tag-pinned upstream seL4 16.0.0 project. The selected revision and complete source, toolchain, profile, and evidence provenance are recorded with each qualified build. Target userspace is pure Rust no_std.

The selected profile manifest, its resolved manifest, and generated coh-rtc outputs define generated interfaces, limits, feature gates, object topology, and selected behavior. The checked-in default-profile snapshot is available in the generated manifest snippet; a target build must use artifacts generated from its selected configs/root_task*.toml file. The selected SEL4_BUILD_DIR supplies exact kernel headers, configuration, object sizes, platform metadata, and timer truth.

The root bootstrap TLS-base cell is real, sixteen-byte-aligned storage owned by sel4-sys, alongside its atomic accessors. The runtime entry crate does not redeclare that symbol. Publishing a base address grants no mutable ownership of the TLS image; its unsafe mutable accessor requires exclusive caller ownership. The current libsel4 IPC-buffer pointer remains separately installed from BootInfo. Exact ELF inspection must confirm the TLS cell occupies sixteen bytes and does not overlap other writable symbols.

1.1 Current implementation boundary

The selected source profiles define one four-core SMP+MCS architecture for QEMU and Raspberry Pi 4. Exact budgets, object counts, capabilities, image identities, and timer frequencies come from the selected manifest, resolved manifest, seL4 build outputs, and generated tables rather than this overview.

See Current Status for the public capability snapshot and Roles and Scheduling for the temporal contract.

1.2 Evidence classes

Implementation and proof remain separate:

• Source, generated descriptors, and a staged image prove that a path can be built; they do not prove that a board booted that image.
• QEMU evidence proves the exact QEMU profile only.
• Fresh Pi evidence proves only the specifically observed behavior for its read-back-bound image and named boot/evidence set; it does not transfer to another image, boot, or target.
• Wired GENET, CYW43 Wi-Fi, USB/local-seat, serial, HDMI, driver-runtime, console, Worker, temporal-isolation, and benchmark proof remain independent ledgers.
• An upstream proof-eligibility profile proves only compatibility with the upstream verified-configuration preconditions. It is not a Cohesix kernel, Rust userspace, boot-path, hardware, DMA, SMP, or timing proof.

The selected AArch64 SMP+MCS configurations are not represented as tag-pinned verified seL4 configurations. The seL4 16 caveats describe AArch64 MCS verification as incomplete and SMP+MCS as less explored. Exact QEMU and Pi acceptance is therefore mandatory, but it does not create a formal-verification claim.

The active scope and proof requirements are normative in BUILD_PLAN.md. Boot-by-boot results are non-canonical evidence; canonical claims point to the tracked plan, test contract, and archived target-qualified artifacts.

2. Current design boundary

Cohesix is a control-plane operating system for secure orchestration and telemetry of edge GPU nodes. It uses a Queen/Worker model and exposes bounded, file-oriented control surfaces.

The complete target trusted software closure contains:

• the selected upstream seL4 kernel build;
• the Rust root task and compiler-generated policy tables; and
• manifest-declared physical-driver runtime images plus their fixed ABI.

Within that closure, the root task is the principal userspace authority domain. Selected physical-driver runtimes are genuine seL4 compartments with restricted CSpace/VSpace authority; they are not part of the root address space. This distinction does not imply that a driver is untrusted for every device property or that BCM2711 DMA is confined by an IOMMU.

The target does not contain CUDA, NVML, container runtimes, a POSIX emulation layer, or general host integration stacks. GPU access, PEFT execution, REST projection, FUSE, systemd, Docker, Kubernetes, federation, SIEM, and other heavy ecosystems remain host-side. The only permitted in-target TCP listener is the authenticated console.

2.1 Current components

The operational QEMU and Pi manifests mark worker-heartbeat, worker-gpu, and worker-lora executable and require their endpoint, lifecycle, notification, image, object, and temporal-authority records. worker-bus is the only selected model_only role. Those declarations and packaged artifacts are implementation truth, not proof that a particular image loaded, resumed, or contained a Worker TCB. See ROLES_AND_SCHEDULING.md.

2.2 Current system boundary

The flowchart groups the build host, operator and integration host, and selected seL4 target. These groups show deployment location; they do not claim that every node has its own address space. The target’s sole TCP ingress reaches console-network-runtime, while Queen authority stays with root. Native CUDA and PEFT providers stay on their selected external hosts; host-ticket-agent runs on the host performing the action. That host may differ from the operator host. The admitted host-ticket path is shown under Hive Gateway in the host-tool guide.

flowchart TB
  subgraph BuildHost[Build host]
    Manifest[Selected profile manifest]
    Compiler[coh-rtc]
    Generated[Resolved manifest and generated artifacts]
    Manifest --> Compiler --> Generated
  end

  subgraph OperatorHost[Operator and integration host]
    HostClients[cohsh coh SwarmUI FUSE REST clients and host bridges]
    ConsoleOwner[one direct owner or hive-gateway]
    HostNineDoor[Host NineDoor library and fixture adapter]
    HostClients -->|live target composition| ConsoleOwner
    HostClients -->|explicit host-model or in-process test Secure9P| HostNineDoor
  end

  subgraph Target[Selected target implementation]
    Serial[Serial and local-seat consoles]
    subgraph Critical[Critical TCBs with independent active SCs]
      EventPump[Root-control event pump and Queen authority]
      RootFault[Root-fault blocking receive and serialized Reply]
      Emergency[Root-emergency fatal output]
      WorkerSupervisor[Worker supervisor]
      DriverSupervisor[Driver supervisor]
      GpuExecutor[GPU Worker executor]
      LoraExecutor[LoRA plus Heartbeat executor]
    end
    ConsoleChild["Active console-network child\nTCP, authentication, and smoltcp\nQEMU VirtIO, Pi direct GENET, or mediated Wi-Fi"]
    NineDoorChild["NineDoor child\none-shot bootstrap SC then passive"]
    subgraph WorkerPopulation["256 passive Worker children"]
      HeartbeatWorker[1 Heartbeat]
      GpuWorkers[127 GPU]
      LoraWorkers[128 LoRA]
    end
    Hal[HAL admission and driver clients]
    Drivers[Profile-selected isolated driver runtimes]

    Serial -->|console lines| EventPump
    ConsoleChild <-->|bounded control and events| EventPump
    ConsoleChild <-->|Wi-Fi packet copies; GENET copies before handoff| EventPump
    EventPump <-->|after bootstrap, depth-one donated Call and Reply| NineDoorChild
    EventPump -->|control records and wake| WorkerSupervisor
    RootFault -->|fault handoff, Reply release, and revoke| WorkerSupervisor
    WorkerSupervisor -->|construct, READY, and teardown| HeartbeatWorker
    WorkerSupervisor -->|construct, READY, and teardown| GpuWorkers
    WorkerSupervisor -->|construct, READY, and teardown| LoraWorkers
    EventPump -->|bounded fair work| GpuExecutor
    EventPump -->|bounded fair work| LoraExecutor
    GpuExecutor <-->|donated SC and instance Reply| GpuWorkers
    LoraExecutor <-->|donated SC and instance Reply| HeartbeatWorker
    LoraExecutor <-->|donated SC and instance Reply| LoraWorkers
    RootFault -->|fault handoff and recovery| DriverSupervisor
    EventPump --> Hal
    Hal -->|bounded ABI service turns| Drivers
    Drivers <-->|Pi GENET post-DHCP DGHO\n32 CPU-only pages and reciprocal wake hints| ConsoleChild
  end

  Generated -->|profile truth| EventPump
  Generated -->|Worker mix and lifecycle records| WorkerSupervisor
  Generated -->|executor budgets and donor allowlists| GpuExecutor
  Generated -->|executor budgets and donor allowlists| LoraExecutor
  Generated -->|resource descriptors| Hal
  Generated -->|console descriptor| ConsoleChild
  ConsoleOwner -->|sole target console session| ConsoleChild
  HostNineDoor -.->|shared contracts; separate state| NineDoorChild

The dotted relationship is semantic parity, not a transport connection. Host NineDoor and target NineDoorBridge are separate adapters with separate state. There is no in-target 9P-over-TCP listener.

3. Current target execution model

3.1 Kernel and root authority

The current root task constructs seL4 objects, validates generated descriptors, creates admitted service, Worker, and physical-driver address spaces, installs their capabilities, and schedules bounded service work. Current source uses untyped retype, guarded CNodes, CSpace derivation/revocation, TCB/VSpace/ASID/IPC-buffer construction, endpoints, notifications, IRQs and badges, fault and timeout endpoints, Reply objects, scheduling contexts, per-core SchedControl, AArch64 mappings and cache maintenance, and MCS TCB configuration.

Current implementation-level capability admission relies on a successful bounded retype, the BootInfo CSpace window, and exact publication state. DebugCapIdentify is optional telemetry; it cannot admit, reject, or recover a capability.

The init TCB is the generated root-control owner and runs the authoritative event loop. Root constructs six restricted active-SC children for root-fault, root-emergency, Worker supervision, driver supervision, and the two bounded passive-Worker executor lanes. The generated fault registry is sealed before any service or Worker child resumes. On Pi, the existing root-fault and root-emergency receivers start immediately after their own construction, before device and network-stack construction. An unsealed fault latches fatal state and reports the copied badge, label, length and four message registers in bounded raw UART chunks; it cannot consult the mutable registry, reply, or invoke recovery. QEMU retains activation after sealing. Root-fault is the sole receiver on one shared standard/timeout fault endpoint. It blocks in Recv with one Reply object and resolves the exact badge and class against the sealed registry after receive. The selected console child retains its reserved timeout identity in that topology but does not install it as a TCB timeout handler; its budget exhaustion uses native postponement instead. Application service-turn and queue bounds remain mandatory beside kernel-enforced MCS budgets. Live QEMU qualification must still prove independent progress, console standard-fault containment, console budget-exhaustion postponement, serialized Reply release, and containment for the selected image.

3.2 Physical task isolation and memory authority

Manifest-declared physical-driver runtimes execute as separate seL4 tasks with task-local address and capability spaces. Root delegates only generated endpoint, notification, frame, shared-ring, IRQ, fault, and mapped-resource authority. Pi profiles preflight root-CNode, slot, untyped, and mapping capacity before partial child construction; the current Pi contract uses a 16-bit root CNode for the complete 256-Worker population and deterministic reserve.

Isolated child image plans reject effective W+X mappings. Code pages are read-only and executable, non-code mappings are ExecuteNever, and writable root aliases of executable frames are removed before child resume. Child-only code/stack authority is transferred deliberately rather than left ambient.

Driver-task isolation is capability and address-space isolation. It is not a claim that every device is protected from malicious DMA: the selected Pi DMA profile remains bounded-no-iommu.

3.3 Current Worker and Queen execution model

Queen is root-task orchestration authority exposed through the console and NineDoor control surfaces; it is not a separate host RPC service or target TCB. The selected operational profiles expose executable Heartbeat, GPU, and LoRA roles plus model-only WorkerBus. Root constructs each executable image as a suspended, W^X, least-authority passive child. Two active executor lanes own the generated Worker-core budgets: the GPU lane serves only GPU instances; the LoRA lane serves LoRA and Heartbeat. A fixed fair queue selects one exact instance, donates the lane SC through a depth-one endpoint Call, and regains it only through that instance’s generation-scoped Reply object. A successful admission request queues or resumes only its exact role instance; it is not a READY receipt. Namespace publication follows the child’s durable READY record, and control/receipt completion is accepted only for the pinned role, slot, logical lease epoch, supervisor generation, and capability generation.

This topology makes Worker cardinality an object/isolation question rather than one active-SC reservation per instance. The QEMU and Pi manifests each expand to one Heartbeat, 127 GPU, and 128 LoRA instances. Code and read-only role-image frames may be shared only under an exact sealed image identity. Writable image pages, stacks, IPC buffers, ABI pages, CSpaces, VSpaces, Reply objects, and fault identity remain per-instance.

A Worker ticket still does not prove execution by itself. ATTACH remains session binding, not task creation. Direct target evidence must observe the generated capabilities, notifications, scheduling authority, READY transition, fault containment, complete teardown, stale-authority refusal, and fresh-generation recreation before the corresponding runtime claim is accepted.

3.4 Current timer and emergency-output qualification

Operational QEMU and Pi timing paths require the selected seL4 build’s exported virtual counter and generated frequency. The compiler and root build reject a missing/zero clock, dummy/read-count timing, an MCS/profile mismatch, or a hard-coded operational frequency fallback. Emergency output is a real selected serial path; null/no-op serial remains fixture-only and cannot enter an operational closure. Exact-image qualification must still observe the selected clock, timeout, budget, and fatal-output paths rather than inferring them from source or configuration.

The physical Pi MCS profile additionally declares one bounded wake producer for an exact direct-GENET globally idle root: BCM system-timer channel 3 is a separately tagged physical duty of the existing isolated pcie-root runtime. Root owns no timer MMIO or IRQ; it consumes the runtime’s post-clear/rearm fan-in hint and reads the exported virtual counter as the sole time authority. The existing runtime task and scheduling context are unchanged. WiFi does not use this global-idle receive; it may block only for a currently issued finite transaction or exact causal-child debt. Static declaration, a timer edge, or QEMU convergence cannot qualify Pi deadline behavior or network latency.

3.5 Current identity and attestation qualification

Root-task reports public manifest measurements as measurement_only, with development_static ticket keys. Schema 1.20 removes automatic TPM/DICE fallback labels. Required evidence and signed modes without an admitted device provider fail before generated ticket registration. /proc/attest/capabilities and /proc/attest/status expose that state without claiming a signature.

The shared host TPM2 verifier validates the signed evidence contract. The stock Pi 4 is excluded from positive signed-device acceptance by the 2026-09-14 owner decision. Physical TPM/DICE issuance and device-bound ticket material remain the separate reopened Milestone 26 device task; the selected images do not claim attested-production admission.

4. Control-plane paths

Cohesix has two distinct operator protocol families:

1. Host-model or in-process Secure9P. A client negotiates the bounded 9P2000.L subset with the Host NineDoor library or fixture adapter. This path has state separate from a live target and cannot create or prove a target task.
2. Target console grammar. Serial carries console lines directly. TCP adds a four-byte little-endian length frame and transport authentication before the same bounded command grammar. Application ATTACH then selects a role and optional capability ticket.

Both adapters project overlapping namespace semantics, but they are not the same wire protocol. Exact framing, operations, acknowledgements, and errors are defined in External Interfaces. Internal task ownership does not change these public authority paths.

Host REST, UI, GPU, PEFT, FUSE, sidecar, and federation tools are projections over documented interfaces. They may validate, batch, perform host-only work, or render data, but they cannot introduce target authority unavailable through the underlying ticketed namespace or console operation.

4.1 Delegated host authority

Root owns a bounded Queen intent dedupe table alongside Queen policy. Physical drivers retain their isolated owners and the authenticated console remains the only target TCP listener. The host gateway verifies per-request capabilities and serializes admitted writes over its existing console session. /proc/authority reports gateway_enforced delegation; selected kernel production profiles and provisioned authority production profiles remain separate selections. Host-ticket writer fencing and provider execution WAL run on the host. The shared cohesix-authority crate is no_std on target and carries correlation records; admission evaluation is outside its current scope. See M27a authority.

5. Boot flow

The target boot sequence is profile-qualified:

1. Firmware and bootloader load the selected seL4 image. Pi 4 acceptance uses firmware → U-Boot → seL4 binary image; it does not depend on UEFI.
2. seL4 supplies BootInfo and generated kernel metadata to root-task.
3. Root validates the kernel/profile contract, establishes CSpace and VSpaces, selects the timer backend, and loads generated policy.
4. Root constructs the restricted namespace, console-network, fault, supervisor, Worker, and selected driver compartments from exact image and generated resource records. Children remain suspended until their admission and fault routes are ready.
5. HAL admits manifest-declared physical resources and starts selected driver runtimes. Owner state is credited only after runtime identity, resources, and service progress are proved.
6. Hardware and policy gates record their state. Emergency serial and bounded root diagnostics may remain available while hardware acceptance is red; a prompt is not device-acceptance evidence.
7. Root initializes the namespace bridge, log ring, and profile-enabled operator surfaces, then enters the bounded event pump. Executable Worker namespace state becomes live only after the exact child publishes READY.

On the Pi bcmgenet-v5 profile, the event pump first obtains DHCP through the bounded bootstrap path. It then proves every root-mediated GENET command, RX, and TX cursor quiescent, publishes the handoff-pending generation, and issues one generation-bound zero-payload DGHO. Only an exact PROGRESS/READY terminal makes the 32-page CPU-only child link READY; exact IDLE/QUIESCING retains the old path for bounded drain and retry. No failure reopens root packet mediation. Other network profiles omit this transition.

Pi saved boot policy is loaded by the staged U-Boot script and passed through bounded /chosen/cohesix,* properties. Saved policy may select or configure an allowed network path, but it does not rewrite the compiled manifest. See Boot Reference and Hardware Bring-up.

6. Principal data flows

6.1 Worker lifecycle and telemetry

An authorized Queen operation appends a bounded control record. Root validates the role, ticket, lifecycle gate, generated slot, image identity, and resource limits before the Worker supervisor may create or resume an executable child. A successful spawn acknowledgement means only that the request was admitted; namespace and telemetry publication begin after the exact generation-stamped READY record.

Control and receipt results are pinned to role, slot, lease epoch, supervisor generation, and capability generation. Kill, shutdown, fault, and construction failure converge on one idempotent teardown that suspends execution, resolves the instance Reply state exactly once, returns any donated executor SC, clears records and signals, unmaps private memory, revokes capabilities, and excludes the old generation before reuse. Host NineDoor performs analogous role and namespace validation only against its separate host-model or fixture state; it cannot create a target child.

The canonical telemetry path is:

/shard/<label>/worker/<id>/telemetry

The legacy /worker/<id>/telemetry alias exists only when the selected manifest enables it.

6.2 GPU and PEFT control

gpu-bridge-host owns hardware discovery and CUDA/NVML interaction and publishes bounded host namespace state. WorkerGpu and WorkerLora are receipt-oriented target tasks; host executors continue to own GPU lease side effects and PEFT/model lifecycle work. Root pins the exact live Worker identity before accepting a correlated terminal result.

No host provider state independently proves Worker READY, and no Worker receipt independently proves a real external side effect. See GPU Nodes for this boundary.

6.3 Pi direct GENET data path

Console-network ABI v6 derives its direct-GENET extension only for the exact Pi bcmgenet-v5 profile. It reuses 32 admitted GENET pages after the handoff cut: page 0 is the aligned sequence-last control page, pages 1 through 15 carry GENET-to-console RX frames, and pages 16 through 31 carry console-to-GENET TX frames. Both children map those pages as cacheable Normal/XN CPU-only memory; the range grants no physical-address, MMIO, DMA, or device-visible authority.

GENET remains the sole MMIO/DMA/IRQ and private-DMA-ring owner and copies between those rings and the CPU link. Console-network remains the sole smoltcp, TCP, and transport-authentication owner. Each direction has one producer and one consumer with generation-bound monotonic cursors and sequence-last commits. Reciprocal send-only notifications are coalescing wake hints; durable cursor state and the mandatory final recheck before waiting carry truth.

A failed handoff, stale generation, invalid cursor or sequence, descriptor drift, peer fault, or containment error poisons the link and couples containment of the two child generations. Root suspends the GENET owner, removes both reciprocal notification caps, and removes all console copies of the 32 pages before anchor revoke. It does not restore a root packet-copy, poll, or GENET packet-command path.

The Pi direct-GENET console image has a 69-page PT_LOAD footprint. Its selected service inventory is 107 frames and 164 retained root CSpace slots; the speed-profile increase is three executable image frames and their retained mapping caps. The 32 direct pages are reused external GENET pages and therefore add console mapping caps, not new data-plane frames or a larger child untyped. These are generated construction bounds. They do not prove a Pi boot, handoff, packet correctness, latency, throughput, QEMU parity, or acceptance.

6.4 Observability

Logs, pressure, session, scheduling, lease, ingest, task, fault, and evidence state are exposed through bounded namespace nodes. The selected manifest gates each generated provider. Exact paths and formats are defined in External Interfaces; host UI and gateway consumers do not own those schemas or raise the evidence level of their source.

6.5 Operator observations and retained evidence

apps/coh/src/operator.rs owns bounded live and canonical-pack observations, exact diffs, and non-attested result classification. Existing evidence and timeline modules provide the pack layout and source-linked case summaries. cohsh-core owns both legacy fixture and live-capture versions of the canonical trace container; cohsh::trace_capture owns passive recording, shared redaction, and offline retained reads reused by coh-status and SwarmUI. These host modules retain the authority of their source observations; recording or replay grants no mutation or physical-device authority. The operator contract defines their authority limits.

6.6 Host field-bus ownership

MODBUS RTU/TCP and DNP3 codecs and transport ownership live in apps/sidecar-bus under its explicit native feature. The manifest compiler selects exact endpoint and point maps. The host ticket agent admits no arbitrary wire function or payload; controls require independently signed exact grants. The device-owning process persists intent before I/O and terminal ACK before publication. host-sidecar-bridge reads that WAL for expiring snapshots without opening the device. WorkerBus and the legacy target /bus coordination files remain model/session-only. See FIELD_BUS.md.

7. Security invariants

• All target physical-device authority passes through HAL.
• Selected steady-state physical drivers are manifest-declared isolated runtimes; the Pi DMA claim remains bounded-no-iommu.
• The Pi direct-GENET range is CPU-only and grants neither child new DMA, MMIO, physical-address, or root-policy authority. Its reciprocal notifications are wake hints, and either peer’s failure triggers coupled fail-closed containment without a root packet fallback.
• Target code remains no_std; host capabilities and heavy ecosystems do not enter the target closure.
• Isolated child mappings are W^X, and executable frames retain no writable root alias when a child resumes.
• Capabilities, tickets, generated bounds, and lifecycle gates are checked before side effects.
• Secure9P, console grammar, Worker interfaces, and driver-task ABIs remain separate bounded interfaces.
• The target has no TCP listener except the authenticated console.
• Every active TCB has an admitted scheduling context, core, budget, and period; every passive TCB has an allowlisted donor, Reply, timeout, fault, cancellation, and recovery chain.
• SchedControl remains root-only, and kernel scheduling budgets do not replace application queue, byte, operation, or service-turn bounds.
• Root control, fault, emergency, Worker-supervisor, and driver-supervisor progress have independent reserves and an acyclic fault graph.
• Every live child has a complete capability, mapping, scheduling-context, and Reply teardown with stale-generation exclusion before reuse.
• Operational profiles contain no silent mock, dummy, stub, no-op, synthetic, or live-to-fixture fallback.
• Current measurement hashing is not hardware-backed attestation.
• Exact SMP+MCS target acceptance is not an upstream formal-verification claim.

8. Source map

• Public capability snapshot: STATUS.md
• Scope and milestones: BUILD_PLAN.md
• Default generated profile summary: snippets/root_task_manifest.md
• Kernel profile contracts: configs/sel4/profiles.toml
• Manifest inputs: configs/root_task.toml and configs/root_task_pi4_uboot_aarch64.toml
• Root task: apps/root-task
• Host NineDoor: apps/nine-door
• Physical-driver runtime: apps/pi4-driver-runtime
• Driver ABI: crates/pi4-driver-abi
• Host-tool boundary: HOST_TOOLS.md
• GPU boundary: GPU_NODES.md
• Role and scheduling contract: ROLES_AND_SCHEDULING.md
• Manifest compiler: tools/coh-rtc
• Validation and acceptance: TEST_PLAN.md