MTE: Clarify how asynchronous tag-check faults should be represented in herd

[diaolo01]

For AArch64 MTE, asynchronous tag-check faults are not architecturally reported with a faulting address or instruction label. Architecturally, software observes that TFSR_ELx has been set, rather than knowing exactly which access caused the fault.
The change under discussion is #1786 and its requirements are:

• asynchronous MTE faults should not carry a location
• asynchronous MTE faults should not carry a label

That means we should not be able to distinguish:

• two async faults on two different locations
• two async faults on two different labels
  because the architecture does not expose that information.

---

Consider the following test:

  AArch64 L07
  Variant=mte,async
  {
   0:X1=x:red;
   0:X2=y:red;
  }
   P0          ;
   MOV W0,#1   ;
   STR W0,[X1] ;
   STR W0,[X2] ;
  forall(fault(P0))

Currently, herd observes:

Fault(P0,x:red,TagCheck);
Fault(P0,y:red,TagCheck);

The behaviour we want, if we keep fault atoms, is a single indication such as:
Fault(P0,TagCheck);

---

Question: What is the right abstraction for asynchronous MTE faults in herd?

Option 1: Keep a fault atom for async faults, but remove location and label. This would model async faults as per thread observations only.

Pros:

• lets us write the same tests for synchronous and asynchronous modes
• keeps fault(...) available across both modes

Cons:

• requires changes in diy
• still uses a fault atom for something that is architecturally observed via TFSR_ELx, not as a synchronous fault
• the hashes of some tests need to be changed

Option 2: Do not use fault atoms for async faults; check only TFSR_ELx. This would align more directly with the architecture.

Pros:

• closest to what the Arm ARM exposes

Cons:

• async and sync tests would have different postconditions
• tests that currently use fault(...) in both modes would need to be rewritten
• probably still needs changes in diy

[murzinv]

Getting some #1079 flashbacks 😄 I'd suggest also taking asymmetric mode (reads are sync, writes are async) into account when considering abstraction.

Anyway, whatever option you take, please, make sure it is reflected in catalogue/aarch64-faults/README.md

[ShaleXIONG]

Follow up an offline chat. Both approaches are reasonable to me, and only need small change to diy.

In short, I will add a new variant async to diy. This will add async to theVariant metadata in the generated test, so herd7 can directly configure the correct variant. Given the new variant, both approaches need small change to the generated post condition. The fault is probably slightly smaller change however I do not think there are big differences.

[diaolo01]

@maranget do you have any thoughts on this?

The requirements are:

• async MTE faults must not carry a location or a label
• multiple async MTE faults in one thread are reported as one observation

The choice is whether that observation should be:

1. fault(Pn)
2. only TFSR_ELx in the postcondition