Modern distributed systems are built on message passing, often in an environment where concurrently sent messages may be received by individual machines in non-deterministic order. To resolve conflicts and reduce non-determinism, programmers often implement a message passing \textit{protocol} that induces some ordering on messages received. One such ordering is \textit{causal ordering}, where each machine in the system orders its received messages by causal order: if an event $a$ has potentially caused an event $b$, and a node in the system learns of both $a$ and $b$, then the node orders $a \prec b$ in its processing queue. A programmer may choose one of many different causal ordering protocols to implement, with the implicit understanding that all protocols are “equivalent” with respect to causal ordering.

In this ongoing work, we argue that such reasoning is correct, because it can be made precise by means of proving a simulation between two protocols for causal ordering, with different underlying semantics: the \textit{buffer protocol} and the \textit{matrix protocol}. Our simulation is based on the idea of proving that both protocols are capable of inducing the same ordering of received messages. This implies correctness of message-ordering protocols can be argued by a notion of observational equivalence.