Model checking transactional memories