About the axioms #11
Description
Hello, I've noticed that the memory model after proxy extension seems to no longer conform to the original six axioms. Although they still exist in ptx.als, it seems that except for seq_cst, they no longer hold true during the check. Is this normal? I'd like to know if this is because the wording of these six axioms needs to be modified? (I noticed that this is consistent with the axioms of the previous PTX memory model that didn't consider proxy extension.) Or is it that in the proxy extension scenario, the model doesn't need to completely adhere to these axioms? Thank you!