search

seL4 / sel4test

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

TK1 and ODROID_XU4 fail `CACHEFLUSH0001` #80

Open lsf37 opened 2 years ago

lsf37 commented 2 years ago

In config ODROID_XU4_debug_hyp_MCS_clang_32 (and apparently only this config and only on clang), ODROID_XU4 is failing the test CACHEFLUSH0001. The configuration is disabled for tests for now.

It looks like this might be a problem with the test setup, not with MCS.

See also discussion on seL4/seL4#877.

lsf37 commented 1 year ago

Occasionally the TK1 board also fails the same test (for the same config, i.e. TK1_debug_hyp_MCS_clang_32).

It looks like something is definitely up there.

lsf37 commented 1 year ago

Comment from Indan on that thread linked above about what might be wrong:

Running test CACHEFLUSH0001 (Test a cache maintenance on pages) *ptrc == 0xBEEFCAFE at line 104 of file /github/workspace/projects/sel4test/apps/sel4test-tests/src/tests/cache.c

I'm not convinced that test_page_flush is correct: It relies on no cache miss or prefetching happening between the seL4_ARM_Page_Invalidate_Data call and the *ptr write. I don't think that's guaranteed.

In case the invalidation performs an implicit clean, the result is the same as for seL4_ARM_Page_CleanInvalidate_Data above, which is already tested.

Indanz commented 1 year ago

This seems a duplicate/extension of #65 btw.