[herd] Attempt to limit the number of spurious AF updates

[maranget]

We attempt to identify the value stored by writes to page table entries. When this value has a set AF flag, there is no need to emit a spurious update. The collected information allows is not to fire spurious updates in some cases.

[relokin]

Thanks for this Luc.

This got me curious do you have an example litmus test which will show spurious updates of the AF when the AF is already set?

[maranget]

The test is rather simple:

AArch64 T
TTHM=HA
{
0:X1=PTE(x);
0:X0=(oa:PA(x));
}
P0          ;
STR X0,[X1] ;
forall [PTE(x)]=(oa:PA(x));

The semantic module yields two execution candidates, one of which includes a spurious update attempt
1.pdf --- To see those diagrams of executions before the rf matching phase, use command-line option -dumpes true and -gv (display) or -o <dir> (save .dot file in <dir>).

The diagram does not show it but the underlying structure includes a assert that S1 (value read by the spurious update) is a PTE with AF=0. Hence, later no write performed by test T can feed this read and the corresponding execution is discarded by the solver phase.

The choice of adding a spurious update or not multiplies the number of executions by two. Then, even if half of them are discarded by the solver and this process takes noticeable time in complex tests.

[relokin]

Thanks for this Luc! A couple of questions/thoughts, otherwise this PR looks good to me.

[relokin]

it looks like, you introduced _tag to help debug or profile? Can you add that functionality perhaps disabled by default? Otherwise having the argument _tag and it doesn't help for functions like lift_memop which already had many arguments.

[maranget]

I'll supress this argument here, but would like to keep it as an optional argument of the function lift_mem_op.

[relokin]

Just out of curiosity, we can't do a similar check for reads, can we? For example, take the following litmus test:

AArch64 foo
Variant=vmsa
TTHM=HA
{
  [PTE(x)]=(oa:PA(x));
  0:X2=x;
}
 P0 ;
 LDR W2,[X2] ;

$> herd7 -dumpes true /tmp/foo.litmus -o /tmp

produces 4 executions, on of which has a hardware update of the AF which is obviously not needed.

[maranget]

I have to check, but there should be no spurious update here.

[maranget]

I have just checked, the HW update involved is not a spurious one. We cannot really get rid of it at Sem time: as a general principle the values in memory are not known at that time. In that very specific case, a global analysis could infer that having the AF flag to be zero is not possible. However, generalisation looks quite involved to me.

[relokin]

If you are planning to keep the 3 commits separate, this belongs to the previous commit.

[maranget]

My intend is to squash the commits.

[maranget]

Thanks for your comments @relokin. In fact I now attempt a global approach in another branch.

Thus I give this one the Draft status again...

[maranget]

Superseded by PR #1733