Lambda OS

ミッションロジックのバグは、制御ループを壊せない。
ミッションは非特権で、ハードウェアに閉じ込められて走る。制御ループはその隣で、ネイティブに走る。MMU の無い 6 ドルのマイコンの上で。

リアルタイムシステムのアーキテクチャ — 感知・分析・決定・作動
x86_64 riscv64 aarch64 RV32 ARMv6-M
どのアーキで何が動くか

問題

小さな組込みシステムでは、性質の違う 2 種類のコードが 1 つのチップを分け合います。

デッドラインを絶対に落とせないコード——制御ループ、安全包絡線。そして何をするかを決めるコード——ミッション、飛行計画、案件ごとに変わる部分。

両者は要求が正反対です。デッドライン側は、信用されていて、変わらないべきもの。ミッション側は、頻繁に変えたいもので、そこにバグがあるのは普通のことです。ところが安価なチップでは、この 2 つが同じ特権で、同じメモリで走る——だからミッションの一つのミスが、制御ループを道連れにします。

逃げ道は 2 つ。すべてを注意深い C で書いて、分離可能なミッションを持たないか。あるいは MMU 付きの大きな SoC を買って Linux を載せるか。前者は開発速度を、後者は電力と単価を差し出すことになります。

一つの決断

Lambda OS は、チップを 2 つの層に分け、両者を 1 本の狭い検査済み境界でだけ触れ合わせます。

アクターが呼べるのは、カーネルが公開した決まった語彙——操作の集合だけです。それ以外に何もできません。以下のすべてが、この一つの分割から導かれます。

分けたから、アクターは閉じ込められる

カーネルはアクターを信用しないので、ハードウェアで閉じ込めます。各アクターは非特権で走り、シリコン自身のメモリ保護が箱に入れます。

これはソフトウェアの約束ではありません。自分の領域の外へストアしたアクターは、ハードウェアフォルトを取ります——x86 はページフォルト、RISC-V はストアアクセスフォルト、Cortex-M は HardFault。起動時のプローブが毎回それを確かめ、閉じ込めを外すと、同じストアが通ります。

そしてアクターが決まった語彙しか呼べないことが、二つ目の閉じ込めになります。ある物を命じる操作が無ければ、アクターはそれを命じられない。目標を提案することは許されても、最終目標を設定する操作を与えられていないアクターは、どう暴れても制御器を上書きできません。

タイミングがネイティブだから、デッドラインを守れる

デッドライン側のコードはカーネルにネイティブ Zig として置かれるので、暴走したアクターはそれを止められません——プリエンプトするタイマが切り替え、フレーム毎の命令数の予算が 1 フレームを有界にします。

スケジューラの時計はナノ秒クロックで、タイマは固定 tick ではなく次のデッドラインに合わせて張られます。だから 1 kHz の制御ループは、ふつうの周期タスクです。実機の RP2350 の上で、本物の制御則がスケジュールされた 1 kHz タスクとして走り、ネットワークとミッションが同じチップを分け合う中、1,741,824 ジョブすべてでデッドラインを守りました——超過ゼロ

同じ制御則の最悪値を、両ボードで 2 万入力の敵対的掃引で実測しました——Cortex-M0+ で 190 µs、Hazard3 で 98 µs。1 kHz の予算に対して 5.2 倍・10.2 倍の余裕です。

ハードを知るのはカーネルだけだから、移植は小さい

ハードウェアより上——スケジューラ、VM、アクター層、ネットワークスタック——は、5 つのターゲットすべてで同じソースです。差し替わるのはカーネルの底(HAL)だけで、コンパイル時に選ばれます。それを実装したアーキは差さり、しないアーキは実行時ではなくコンパイル時に落ちます。

だから、64bit の x86 マシン向けに書かれた 1 つの OS が、MMU も FPU もアトミック命令も一つも無い ARMv6-M の Cortex-M0+ まで一続きに降りて、スケジューラが譲ったのはサイズ表だけでした。

0アクターが自分のメモリの外へ書けるバイト数 — MMU の無い 2 つのチップを含む、全ターゲットで
190 µsCortex-M0+ 実機で実測した制御カスケードの最悪値 — 1 kHz の予算に対し 5.2 倍の余裕
1 kHz本物の制御則を、スケジュールされたタスクとして実機の RP2350 で。1,741,824 ジョブ中デッドライン超過 0 回
5単一の Zig ツールチェーンが出力するターゲット。x86_64 · riscv64 · aarch64 · RV32 · ARMv6-M

二層が地に着くところ:配送ドローン

この分割が最も見えやすいのは、Raspberry Pi Pico 2 W(RP2350、MMU 無し)の上で、実機で、ふつうの Wi-Fi 越しに走る飛行制御です。

**カーネルが、機体を飛ばします。**カスケード PID + 四元数の制御ループと安全包絡線は、ネイティブ Zig で、カーネルの中にあります。安全包絡線はジオフェンスを保持し、バッテリ低下で帰投し、故障した IMU を切り離してバックアップで飛び続け、制御を本当に失ったときにパラシュートを開きます。

**ミッションは、1 つの隔離されたアクターです。**それは飛行計画——基地から上昇し、海上を 90 m 先の島まで巡航し、貨物を落とし、帰り、着陸する——で、バイトコードとしてアップロードされ、非特権で、PMP に箱詰めされています。次の航点を提案し、制御器が実際に飛ぶ目標は、ネイティブの安全包絡線が決めます。飛行計画のバグは、安全包絡線にも制御ループにも触れられません。カーネル境界の向こう側にあるからです。

