Verification of snapshot isolation in transactional memory Java programs