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), seL4bench (https://github.com/seL4/sel4bench), 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.
2. Try actually running sel4test to make sure that sel4test itself is working for you.
4. Use the DEFINE_TEST() macro to tell seL4test that your test exists, and that it should execute it.
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 point onward.
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 TChild.
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
Kernel engineer
DATA61 | CSIRO