The method for debugging seL4 threads with Renode is relatively simple, and involves the usual suspects of m simulate-debug and kgdb.sh, but the interface through GDB has changed slightly. In general, a debugging session now looks like the following:
On one terminal, start an instance of Renode:
source build/setup.sh m simulate-debug
Once Renode has started and starts outputting green debug logs, in another terminal start up GDB with:
kgdb.sh
At this point, GDB should connect to the running Renode instance started by simulate-debug, and you'll see something equivalent to the following (output is not exact -- symbol reading may differ):
ghost:~/$ kgdb.sh
Source directories searched: /usr/local/google/home/jtgans/shodan/sw/tock:$cdir:$cwd
Reading symbols from out/shodan_boot_rom/build-out/multihart_boot_rom/multihart_boot_rom_sim_verilator.elf...
add symbol table from file "out/shodan_boot_rom/build-out/multihart_boot_rom/multihart_boot_rom_sim_verilator.elf"
Reading symbols from out/shodan_boot_rom/build-out/multihart_boot_rom/multihart_boot_rom_sim_verilator.elf...
add symbol table from file "out/matcha/riscv32imc-unknown-none-elf/debug/matcha_platform"
Reading symbols from out/matcha/riscv32imc-unknown-none-elf/debug/matcha_platform...
add symbol table from file "out/matcha/riscv32imc-unknown-none-elf/debug/matcha_app"
Reading symbols from out/matcha/riscv32imc-unknown-none-elf/debug/matcha_app...
Remote debugging using localhost:3333
warning: multi-threaded target stopped without sending a thread-id, using first non-exited thread
0x20007b4a in tock_cells::map_cell::MapCell<kernel::callback::AppId>::is_some<kernel::callback::AppId> (self=0x10005af4 <matcha_platform::reset_handler::BUF>)
at /usr/local/google/home/jtgans/shodan/sw/tock/libraries/tock-cells/src/map_cell.rs:47
47 self.occupied.get()
(gdb)
At this point, GDB has stopped the simulator, giving you a chance to set breakpoints and examine the system.
kgdb.sh will automatically load symbols on the seL4 side, based upon their thread names, so there is no need to manually find the associated symbol file and load it with the correct offsets. It may be necessary to switch symbol tables, which can easily be done using sel4 switch-symbols <threadname>, which will automatically load them with the appropriate offsets.
In this environment, there are two sets of breakpoints that can be used: standard gdb break-style breakpoints, and renode-side sel4 break breakpoints. The former work within the currently executing thread and can be used for “local” breaks inside of a thread, whereas the latter can be set in any thread that was previously discovered by the Renode extension.
Once you‘ve setup your breakpoints using sel4 break, you’ll need to tell Renode to enable breakpoints as well with sel4 breakpoints-enabled True, and then continue. For example, consider this debugging session:
<assuming cpu1 is halted and gdb is waiting at a prompt> (gdb) # Wait until 'rootserver' thread is set up in seL4 (gdb) sel4 wait-for-thread rootserver (gdb) # rootserver thread is now the symbol "main" in the thread/program, so we (gdb) # can break on stopped and associated symbols are loaded. (gdb) sel4 break rootserver main (gdb) # Enable extension breakpoints (it's disabled by default as it's pretty (gdb) # performance-heavy as Renode has to break on every context-switch) (gdb) sel4 breakpoints-enabled True (gdb) c (gdb) # We are in capdl-loader main() function, disable extension breakpoints (gdb) sel4 breakpoints-enabled False (gdb) # As we are in capdl-loader thread and proper symbols are loaded, all commands (gdb) # like break are working correctly (gdb) b init_system (gdb) c
The kgdb.sh / Renode symbol lookup mechanism is composed of two parts: a custom Renode extension in sim/config/shodan_infrastructure/seL4Extensions.cs and a custom GDB extension in sim/config/gdbscript.py. kgdb.sh is a simple bash script that starts GDB and connects to the appropriate remote with the extension loaded.
The Renode extension tracks the VSpace setup for each thread and translates virtual addresses to physical addresses. Without this work symbols may be incorrectly resolved because every VSpace memory range starts at 0.
In addition, the extension provides commands to Renode to add debugging hooks to an execution, all prefixed with the subcommand seL4 (case matters at the Renode prompt!). In our simulation config, Renode is configured to start the seL4 extension on cpu1 using the cpu1 CreateseL4 command.
The GDB extension provides a matching set of wrappers via the sel4 command prefix to examine the simulator state and take a look at threads in the system.
Both extensions provide built in help at their respective command lines, but suffice it to say, the GDB extension is essentially just an automation mechanism to load in symbols for the current thread context from disk when the Renode extension detects a context switch.
During debugging, not all symbols will be loaded in GDB at the start, so it can be helpful to use sel4 wait-for-thread <threadname> to tell Renode to break execution upon entry of the given thread. When the break occurs, Renode will instruct GDB to load the correct symbol table, and then symbols can be resolved for later breakpoints, etc.
To set a breakpoint for a thread that is not the current context, use the sel4 break <threadname> <symbol> command. This will instruct Renode to load the appropriate symbol table and break at the right place once that thread is running. If, however, you need to set a breakpoint in the current thread context, it's fine to use break as normal, since the symbols for the current thread should be loaded.