Re: [seL4] CAmkES Question

Hi Chris, You may not have to do anything... We have already implemented gdb debug support for CAmkES. While it hasn’t been released into the master branch yet (we are fixing some bugs when run with a virtual machine and finishing code review) you can have a look at it (and try it out) using this manifest: https://github.com/smaccm/camkes_debug_manifest/blob/gtt_deliverable/simple.... There is some documentation about the debug support at: https://github.com/smaccm/camkes-tool/blob/gtt_deliverable_debug_no_rt/debug... The way it works in a nutshell is that there is a new feature in the CAmkES toolchain that will rewrite a CAmkES architecture to insert a gdb debug component and then do all the work to hook up the fault exception and serial connections appropriately. It also makes use of some kernel extensions to allow manipulation of debug registers, so you can set breakpoints and do single stepping. Currently it only works on x86. To answer the more general questions about how to set up new endpoints and connections in CAmkES the answer is: since CAmkES is a static system you shouldn’t. Instead you should do it within the CAmkES tool or templates statically (that’s how our debug tool does it - it generates appropriate capdl to have the endpoints and fault handlers setup at system startup time). If you really really really want to retype and manipulate caps at runtime, then you could do it like the VMM does, and get CAmkES to give a bunch of untypeds and then manipulate those as desired. Ihor.

On 2 Sep 2016, at 4:53 am, Chris Guikema wrote:

Hello Ihor,

My name is Chris Guikema, and I am an embedded systems engineer at DornerWorks, located in Grand Rapids Michigan. I am currently working on a project that requires the use of the CAmkES system, and I would like some help, if you are willing to.

The project is to allow for debugging using CAmkES. The debugging process was successfully implemented in a simple seL4 program by using the init thread to set up an exception thread and setting up the exception endpoint, which was mapped to the init thread. The init thread was then used to implement a bad assembly code, which fired an exception. The exception handler thread was waiting on something to appear at the endpoint, and then grabbed the program counter and the stack of the init thread and sent it to a GDB function, which allowed debugging. My job is to replicate the debugging using CAmkES.

However, CAmkES doesn’t seem to want the application to utilize any of the seL4 system calls, and I don’t believe the application knows its root cspace and vspace, so any attempt to initialize a debug thread and setup an exception endpoint just don’t work. What steps do I need to take to 1, set up an endpoint that I could map to the exception endpoint (the simple libraries cause a vm fault), and 2, set up a thread that waits on the application to throw an exception and allow the debugging to occur.

Any help you could send me would be appreciated. I look forward to hearing from you.

Thanks Chris Guikema