[seL4] sel4test data abort when boot strap test program

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


Hi Alex,
I turning the caches off in configuration. Then it can boot. Thank you.
Below is my procedure.
$ make menuconfig
Navigate through: seL4 Kernel -> Build Options
DEBUG_DISABLE_L1_DCACHE [=y]
DEBUG_DISABLE_L1_ICACHE [=y]
DEBUG_DISABLE_L2_CACHE [=y]

But how those configurations affect seL4.
I confuse what it let the page table of application in seL4 can't access correctly. 


Thanks,
Joyce Peng
-----Original Message-----
From: Joyce Peng(彭美僑) 
Sent: Friday, May 12, 2017 12:26 AM
To: 'Alexander.Kroh at data61.csiro.au'
Cc: devel at sel4.systems
Subject: RE: [seL4] sel4test data abort when boot strap test program

Hi Alex,

The content of the DFSR is 0x805 and DFAR is 0xDF7FEFFFF.
And caching is turning off.
$make menuconfig
DEBUG_DISABLE_L1_DCACHE [=n]
DEBUG_DISABLE_L1_ICACHE [=n]
DEBUG_DISABLE_L2_CACHE [=n]

Thanks,
Joyce.peng

-----Original Message-----
From: Alexander.Kroh at data61.csiro.au [mailto:Alexander.Kroh at data61.csiro.au]
Sent: Thursday, May 11, 2017 11:39 AM
To: Joyce Peng(彭美僑)
Cc: devel at sel4.systems
Subject: Re: [seL4] sel4test data abort when boot strap test program

Hi Joyce,

Can you provide the content of the DFSR? It provides a lot of useful information about the cause of a data abort. If it is not printed, You can find it in the context of the fault handler with:

seL4_Word fsr = seL4_GetMR(seL4_VMFault_FSR);

Beware that this message register will be clobbered if you perform a system call. This may include the use of printf(..).


You might have a caching problem. You can check this by turning the caches off via:
$ make menuconfig
Navigate through: seL4 Kernel -> Build Options


 - Alex




On Wed, 2017-05-10 at 06:13 +0000, Joyce Peng(彭美僑) wrote:
> 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
> _______________________________________________
> Devel mailing list
> Devel at sel4.systems
> https://sel4.systems/lists/listinfo/devel



More information about the Devel mailing list