Life in the Armoury
Thursday 3:40 p.m.–4:25 p.m.
Target audience: Developer
Our group does seL4, eChronos and Linux kernel development across many different embedded platforms, including various ARM, aarch64, PPC, and Intel. Even though the core of the released seL4 kernel is formally verified, the experimental versions are not, and need to be tested on all these platforms. In addition only one of the platforms corresponds to the verified kernel. We have a very limited budget, so often have only one of a platform. This talk explains how we do continuous integration and continued development without going mad, We have developed custom hardware (the switcheroo) that is essentially an arduino-controlled multi-output high current power supply, use commercial-off-the-shelf telnet to serial gadgets, use a Cubietruck running Debian to boot some things via fastboot, but everything we can we boot via TFTP. Clever python scripts talk to everything as glue. Interesting problems include hard-wired fastboot identifiers (what do you do when three of your development boards identify as 123456789abcdef as a fastboot ID?), multiplexing between different users (the obvious solutions have problems, and we still don't have a good way to do this), and the need for custom u-boot that means that sometimes the things we test don't match what's available to the average punter.
Peter has been a Unix and then a Linux hacker since the '80s; he has never used a Windows computer except under protest. Hobbies include music, fine wines and keeping tropical fish; these occasionally lead to neat techo projects.