The method for debugging seL4 threads with Renode is relatively simple, and involves the usual suspects of m debug-simulation (or 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 debug-simulation
[Note m debug-simulation gives GDB control before anything runs while m simulate-debug lets Renode run until kgdb.sh is invoked and contacts GDB. The former is necessary to debug issues in the boot process (bootstrap, kernel, rootserver).]
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 debug-simulation, 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/sleffler/shodan/sw/tock:$cdir:$cwd Reading symbols from out/shodan_boot_rom/multihart_boot_rom/multihart_boot_rom.elf... add symbol table from file "out/shodan_boot_rom/multihart_boot_rom/multihart_boot_rom.elf" Reading symbols from out/shodan_boot_rom/multihart_boot_rom/multihart_boot_rom.elf... Remote debugging using localhost:3333 warning: multi-threaded target stopped without sending a thread-id, using first non-exited thread _reset_start () at /usr/local/google/home/sleffler/shodan/sw/multihart_boot_rom/multihart_boot_rom/rom_crt.S:29 29 li x7, 0x0 Symbol autoswitching is now disabled (gdb)
At this point, GDB has stopped the simulator, giving you a chance to set breakpoints and examine the system.
kgdb.sh will load symbols on the seL4 side, based on their thread / CAmkES component, 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 <component>, which will automatically load the symbols for CAmkES <component> with the appropriate offsets (a <component> is the lower-case version of the CAmkES name, e.g. the CAmkES component DebugConsole translates to debug_console.)
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 a breakpoint is setup using sel4 break one can just continue. For example, consider this debugging session:
<assuming cpu1 is halted and GDB is waiting at a prompt>
(gdb) sel4 wait-for-thread rootserver
Thread 2 "matcha.cpu1" received signal SIGTRAP, Trace/breakpoint trap.
[Switching to Thread 2]
0xff814802 in ?? ()
(gdb) # Switch to the 'rootserver' thread's symbol table and set a breakpoint on main
(gdb) sel4 switch-symbols rootserver
Reading symbols from out/kata/riscv32-unknown-elf/debug/capdl-loader...
(gdb) sel4 break rootserver main
(gdb) c
Continuing.
Thread 2 "matcha.cpu1" received signal SIGTRAP, Trace/breakpoint trap.
kata_os_rootserver::main () at src/main.rs:164
164 pub fn main() {
(gdb)
(gdb) # As we are in capdl-loader thread and proper symbols are loaded, all commands
(gdb) # like break work as expected.
(gdb) b init_system
Breakpoint 1 at 0x4c632: file /usr/local/google/home/sleffler/shodan/kata/projects/kata/apps/system/components/kata-os-common/src/model/mod.rs, line 200.
(gdb) c
Continuing.
Thread 2 "matcha.cpu1" hit Breakpoint 1, model::KataOsModel::init_system (self=0x8e3cc8)
at /usr/local/google/home/sleffler/shodan/kata/projects/kata/apps/system/components/kata-os-common/src/model/mod.rs:200
200 self.init_copy_region();
Note that symbol tables are per-component but breakpoints are per-thread. The seL4 GDB extentions assume all threads in a component share the same VSpace and hence the same symbol table. Beware also that when symbol names are ambiguous you can specify fully-qualified names; e.g. above main was expanded to kata_os_rootserver::main and init_system to model::KataOsModel::init_system. Several well-known special symbols are supported: kernel for the seL4 Kernel, user for any thread running in user space, and rootserver for the first seL4 thread that runs after boot.
In addition to regular GDB breakpoints the sel4 extentions support temporary breakpoints. The syntax is sel4 tbreak <threadname> [<symbol>]. If <symbol> is not specified GDB will stop on the next entry to <threadname>. This is especially useful for stopping the next time you enter user space:
(gdb) sel4 thread kernel (gdb) sel4 tbreak user (gdb) c Continuing. Thread 2 "matcha.cpu1" received signal SIGTRAP, Trace/breakpoint trap. [Switching to Thread 2] 0xff80311c in ?? ()
or the kernel:
(gdb) sel4 tbreak kernel (gdb) sel4 list-breakpoints -------------------------- |Thread|Address|Temporary| -------------------------- |kernel|any |True | -------------------------- (gdb) c Continuing. Thread 2 "matcha.cpu1" received signal SIGTRAP, Trace/breakpoint trap. 0xff803000 in ?? () (gdb)
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/renode/tools/sel4_extensions/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 will be (almost always) 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, most symbols will not 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 a break occurs the appropriate symbols may be loaded with the sel4 switch-symbols <threadname> command or, if sel4 symbol-autoswitching true is set then Renode will automatically switch symbol tables based on the current thread. Symbol-autoswitching is disabled by default because there GDB does not have a reliable way to synchronize the cmdline with the runtime so repeatedly switching between threads can leave GDB in a bad state where it will crash on an assert.
To set a breakpoint for a thread that is not the current context, the thread needs to be entered at least once. After that symbols in that thread can be resolved so the sel4 break <threadname> <symbol> command works. Beware that if <symbol> is wrong (e.g. mis-typed) the error diagnostic will go to the Renode console, not to the GDB cmdline. Note also that using regular GDB breakpoints will generate complaints about not being able to set the breakpoints when switching to a different thread. Best to use sel4 break in seL4 user threads and limit GDB break to contexts like the kernel or boot rom.
See Renode GDB seL4 extensions for more detail.
The Renode extensions identify seL4 threads by intercepting seL4_DebugNameThread system calls that assign a thread an ASCII string. Typically this happens when the thread first starts up but it can also happen otherwise; e.g. when the rootserver constructs a thread it may assign a name. This means that a command like sel4 wait-for-thread <threadname> may stop GDB in an unexpected context (e.g. the rootserver).
In order for the Renode extension to intercept seL4_DebugNameThread system calls it must know the system call ID. Because seL4 does not have a fixed ABI this number may change depending on how the system is built and/or if the system source is modified. To deal with this the system call ID is specified as an argument to the CreateSeL4 Renode directive; e.g. monitor cpu1 CreateSeL4 0xffffffee. If you notice seL4 threads are not identified and simulations slow to a crawl then check the setting--when there is a msimatch Renode will be single-stepping execution waiting for threads to be entered for the first time (the sel4 ready command may also be helpful in diagnosing this behaviour).