This document describes the structure and use of the CAmkES debug tool, which allows you to debug systems built on the CAmkES platform. The Usage section describes how to debug a component built on CAmkES, as well as the current limitations of the tool. The Implementation section describes the internal implementation of the tool. This document assumes some familiary with CAmkES and the seL4 microkernel. If you are not familiar with them then you should read their documentation first.
A working example app, debug-simple, can be found in the camkes sample apps project.
This debug tool will provide an interface for you to debug components within CAmkES. Currently, the debug tool is only compatible with ia32.
Configuring a component for remote debugging the following is required:
#include <camkes/gdb/adl.h> which imports the DEBUG CPP macros used to easily modify existing components.DEBUG_COMPONENT() to the definition of your component. This creates connectors that the gdb server uses to modify the components state.DEBUG_COMPOSITION(client, 3, "0x2f8:0x2ff") under your assembly section. This adds additional assembly information that creates the debug server and connects it to the serial hardware and your component to debug. 3 is the interrupt number of the serial port and “0x2f8:0x2ff” refers to the hardware IOPort addresses. If you are debugging on hardware with a single serial port, you will need to stop your application and the kernel from using it for output.import <std_connector.camkes>; #include <camkes/gdb/adl.h> import "Simple.idl4"; component Client { control; uses Simple a; /* This adds the required connector interfaces for the debug server to use */ DEBUG_COMPONENT() } component Echo { provides Simple b; } assembly { composition { component Echo echo; component Client client; connection seL4RPCCall simple(from client.a, to echo.b); } } /* This adds the assembly and configuration parts for the debug server to connect to `client` and specifies the serial port settings. */ DEBUG_COMPOSITION(client, 3, "0x2f8:0x2ff")
After you have built the image, you should be able to connect to the serial port via GDB. The GDB connection will only be opened once there is a fault or breakpoint, so if you want to inspect on startup you should set a code breakpoint within the component you are debugging. This is achieved by using camkes_software_breakpoint(); provided by #include <camkes/debug.h>
Current functionality includes:
It's possible to debug a system running in qemu. To do this, one must forward the output of the second serial port to the tcp port gdb is connected to (1234 by default). We provide a script that runs the current image in the “images” directory on qemu, forwarding the first serial port to the terminal where the script is running, and the second serial port to 127.0.0.1:1234.
To debug with the script, run tools/camkes/debug/debug_qeum in one terminal, and run gdb in a second terminal, running both commands from the top level of this project.
qemu-system-i386 -nographic -m 512 -cpu Haswell \ -kernel kernel-ia32-pc99 \ -initrd capdl-loader-experimental-image-ia32-pc99 \ -device isa-serial,chardev=ch0 \ -device isa-serial,chardev=ch1 \ -chardev file,path=/dev/tty,id=ch0 \ -chardev socket,host=127.0.0.1,port=1234,id=ch1,server,wait
The information below assumes you are familiar with the functionality of CAmkES.
To enable debugging, a debug server component is created that can communicate with a remote GDB client over serial using the GDB remote serial protocol. Currently it communicates over serial by having exclusive access to the serial device. Once a client attaches, the server interprets GDB commands from the client and provides responses. To achieve this the GDB server component is connected to the debug target component using a seL4GDB rpc connection. This connection allows the server to read and write memory and registers, as well as set hardware breakpoints and watchpoints. Additionally the target thread's fault handler endpoints are all set to an endpoint that the GDB server waits on. When the target first faults, this results in seL4 sending a fault message to the GDB server, that then decodes this message and sends the relevant serial packet to the remote GDB client. The remote GDB client can then interract with the debug target.
include/builtin/gdb-delegate.camkes - This defines the CAmkES ADL required to create the GDB components and connections.
libsel4camkes/include/camkes/gdb/idl.h - Contains the CPP macros for more easily modifying a CAmkES project for debugging.
camkes/templates/component.debug.c - Debug target implementation of the RPC interface for reading and writing, registers and memory.
camkes/templates/seL4GDB-from.template.c - Template for the fault ep on the component side. This should just be generating a cap, since it is set manually later. camkes/templates/seL4GDB-to.template.c - Template code for the GDB server fault handler. This decodes the fault type and uses the gdb server library code for handling.
libsel4camkes/src/gdb_server/[gdb.c|serial.c] - GDB server and serial implementation can be found here. libsel4camkes/include/camkes/gdb/[gdb.h|serial.h|delegate_types.h] - Header files for GDB server and serial interfaces.
camkes/templates/[seL4GDBMem-to.template.c|seL4GDBMem-from.template.c] - Template code for a fault handler to check if memory is readable or writeable on the debug target.