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

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.

     L1: B = A;
     L2: D = C;
The events for the execution are:
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)
     (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)

Site Map

Last updated August 11, 2008.