I've put up reasonably detailed instructions on how to build and run
seL4test on the Sabre Lite, BeagleBoard, Odroid XU and IFC6410.
I'm still working on instructions for the Arndale.
Dr Peter Chubb peter.chubb AT nicta.com.au
http://www.ssrg.nicta.com.au Software Systems Research Group/NICTA
These seem to be missing from the system documentation, especially on
how to use it with qemu. I've built the simulator, but am unsure how
to use it. The build generates a libHSSEL4-0.3.a, but I can't find an
Also, the simulator manual says it is out-of-date, but the manual
seems to include the Haskell literate sources directly. It also says
the Haskell code is kept up-to-date. That sounds a bit contradictory.
Are the comments in the sources that obsolete?
[Congratulations on the open-sourcing and excellent license choices!]
I am trying to create a test for beaglebone using the seL4test suite but I
am having the following error:
seL4Test/libs/libplatsupport/src/plat/am335x/dm.c:56:25: error: ‘timer’
undeclared (first use in this function)
dm_t *dm = (dm_t *) timer->data;
I just did "make menuconfig" and change:
Architecture Type (ARM) --->
ARM CPU selection (Cortex A8) --->
Platform Type (AM335X (BeagleBone)) --->
Save the configuration and "make".
Here is my experience building and running seL4 on the
BeagleBoard (original, redboard, revision D). I'm hoping
the notes will be helpful for others who arent very experience
with this platform, like myself.
Start with a BeagleBoard, a 5volt power supply (or the USB
cable for power), a SDCard and an RS232 serial connector.
Note: the BeagleBoard uses RS232 serial levels, not TTL
levels, so you'll need some kind of RS232 connector. I used
a USB<->RS232 (9-pin D-connector) cable. The beagle board
has serial on header P9, which is a 2x5 header.
P9 pin 2 (RX) <--> D-connector pin 3 (TX)
P9 pin 3 (TX) <--> D-connector pin 2 (RX)
P9 pin 5 (GND) <--> D-connector pin 5 (GND)
I use "screen" or "cu" from linux to connect to the serial line with
one of the following commands (note: I'm in linux and my
account has permissions on /dev/ttyUSB0):
$ cu -l /dev/ttyUSB0 -s 115200
$ screen /dev/ttyUSB0 115200
Verify that when you power on the device (no SDCard necessary
yet) you get the u-boot bootloader in your terminal.
Next get and build your seL4 image for the beagleboard. I'm
running the sel4 test project in a debug build. You'll need to have
the proper prerequisites, as covered in the sel4 build notes.
$ mkdir sel4/beagle
$ cd sel4/beagle
$ repo init -u https://github.com/seL4/sel4test-manifest.git
$ repo sync
$ make beagle_debug_xml_defconfig
$ make menuconfig
# at this point I adjusted the tools prefix to
# "arm-none-eabi-" to match the arm toolchain I have
At this point you've got an ELF image in the images dir. It has one
section at 0x82000000 starting at offset 0x8000 in the file, and the
start address is 0x82000000. Mount an SDCard with a FAT filesystem
and nothing else on it and copy the image to your sdcard
$ cp images/sel4test-driver-image-arm-omap3 /media/SDCARD/
$ umount /media/SDCARD
now power off the beagle board, move the SDCard to the beagleboard,
power it on and interrupt the u-boot sequence to get a boot loader
prompt. Enter the following commands to boot the image. They will
load the file so that offset 0x8000 is at 0x82000000 (by loading
the entire file 0x8000 bytes before 0x82000000). Then it will jump
to the entry point and run the sel4 loader, kernel and tests.
mmc rescan 0
fatload mmc 0 0x81ff8000 sel4test-driver-image-arm-omap3
At this point sel4 is up and running and the test program is
running through its tests!
The full output of the tests can be seen at
There are some errors printed during the test, but happily the
test ends with:
136/136 tests passed.
All is well in the universe.
I would like to thank the development teams and sponsoring institutions for
releasing this amazing work into the public domain. It may be some time
before the importance of this is fully understood by the software industry,
but I believe we finally have a reference platform for how software is to
be correctly engineered. You have raised the bar for all of us.
I would also like to share with you a POSIX C implementation of a
non-deterministic Digital Random Bit Generator for your evaluation.
It can be downloaded from http://www.tag.md/public/
This patch targets the core "seL4" repo.
I idly submitted a PR on github before reading anything at all really
(beyond checking to see if the issue was made more consistent in
subsequent commits). Apologies if this is/was inconvenient.
I saw some prior github discussion on whether "python2" or "python" is
best'; IMHO, "python" is best as virtualenv allows the desired binary to
be specified at env creation time.
CLA forthcoming, I'm quite a long way from printers/scanners and all
those sorts of things.
I am trying to boot seL4 on beaglebone white. I have an initial code just
to configure the DDR2 memory at range 0x80000000-0xbfffffff.
As we can see below, the start address is the virtual address 0xf0000000
but at this point I have no MMU configured. I was thinking that the segment
.boot should be the code to prepare all details about MMU/D-CACHE/I-CACHE
but it's not what gdb is understanding based in the elf header.
Someone could explain to me how is the kernel boot; what do I have to
consider. I guess that beaglebone is not supported but this is exactly my
goal, to make seL4 boot on beaglebone.
Any help or suggestion is very welcome.
(gdb) load kernel.elf
> Loading section .boot, size 0x10000 lma 0x80000000
> Loading section .text, size 0xf1ec lma 0x80010000
> Loading section .text.unlikely, size 0xd98 lma 0x8001f1ec
> Loading section .rodata, size 0x4170 lma 0x8001ff84
> Loading section .data, size 0x8 lma 0x800240f4
> Start address 0xf0000000, load size 147708
> Transfer rate: 319 KB/sec, 3787 bytes/write.
(gdb) monitor poll
background polling: on
TAP: am335x.dap (enabled)
target state: halted
target halted in ARM state due to debug-request, current mode: System
cpsr: 0x6000019f pc: 0xf0000000
MMU: disabled, D-Cache: disabled, I-Cache: disabled
A question I had about how the sel4 project is run internally:
What is your process of developing ongoing
changes and how does verification fit into it?
Do you maintain the proofs with kernel modifications
on an ongoing basis? On a semi-regular basis?
Is the "experimental" branch verified?
When time slices are no longer global, will those changes