Hello I ran into the following issue while running seL4test suite on Odroid-XU4: Exynos5422 # fatload mmc 0 0x48000000 sel4test-driver-image-arm-exynos5 there are pending interrupts 0x00000001 reading sel4test-driver-image-arm-exynos5 3149364 bytes read Exynos5422 # bootelf 0x48000000 ## Starting application at 0x41000000 ... ELF-loader started on CPU: ARM Ltd. Cortex-A7 r0p3 Switching CPU... ELF-loader started on CPU: ARM Ltd. Cortex-A15 r2p3 paddr=[41000000..4130441f] ELF-loading image 'kernel' paddr=[60000000..60037fff] vaddr=[e0000000..e0037fff] virt_entry=e0000000 ELF-loading image 'sel4test-driver' paddr=[60038000..60411fff] vaddr=[10000..3e9fff] virt_entry=1e74c Enabling MMU and paging Jumping to kernel-image entry point... Bootstrapping kernel Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info Kernel init: Too many untyped regions for boot info .... 1 untypeds of size 10 1 untypeds of size 11 126 untypeds of size 12 2 untypeds of size 13 3 untypeds of size 14 3 untypeds of size 15 5 untypeds of size 16 3 untypeds of size 17 3 untypeds of size 18 3 untypeds of size 19 3 untypeds of size 20 2 untypeds of size 21 2 untypeds of size 22 1 untypeds of size 23 2 untypeds of size 24 2 untypeds of size 25 2 untypeds of size 26 2 untypeds of size 27 1 untypeds of size 29 Switching to a safer, bigger stack... seL4 Test ========= _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 31 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 2147483648, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 30 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 1073741824, error 1 _allocman_utspace_alloc@allocman.c:301 Regular utspace alloc failed and not watermark for size 29 type 0 vka_alloc_object_at@object.h:57 Failed to allocate object of size 536870912, error 1 ..... _utspace_split_alloc@split.c:247 Failed to find any untyped capable of creating an object at address 0x12dd0000 vka_alloc_object_at@object.h:64 Failed to allocate object of size 4096 at paddr 0x12dd0000, error 1 init_timer_caps@main.c:348 [Cond failed: error] Failed to get untyped at paddr 0x12dd0000 for timer Ignoring call to sys_rt_sigprocmask Ignoring call to sys_gettid sys_tkill assuming self kill HYP mode is enabled, and seL4test suite is compiled in Debug Mode. Prior to running seL4test, I ran code from seL4 tutorials and those ran w/o any problems. Any suggestions on what I might have done wrong? Thanks
"Yevgeny" == Yevgeny Lavrov
writes:
Yevgeny> Hello I ran into the following issue while running seL4test Yevgeny> suite on Odroid-XU4: seL4test isn't validated for the XU4 --- we have none of them here. What did you do to port seL4 to the XU4? Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)
Mostly followed the same steps from this seL4 mailing lists post: Problem porting sel4 into XU4 https://sel4.systems/pipermail/devel/2016-April/000788.html My starting point was enabling HYP mode on Odroid as it is described here https://wiki.sel4.systems/Hardware/odriod-XU except that I've ended up using different signed bootloader, the one for Odroid-XU3. Then I've tested the bootloader with Ubuntu-16.04-mate-odroid-xu3 which gave me a successful boot along with: [ 0.196212] [c0] Brought up 8 CPUs [ 0.196525] [c0] SMP: Total of 8 processors activated (384.00 BogoMIPS). [ 0.196566] [c0] CPU: All CPU(s) started in HYP mode. [ 0.196600] [c0] CPU: Virtualization extensions available.
From there, I took one of the seL4 tutorials, and compiled it with the following parameters in menuconfig: seL4 System -> Architecture Type (ARM) & Platform Type (EXYNOS5422 (ODROID-XU3, ARMv7a, Cortex A15)) seL4 Libraries -> libsel4platsupport -> Redirect putchar( ) to seL4_DebugPutchar( )
Then copied the produced .elf image over to the first partition of my
MicroSD (Drag & Drop)
Plugged MicroSD into Odroid-XU4, connected to Odroid via UART and
interrupted the u-boot's autoboot process
Exynos5422 # fatload mmc 0 0x48000000 <seL4-image-name>
Exynos5422 # bootelf 0x48000000
The seL4 tutorial image executed and returned the expected output.
Then I've applied the same procedure for seL4test image. It did run, but
the test suite failed for some reason. So I wonder whether it is caused by
seL4test itself or is it because of bootloader that I'm using (not the one
mentioned in seL4 odroid-XU wiki).
Here's the link to the bootloader (sd_fuse.xu3.tgz) that I'm using:
http://forum.odroid.com/viewtopic.php?f=98&t=6147&p=50724&hilit=fanta_spl#p49315
I've also tried to enable seL4 System -> Build as Hypervisor option.
Judging from the output provided in "Problem porting sel4 into XU4" post,
this option was enabled. But the result is still the same.
On Fri, Dec 2, 2016 at 3:43 AM,
"Yevgeny" == Yevgeny Lavrov
writes: Yevgeny> Hello I ran into the following issue while running seL4test Yevgeny> suite on Odroid-XU4:
seL4test isn't validated for the XU4 --- we have none of them here. What did you do to port seL4 to the XU4?
Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)
Hello
Is there any update on my topic? If no, then I just need to confirm the
following for my report: If seL4 test suite fails, but the code taken from
completed seL4 tutorials runs w/o any issues, then does it mean that seL4
supports the device (at least partially)?
Thank you
On Fri, Dec 2, 2016 at 5:06 PM, Yevgeny Lavrov
Mostly followed the same steps from this seL4 mailing lists post: Problem porting sel4 into XU4 https://sel4.systems/pipermail/devel/2016-April/000788.html
My starting point was enabling HYP mode on Odroid as it is described here https://wiki.sel4.systems/Hardware/odriod-XU except that I've ended up using different signed bootloader, the one for Odroid-XU3. Then I've tested the bootloader with Ubuntu-16.04-mate-odroid-xu3 which gave me a successful boot along with:
[ 0.196212] [c0] Brought up 8 CPUs
[ 0.196525] [c0] SMP: Total of 8 processors activated (384.00 BogoMIPS). [ 0.196566] [c0] CPU: All CPU(s) started in HYP mode. [ 0.196600] [c0] CPU: Virtualization extensions available.
From there, I took one of the seL4 tutorials, and compiled it with the following parameters in menuconfig: seL4 System -> Architecture Type (ARM) & Platform Type (EXYNOS5422 (ODROID-XU3, ARMv7a, Cortex A15)) seL4 Libraries -> libsel4platsupport -> Redirect putchar( ) to seL4_DebugPutchar( )
Then copied the produced .elf image over to the first partition of my MicroSD (Drag & Drop) Plugged MicroSD into Odroid-XU4, connected to Odroid via UART and interrupted the u-boot's autoboot process
Exynos5422 # fatload mmc 0 0x48000000 <seL4-image-name> Exynos5422 # bootelf 0x48000000
The seL4 tutorial image executed and returned the expected output. Then I've applied the same procedure for seL4test image. It did run, but the test suite failed for some reason. So I wonder whether it is caused by seL4test itself or is it because of bootloader that I'm using (not the one mentioned in seL4 odroid-XU wiki).
Here's the link to the bootloader (sd_fuse.xu3.tgz) that I'm using: http://forum.odroid.com/viewtopic.php?f=98&t=6147&p= 50724&hilit=fanta_spl#p49315 I've also tried to enable seL4 System -> Build as Hypervisor option. Judging from the output provided in "Problem porting sel4 into XU4" post, this option was enabled. But the result is still the same.
On Fri, Dec 2, 2016 at 3:43 AM,
wrote: > "Yevgeny" == Yevgeny Lavrov
writes: Yevgeny> Hello I ran into the following issue while running seL4test Yevgeny> suite on Odroid-XU4:
seL4test isn't validated for the XU4 --- we have none of them here. What did you do to port seL4 to the XU4?
Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA)
Hi Yevgeny,
We cannot provide much assistance as you are developing on a platform that we simply do not have. You say the 'test suite failed for some reason' but you do not elaborate. Did the test suite fail to produce any output, did one of the tests report a failure, did the test suit pause mid way and if so on what test?
There is no formal definition of 'partial support' that I am aware of, so if you want to define being able to run the seL4 tutorials but not sel4test as 'partial support' then I do not think anyone can say you are incorrect, although that doesn't imply that it's a useful thing to say without qualifications.
Adrian
On Wed 04-Jan-2017 11:56 AM, Yevgeny Lavrov wrote:
Hello
Is there any update on my topic? If no, then I just need to confirm the following for my report: If seL4 test suite fails, but the code taken from completed seL4 tutorials runs w/o any issues, then does it mean that seL4 supports the device (at least partially)?
Thank you
On Fri, Dec 2, 2016 at 5:06 PM, Yevgeny Lavrov
From there, I took one of the seL4 tutorials, and compiled it with the following parameters in menuconfig: seL4 System -> Architecture Type (ARM) & Platform Type (EXYNOS5422 (ODROID-XU3, ARMv7a, Cortex A15)) seL4 Libraries -> libsel4platsupport -> Redirect putchar( ) to seL4_DebugPutchar( )
Then copied the produced .elf image over to the first partition of my MicroSD (Drag & Drop)
Plugged MicroSD into Odroid-XU4, connected to Odroid via UART and interrupted the u-boot's autoboot process
Exynos5422 # fatload mmc 0 0x48000000 <seL4-image-name>
Exynos5422 # bootelf 0x48000000
The seL4 tutorial image executed and returned the expected output.
Then I've applied the same procedure for seL4test image. It did run, but the test suite failed for some reason. So I wonder whether it is caused by seL4test itself or is it because of bootloader that I'm using (not the one mentioned in seL4 odroid-XU wiki).
Here's the link to the bootloader (sd_fuse.xu3.tgz) that I'm using: http://forum.odroid.com/viewtopic.php?f=98&t=6147&p=50724&hilit=fanta_spl#p49315
I've also tried to enable seL4 System -> Build as Hypervisor option. Judging from the output provided in "Problem porting sel4 into XU4" post, this option was enabled. But the result is still the same.
On Fri, Dec 2, 2016 at 3:43 AM,
"Yevgeny" == Yevgeny Lavrov
mailto:ylavrov13@gmail.com> writes:
Yevgeny> Hello I ran into the following issue while running seL4test Yevgeny> suite on Odroid-XU4: seL4test isn't validated for the XU4 --- we have none of them here. What did you do to port seL4 to the XU4? Peter C -- Dr Peter Chubb Tel: +61 2 9490 5852tel:%2B61%202%209490%205852 http://ts.data61.csiro.au/ Trustworthy Systems Group Data61 (formerly NICTA) _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
participants (3)
-
Adrian.Danis@data61.csiro.au
-
Peter.Chubb@data61.csiro.au
-
Yevgeny Lavrov