I got seL4 running on my Raspberry Pi 3B tonight.
Even though I worked with Dale Dougherty in the early '90s, I've been on the sidelines of the whole maker thing until September when Micro Center bundled a Google AIY VOICE KIT with Raspberry Pi 3B for $35.
After I verified that it works as a voice device, I remembered the tantalizing seL4 on the Raspberry Pi 3 item from early this year. The build dependencies were greatly simplified by the seL4 dockerfiles. Building the seL4-Test project went without a hitch:
mkdir sel4test && cd sel4test repo init --config-name -u firstname.lastname@example.org:seL4/sel4test-manifest.git repo sync make rpi3_debug_xml_defconfig && make ... [GEN_IMAGE] sel4test-driver-image-arm-bcm2837
The only way to see the seL4 test project do its thing is via the serial console. Before I overwrote the working voice kit SD card, I wanted to test connectivity. I have plenty of experience with RS-232 serial cables (I even had a job in high school where I helped a tech by putting together serial terminal cables) but RS-232 vs. TTL serial is not just a matter of wires and connectors; the voltage levels are different. USB to TTL cables usually go for around $15, which is more than half of what I paid for the Pi!
Meanwhile, this summer Micro Center had a beaglebone green wireless, which usually goes for around $50, on clearance for $20, and I couldn't pass it up. The beaglebone uses the same TTL levels and works fine as an ssh server, so I put together a cable
config-pin tinkering, I confirmed that I could get
UART1 and UART2 on the beaglebone to talk to each other (UART0
is debug outputonly), but I couldn't get any console output from the Pi to show up.
After discovering a JBtek Raspberry Pi USB to TTL Serial Cable on Amazon for $7, I ordered it and set the project aside.
That didn't work either until I connected an HDMI monitor and keyboard and
raspi-config to enable the serial console. I wonder if the beaglebone
would have worked given that fix.
With serial console hardware issues in hand, I loaded the SD card as instructed.
The first few boot stages worked, but I struggled to
Hit any key to stop autoboot.
Minicom (remember minicom?) showed "Offline" so I turned off hardware flow control.
U-Boot> fatls mmc 0 50248 bootcode.bin 2818372 start.elf 35 config.txt 393408 u-boot.bin 4064956 sel4test-driver-image-arm-bcm2837 U-Boot> fatload mmc 0 0x100000 sel4test-driver-image-arm-bcm2837 reading sel4test-driver-image-arm-bcm2837 4064956 bytes read in 328 ms (11.8 MiB/s) U-Boot> bootelf 0x100000 ... Test suite passed. 119 tests passed. 42 tests disabled. All is well in the universe