Characterizing transactional memory consistency conditions using observational refinementHagit AttiyaSandeep Hanset al.2017Journal of the ACM