**そして基板は、飛ぶ前に境界を実証します。**プリフライトの手順が、非特権からカーネルメモリへのストアを試みます。ハードウェアがそれを拒否しなければ、基板は失敗を報告し、ミッションを起動しません。拒否が観測されて初めてミッションが起動され、基板は人間が発進を許可するまで待ちます。

プラント——物理、風、センサノイズ、注入される故障——は PC で走ります。コントローラは、机の上の RP2350 で走ります。その 2 つが、無線越しにループを閉じます。デモの全体は 飛行制御 のページにあります。

Lambda C で書いたミッション

ミッションアクターが、本物のハードウェアタイマを読み、50 ms ごとにピンを駆動し、カウントを別のアクターへ渡します。

// actor.c — ハードウェア隔離で走る Lambda C スクリプト
int self(void);
int send(int dest, int tag, int a, int b);
int recv(void);            // メッセージの tag を返す
int msg_a(void);           // そのメッセージの先頭ペイロード
int micros(void);          // 本物のハードウェアタイマ
int pin(int n, int v);     // 出力ピンを駆動

int last, state, count;

int main() {               // スケジューラのフレーム毎に 1 回呼ばれる
    if (self() == 0) {                       // 生産者
        int now = micros();
        if (now - last >= 50000) {           // 50 ms ごと
            last = now;
            state = state == 0 ? 1 : 0;
            count = count + 1;
            pin(0, state);                   // 作動
            send(1, 0, count, 0);            // 協調:tag 0、ペイロード = count
        }
    } else {                                 // 消費者
        int tag = recv();
        if (tag >= 0) host_log(msg_a());
    }
    return 0;
}

スクリプトはレジスタに一切触れません。micros()pin()send()決まった語彙——本物のタイマを読み、本物の GPIO を書き、カーネルが所有するメールボックスに積む、カーネル内の FFI ハンドラです。バイトコードが意図、カーネルが機構。

内部に無限ループも書きません。スケジューラが main() をフレーム毎に呼び直します。グローバルはフレームを跨いで残り、オペランドスタックは毎フレームリセットされる。だから全アクターが細かくプリエンプト可能なまま保たれ、暴走したフレームが機械を固めることもありません。

別々のチップのアクターが、互いに話す

あるチップのアクターが、別のチップのアクターへメッセージを送れます。それはふつうのメールボックスに届き、同じ recv() で読まれ、同じ tag で分岐されます——ゲートウェイも、プロトコル変換も、境界の第二のランタイムもありません。Pico 2 W 上の PMP 隔離アクターが、実 Wi-Fi と実 LAN 越しに、x86 の Lambda OS 上のアクターへメッセージを送り、返値を自分のメールボックスで受け取っています。

ここでのアクターモデルの狙いは、多数のアクターを 1 つの安いチップに詰め込むことではなく、各小型基板が少数のアクターを持ってネットワーク上で協調することです——末端がたまたま数ドルの、分散システム。

だから 2 種類のノードには別々の仕事があります。オーケストレータ(x86_64・riscv64・aarch64)は多数のアクターを抱え、そのための機構——動的な spawn、死んだワーカーを作り直す監視——を持ちます。エッジノード(MMU 無しの MCU)は 1〜2 個を持ち、ワイヤ越しに協調します。多数アクターの機構を小さいチップに載せるのは、分散アクターがそもそも避けるために存在する当のものです。

それ自体で完結した RTOS

Lambda OS は、ゼロから作られた RTOS で、それ自体で完結しています。カーネル——スケジューラ、ドライバ、ネットワークスタック、リアルタイムプリミティブ——は単独で立ち、デッドラインを絶対に落とせない制御はネイティブ Zig として走ります。構成を丸ごとネイティブにできます。バイトコードは一切無しでも。

ネットワークスタックは本物です。Ethernet、ARP、IPv4、ICMP、UDP、DHCP、DNS、そして再送・輻輳制御・高速再送・SACK・3 本の同時接続を持つ TCP——有線 Ethernet でも Wi-Fi でも同じソース。リアルタイムプリミティブは RTOS の定番一式です。優先度継承ミューテックス、CPU 時間の予約、レート単調解析、ナノ秒クロック。

ミッションが使われる場合、それは単一の信頼ドメインの中で走ります。すべてのバイトコードが同じ運用者から信頼経路で来るので、Lambda OS は意図的に、マルチテナント実行も、敵対的バイトコードの検証器も、汎用スクリプティング——クロージャ、GC、動的型付け——も提供しません。ここでの隔離は堅牢性の境界(バグの封じ込め)であって、敵対者への防御ではありません。

どこに合うか

Lambda OS はプロプライエタリソフトウェア、全権利留保——オープンソースではありません。共同開発、特定ハードウェア向けのカスタマイズ、そして有償エンゲージメントの一部としての NDA 下でのソース開示という形で関与します。

こういう状況のために作られました。

**いま使っている RTOS がこれらに答えているなら、それが正しい道具です。**答えていないなら、どのアーキで何が動くか を余さず書き出してあり、このサイトのすべての主張はそこで検算できます。

連絡先:Lambda LLC · ホストする姉妹 VM は Lambda C です。