We currently do not have a base system for seL4. There is currently the seL4 microkernel,
and a series of "environments" which exist, and are separate bootable
applications. These bootable applications are seL4test (https://github.com/seL4/sel4test
), and then several CAmkES-based environments
such as the CAmkES sample applications loader (https://github.com/seL4/camkes
) and the
CAmkES x86 VMM application (https://github.com/seL4/camkes-vm
). All of these are separate
bootable applications which do not interlink or interoperate. In a sense they are
independent mini-OSes, though not quite.
In order to develop on seL4 right now, you will either have to construct your own new
bootable application (i.e, write your own mini-OS), or if you don't want to do that,
use one of the bootable applications above. I'd recommend using seL4test. The rest of
my advice here will be to guide you on how to use seL4test as your environment for
developing and testing your driver. If you want to write your own bootable application,
that's a much larger goal.
1. First clone seL4test by following the instructions here:
2. Try actually running sel4test to make sure that sel4test itself is working for you.
3. Now create your own test file inside of sel4test. I.e, create a new file here:
4. Use the DEFINE_TEST() macro to tell seL4test that your test exists, and that it should
5. Since you don't want to run all of the other tests and you just want to run your
test, use `make select-test TEST='YOUR_TEST_NAME_HERE'` before you build from that
At this point you should have a blank running test which does nothing. Now you can start
to develop your driver.
6. Create a new file (or files) for your driver inside of libplatsupport. To locate
libplatsupport, make sure you are in the root directory of your sel4test repository, and
then: `cd projects/util_libs/libplatsupport/src/plat`.
7. Inside of the "plat/" folder, you should see several hardware platforms
listed. You are probably trying to develop a driver for an ARM platform, since you talked
about a UART driver. Look for your target platform here. If your target platform is not
here, then you have bigger problems to solve, because that means you have to port the
entire kernel and then the userspace libraries and so on, to your platform from scratch.
8. If your target platform is listed inside "plat/" then: `cd
YOUR_PLATFORM/" and create a new file there for your driver.
9. Look at the other C source files in there for information about how our driver
framework currently works when building your driver.
Now you have a driver to begin using within your test inside of sel4test. Libplatsupport
is automatically linked to the tests, so your driver is automatically linked against your
new test. You have one remaining problem: you need to obtain the capabilities that your
driver needs to be able to operate correctly. Your UART driver probably requires at least
1 Frame cap and probably 1 IRQ cap if you plan to use IRQs.
The kernel gives all caps to all things that exist, to the root task. The seL4test
application is actually 2 tasks: the Test-Driver (hereafter "TDriver") and the
Test-Child (hereafter, "TChild"). The TDriver is the root task; so it has
already been given all caps by the kernel. You need to tell the TDriver to save the caps
that your driver needs. Then you need to tell the TDriver to pass these caps to the
Whatever scheme you use to save the caps and pass them to the TChild is up to you, but
don't hesitate to reply here and ask for more explanation. But those first steps
outlined above are probably the bulk of what needs to be explained.
Kofi Doku Atuah
DATA61 | CSIRO
From: Devel <devel-bounces(a)sel4.systems> on behalf of ashokk(a)spanidea.com
Sent: 25 September 2017 14:47
Subject: [seL4] User-space drivers
This is Ashokkumar, i want to write a sample serial(UART) communication user-space
driver in sel4,
can i get any help from your side. I am just started sel4 i don't know how to build
and execute the programs,
if you have any documents or examples about user-space programs please share with me...