[herd] Read-after-write initialised registers results in an assertion failure

[yuxiliu-arm]

Consider this (fake) semantics for IRG:

let irg (rd : AArch64Base.reg) _rn _rm ii =
  write_reg_dest rd V.one ii >>= fun one ->
    read_reg_ord rd ii >>= fun v ->
      Format.eprintf "v: %s\n" (V.pp_v v);
      B.nextSetT rd one

With this test:

AArch64 Ydebug
{ 0:X1=0; }
P0         ;
IRG X1,X0  ;
forall (0:X1=1)

An assertion failure happens:

Contradiction on reg 0:X1: loaded 0 vs. stored 1

Fatal: File "./herd/tests/instructions/AArch64.MTE/Ydebug.litmus" Adios
v: 0
Fatal error: exception File "herd/mem.ml", line 841, characters 16-22: Assertion failed

As can be seen, the value read is 0 even we have set it to 1. However, removing the initialization 0:X1=0 fixes the issue and the test passes.

The reason is revealed by the debug output for the latter case: v: S1. For a read, herd tries to find the value from the environment. Only when it's not found, a fresh variable is created. The problem is that even X1 is in the environment (of the instruction), the read value should really be a fresh variable, since it's not known to be fixed during the execution of the instruction.

One potential fix is to always return a fresh variable in the above line, since the value will be known when the read-from relation is resolved and the value constraint is added (exactly where the assertion failure might happen).

The above fake instruction and the example test can be found in this branch. The fresh variable fix is implemented in this commit and is reverted on the tip of the branch to illustrate the problem.

I'm not sure if the fix is correct in all cases, so it would be helpful if @maranget can have a look. I can submit the fix as a PR if needed.

[maranget]

Hi @yuxiliu-arm. Having an instruction that reads from a register it writes seldom occurs, if ever. I'll have a deeper look at your example tomorrow.

[yuxiliu-arm]

Hi @yuxiliu-arm. Having an instruction that reads from a register it writes seldom occurs, if ever. I'll have a deeper look at your example tomorrow.

Thank you. A practical example is an alternative modelling of the IRG instruction different from that of #965. If the ASL spec is strictly followed, when pseudo-random generation is enabled (GCR_EL1.RRND == 0), the RGSR_EL1 register is read and written 4 times, because its field SEED (for the pseudo-random generation) is updated to generate each bit of the tag (see AArch64.RandomTag and AArch64.NextRandomTagBit).

In #965, however, the RGSR_EL1 register is read and written once. This bypasses the problem described in this issue and is consistent with the ASL spec because accesses to the register are required to always appear in program-order.

[maranget]

Hi @yuxiliu-arm. Here is a fix:

let irg (rd : AArch64Base.reg) _rn _rm ii =
    write_reg_dest rd V.one ii >>= fun one ->
      let regs =  A.set_reg rd one  ii.A.env.A.regs in
      let env = { ii.A.env with A.regs; } in
      let ii = { ii with A.env; } in (* Binding rd -> one has now been added to ii.E.env.A.regs *)
      read_reg_ord rd ii >>= fun v ->
          Format.eprintf "v: %s\n" (V.pp_v v);
          B.nextSetT rd one

The root cause of the problem resides in a discrepancy between the semantics-time environment (ii.A.env.A.regs) and the matching of write and read effects that will be performed in a later phase. As this matching looks to be implemented correctly (i.e. the read of rd is matched by the write to rd performed by the irg function, as it should), I have corrected the environment.

[yuxiliu-arm]

Thank you. This is very helpful.