[herd] Unexpected(?) solver behaviour

[relokin]

For the following litmus test:

AArch64 A
{
 [y]=1;
 0:X4=y;
 1:X6=(oa:PA(z)); 1:X1=PTE(y);
}
 P0          | P1          ;
L0:          | STR X6,[X1] ;
 LDR W3,[X4] |             ;
exists(0:X3=0)

herd7 produces only one execution:

States 1
0:X3=1;
No
Witnesses
Positive: 0 Negative: 1

when there should be two (0:X3=0 when the LDR in P0 reads PTE(y)=(oa:PA(z)). The problem seems to be that herd7 won't automatically add an initial write for z. A workaround is to explicitly initialize z (e.g., [z]=0;) or help herd7 add the default initialization for z (for example, 0:X0=z;).

This issue was reported by @chacon01.

[relokin]

I had a quick look at this and the solution I come up with is not straightforward, primarily because pteval is architecture specific. Is this a known issue that it was intentionally ignored?

[maranget]

Is this a known issue that it was intentionally ignored?

I would not say that exactly. But given that there is a simple workaround, as you write yourself. I may have run across the problem and worked around it...