PLDI’18 Artifact

This webpage contains (i) companion material and (ii) instructions for replicating the claims of the PLDI’18 paper The Semantics of Transactions and Weak Memory in x86, Power, ARM, and C++ by Nathan Chong, Tyler Sorensen, and John Wickerson.

Companion material

We provide all the models we propose (in the .cat format), the automatically-generated litmus tests used to validate our models, litmus tests corresponding to all executions discussed in our paper, and Isabelle proofs. Our proposed amendment to the transactional C++ specification is given in Appendix B of the extended version of the paper.