Cohesix 1.0.0-beta — AArch64 SMP+MCS, isolated Rust drivers, and Pi 4 images
Hi all, Following my initial announcement in January, I’m pleased to announce Cohesix 1.0.0-beta. Cohesix is an Apache-2.0 research operating system for edge GPU orchestration, built on seL4 with pure Rust no_std target userspace. It combines capability-based resource control with a Plan 9-inspired namespace for commands, telemetry, and policy. GPU execution stays on the host; Cohesix coordinates authority, leases, and task lifecycles. This is a substantial architectural change from 0.9.0. Several parts may be of particular interest to this list. - AArch64 SMP+MCS on seL4 16.0.0 The QEMU and Pi 4 profiles use four cores, with explicit scheduling contexts for control, fault handling, supervision, drivers, and Worker executors. The NineDoor namespace service and executable Workers are passive children served through scheduling-context donation and Call/Reply. The aim is to make execution budgets and the authority to consume them inspectable alongside the capability topology. - Isolated drivers with explicit cooperation between runtimes Pi drivers execute in separate CSpaces/VSpaces, with HAL admitting their device resources. Generated links use bounded, pointer-free request/completion records, shared buffers, and notifications. For example, CYW43 owns Wi-Fi firmware and protocol state while a separate SDIO runtime owns the physical bus. On Ethernet, an explicit post-DHCP handoff connects the GENET driver directly to the isolated TCP/console service, removing root from the steady packet path. - Manifest-driven system construction The coh-rtc compiler validates the selected profile and generates resource inventories, scheduling parameters, runtime descriptors, and policy tables. Device ownership, shared-memory links, and queue bounds are declared together, giving contributors a concrete contract for adding or reviewing a runtime. - Passive Worker populations with bounded execution Both target profiles configure 256 Worker instances across heartbeat, GPU-lease, and model-lifecycle roles, served by two active executor lanes. Each instance retains its own capability and lifecycle identity, including generation checks across replacement. This separates the number of represented control-plane tasks from the number of active scheduling contexts. - Trying the release There are prebuilt bundles for Apple Silicon macOS and Linux AArch64, including their matching QEMU guests and host tools, plus a complete Raspberry Pi 4 SD image. No GPU is needed to explore the OS in QEMU. Downloads: https://github.com/lukeb-aidev/cohesix/tree/main/releases Release notes: https://github.com/lukeb-aidev/cohesix/blob/main/releases/RELEASE_NOTES-1.0.... Quickstart: https://github.com/lukeb-aidev/cohesix/blob/main/docs/QUICKSTART.md Architecture: https://github.com/lukeb-aidev/cohesix/blob/main/docs/ARCHITECTURE.md Driver contracts: https://github.com/lukeb-aidev/cohesix/blob/main/docs/DRIVERS.md I’d particularly welcome feedback on the passive-service donation model, driver-link ownership, and the boundary between generated policy and runtime enforcement. Code review, hardware observations, and comparisons with other seL4 system designs would all be valuable. This remains a research beta. No formal verification of Cohesix or its selected SMP+MCS configuration is claimed. The release notes document qualification limits, including outstanding fault/wake evidence, an unrepeated full burn-in, and the absence of fresh runtime qualification for the published builds. Best, Lukas Bower
participants (1)
-
Lukas Bower