"It's not terribly surprising that if causality is baked into your specification, then you're going to have to use causality as part of your implementation." I dont understand this statement. Causality is the base of the ordering specification, that's correct to say as "baked into your specification". What does "use causality as part of your implementation."? The paper does not use causality to implement causality, it uses causality to implement mutex. Any contradiction here?