[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.

Commencez par lire cat/spirv.cat et les tests portés sous litmus/VULKAN/Kronos-Group, puis examinez l’outil Dat3M lié ainsi que sa prise en charge de la simulation et de la vérification. La tâche sera considérée comme terminée lorsqu’un maintainer aura décidé si ce modèle, ce format de test et cette prise en charge de l’outil doivent être adoptés dans ce dépôt.

Rédigé par le modèle d'indexation à partir du texte de l'issue.