Hi all,

I tried to run seL4 test suite on my ARM Cortex-A7 target board.

There is no error message when boot up seL4 kernel and boot strap test program on seL4 user land.

But I got a “data abort” message after call sel4utils_map_page(..vaddr) and do memset(vaddr, 0, PAGE_SIZE_4K);

There are some debug information list below.

<1> I add debug message before the program that happen data abort

diff --git a/libsel4utils/src/vspace/bootstrap.c b/libsel4utils/src/vspace/bootstrap.c

index c366a35..70d378a 100644

--- a/libsel4utils/src/vspace/bootstrap.c

+++ b/libsel4utils/src/vspace/bootstrap.c

@@ -107,13 +107,13 @@ static void *alloc_and_map(vspace_t *vspace, size_t size) {

             error = sel4utils_map_page(data->vka, data->vspace_root, frame.cptr, vaddr,

                                        seL4_AllRights, 1, objects, &num);

+               LOG_ERROR("my-hacker\n");

             if (error) {

                 vka_free_object(data->vka, &frame);

                 LOG_ERROR("Failed to map bootstrap frame at %p, error: %d", vaddr, error);

                 return NULL;

             }

+               LOG_ERROR("my-hacker alloc_and_map() before memset vaddr=0x%x\n",vaddr);

             /* Zero the memory */

             memset(vaddr, 0, PAGE_SIZE_4K);

<2>Printed messages:

ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p5

  paddr=[20000000..2051881f]

ELF-loading image 'kernel'

  paddr=[22000000..22032fff]

  vaddr=[e0000000..e0032fff]

  virt_entry=e0000000

ELF-loading image 'sel4test-driver'

  paddr=[22033000..22463fff]

  vaddr=[8000..438fff]

  virt_entry=15f50

Enabling MMU and paging

Jumping to kernel-image entry point...

Bootstrapping kernel

Booting all finished, dropped to user space

Warning: using printf before serial is set up. This only works as your

printf is backed by seL4_Debug_PutChar()

alloc_and_map@bootstrap.c:111 my-hacker

alloc_and_map@bootstrap.c:119 my-hacker alloc_and_map() before memset() vaddr=0xdf7fe000

<3>When happen data abort, the value of CPU registers:

r1:0

r3:0xdf7fe000

lr:0xcbe8

<4>Objdump sel4test-driver.

0000cbc8 <memset>:

    cbc8:       e3520000        cmp     r2, #0

    cbcc:       e92d4030        push    {r4, r5, lr}

    cbd0:       08bd8030        popeq   {r4, r5, pc}

    cbd4:       e0803002        add     r3, r0, r2

    cbd8:       e6ef1071        uxtb    r1, r1

    cbdc:       e3520002        cmp     r2, #2

 cbe0:       e5431001        strb    r1, [r3, #-1]

    cbe4:       e5c01000        strb    r1, [r0]

    cbe8:       98bd8030        popls   {r4, r5, pc}

    cbec:       e3520006        cmp     r2, #6

It seems to write virtual address 0xdf7ff000.

<5>The virtual address 0xdf7fe000 is not map in page table

It seems sel4utils_map_page() not create page table for user land program correctly.

Can anyone help me, how to solve this problem? Thanks!

Joyce Peng(彭美僑)