Re: [seL4] seL4test on Odroid-XU4

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)