Hello Leonid,
On 2024-03-28 20:18, Leonid Meyerovich wrote:
I run sel4test on the aarch64 platform.
What CPU are you testing on?
My CACHEFLUSH0001 test in sel4test failed /* Clean makes data observable to non-cached page */ *ptr = 0xC0FFEE; *ptrc = 0xDEADBEEF; test_assert(*ptr == 0xC0FFEE); test_assert(*ptrc == 0xDEADBEEF);
The problem is that the test is not reliable, it assumes things it can't safely assume, even though they're usually correct. In this case it assumes that the cache line containing ptrc doesn't get evicted and that no memory reordering happened between the ptr and ptrc writes. See also https://github.com/seL4/sel4test/issues/80.
That said, it should usually pass. Is it consistently failing for you?
I have tried to make to 'improve' memory/cache coherence, but the last assertion still failed
It's more likely that the 0xC0FFEE assertion fails, but for you the 0xDEADBEEF one fails?
/* Clean makes data observable to non-cached page */ *ptr = 0xC0FFEE; *ptrc = 0xDEADBEEF;
error = seL4_ARM_Page_Clean_Data(framec, 0, PAGE_SIZE_4K); error = seL4_ARM_Page_Invalidate_Data(framec, 0, PAGE_SIZE_4K);
__asm volatile("dmb sy" ::: "memory");
Try putting this after the *ptr = 0xC0FFEE; write.
Tip for anyone needing cache maintenance on Aarch64: There is no need to use the seL4 system calls, you can do (non-invalidating) cache maintenance instructions from user space.
Greetings,
Indan