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: [email protected] [mailto:[email protected]] Sent: Thursday, May 11, 2017 11:39 AM To: Joyce Peng(彭美僑) Cc: [email protected] 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: [email protected] > [mailto:[email protected]] > Sent: Wednesday, May 10, 2017 9:32 AM > To: Joyce Peng(彭美僑); [email protected] > 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() > > > > [email protected]:111 my-hacker > > > > [email protected]: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 > > [email protected] > > https://sel4.systems/lists/listinfo/devel > Cheers, > Hesham > _______________________________________________ > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
