search

seL4 / sel4test

Test suite for seL4.
http://sel4.systems
Other
25 stars 63 forks source link

TK1 sometimes fails CACHEFLUSH0001 #65

Closed lsf37 closed 8 months ago

lsf37 commented 2 years ago

The TK1 (jetson1) board sometimes fails the CACHEFLUSH0001 test:

<testcase classname="sel4test" name="CACHEFLUSH0001">
  Running test CACHEFLUSH0001 (Test a cache maintenance on pages)
        <failure type="failure">*ptrc == 0xBEEFCAFE at line 104 of file /github/workspace/projects/sel4test/apps/sel4test-tests/src/tests/cache.c</failure>
  Test CACHEFLUSH0001 failed
        <failure type="failure">result == SUCCESS at line 291 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/testtypes.c</failure>
        <error>result == SUCCESS at line 217 of file /github/workspace/projects/sel4test/apps/sel4test-driver/src/main.c</error>
    </testcase>

I've only seen this for clang-11 so far, in the configuration TK1_debug_hyp_MCS_clang_32, but it doesn't occur extremely often, so the may be others as well.

Example run: https://github.com/seL4/seL4/runs/4491614422?check_suite_focus=true#step:4:5733

lsf37 commented 8 months ago

Duplicate of #80 (actually #80 is the duplicate, but it has more info in the discussion).