Ejecución en una Raspberry Pi 5

La Raspberry Pi 5 es la placa de referencia de NoWayOS: de bajo coste, fácil de conseguir y la placa en la que se ejecutan sus primeras pruebas en hardware. Un sistema que supera la prueba en QEMU se comprueba en la Pi con el mismo archivo de salida esperada, a partir del registro serie de la placa.

Dos reglas para la placa. Nunca conecte un adaptador serie de 5 V a la UART de la Pi: es un puerto de 3,3 V. Y nunca programe la memoria programable una sola vez (OTP) de la Pi ni active el arranque seguro en una placa de desarrollo: ambas cosas son irreversibles. make sdcard rechaza un config.txt que haga cualquiera de las dos, o que cambie el voltaje de la placa.

Qué necesita

Construya la tarjeta SD

make sdcard BOARD=rpi5b_2gb SYSTEM=hello

Esto escribe la partición de arranque de la tarjeta en build/rpi5b_2gb/hello/sdcard/: U-Boot, el árbol de dispositivos y las superposiciones, config.txt, la imagen de seL4 loader.img, los archivos de licencia y un SHA256SUMS para comprobar la tarjeta después. U-Boot se compila desde el código fuente en el contenedor, de forma reproducible.

Grabe la tarjeta

En macOS

1. Localice la tarjeta con diskutil list: es external, physical y tiene el tamaño de la tarjeta. El paso siguiente borra ese disco entero, así que compruebe el número dos veces.
2. Formatéela con la etiqueta PIBOOT:

diskutil eraseDisk FAT32 PIBOOT MBRFormat /dev/diskN

3. Copie los archivos y compruebe que todos han llegado intactos (no se imprime nada cuando todos coinciden):

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$')

4. Expúlsela con diskutil eject /dev/diskN e insértela en la Pi.

En Linux

Los mismos pasos con las herramientas de Linux (las tarjetas del propio proyecto se preparan en macOS):

1. Localice la tarjeta con lsblk -p: un disco del tamaño de la tarjeta, como /dev/sdX o /dev/mmcblk0. El paso siguiente borra ese disco entero, así que compruebe el nombre dos veces y desmonte cualquiera de sus particiones.
2. Cree en ella una sola partición FAT32 con la etiqueta PIBOOT (con dosfstools y parted instalados):

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

3. Copie los archivos y compruebe que todos han llegado intactos (no se imprime nada cuando todos coinciden):

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

4. Insértela en la Pi.

Conecte la consola serie

Conecte la Debug Probe al conector de depuración dedicado de 3 pines de la Pi 5, entre los puertos HDMI, no a los pines GPIO. Funciona a 115200 baudios, 8N1. La sonda aparece en un Mac como /dev/cu.usbmodem… y en Linux como /dev/ttyACM0 o similar (su usuario debe pertenecer al grupo dialout).

Empiece a capturar antes de encender la Pi, un arranque por registro:

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

Mantenga la configuración y la lectura en un solo comando, como aquí: en macOS, una segunda apertura del puerto vuelve a 9600 baudios. En Linux, configure el puerto con stty -F /dev/ttyACM0 115200 raw -echo y léalo con cat /dev/ttyACM0. Deténgalo con Ctrl-C después de la última línea esperada.

Al encender, U-Boot hace una cuenta atrás de tres segundos y después arranca el loader.img de la tarjeta. Para detenerse en su prompt, escriba stopboot durante la cuenta atrás. (Solo esa palabra lo detiene, así que el ruido que capta una línea serie desconectada nunca puede dejar un dispositivo parado en U-Boot).

Compruebe el registro

Compruebe el registro de la placa con el archivo de salida esperada del sistema, con las mismas reglas con las que se comprueba la salida de QEMU:

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

Añada BOARD=rpi5b_2gb para un sistema que tenga un archivo de salida esperada propio para la Pi.

Ejecute sistemas de forma desatendida

Con la sonda conectada, make pi-run ejecuta una serie de sistemas en la placa sin mover ninguna tarjeta y sin nadie delante de la placa. Ejecútelo en su propia máquina, no en el contenedor (en un Mac, la máquina virtual de Podman no ve los dispositivos serie USB). Necesita ahí Python 3.11 o posterior, solo con la biblioteca estándar:

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

Para cada sistema, compila la imagen en el contenedor, reinicia la placa, envía la imagen por la línea serie y comprueba que ha llegado intacta, arma el watchdog de la placa y la inicia. Cada registro se comprueba a medida que llega, y el watchdog reinicia la placa para el siguiente. Cada comando que escribe se devuelve como eco y se comprueba antes de introducirlo. Los registros se guardan en build/rpi5b_2gb/pi-run/.

Vea la interfaz de usuario

Con el monitor conectado antes de encender:

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

ejecuta la sesión guionizada de la interfaz de usuario en la pantalla HDMI y comprueba un hash de cada fotograma. Para dejar un sistema en marcha para que una persona lo vea, sin watchdog, use make pi-show PI_DEVICE=… SYSTEM=ui-demo; se ejecuta hasta que se apaga y se vuelve a encender la placa.

Cuando algo falla

Vuelva a la última imagen que funcionó y compruebe de nuevo la línea serie y la cadena de arranque antes de cambiar más de una cosa a la vez. Si no aparece absolutamente nada antes de U-Boot, compruebe el ajuste BOOT_UART del cargador de arranque y enable_uart=1 en el config.txt de la tarjeta antes de sospechar de la sonda o del cableado.