[RFC] Formal model written in cat and tool support for simulation

Together with @hernanponcedeleon, we wrote the [vulkan model in the cat language](https://github.com/hernanponcedeleon/Dat3M/blob/master/cat/spirv.cat) (a standard language to formalize memory models), [ported all the tests](https://github.com/hernanponcedeleon/Dat3M/tree/master/litmus/VULKAN/Kronos-Group) in this repository to a more standardized format, and [added tool support](https://github.com/hernanponcedeleon/Dat3M) for simulation/verification.

We believe the tool would be valuable for the community and we wanted to get feedback if it would make sense to have the model and the tests in this repository.

The new tool has the following advantages
- it supports `goto` instructions which allow to write more realistic examples e.g. the [XF-barrier](https://github.com/hernanponcedeleon/Dat3M/blob/master/litmus/VULKAN/Manual/XF-Barrier-relacq.litmus).
- it also supports the Nvidia's PTX model, meaning that it can be used to compare how the same program (modulo ISA syntax) behaves according to the different notions of consistency.
- it scales much better than Alloy-based tools. For litmus tests scalability might not be an issue, but it could be used to verify more realistic code.
- it allows to find certain liveness violations due to spinloops not synchronizing correctly.

Start by reading cat/spirv.cat and the ported tests under litmus/VULKAN/Kronos-Group, then review the linked Dat3M tool and its simulation and verification support. Done would require a maintainer decision on whether this model, test format, and tool support should be adopted in this repository.

Written by the indexing model from the issue text.