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
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel

Reply via email to