[seL4] sel4test data abort when boot strap test program

Joyce Peng(彭美僑) joyce.peng at mstarsemi.com
Wed May 10 16:13:17 AEST 2017


Hi Hesham,

The board is one of our company's product. 
We want to evaluate capability and performance of seL4 for future product.
So we do some modification of seL4 to let it can run on our board.
Now this board has single ARM Cotex-A7 and 512 MB RAM.

First, we try software sel4test that repo from https://github.com/seL4/sel4test-manifest.git.

And we use QEMU to simulate Zynq-7000 (Xilinx ZC706, ARMv7a, Cortex A9) as golden.
$ make zynq_simulation_debug_xml_defconfig
$ make
$ qemu-system-arm -machine xilinx-zynq-a9 -nographic -m 512 -serial null -serial mon:stdio -kernel images/ sel4test-driver-image-arm-zynq7000  > simulate-zynq7000-golden

So we porting our board from Zynq-7000 and do some relative modification in software sel4test.
And we can build it directly. 

For example, the modification of loader address for our board
--- a/sel4test/projects/elfloader-tool/gen_boot_image.sh
+++ b/sel4test/projects/elfloader-tool/gen_boot_image.sh
@@ -49,6 +49,10 @@ case "$PLAT" in
         ENTRY_ADDR=0x10000000;
         FORMAT=elf32-littlearm
         ;;
+     "our_platform")
+        ENTRY_ADDR=0x20000000;
+        FORMAT=elf32-littlearm
+        ;;
     "apq8064")
         ENTRY_ADDR=0x82008000;
         FORMAT=elf32-littlearm

For example, the Kconfig of kernel
--- a/sel4test/kernel/Kconfig
+++ b/sel4test/kernel/Kconfig
@@ -229,6 +229,15 @@ menu "seL4 System"
             help
                 Support for Xilinx Zynq-7000 platforms.

+        config PLAT_OUR_PLATFORM
+            bool " OUR_PLATFOR (ARMv7a, Cortex A7)"
+            depends on ARCH_AARCH32
+            select ARM_CORTEX_A7
+            select ARCH_ARM_V7A
+            help
+                Support for our platforms.
+
+ 

Beside, we found sel4utils_map_page() calls seL4_ARM_Page_Map() and seL4_ARM_Page_Map() then uses IPC to do page tabe mapping.
We want to know the call flow of the VSpace page mapping. By tracing the detail of VSpace page mapping to see if there's any missing when porting to our platform.


Thanks,
Joyce Peng

-----Original Message-----
From: Hesham.Almatary at data61.csiro.au [mailto:Hesham.Almatary at data61.csiro.au] 
Sent: Wednesday, May 10, 2017 9:32 AM
To: Joyce Peng(彭美僑); devel at sel4.systems
Subject: Re: [seL4] sel4test data abort when boot strap test program

Hi Joyce,


On 09/05/17 17:15, Joyce Peng(彭美僑) wrote:
>
> Hi all,
>
> I tried to run seL4 test suite on my ARM Cortex-A7 target board.
>
What is the name of the board you have? How do you build and run sel4test?
>
> 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 at bootstrap.c:111 my-hacker
>
> alloc_and_map at 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 anyonehelp me, how to solve this problem? Thanks!
>
> Joyce Peng(彭美僑)
>
>
>
> _______________________________________________
> Devel mailing list
> Devel at sel4.systems
> https://sel4.systems/lists/listinfo/devel
Cheers,
Hesham


More information about the Devel mailing list