Add SC-per-Location Axiom

[tonghaining]

This commit adds the Sequential Consistency Per Location axiom(https://docs.nvidia.com/cuda/parallel-thread-execution/index.html#sc-per-loc-axiom) which is missing in the model. We add a litmus test from issue(#4). If the Program Order (PO) relation removed from cause_base relation which makes the model roll back to ptx-v6.0 (proxy-less version), this test shows the SC-per-Location axiom is missing.

[daniellustig]

I agree that if po is taken back out of cause_base, we need SC-per-location. But given that po is now included in cause_base, isn't SC-per-location redundant?

[hernanponcedeleon]

I don't fully see if this axiom is redundant or not.

I understand that now po-loc pairs in the generic proxy are also part of roxy-preserved-cause-base. This together with irreflexive ((rf | fr); cause) as axiom-Causality might allow to derive some more information, but I don't see how to infer they cannot form a cycle when making the union to morally strong communication (rf+fr+co) pairs.

Even if this is redundant, I think it is a matter of taste between being simple and being explicit. The documentation still explicity mentions this axiom, so I don't see why the formal model should opt for being simple. Personally, I dislike the fact that one could simply modify the definition of cause-base and this would have "hidden" implications.

The formal model has other situations like this. E.g., it uses

pred causality {
  irreflexive[optional[com].cause]
}

which includes co. The documentation and the proxy-less model only refer to rf and fr. I have the feeling that adding co might not have semantic implications (due to the coherence axiom), but I was still planning to open a PR about that one (I wanted first to see if I could find a test showing a problem or some "proof" that there are indeed no semantic differences).

[daniellustig]

I would be very interested in any concrete litmus tests you might be able to find that would help us distinguish cases like these. We try to do some sanity checking and model checking as we refactor, but the model has become complex enough that it's entirely possible that cases have slipped through.

Alternatively, if you convince yourselves the changes are indeed sound/redundant, then that would be interesting too. And yes, I agree it turns into a matter of taste at that point, but if we prove everything is equivalent then there is no contradiction in everyone having their own preferences :)