Hibana ist ein in Rust entwickelter Laufzeit-Durchsetzungskernel für choreografierte, verteilte Protokolle, der speziell für ressourcenbeschränkte und no_std-Umgebungen ohne Heap-Allokator optimiert ist. Das System projiziert eine globale Kommunikationschoreografie in kompakte, lokale Endpunkt-Deskriptoren für bis zu 256 Rollen. Es garantiert die Einhaltung multiparter Protokolle durch affine, asynchrone Endpunkte und eine transportneutrale Schnittstelle. Die logische und funktionale Korrektheit wird durch formale Verifikation mittels Lean, Kani und Miri abgesichert, wobei ein minimaler Speicherabdruck von unter 6 KB SRAM erzielt wird.
Wichtigste Punkte
Speicherarchitektur: Der Kernel arbeitet bedingungslos no_std-kompatibel, benötigt keinen globalen Heap-Allokator und betreibt die gesamte Zustandsverwaltung über vom Aufrufer bereitgestellte Byte-Puffer (SessionKitStorage).
Rollen- und Adressierungsdomäne: Unterstützt exakt bis zu 256 Rollen (0..=255 im u8-Bereich) sowie kompakte Programmabbilder bis maximal 65.535 Bytes pro Rolle oder globale Choreografie.
Protokoll-Operatoren: Bietet fundamentale Operatoren zur Zusammensetzung wie asynchrone Nachrichtenübertragung (g::send), Sequenzen (g::seq), parallele Verzweigungen (g::par), binäre Routen (g::route) und gesicherte Schleifen (.roll()).
Transportunabhängigkeit: Ein strikter Fünf-Operationen-Vertrag (open, poll_send, cancel_send, poll_recv, requeue) entkoppelt die Protokolllogik vollständig von der physischen Transportschicht.
Ressourcen-Fußabdruck: Gemessene Spitzenwerte auf eingebetteten ARM-Zielarchitekturen (thumbv6m-none-eabi) betragen 5.274 Bytes für den modellierten Laufzeit-SRAM und 2.591 Bytes für den Operations-Stack.
Formale Verifikation: Kombiniert den Theorembeweiser Lean für globale Semantik, den Bounded Model Checker Kani/CBMC für kompakte Kernel-Prüfungen sowie Miri für Leih- und Speichersicherheitsanalysen.
Diskussions-Highlights
Vergleich mit ChoRus: Kommentatoren hoben hervor, dass Hibana im Gegensatz zu Rusts bestehendem choreografischen Framework ChoRus (entwickelt von Lindsey Kupers Gruppe an der UC Santa Cruz, dokumentiert in arXiv:2311.11472) vollständig no_std-kompatibel ist.
Verwandte Frameworks und Sprachen: Die Diskussion verglich den Ansatz mit zahlreichen alternativen Projekten, darunter das Java-basierte Choral, die akteursbasierte Sprache March, die Elixir-Choreografiebibliothek Chorex sowie Microsofts Orleans (Virtual Actors).
Quic-Erweiterung: Der Autor (o8vm) verwies im Thread auf das ergänzende Projekt hibana-quic zur Implementierung von QUIC und HTTP/3 auf Basis von Hibana-Choreografien.
Kritik an der Dokumentation: Mehrere Teilnehmer kritisierten den README-Schreibstil als schwer verständlich und merkten an, dieser wirke stark KI-generiert („Claudish“), während andere den hohen Grad an theoretischer Informatik-Präzision verteidigten.
Glossar
Choreografische Programmierung (Choreographic Programming): Ein Programmierparadigma, bei dem verteilte Kommunikationsprotokolle aus einer globalen, einheitlichen Perspektive anstatt durch isolierte Endpunkt-Implementierungen beschrieben werden.
no_std: Eine Rust-Compiler-Direktive, die den Standard-C-Laufzeitbibliotheken (std) den Zugriff entzieht, wodurch die Ausführung auf Mikrocontrollern und in kernelnaher Systemsoftware ohne Betriebssystem möglich wird.
Affine Typen (Affine Types): Ein Typsystem-Konzept, bei dem eine Ressource (wie ein Kommunikationsendpunkt) höchstens einmal verwendet, aber im Gegensatz zu linearen Typen nicht zwingend verbraucht werden muss.
Lean: Ein interaktiver Theorembeweiser und formales System zur mathematischen Beweisführung von Software- und Protokolleigenschaften.
Kani: Ein formales Verifikationswerkzeug (Bounded Model Checker) für Rust-Code, das Programme auf mathematische Invarianten und Speicherfehler untersucht.
Miri: Ein experimenteller Interpreter für die Rust-Zwischensprache MIR, der undefiniertes Verhalten, Datenrennen und Verstöße gegen Zeigerregeln (Stacked Borrows) aufdeckt.
SRAM (Static Random-Access Memory): Ein schneller, flüchtiger Halbleiterspeicher, der in Mikrocontrollern für temporäre Laufzeitdaten und Funktions-Stacks eingesetzt wird.