Hi Robert,

I am unable to reproduce this failure. Can I ask what host system and toolchain you are using? Also which of the configs in sel4test?

Adrian

On Mon 17-Apr-2017 6:03 PM, Robert Kaiser wrote:
Hi all,

I just tried to run the test suite on iMX6. Using the current version
from github, I got this result:

----------------------------
.....
Test suite failed. 200/202 tests passed.

200/202 tests passed.
*** FAILURES DETECTED ***
----------------------------

Further checking into the log shows this:

----------------------------
.....
Starting test 51: TEST_SCHED0004
  TEST_SCHED0004
Running test SCHED0004 (Test threads at all priorities)
_allocman_cspace_alloc@allocman.c:252 Regular cspace alloc failed, and
failed from watermark

vka_alloc_object_at_maybe_dev@object.h:46 Failed to allocate cslot: error 1

new_pages_at_vaddr@vspace.c:331 Failed to allocate page
sel4utils_configure_thread_config@thread.c:77 ipc buffer allocation failed
Assertion failed: error == 0
([.....]/seL4test/apps/sel4test-tests/src/helpers.c:
create_helper_thread: 346)
    Failure: result == SUCCESS at line 343 of file
[.....]/seL4test/apps/sel4test-driver/src/main.c
    Failure: Test check failure (see log). at line 0 of file
.....
----------------------------

The same test is run a second time further down below the log, giving
the same result.

I tested this on two different IMX6 platforms (SabreLite and Wandboard).
Both showed identical results.

Is this a known problem?

Cheers

Robert