Improvements to GPU grammars + new benchmark

[hernanponcedeleon]

This PR makes a few improvements to the grammars of PTX and Vulkan and adds a new benchmark for a synchronization barrier which forces threads to wait until all of them reached the barrier.

The benchmark shows that PTX can be stronger than Vulkan in the sense that we can achieve correctness with relaxed operations while Vulkan requires release-acquire.

[ThomasHaas]

I was always confused by the distinction made when parsing operations over constants vs. over registers. I thought it was related to semantics differences, but I guess the grammar was just inadequate.

I'm not going to try to wrap my head around the litmus tests, but the remaining code changes seem straightforward (and good :)), so I will approve.

[hernanponcedeleon]

I was always confused by the distinction made when parsing operations over constants vs. over registers. I thought it was related to semantics differences, but I guess the grammar was just inadequate.

It used to be like that due to the modeling of the constant proxy. But this has changed in #531.

[hernanponcedeleon]

I found a bug in the PTX v7.5 model (the bug comes from the alloy model).
Similart to v6.0. the definition of cause should be let cause = cause-base | (observation?; ...) as stated in the documentation.

@tonghaining can you please translate the test MP-cause-base to the alloy format and open a PR in their repo with a fix to the model and the test?

[ThomasHaas]

Your two changes to let cause = ... ended up giving the original model. I guess the Alloy model was correct then, and you misread the documentation?

[hernanponcedeleon]

I was getting some different results between v6.0 and v7.5 (maybe I built from the wrong branch) due to the control barriers. This made me take a look to where those were used in the cat file and I noticed the union was missing, but I did not noticed the use of ? which was actually making the relation be semantically equivalent.