Does it work if you try using hardware breakpoints? The camkes-vm-linux tutorial uses hardware virtualisation via kvm so the software breakpoints likely won't work.  Replacing break with hbreak may fix your issue.

From: Devel <> on behalf of Jiusheng Liu <>
Sent: Wednesday, 27 November 2019 1:51 PM
To: <>
Subject: [seL4] Userspace debugging with QEMU/gdb

>From the page (section Userspace debugging), I know we can debug userspace process by command below:

---------------------------- cmd example start ----------------------------------------
gdb ./dynamic-2
Reading symbols from ./dynamic-2...done.
(gdb) target remote :1234
Remote debugging using :1234
0x000000000000fff0 in ?? ()
(gdb) break main
Breakpoint 1 at 0x402011: file sel4-tutorials-manifest/dynamic-2/main.c, line 161.
(gdb) c

Breakpoint 1, main () at sel4-tutorials-manifest/dynamic-2/main.c:161
---------------------------- cmd example end  ---------------------------------------- 

It works for normal userspace process (such as the example code in tutorials: ). 

But when I want to debug the userspace process for the code in the tutorials page (one virtual machine in seL4), I cannot catch the breakpoints.

So can you help me to explain why I cannot catch the breakpoint? and can we debug the vmm create process with qemu/gdb?