seL4 userspace debugging with GDB extensions in Renode

Debugging is an integral part of the embedded systems development process especially in the context of userspace applications running inside an OS, where it can be difficult to follow the flow of the code.

OS-aware debugging capabilities, which allow developers to inspect the kernel’s inner-workings and understand what’s happening on the userspace level, are key to good developer experience in this use case.

Therefore, as part of our work for Google Research focusing on developing a complete, simulation-driven flow for secure machine learning solutions, we have been working on bringing OS-aware debugging into Renode, our open source simulation framework.

The project uses the formally verified, high-assurance seL4 OS which thus was a logical first target - and we have recently released dedicated extensions which bring seL4 OS-aware features to both Renode and GDB.

GDB support in Renode

Renode’s GDB debugging capabilities is one of the key features, enabling deterministic debugging of embedded applications in simulation. After setting up the simulated machine, a GDB remote server can be started by issuing the following command in the Renode Monitor’s prompt:

(machine-0) machine StartGdbServer 3333

This will start a GDB server on port 3333, to which we can attach GDB:

(gdb) target remote :3333

Now, assuming the symbol file is already loaded, the guest application can be debugged as usual.

One of Renode’s core features is that it’s fully deterministic, therefore all debug sessions will always follow the same code path, in the same virtual time each time a simulation is run. In GDB you will have access to all the emulated CPU’s registers, including the recently added v0-v31 registers provided by RISC-V vector extension, which were also implemented as part of our collaboration with Google.

OS versus kernel debugging

Debugging can be executed on two conceptual levels: kernel and userspace. Most RTOSes operate on the kernel level, and even if userspace applications are considered they are almost always shipped as a single binary blob linked with the kernel image. On the other hand CAmkES, seL4’s development framework, splits each component to a different binary, which are then packed into a single CPIO archive and linked against capDL-loader and kernel. Developers also explicitly specify interaction interfaces as well as connections between the components, which allows them to seamlessly communicate using IPC.

Although this approach provides separation, it also causes the debugging process to be rather difficult, as now there are multiple symbols files which potentially are using the same virtual address space. Correspondingly, loading all the object files into the debugger will cause symbol clashes and yield the problem-solving process rather frustrating. There is also no clear indication of which component is currently running, thus manually changing symbol files is also a cumbersome task. This requires a custom approach and prevents the use of standard GDB features to implement support for seL4 userspace applications.

OS-aware seL4 debugging in practice

To address this, we have developed seL4 extensions for Renode with an accompanying glue script for GDB. With it, the user is able to create thread-aware breakpoints, jump back-and-forth between userspace and kernel or switch symbol files. Additionally, the user can opt-in for automatic symbol switching when some kind of breakpoint is hit. The required setup is straightforward, and consists of only two steps:

• Enabling seL4 extensions in Renode on a CPU running the seL4 system
• Loading the Python glue script in GDB

As an example, let’s investigate one of the samples provided by the CAmkES, reversestring, which consists of two components.

First, we have to clone the repository tree using the repo tool:

$ mkdir camkes && cd camkes 
$ repo init https://github.com/seL4/camkes-manifest -b 4d7db975d4725a1c6941f9a2dfa26f7fc7ad31be
$ repo sync -j$(nproc) 

Then, to build the sample we have to prepare the project and run the ninja build system. For our purposes we will use ARM Cortex-A9 zynq-7000, for which we have a ready-to-use platform in Renode.

$ mkdir build && cd build
$ ../init-build.sh -DPLATFORM=zynq7000 -DCAMKES_APP=reversestring -DKernelDebugBuild=1
$ ninja

The compiled binary can now be found in the images directory.

At this point, we can run the sample in Renode and start the debugging session. If you are using a Linux-based operating system, you can use renode-run to bootstrap and run Renode in your environment. Alternatively, use our nightly builds or simply build Renode from sources.

(monitor) mach add "zynq7000" 
(monitor) machine LoadPlatformDescription @platforms/cpus/zynq-7000.repl
(monitor) sysbus LoadELF @<path/to/images/capdl-loader-image-arm-zynq7000>
(monitor) sysbus LoadSymbolsFrom @<path/to/kernel/kernel.elf>
(monitor) showAnalyzer sysbus.uart1 
(monitor) include @tools/sel4_extensions/seL4Extensions.cs 
(monitor) sysbus.cpu CreateSeL4
(monitor) machine StartGdbServer 3333 

Before running GDB we have to indicate where the source files and the build artifacts are stored. This can be done by exporting the SOURCE_DIR and BUILD_DIR environment variables:

$ export SOURCE_DIR=$(pwd)
$ export BUILD_DIR=$(pwd)/build

Then we can run GDB and connect to Renode’s GDB stub:

(gdb) target remote :3333
(gdb) source <renode/tools/sel4_extensions/gdbscript.py>
(gdb) monitor start

The simple application we are about to run consists of two threads, client and server, in a scenario where the client asks the server to reverse a string. First, let’s investigate client’s control flow:

(gdb) sel4 wait-for-thread client_client_0_control_tcb

Now client_client_0_control_tcb should show up in autocompletion for sel4 break and sel4 tbreak. Let’s create a breakpoint on the client component control thread’s entrypoint. Note that we have to switch to the client component symbols before we are able to plant a breakpoint on the run function.

(gdb) sel4 switch-symbols client
(gdb) sel4 tbreak client_client_0_control_tcb run
(gdb) continue

We now would like to skip to the part where the client has already written a string it wants to be reversed. Therefore, we can create a breakpoint on the line of code that is interesting for us:

(gdb) sel4 tbreak client_client_0_control_tcb client.c:28
(gdb) continue

Now when we break on next context switch to the server thread, we should land in the part where it received data from the client.

(gdb) sel4 tbreak server_server_0_control_tcb
(gdb) continue
[...]
(gdb) frame
#0 run () at /storage/camkes/projects/camkes/apps/reversestring/src/server.c:17
17     while (buffer_str[REVERSE_STRING_END_IDX] == 0) {
(gdb) tbreak server.c:24
(gdb) continue
(gdb) p buffer_str
$1 = 0x155000 "Hello, World!"

Note that as we switched to the server’s control thread context, the current symbol file has been updated automatically. We can now either step through the server code, or wait until we come back again to the client context.

Zephyr and beyond

seL4 is just the beginning, as it’s only a part of our wider effort to bring OS-aware debugging to Renode. We are currently working on the OpenOCD-style support for Zephyr, to allow RTOS-aware debugging for Zephyr applications in Renode, and we have plans to expand this support further to other OSes and CPU architectures.

If you are interested in bringing platform or OS-aware functionalities for your application, don’t hesitate to contact us at contact@antmicro.com.