Hey Ashokkumar,

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​
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 protected]> on behalf of [email protected] 
<[email protected]>
Sent: 25 September 2017 14:47
To: [email protected]
Subject: [seL4] User-space drivers

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...

Regards
Ashok
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to