Subtyping rules violate transitivity. See first author's PhD thesis ("Rely-Guarantee Protocols for Safe Interference over Shared Memory") for the corrected subtyping rules.