[aarch64] same location, different cacheability attributes

[gonzalobg]

Following this blog, I am trying to use herd to check a litmus test for accessing a single memory location using two virtual aliases with different cacheability attributes, depending on the value of CLIDR_EL1.LoC=0 .

Did I understand correctly that cacheability attributes are currently only supported per location? That is, two locations may have different cacheability attributes, but one cannot currently check litmus tests that access a single location with two different attributes?

Thanks Gonzalo

[gonzalobg]

@jalglave maybe?

[relokin]

You can specify a litmus test where you access a single location with different memory attributes like so:

AArch64 coWR-ISH-WB-Device-nGnRnE
{
 [x]=0;
 [PTE(y)]=(oa:PA(x),attrs:(Normal,Inner-Shareable,Inner-Writeback,Outer-Writeback));
 [PTE(z)]=(oa:PA(x),attrs:(Device-nGnRnE));
 0:X1=y; 0:X3=z;
}
 P0          ;
 MOV W0,#1   ;
 STR W0,[X1] ;
 LDR W2,[X3] ;
exists(0:X2=0)

Symbolic virtual address y and z map to the symbolic physical location x but they have different memory attributes. herd7 will parse and execute this litmus test. It will also generate the right events and relations. However, it will not produce the right outcomes; the precise semantics of access with attributes other than the default (Inner-shareable, Inner-Writeback and Outer-Writeback) have not been formalized yet, or in other words, the aarch64.cat is missing the necessary definitions for herd7 to work out which executions should be forbidden. This is still work in-progress for us.

@jalglave please chime if I missed something.

[relokin]

@gonzalobg, I just wanted to let you know that we have also updated the blog as well. If you have any comments/thoughts/feedback, please do let me/us know!

[gonzalobg]

Thank you, I'll check it out.