Screen Version
School of Computer Science & Engineering
University of New South Wales

 Advanced Operating Systems 
 COMP9242 2012/S2 

seL4 Debugging Guide

When developing an operating system on top of seL4 you do not have the luxury of using a debugger such as gdb. Your best bet is a combination of dprintf and objdump. If you are doing the project on a Linux machine (using our linux toolchain) you can also use the backtrace function, combined with a script for parsing objdump output to obtain a primitive stack trace.

Debugging Faults

All exceptions result in a context switch to the seL4 kernel. The kernel exports fault handling policies to user level by sending an IPC to the appropriate IPC endpoint (see Chapter 5 of the seL4 manual). For applications such as tty_test, the assigned endpoint will usually be the IPC endpoint that SOS waits on in the syscall_loop. SOS on the other hand is initialised with no fault endpoint and hence is expected to ensure that it does not cause a fault.

SOS faults

Below is an example of a page fault that is caused by SOS:

388 int main(void) {           
390     dprintf(0, "\nSOS Starting...\n");
391     *((char*)0xDEADBEEF) = 0;
SOS Starting...                                                                 
Caught cap fault in send phase at address 0x0                                   
while trying to handle:                                                         
vm fault on data at address 0xdeadbeef with status 0xf5                         
in thread 0xf0063e00 at address 0x8ae4

A capability fault occurs while sending the fault IPC to the fault handler because the capability address of SOS's fault endpoint is 0x0 (seL4_CapNull). 0x0 does not address a valid synchronous endpoint in the capability space of the faulting thread (SOS). From the provided information, we also see that SOS caused a vm fault. The fault address register (FAR) was set to 0xdeadbeef while the fault status register (FSR) was set to 0xf5 (see Section 3.6 of the ARMv5 manual). Lastly, and most importantly, we see the value of the instruction pointer at the time of the fault is 0x8ae4. objdump may then be used to determine the context of fault.

Application faults

When an application thread is created, an appropriate fault handler IPC endpoint should be set in the thread's TCB (see Chapter 5 of the seL4 manual). If the applciation causes a fault and IPC will be sent to the assigned fault endpoint. Message registers provide important imformation regarding the cause and location of the fault. objdump may then be used to determine the context of fault.

Using objdump

Whenever you cause a fault, you should be able to see the current program counter printed out. You can use objdump to find where the offending code is.

% armeb-oe-linux-gnueabi-objdump -Dlx stage/arm/nslu2/bin/sos  | less

You can now use the searching facility in less to search for the faulting address. In this case I find the following fragment of output:

    8adc:       e3a02000        mov     r2, #0
    8ae0:       e59f367c        ldr     r3, [pc, #1660] ; 9164 
    8ae4:       e5432010        strb    r2, [r3, #-16]

We can see that the error has occured on code at line 391 of main.c. If the file name and line number does not appear in your dump, run make menuconfig, select Emit debugging information in the Toolchain Options menu and recompile.

If the fault occurs in an application (such as tty_test or sosh) rather than SOS, the following command should be used:

% armeb-oe-linux-gnueabi-objdump -Dlx stage/arm/nslu2/bin/appname  | less

More on objdump

objdump is a very handy utility for working out exactly what is where in an executable so you can work out what exactly is going wrong.

The two standard incantations for objdump are:

% armeb-oe-linux-gnueabi-objdump -dl my_elf.file | less


% armeb-oe-linux-gnueabi-objdump -lx my_elf.file | less

The first command (-dl) disassesmbles the text segment and shows you all the instructions and at what address. Using this information you can find out things such as:

NB: In case it's not yet obvious, you will need to get up to speed on your ARM assembly and not be afraid to get your hands dirty if you want to minimise the time you spend debugging.

The second objdump command (-lx) is useful for when addresses appear inside an object file but outside of the text segment. This is especially useful when debugging ELF loading. The -lx option displays section and symbol information. Further options can be added to dump data segments etc. man objdump is your friend.

Generating a Stack Trace

Warning: Backtrace only works for the Linux toolchain

The backtrace() function is called by default by assert() and conditional_panic(). You can also call it from within any arbitrary place in your code. Backtrace will traverse the stack and print out the addresses of each function in the call stack (as long as you haven't done anything to the stack). This can be useful if you need to know what your code is doing.

Backtrace output looks like this:

Assertion failed: 0, function _sos_init, file /home/qiang/aos-2012/apps/sos/src/main.c, line 385.
seL4 root server aborted
Backtracing stack PCs:  0xb06c  0xbe88  0x9124  <------------------------------the back trace
Debug halt syscall from user thread 0xf0063e00

We have also provided a script to parse the objdump output and lookup the addresses in the stack trace and show the assembler and C code that they correspond to. Copy the script into the root directory of you project and execute as follows:

USEAGE:   backtrace_symbol [OPTIONS] <<EOF
OPTIONS:  -l printout line number for disassembly
          -S printout source code for disassembly
          -w WIDTH extra lines of disassembly for each side of the target PC, between 4 and 10 (default is 4)
          --start-address=0xADDR only process data whose address is <= ADDR
          --stop-address=0xADDR  only process data whose address is >= ADDR
          --h printout this message
Format:   the PCs should be started with a new line each
          PCs are hex numbers, start with "0x"

Finally, here is an example usage of the backtrace script:

./ -l -S -w 5 <<EOF
This should output something like:
    # 0  0x0000b074 in  __conditional_panic           

    b060:	e59f00b8 	ldr	r0, [pc, #184]	; b120 <__conditional_panic+0xdc>
    b064:	eb0004aa 	bl	c314 <printf>
    b068:	e58d5000 	str	r5, [sp]
    b06c:	e59f00b0 	ldr	r0, [pc, #176]	; b124 <__conditional_panic+0xe0>
    b070:	e1a01004 	mov	r1, r4
    b074:	e1a02006 	mov	r2, r6
    b078:	e59d3050 	ldr	r3, [sp, #80]	; 0x50
    b07c:	ebfffce7 	bl	a420 <plogf>
    b080:	e59f00a0 	ldr	r0, [pc, #160]	; b128 <__conditional_panic+0xe4>
    b084:	eb0004a2 	bl	c314 <printf>

    b088:	e28d0008 	add	r0, sp, #8
    # 1  0x0000b034 in  _logf                         

    b020:	e24dd00c 	sub	sp, sp, #12
    va_list alist;

    va_start(alist, msg);
    b024:	e28d1014 	add	r1, sp, #20
    b028:	e58d1004 	str	r1, [sp, #4]
    plogf(msg, alist);
    b02c:	e59d0010 	ldr	r0, [sp, #16]
    b030:	ebfffcfa 	bl	a420 <plogf>
    b034:	e28dd00c 	add	sp, sp, #12
    b038:	e49de004 	pop	{lr}		; (ldr lr, [sp], #4)
    b03c:	e28dd010 	add	sp, sp, #16
    b040:	e12fff1e 	bx	lr

0000b044 <__conditional_panic>:
#define verbose 1

inline void __conditional_panic(int condition, const char *message,
        const char *file, const char *func, int line) {
    if (condition) {
        _dprintf(0, "\033[22;31m", "PANIC %s-%s:%d %s\n\n", file, func, line, message);
    b044:	e92d45f0 	push	{r4, r5, r6, r7, r8, sl, lr}
    b048:	e24dd034 	sub	sp, sp, #52	; 0x34
    # 2  0x000091e0 in  main                          

    91cc:	e3a03f52 	mov	r3, #328	; 0x148
    91d0:	e2833003 	add	r3, r3, #3
    91d4:	e58d3000 	str	r3, [sp]
    91d8:	e1a00621 	lsr	r0, r1, #12
    91dc:	e59f1178 	ldr	r1, [pc, #376]	; 935c <main+0x768>
    91e0:	e1a02006 	mov	r2, r6
    91e4:	e1a03008 	mov	r3, r8
    91e8:	eb000795 	bl	b044 <__conditional_panic>

    /* Create an endpoint for user application IPC */
    ep_addr = ut_alloc(seL4_EndpointBits);
    91ec:	e3a00004 	mov	r0, #4
    91f0:	eb000274 	bl	9bc8 <ut_alloc>
    conditional_panic(!ep_addr, "No memory for endpoint");
    91f4:	e1a05000 	mov	r5, r0

Last modified: Wed Aug 06 11:00:11 EST 2008