Together with @hernanponcedeleon, we wrote the ptx model in the cat language (a standard language to formalize memory models), ported all the tests in this repository to a more standardized format, and added tool support 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 and barrier instructions which allow to write more realistic examples e.g. the XF-barrier.
- it also supports the Vulkan 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.
Together with @hernanponcedeleon, we wrote the ptx model in the cat language (a standard language to formalize memory models), ported all the tests in this repository to a more standardized format, and added tool support 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
gotoandbarrierinstructions which allow to write more realistic examples e.g. the XF-barrier.