seL4tests on Zynq7000 failing

New to seL4
1

Hello!
Following the instructions in Zynq7000 | seL4 docs to run sel4test on Zynq700 in Renode fails with:

vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 2147483648, error 1
vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 1073741824, error 1
vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 536870912, error 1
vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 268435456, error 1

Yes, is in Renode simulator - I am following this guide Antmicro · seL4 userspace debugging with GDB extensions in Renode and I can run the CAMKES example in simulation just fine.

The error looks like an OOM error, is that correct?

Any idea what I should look at to fix it?

Regards

2

Hi @mpodhradsky,

Is there more output? That is common output when running the tests in debug mode:

  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 2147483648, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 1073741824, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 536870912, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 268435456, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 134217728, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 67108864, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 33554432, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 16777216, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 8388608, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 4194304, error 1
  
  vka_alloc_object_at_maybe_dev@object.h:57 Failed to allocate object of size 2097152, error 1
3

Hi @kent-mcleod2 !
Good point - I did let the test run for longer, and it eventually proceed!

Here is the result:

[host: 2/2/2023 10:55:47 AM, virt:  262757] Starting test 130: Test all tests ran
[host: 2/2/2023 10:55:47 AM, virt:  262757] Test suite failed. 127/130 tests passed.
[host: 2/2/2023 10:55:47 AM, virt:  262757] *** FAILURES DETECTED ***

The failing tests are:

[host: 2/2/2023 10:46:06 AM, virt:   12718] Starting test 22: CACHEFLUSH0001
[host: 2/2/2023 10:46:07 AM, virt:   12895] Failure: result == SUCCESS at line 291 of file /sel4test/projects/sel4test/apps/sel4test-driver/src/testtypes.c
[host: 2/2/2023 10:46:07 AM, virt:   13278] Error: result == SUCCESS at line 217 of file /sel4test/projects/sel4test/apps/sel4test-driver/src/main.c
[host: 2/2/2023 10:46:07 AM, virt:   13278] Starting test 23: CACHEFLUSH0002
[host: 2/2/2023 10:46:08 AM, virt:   13455] Failure: result == SUCCESS at line 291 of file /sel4test/projects/sel4test/apps/sel4test-driver/src/testtypes.c
[host: 2/2/2023 10:46:08 AM, virt:   13838] Error: result == SUCCESS at line 217 of file /sel4test/projects/sel4test/apps/sel4test-driver/src/main.c
...
[host: 2/2/2023 10:52:30 AM, virt:  169028] Starting test 89: SCHED0021
[host: 2/2/2023 10:52:31 AM, virt:  169251] Failure: result == SUCCESS at line 291 of file /sel4test/projects/sel4test/apps/sel4test-driver/src/testtypes.c
[host: 2/2/2023 10:52:31 AM, virt:  169635] Error: result == SUCCESS at line 217 of file /sel4test/projects/sel4test/apps/sel4test-driver/src/main.c

Looks like two cache-flushes and one scheduling test - is that an expected result?

Otherwise, could it be something with the platform config?

Regards

4

These are all tests that are normally disabled when running on a simulator. There is a CMake configuration option: SIMULATION which when set to ON disables these tests.
I’m not sure whether the Renode simulator would emulate the cache behavior. Looking from the test failure it appears to not.

5

Thanks for the suggestion.After playing with the options a bit, this is a working config:

../init-build.sh -DPLATFORM=zynq7000 -DSel4testSimulation=1 \
-DSel4testHaveCache=0 -DSel4testAllowSettingsOverride=1

I had to manually disable the caching tests, not sure why Sel4testSimulation=1 didn’t do that?

On a side note, I noticed a mix of UPPERCASE (PLATFORM…) and CamelCase ( Sel4testSimulation…) parameters - are you slowly migrating to the CamelCase ones, or is there something else I am missing?

6

Does

../init-build.sh -DPLATFORM=zynq7000 -DSIMULATION=1

work better? (From the zynq7000 docs page)

7

Good point, that worked as well! Not sure how I missed it. Thanks!

1 Like