HI Indan,
*ptr = 0xC0FFEE;
__asm volatile("dmb sy" ::: "memory");
*ptrc = 0xDEADBEEF;
test_assert(*ptr == 0xC0FFEE); <======== failed
test_assert(*ptrc == 0xDEADBEEF);
In this case 0xC0FFEE assertion failed.
Leonid
On Thu, Mar 28, 2024 at 5:39 PM Indan Zupancic <in...@nul.nu> wrote:
> 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
>
_______________________________________________
Devel mailing list -- devel@sel4.systems
To unsubscribe send an email to devel-leave@sel4.systems
