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.

• The extended version of the paper
• The shorter conference version of the paper

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.

• Models
• Experimental data
• Figures
• Isabelle proofs

Replication

• Instructions for replicating the experimental results of Table 1 in Section 5.3
• Instructions for replicating the metatheory results of Table 2 in Section 8