### Ghughal's Theorem. A(CMP,WR) => A(CMP,PO)

This theorem is taken from the work of Rajnish Ghughal [ghug99].
For a definition of the rules of PO, RR, WW, RW, and WR, see
www.mpdiag.com/analysis.html#poo

Many contemporary machines violate the rule of WR. So far as I
know (as of 080808), none violate any of the other components of
PO.
Ghughal's theorem explains why, if an execution relaxes PO,
then it must be that it relaxes WR.

Proof. Consider an execution containing two statements
accessing arbitrary operands.

P1
L1: B = A;
L2: D = C;

The events for the execution are:
(P1,L1,R,-,A,S)
(P1,L1,W,-,B,S)
(P1,L2,R,-,C,S)
(P1,L2,W,-,D,S)

Since all executions obey CMP, we know that
(P1,L1,R,-,A,S) <srw (P1,L1,W,-,B,S)
(P1,L2,R,-,C,S) <srw (P1,L2,W,-,D,S)

If the machine obeys WR, then
(P1,L1,W,-,B,S) <wr (P1,L2,R,-,C,S)

Therefore,
(P1,L1,R,-,A,S) <srw (P1,L1,W,-,B,S)
<wr (P1,L2,R,-,C,S)
<srw (P1,L2,W,-,D,S)

In this sequence the events in the two statements also obey WW, RR, and RW and thus obey PO.
Since the statements are arbitrary, if all events for any two statements in an
execution obey WR, then they all obey PO.

Since this argument holds for any execution, A(CMP,WR) => A(CMP,PO)

Last updated August 11, 2008.