Hi Alex, Many thanks for your explanation. Joyce is in a vacation thus cannot reply herself. She just want to make sure the compatibility of A15/A7. I am on behalf of her to express our gratitude.
BRs, Jesse -----Original Message----- From: [email protected] [mailto:[email protected]] Sent: Wednesday, May 17, 2017 6:20 AM To: Joyce Peng(彭美僑) Cc: [email protected]; Jesse-SC Chou (周書正); [email protected] Subject: Re: [seL4] sel4test data abort when boot strap test program Hi Joyce, Sorry for the delay. I see that your question about Cortex-A7 support has already been answered: http://sel4.systems/pipermail/devel/2017-May/001410.html Which CP15 registers are you having trouble accessing, and from which CPU mode are you trying to access them (PL1/kernel or PL0/user)? - AlexK On Mon, 2017-05-15 at 09:35 +0000, Joyce Peng(彭美僑) wrote: > Hi Alex, > > We want to avoid the most of error to access ARM CP15 register in Cortex-A7. > Is there has any seL4 official github support ARM Cortex-A7 ? > https://github.com/seL4 > https://github.com/SEL4PROJ > > For example, we found Xilinx zynq7000 support ARM Cortex-A9 in sel4test like > below. > > File: > sel4test/projects/sel4test/master-configs/zynq7000_release_xml_defconf > ig > # > # seL4 System > # > # CONFIG_ARCH_X86 is not set > CONFIG_ARCH_ARM=y > CONFIG_ARCH_AARCH32=y > # CONFIG_ARM1136JF_S is not set > # CONFIG_ARM_CORTEX_A8 is not set > CONFIG_ARM_CORTEX_A9=y > # CONFIG_ARM_CORTEX_A15 is not set > # CONFIG_PLAT_EXYNOS54XX is not set > > > Thanks, > Joyce Peng > > -----Original Message----- > From: [email protected] > [mailto:[email protected]] > Sent: Friday, May 12, 2017 11:40 AM > To: Joyce Peng(彭美僑) > Cc: [email protected]; Jesse-SC Chou (周書正); > [email protected] > Subject: Re: [seL4] sel4test data abort when boot strap test program > > Hi Joyce Peng, > > The ARM has a hardware page table walker, but the walker and CPU don't have > the same view of memory. Once the CPU has written to the page table, it must > clean the cache line before it is visible to the walker. > > My hunch is that you will need to modify the following code which determines > to which level the cache will be flushed: > https://github.com/seL4/seL4/blob/master/include/arch/arm/arch/32/mode > /machine.h#L290 > > I think that c10 should be used in place of c11, as has been done for other > specific platforms. > > - AlexK > > > > On Fri, 2017-05-12 at 03:17 +0000, Joyce Peng(彭美僑) wrote: > > 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: '[email protected]' > > Cc: [email protected] > > 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: [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
