AXE Checker gets confused if there are multiple writes of the same data to the same address

[zhemao]

I am seeing an AXE failure in tracegen. The summary given by axe-shrink.py is as follows

0: { M[1] == 51; M[1] := 114} @ 1613:
1: M[1] := 51 @ 1619:
1: { M[1] == 51; M[1] := 55} @ 1620:1678

I don't think this is actually a consistency violation. I think AXE is confused because it thinks both atomic swaps read the old value of 51. However, it's more likely the second swap read the 51 that was just written by the same processor.

[mn416]

Hi @zhemao, thanks for the report.

A few points in response:

1. If tracegen is generating multiple writes of the same data to the same address then that is a bug in tracegen. (By design, axe requires that all writes have a unique address-value pair and tracegen is designed to meet this property. If a trace doesn't satisfy this property then axe should give an error message - it cannot say "OK" or "NO" with respect to any consistency model.)
2. This trace (at least the shrunk version) doesn't actually contain multiple writes of the same data to the same address (there is one write of 51, one write of 114, and one write of 55).
3. I confirm that axe is behaving as intended by saying "NO" to this trace. Two atomic RMWs have read the same value which, combined with the unique writes property, cannot be atomic under any of the consistency models supported.

Q. What is the output of "axe check wmo trace.axe" where "trace.axe" is the original failing trace before shrinking? If the output is "NO" then trace satisfies the unique writes property but fails wmo. If the output is an error message then axe cannot say "OK" or "NO" and there is probably a bug either in tracegen or the memory subsystem or the script that converts traces to axe format.

[zhemao]

Oh, I see. You're saying that the write of 51 from core 1 is actually coming logically before the AMO from core 0. That makes much more sense.

I ran into this issue when attempting to run multiple trace generators against the same L1. I now realize that this might violate some assumptions the AXE checker has (since it assume generators 0 and 1 are separate cores). I'll close this issue for now and Henry and I will revisit what the semantics of multiple clients to the same L1 are.