Esecuzione su Raspberry Pi 5

Il Raspberry Pi 5 è la scheda di riferimento di NoWayOS: economica, facile da trovare, e la scheda su cui girano i suoi primi test sull'hardware. Un sistema che passa in QEMU viene verificato sul Pi con lo stesso file expect, a partire dal log seriale della scheda.

Due regole per la scheda. Non collegare mai un adattatore seriale a 5 V alla UART del Pi: è una porta a 3,3 V. E non programmare mai la memoria programmabile una sola volta (OTP) del Pi né abilitare l'avvio sicuro su una scheda di sviluppo: entrambe le operazioni sono irreversibili. make sdcard rifiuta un config.txt che farebbe l'una o l'altra cosa, o che modifica la tensione della scheda.

Cosa serve

Preparare la scheda SD

make sdcard BOARD=rpi5b_2gb SYSTEM=hello

Questo comando scrive la partizione di avvio della scheda in build/rpi5b_2gb/hello/sdcard/: U-Boot, il device tree e gli overlay, config.txt, l'immagine seL4 loader.img, i file di licenza e un SHA256SUMS per verificare la scheda in seguito. U-Boot viene compilato dai sorgenti nel container, in modo riproducibile.

Scrivere la scheda

Su macOS

1. Trovare la scheda con diskutil list: è external, physical, con la dimensione della scheda. Il passaggio successivo cancella l'intero disco, quindi controllare due volte il numero.
2. Formattarla con l'etichetta PIBOOT:

diskutil eraseDisk FAT32 PIBOOT MBRFormat /dev/diskN

3. Copiare i file e verificare che siano arrivati tutti integri (il comando non stampa nulla se corrispondono tutti):

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. Espellerla con diskutil eject /dev/diskN e inserirla nel Pi.

Su Linux

Gli stessi passaggi con gli strumenti di Linux (le schede del progetto vengono preparate su macOS):

1. Trovare la scheda con lsblk -p: un disco della dimensione della scheda, come /dev/sdX o /dev/mmcblk0. Il passaggio successivo cancella l'intero disco, quindi controllare due volte il nome e smontare tutte le sue partizioni.
2. Creare una sola partizione FAT32 con l'etichetta PIBOOT (con dosfstools e parted installati):

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. Copiare i file e verificare che siano arrivati tutti integri (il comando non stampa nulla se corrispondono tutti):

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. Inserirla nel Pi.

Collegare la console seriale

Collegare il Debug Probe al connettore di debug dedicato a 3 pin del Pi 5, tra le porte HDMI, non ai pin GPIO. Funziona a 115200 baud, 8N1. Il probe compare su un Mac come /dev/cu.usbmodem…, e su Linux come /dev/ttyACM0 o simile (l'utente deve far parte del gruppo dialout).

Avviare la cattura prima di accendere il Pi, un avvio per log:

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

Tenere le impostazioni e la lettura in un unico comando, come qui: su macOS una seconda apertura della porta torna a 9600 baud. Su Linux, impostare la porta con stty -F /dev/ttyACM0 115200 raw -echo e leggerla con cat /dev/ttyACM0. Interrompere con Ctrl-C dopo l'ultima riga attesa.

All'accensione, U-Boot conta alla rovescia per tre secondi e poi avvia il loader.img della scheda. Per fermarsi invece al suo prompt, digitare stopboot durante il conto alla rovescia. (Solo quella parola lo ferma, così il rumore captato da una linea seriale scollegata non può mai bloccare un dispositivo in U-Boot.)

Verificare il log

Verificare il log della scheda rispetto al file expect del sistema, con le stesse regole con cui si verifica l'output di QEMU:

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

Aggiungere BOARD=rpi5b_2gb per un sistema che ha un file expect specifico per il Pi.

Eseguire sistemi senza presidio

Con il probe collegato, make pi-run esegue una serie di sistemi sulla scheda senza spostare la scheda SD e senza nessuno davanti alla scheda. Va eseguito direttamente sulla propria macchina, non nel container (su un Mac, la macchina virtuale di Podman non vede i dispositivi seriali USB). Lì serve Python 3.11 o successivo, solo con la libreria standard:

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

Per ogni sistema compila l'immagine nel container, resetta la scheda, invia l'immagine sulla linea seriale e verifica che sia arrivata integra, arma il watchdog della scheda e avvia l'immagine. Ogni log viene verificato man mano che arriva, e il watchdog resetta la scheda per il sistema successivo. Ogni comando che digita viene rimandato indietro in eco e verificato prima di essere confermato. I log vengono conservati in build/rpi5b_2gb/pi-run/.

Guardare l'interfaccia utente

Con il monitor collegato prima dell'accensione:

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

esegue la sessione scriptata dell'interfaccia utente sullo schermo HDMI e verifica l'hash di ogni frame. Per lasciare un sistema in esecuzione perché qualcuno lo guardi, senza watchdog, usare make pi-show PI_DEVICE=… SYSTEM=ui-demo; resta in esecuzione finché la scheda non viene spenta e riaccesa.

Quando qualcosa non va

Tornare all'ultima immagine che funzionava e ricontrollare la linea seriale e la catena di avvio, prima di cambiare più di una cosa alla volta. Se prima di U-Boot non compare assolutamente nulla, controllare l'impostazione BOOT_UART del bootloader e enable_uart=1 nel config.txt della scheda, prima di sospettare del probe o del cablaggio.