Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement