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(彭美僑)
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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham
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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham
Hi Joyce,
The work to add a new platform requires some work on: 1) seL4, mainly you've to look at all plat/ directories and modify them to fit with your platform, specifically, physical memory range and virtual memory/device drivers mapping. 2) sel4libs, again have a look at plat/ directories there, you've to create corresponding ones for your new platform.
From the error message you provided, I would suggest to debug what should be at this address (normal memory?), what is the corresponding physical memory for this page, and whether this physical address is within your platform's physical memory range.
Hope that helps.
Cheers, Hesham On 10/05/17 16:13, 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-littlearmFor 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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham
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;;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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Thursday, May 11, 2017 11:39 AM To: Joyce Peng(彭美僑) Cc: devel@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;;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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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@data61.csiro.au' Cc: devel@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@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Thursday, May 11, 2017 11:39 AM To: Joyce Peng(彭美僑) Cc: devel@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;;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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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/machi...
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: 'Alexander.Kroh@data61.csiro.au' Cc: devel@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@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Thursday, May 11, 2017 11:39 AM To: Joyce Peng(彭美僑) Cc: devel@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;;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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi Alex/Hesham,
According last mail, I add below modification and fix this issue.
--- a/include/arch/arm/arch/32/mode/machine.h +++ b/include/arch/arm/arch/32/mode/machine.h @@ -286,6 +286,8 @@ static inline void cleanByVA_PoU(vptr_t vaddr, paddr_t paddr) asm volatile("mcr p15, 0, %0, c7, c10, 1" : : "r"(vaddr)); #elif defined(ARM_CORTEX_A53) asm volatile("mcr p15, 0, %0, c7, c10, 1" : : "r"(vaddr)); +#elif defined(ARM_CORTEX_A7) + asm volatile("mcr p15, 0, %0, c7, c10, 1" : : "r"(vaddr)); #else asm volatile("mcr p15, 0, %0, c7, c11, 1" : : "r"(vaddr)); #endif
This solution is very correctly and give us much help. According the description of last mail, I understand what happen of this issue very clear. I think this help give us more confident about seL4 and let us know seL4 group has rich experience. Thanks.
Joyce Peng
-----Original Message----- From: Alexander.Kroh@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Friday, May 12, 2017 11:40 AM To: Joyce Peng(彭美僑) Cc: devel@sel4.systems; Jesse-SC Chou (周書正); Alexander.Kroh@data61.csiro.au 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/machi...
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: 'Alexander.Kroh@data61.csiro.au' Cc: devel@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@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Thursday, May 11, 2017 11:39 AM To: Joyce Peng(彭美僑) Cc: devel@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;;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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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_defconfig # # 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: Alexander.Kroh@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Friday, May 12, 2017 11:40 AM To: Joyce Peng(彭美僑) Cc: devel@sel4.systems; Jesse-SC Chou (周書正); Alexander.Kroh@data61.csiro.au 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/machi...
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: 'Alexander.Kroh@data61.csiro.au' Cc: devel@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@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Thursday, May 11, 2017 11:39 AM To: Joyce Peng(彭美僑) Cc: devel@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;;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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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_defconfig # # 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: Alexander.Kroh@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Friday, May 12, 2017 11:40 AM To: Joyce Peng(彭美僑) Cc: devel@sel4.systems; Jesse-SC Chou (周書正); Alexander.Kroh@data61.csiro.au 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/machi...
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: 'Alexander.Kroh@data61.csiro.au' Cc: devel@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@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Thursday, May 11, 2017 11:39 AM To: Joyce Peng(彭美僑) Cc: devel@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;;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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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: Alexander.Kroh@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Wednesday, May 17, 2017 6:20 AM To: Joyce Peng(彭美僑) Cc: devel@sel4.systems; Jesse-SC Chou (周書正); Alexander.Kroh@data61.csiro.au 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: Alexander.Kroh@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Friday, May 12, 2017 11:40 AM To: Joyce Peng(彭美僑) Cc: devel@sel4.systems; Jesse-SC Chou (周書正); Alexander.Kroh@data61.csiro.au 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: 'Alexander.Kroh@data61.csiro.au' Cc: devel@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@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Thursday, May 11, 2017 11:39 AM To: Joyce Peng(彭美僑) Cc: devel@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;;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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
Hi Alex, Thanks for your help.
Joyce Peng -----Original Message----- From: Jesse-SC Chou (周書正) Sent: Thursday, May 18, 2017 9:54 AM To: Alexander.Kroh@data61.csiro.au; Joyce Peng(彭美僑) Cc: devel@sel4.systems Subject: RE: [seL4] sel4test data abort when boot strap test program
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: Alexander.Kroh@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Wednesday, May 17, 2017 6:20 AM To: Joyce Peng(彭美僑) Cc: devel@sel4.systems; Jesse-SC Chou (周書正); Alexander.Kroh@data61.csiro.au 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: Alexander.Kroh@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Friday, May 12, 2017 11:40 AM To: Joyce Peng(彭美僑) Cc: devel@sel4.systems; Jesse-SC Chou (周書正); Alexander.Kroh@data61.csiro.au 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: 'Alexander.Kroh@data61.csiro.au' Cc: devel@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@data61.csiro.au [mailto:Alexander.Kroh@data61.csiro.au] Sent: Thursday, May 11, 2017 11:39 AM To: Joyce Peng(彭美僑) Cc: devel@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;;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_PLATFORMbool " OUR_PLATFOR (ARMv7a, Cortex A7)"depends on ARCH_AARCH32select ARM_CORTEX_A7select ARCH_ARM_V7AhelpSupport 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@data61.csiro.au [mailto:Hesham.Almatary@data61.csiro.au] Sent: Wednesday, May 10, 2017 9:32 AM To: Joyce Peng(彭美僑); devel@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@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, #2cbe0: e5431001 strb r1, [r3, #-1]
cbe4: e5c01000 strb r1, [r0] cbe8: 98bd8030 popls {r4, r5, pc} cbec: e3520006 cmp r2, #6It 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@sel4.systems https://sel4.systems/lists/listinfo/devel
Cheers, Hesham _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
-
Alexander.Kroh＠data61.csiro.au -
Hesham.Almatary＠data61.csiro.au -
Jesse-SC Chou (周書正) -
Joyce Peng(彭美僑)