Raspberry Pi 5で動かす

何を買えばよいか、SDカードのビルドと書き込み方、ボードのシリアルログの読み方とチェックの仕方、そしてPi 5でシステムを無人で実行する方法や、HDMI画面でユーザーインターフェースを見る方法。

Raspberry Pi 5は、NoWayOSのリファレンスボードです。低価格で広く手に入り、最初のハードウェアテストもこのボードで行っています。QEMUで合格したシステムは、Pi上でも同じ期待出力ファイルを使い、ボードのシリアルログからチェックします。

ボードについての二つのルール。 PiのUARTには、5 Vのシリアルアダプターを決してつながないでください。3.3 Vのポートです。また、開発用ボードでは、Piのワンタイムプログラマブルメモリに書き込んだり、セキュアブートを有効にしたりしないでください。どちらも元に戻せません。make sdcardは、そのどちらかを行うconfig.txtや、ボードの電圧を変えるconfig.txtを拒否します。

必要なもの

品目	備考
Raspberry Pi 5	16 GBモデルで開発・テストしています。どのコマンドもボードを`rpi5b_2gb`と指定します。これはPi 5のメモリのうち最初の2 GBを使うseL4の構成で、ビルドはそのうち1 GB弱をseL4に与えます。そのため、2 GB、4 GB、8 GBのモデルでも何も変える必要はないはずですが、試してはいません
電源	公式の5 V・5 AのUSB-C電源か、それと同等のもの。電力が足りないPi 5は、ソフトウェアのバグのような振る舞いをします
microSDカード	`make sdcard`がビルドするブートパーティション用
Raspberry Pi Debug Probe	そのUARTケーブルが、Pi 5の3ピンのデバッグ用コネクタに合います。適切なケーブルがあれば、3.3 VのUSBシリアル変換アダプターならどれでも使えます
HDMIモニター、USBキーボードとマウス	ユーザーインターフェース用。モニターは電源を入れる前につないでください。ファームウェアが画面を設定するのは起動時だけです。USBのブートプロトコル対応キーボードとマウスは使えますが、ハブはまだ使えません

SDカードをビルドする

make sdcard BOARD=rpi5b_2gb SYSTEM=hello

これで、カードのブートパーティションがbuild/rpi5b_2gb/hello/sdcard/に書き出されます。U-Boot、デバイスツリーとオーバーレイ、config.txt、seL4イメージloader.img、ライセンスファイル、そして後でカードをチェックするためのSHA256SUMSです。U-Bootは、コンテナの中でソースから再現可能な形でビルドされます。

カードに書き込む

macOSの場合

diskutil listでカードを見つけます。external, physicalと表示され、カードの容量と同じものです。次の手順でそのディスク全体が消去されるので、番号を二度確かめてください。
PIBOOTというラベルでフォーマットします。

diskutil eraseDisk FAT32 PIBOOT MBRFormat /dev/diskN

ファイルをコピーし、すべてが無傷で届いたことを確かめます（すべて一致すれば、何も表示されません）。

cp -RX build/rpi5b_2gb/hello/sdcard/ /Volumes/PIBOOT/
dot_clean -m /Volumes/PIBOOT
(cd /Volumes/PIBOOT && shasum -a 256 -c SHA256SUMS | grep -v ': OK$')

diskutil eject /dev/diskNで取り出し、Piに挿します。

Linuxの場合

同じ手順を、Linuxのツールで行います（プロジェクト自身のカードはmacOSで作っています）。

lsblk -pでカードを見つけます。/dev/sdXや/dev/mmcblk0のような、カードの容量と同じディスクです。次の手順でそのディスク全体が消去されるので、名前を二度確かめ、そのパーティションがマウントされていれば、すべてアンマウントしてください。
PIBOOTというラベルのFAT32パーティションをひとつ作ります（dosfstoolsとpartedが必要です）。

sudo parted --script /dev/sdX mklabel msdos mkpart primary fat32 1MiB 100% set 1 lba on
sudo mkfs.vfat -F 32 -n PIBOOT /dev/sdX1

