Hi guys, 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... RegardsAshok
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.
1. First clone seL4test by following the instructions here: https://wiki.sel4.systems/Testing 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: https://github.com/seL4/sel4test/tree/master/apps/sel4test-tests/src/tests%E... 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
________________________________ From: Devel email@example.com on behalf of firstname.lastname@example.org email@example.com Sent: 25 September 2017 14:47 To: firstname.lastname@example.org 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...