Alternatives to partial coherence in the anarchic semantics for PTX

[ThomasHaas]

This issue is a summary of what we discussed in #528

Context: PTX requires a partial notion of coherence rather than a total one. We adapted our anarchic semantics to allow coherence to be partial to accomodate this use-case. Our partial encoding simply drops the totality constraint, meaning that coherence is just any acyclic relation over stores to the same address. This causes two issues: (1) coherence need not be transitive and (2) it doesn't need to relate anything (it can just be empty). Currently, we fix these short-comings by redefining co = co+ (fixing point 1) and adding an axiom to force co to contain certain minimal pairs (e.g., atomic stores) in the PTX model.

Problem: The definition of coherence is now awkwardly split between the anarchic semantics and the cat model. Also, we need to switch to the partial coherence notion based on what architecture we are handling (partial for PTX, total for the rest).

Solutions: There are two solutions to that problem that allow us to keep the total coherence and avoid any case distinction based on the target architecture (i.e., the CAT model itself can define its coherence to be partial!)

Solution 1: We just use the total coherence order and then define in PTX a partial coherence order from the total order by restricting to morally-strong edges and adding causally-related stores: let co = ((co & morally-strong) | (([W]; cause; [W]) & loc) | (([IW];loc;[W]) \ id))+ Here we still rely on the anarchic semantics of co and just derive a new relation that fits the needs of the PTX model.

Solution 2: A more general approach is to define a partial co directly in CAT instead of relying on the anarchic semantics at all. This requires a new primitive in the CAT language, namely "free relations". Suppose free was a relation that could take any value, then we can define

let co = ([W];free;[W] & loc)+ // co is ANY transitive relation that relates same-address writes
acyclic (co) // co is acyclic
empty (([W];morally-strong;[W] & loc) \ (co | co^-1)) // co is total on morally-strong writes
empty (([W];cause;[W] & loc) \ co) // co relates causally-ordered writes (even if they are not morally strong)
// Alternative to the last axiom by just extending the initial definition:
// let co = ([W];free;[W] & loc | ([W];cause;[W] & loc))+
// NOTE: In both versions the treatment of init writes needs to be added

This is a full specification without relying on any anarchic semantics. In a similar way, the user could define any new custom relation.

[hernanponcedeleon]

There is the issue that both the semantics of the litmus final conditions and the liveness check depends on co. We have at least one litmus test that was causing problems to solution 1. Not sure how much solution 2 is affected by this.

[ThomasHaas]

You are right, I forgot to mention this. Both solutions 1 and 2 have problems with final conditions and liveness. I think the final condition problem can be circumvented by simply not using those conditions. I don't even know what our current behavior is, i.e., what happens if there are two co-maximal writes due to the partialness.

Liveness is certainly harder to deal with. I think for this, we will need to move the liveness definition into CAT, which we eventually need to do anyways to handle liveness with interrupts and uncachable memory regions. A "simple" solution might be to add a new primitive check liveness(r) that allows the CAT model to specify that spinloops that read r-maximal values can be considered stuck. The standard definition is then just check liveness(co), but it could be changed to a subset for PTX/Vulkan and interrupt handling.

[ThomasHaas]

I would really like to add support for free relations to CAT, so I wanna discuss how this should work syntactically. I think declaring a free relation should be a function call, either called free() or new() (possibly with underscores __ to avoid name clashes?). This requires our parser to support function calls, which is a nice-to-have feature we should have. It is also required to support the new CAT models for ARM/ASL. The syntax would look like this:

let co = ([W];new();[W] & loc)+

Such new syntax will not be compatible with herd7, but neither is our partial notion of co right now. I also think that it is not a good idea to forever stick to herd7's CAT syntax in the long run anyway.

Efficiently handling such relations in RA requires implicit representations I believe. A free relation has a full may-set and thus gets huge when represented explicitly. However, this will NOT(!) result in a huge encoding, because the active set in the above example will only contain Write-Write pairs that can alias. This is not any larger than what our current co encoding generates.