On 24 May 2016, at 6:41 am, Norrathep Rattanavipanon wrote:

Hello,

I currently had codes, implemented as regular seL4, since camkes does not support some features (i.e. transferring capabilities or accessing address space outside the process),

Everything is fine up to this point but now I want to create several drivers. And I found that the best and easiest way to do that is to use camkes. So is it possible to use existing regular codes in conjunction with camkes?

In principle CAmkES component code should be seL4 independent - all the seL4 specific functionality should be done by generated glue code. So ‘porting’ regular sel4 code to CAmkES will require removing seL4 functionality that is meant to be done by the glue code. With regards to connecting regular seL4 code to CAmkES components, it can be done, and would require the seL4 component to basically implement the glue code that CAmkES would normally generate (in particular to do appropriate marshalling and unmarshalling).

Or would the best way be to implement drivers as regular seL4 codes?

The way we typically implement drivers is to write the sel4/CAmkES independent code, and place it in a library. Then to separately write a sel4 or CAmkES wrapper to use it. Look at examples of sel4/CAmkES independent driver code in: https://github.com/seL4/util_libs/tree/master/libplatsupport and seL4 wrappers in: https://github.com/seL4/seL4_libs/tree/master/libsel4platsupport Ihor. -- Dr. Ihor Kuz Senior Research Engineer | Trustworthy Systems | DATA61 | CSIRO Conjoint Senior Lecturer | CSE | UNSW E ihor.kuz@nicta.com.au T + 61 2 8306 0582 Locked Bag 6016, UNSW, Sydney NSW 1466, Australia www.data61.csiro.au CSIRO’s Digital Productivity business unit and NICTA have joined forces to create digital powerhouse Data61 ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.