ファイルをコピーし、すべてが無傷で届いたことを確かめます（すべて一致すれば、何も表示されません）。

sudo mount /dev/sdX1 /mnt
sudo cp -r build/rpi5b_2gb/hello/sdcard/. /mnt/
(cd /mnt && sha256sum -c SHA256SUMS | grep -v ': OK$')
sudo umount /mnt

Piに挿します。

シリアルコンソールをつなぐ

Debug Probeは、GPIOピンではなく、HDMIポートの間にあるPi 5の専用の3ピンのデバッグ用コネクタに挿します。通信速度は115200ボー、8N1です。プローブは、Macでは/dev/cu.usbmodem…として、Linuxでは/dev/ttyACM0などとして現れます（ユーザーがdialoutグループに入っている必要があります）。

Piの電源を入れる前にキャプチャを始めてください。ログひとつにつき、起動は一回です。

mkdir -p build/rpi5b_2gb/hello
(stty 115200 raw -echo; cat) < /dev/cu.usbmodemXXXX | tee build/rpi5b_2gb/hello/serial.log

この例のように、設定と読み取りはひとつのコマンドにまとめてください。macOSでは、ポートを二度目に開くと9600ボーに戻ってしまいます。Linuxでは、stty -F /dev/ttyACM0 115200 raw -echoでポートを設定し、cat /dev/ttyACM0で読み取ります。最後の期待される行が出たら、Ctrl-Cで止めます。

電源を入れると、U-Bootが3秒カウントダウンしてから、カードのloader.imgを起動します。代わりにU-Bootのプロンプトで止めるには、カウントダウン中にstopbootと入力します（止められるのはこの単語だけなので、何もつながっていないシリアル線が拾うノイズで、デバイスがU-Bootで止まってしまうことはありません）。

ログをチェックする

QEMUの出力をチェックするのと同じルールで、ボードのログをシステムの期待出力ファイルと照合します。

make check-serial SYSTEM=hello LOG=build/rpi5b_2gb/hello/serial.log

Pi専用の期待出力ファイルを持つシステムでは、BOARD=rpi5b_2gbを付けてください。

システムを無人で実行する

プローブをつないでおけば、make pi-runが、カードの差し替えも、ボードの前に人がいることもなしに、一連のシステムをボード上で実行します。これはコンテナの中ではなく、手元のマシン上で直接実行してください（Macでは、Podmanの仮想マシンからUSBシリアルデバイスが見えません）。そのマシンにはPython 3.11以降が必要で、使うのは標準ライブラリだけです。

make pi-run PI_DEVICE=/dev/cu.usbmodemXXXX PI_SYSTEMS="hello ipc-demo isolation-test"

システムごとに、コンテナの中でイメージをビルドし、ボードをリセットし、シリアル線でイメージを送って無傷で届いたことを確かめ、ボードのウォッチドッグを有効にしてから起動します。各ログは届くそばからチェックされ、ウォッチドッグが次のシステムのためにボードをリセットします。入力するコマンドはすべてエコーバックされ、確定する前にチェックされます。ログはbuild/rpi5b_2gb/pi-run/に保存されます。

ユーザーインターフェースを見る

電源を入れる前にモニターをつないだ状態で、次を実行します。

make pi-run PI_DEVICE=/dev/cu.usbmodemXXXX PI_SYSTEMS=ui-demo PI_WATCHDOG=15

これで、ユーザーインターフェースのスクリプト化されたセッションがHDMI画面上で動き、すべてのフレームのハッシュがチェックされます。人が見られるように、ウォッチドッグなしでシステムを動かしたままにするには、make pi-show PI_DEVICE=… SYSTEM=ui-demoを使います。ボードの電源を入れ直すまで動き続けます。

失敗したときは

最後に動いたイメージに戻り、シリアル線とブートチェーンをもう一度確かめてください。一度に二つ以上のことを変えるのは、その後です。U-Bootより前に何ひとつ表示されない場合は、プローブや配線を疑う前に、ブートローダーのBOOT_UART設定と、カードのconfig.txtにあるenable_uart=1を確認してください。