Allowed by Flat-axiomatic2 => allowed by Flat-operational -------------------------------------------------------- ******************************************************************************** This proof assumes 0. Finite candidate executions and finite Flat traces. 1. That if a write-exclusive is successfully paired with a read-exclusive, then they are to the same address. 2. Axiomatic and Operational model use the same instruction semantics. 3. (E,E') in addr iff: E is a read and E' is a read or a write and E feeds into a register write that affects the address of E'. Note: this means addr(E,E') does not hold if E is a write-exclusive. 4. (E,E') in data iff: E is a read and E' is a write and E feeds into a register write that affects the value written by E'. Note: this means data(E,E') does not hold if E is a write-exclusive. 5. (E,E') in ctrl iff: E is a read and E' is a write and E feeds into a register write that affects a conditional branch or a computed branch instruction program-order before E'. Note: this means ctrl(E,E') does not hold if E is a write-exclusive. ******************************************************************************** Note: In herd a successful write-exclusive's success bit introduces dependencies *from its matching read-exclusive*: For example, in the program-fragment a: LDXR W1,[X0] b: STXR W2,W1,[X0] c: STR W2,[X3] where c stores the success bit of b into some location in memory, in herd it will be (a,c) in data. This does not match ARMv8's concurrency semantics where it is neither (a,c) in data, nor (b,c) in data. ******************************************************************************** Show: candidate executions accepted by ARMv8-axiomatic are accepted by Flat-axiomatic. Since the 'internal' and 'atomic' axioms are the same in both models, only have to show that when ARMv8-axiomatic's axioms hold, then Flat-axiomatic's 'Order' acyclic. To do this, start with Order, and show step-by-step that any edges in Order that are not included in ARMv8-axiomatic's ob are can be deleted safely: if there is a cycle in Order with them, then there is also one in the relation without them. let Order = (BC_RS | WC_RS | RS_RS | RS_RC; RC_RC*; (RC_BC | RC_WC) | WC_RC; RC_RC*; (RC_BC | RC_WC) | BC_RC; RC_RC*; (RC_BC | RC_WC) | BC_BC | RC_BC | WC_BC | RC_WC | WC_WC | BC_WC | co | rfe | fr )* (* Apply most of the definitions *) = ([DMB.SY|ISB|DMB.LD]; po; [R] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | [W];(po-loc\rf\(po;rf));[R] | [Acq];po;[R] | [R];addr;[R] | [R];(addr|data);rfi;[R] | [R];(po-loc\(rf^-1;rf)\(po;rf));[R] | RC_RC*; (RC_BC | RC_WC) | WC_RC; RC_RC*; (RC_BC | RC_WC) | BC_RC; RC_RC*; (RC_BC | RC_WC) | [DMB.SY];po;[F] | [F];po;[DMB.SY] | [R];po;[DMB.SY|DMB.LD] | [R];ctrl;[F] | [R];addr;po;[ISB] | [W];po;[DMB.SY|DMB.ST] | [R];po;[Rel] | [R];addr;[W] | [R];data;[W] | [R];ctrl;[W] | [R];addr;po;[W] | [Acq];po;[W] | [R];po-loc;[W] | [R];rmw;[W] | [W];po-loc;[W] | [W];po;[Rel] | [F];po;[W] | co | rfe | fr )* (* Simplify *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | RC_RC*; (RC_BC | RC_WC) | WC_RC; RC_RC*; (RC_BC | RC_WC) | BC_RC; RC_RC*; (RC_BC | RC_WC) | co | rfe | fr | [R];(po-loc\(rf^-1;rf)\(po;rf));[R] | [W];(po-loc\rf\(po;rf));[R] | [W];po-loc;[W] | [R];po-loc;[W] )* (* [W]; po-loc; [W] is included in co, so can delete this edge *) (* [R];po-loc;[W] included in fr, so can delete this edge. *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | RC_RC*; (RC_BC | RC_WC) | WC_RC; RC_RC*; (RC_BC | RC_WC) | BC_RC; RC_RC*; (RC_BC | RC_WC) | co | rfe | fr | [R];(po-loc\(rf^-1;rf)\(po;rf));[R] | [W];(po-loc\rf\(po;rf));[R] )* (* Consider (W,R) in [W];(po-loc\rf\(po;rf));[R]. By definition (W,R) not in rf. Let (W',R) in rf with W <> W'. By definition it is not {(W,W')(W',R)} <= po. By coherence axiom it also cannot be (W',W) in po, because otherwise cycle in fr;po. Also cannot be (R,W') in po because otherwise cycle in po;rf. So (W',R) in rfe, and by coherence axiom again it must be (W,W') in co, otherwise cycle in fr;po. So then (W,R) in co;rfe. So the above edge is subsumed by co;rfe *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | RC_RC*; (RC_BC | RC_WC) | WC_RC; RC_RC*; (RC_BC | RC_WC) | BC_RC; RC_RC*; (RC_BC | RC_WC) | co | rfe | fr | [R];(po-loc\(rf^-1;rf)\(po;rf));[R] )* (* Consider (R,R') [R];(po-loc\(rf^-1;rf)\(po;rf));[R] and let (W,R) in rf, (W',R') in rf. By definition W <> W' and not {(R,W'),(W',R')} <= po. It must be (W,W') in co as otherwise (R',W) in fr and there is a cycle in fr;rf;po. By per-thread-coherence it cannot be (R',W') in po. Also cannot be (W',R) in po, since otherwise cycle in fr;po. So W' not from the same thread as R and R' and it is (R,R') in fr;rfe. So [R];(po-loc\(rf^-1;rf)\(po;rf));[R] subsumed by fr;rfe and can delete the edge. *) *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | RC_RC*; (RC_BC | RC_WC) | WC_RC; RC_RC*; (RC_BC | RC_WC) | BC_RC; RC_RC*; (RC_BC | RC_WC) | co | rfe | fr )* (* Now apply the definitions of WC_RC and BC_RC *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | RC_RC*; (RC_BC | RC_WC) (* E2 *) | ([Rel];po;[Acq] | [W];(po-R-loc\rf);[R]); RC_RC*; (RC_BC | RC_WC) | [DMB.SY|ISB|DMB.LD];po;[R]; RC_RC*; (RC_BC | RC_WC) (* E1 *) | co | rfe | fr )* (* E1 = [DMB.SY|ISB|DMB.LD];po;[R];E2 [DMB.SY|ISB|DMB.LD];po;[R] already contained in the relation using ([DMB.SY];po) and ([ISB|DMB.LD];po;[R]). So E1 is already contained in the relation using ([DMB.SY];po), ([ISB|DMB.LD];po;[R]), and E2, and we can delete E1. *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | RC_RC*; (RC_BC | RC_WC) (* E2 *) | ([Rel];po;[Acq] | [W];(po-R-loc\rf);[R]); RC_RC*; (RC_BC | RC_WC) (* E1 *) | co | rfe | fr )* (* E1 = ([Rel];po;[Acq] | [W];(po-R-loc\rf);[R]); E2 Let (W,R) in [W];(po-R-loc\rf);[R]. By definition R does not read from W, so it is (W',R) in rf for W' <> W. W and W' have to be coherence related. It cannot be (W',W) in co, because then there is a cycle in po;fr. So we have (W,W') in co. By (W,W') in co it cannot be (W',W) in po. By (W',R) in rf it cannot be (R,W') in po. And by definition of po-R-loc it cannot be {(W,W'),(W',R)} in po. So W' not from the same thread as R and it is (W',R) in rfe. Therefore it is (W,W');(W',R) in co;rfe, so (W,R) in co;rfe. So [W];(po-R-loc\rf);[R] is included in co;rfe. Then ([Rel];po;[Acq] | [W];(po-R-loc\rf);[R]) is already included in the above relation using [Rel];po;[Acq] and co and rfe, and E1 is subsumed by the combination of these and E2. So can delete E1. *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | RC_RC*; (RC_BC | RC_WC) | co | rfe | fr )* (* Now consider RC_RC*: ([R];addr;[R] | [R];addr;po-no-W-loc;[R] | [Acq];po;[R] | [R];ctrl;[R] | [R];(addr|data);rfi;[R] | [R];po-R-loc;[R])* = (addr;[R] | addr;po-no-W-loc;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | [R];po-R-loc;[R])* This is included in the following: (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | [R];po-R-loc;[R])*. Can rewrite this to the following using the fact that [R];po-R-loc;[R] is transitive: ([R];po-R-loc;[R])?; (addr;[R] | addr;[R];po-R-loc;[R] | addr;po;[R] | addr;po;[R];po-R-loc;[R] | [Acq];po;[R] | [Acq];po;[R];po-R-loc;[R] | ctrl;[R] | ctrl;[R];po-R-loc;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])* But many edges are subsumed by others: - addr;[R];po-R-loc;[R] by addr;po;[R] - addr;po;[R];po-R-loc;[R] by addr;po;[R] - [Acq];po;[R];po-R-loc;[R] by [Acq];po;[R] - ctrl;[R];po-R-loc;[R] by ctrl;[R] ([R];po-R-loc;[R])?; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])* = So RC_RC* included in ([R];po-R-loc;[R])?; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])* So can strengthen the order below by including this edge instead. *) subset ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | ([R];po-R-loc;[R])?; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])*; (RC_BC | RC_WC) | co | rfe | fr )* (* Apply the definition of RC_BC and RC_WC *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | ([R];po-R-loc;[R])?; [R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])*; ([R];po;[DMB.SY|DMB.LD] | [R];ctrl;[F] | [R];addr;po;[ISB] | [R];po;[Rel] | [R];addr;[W] | [R];data;[W] | [R];ctrl;[W] | [R];addr;po;[W] | [Acq];po;[W] | [R];po-loc;[W] | [R];rmw;[W]) | co | rfe | fr )* (* Some variants of the long edge are subsumed by existing edges in the relation, so can delete these: The variant ending in [R];po;[DMB.SY|DMB.LD] is subsumed by po;[DMB.SY] and [R];po;[DMB.LD] The variant ending with [R];po;[Rel] is subsumed by po;[Rel] *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | ([R];po-R-loc;[R])?; [R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])*; ([R];ctrl;[DMB.ST|ISB] | [R];addr;po;[ISB] | [R];addr;[W] | [R];data;[W] | [R];ctrl;[W] | [R];addr;po;[W] | [Acq];po;[W] | [R];po-loc;[W] | [R];rmw;[W]) | co | rfe | fr )* (* The long edge is a subset of program order and cannot create cycles by itself. So it can only create cycles in composition with other edges. In particular, the variant ending with the [DMB.ST] can only create cycles in composition with others. Since the edge cannot be composed with itself, replace it with its postcomposition with every other edge from the relation above. *) has a cycle only if the following has a cycle ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | ([R];po-R-loc;[R])?; [R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])*; ([R];ctrl;[DMB.ST];(po;[DMB.SY]|po;[W]|po;[Rel]) | [R];ctrl;[ISB] | [R];addr;po;[ISB] | [R];addr;[W] | [R];data;[W] | [R];ctrl;[W] | [R];addr;po;[W] | [Acq];po;[W] | [R];po-loc;[W] | [R];rmw;[W]) | co | rfe | fr )* (* The big disjunction in the suffix contains some duplication: clean up. *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD]; po; [R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | ([R];po-R-loc;[R])?; [R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])*; ([R];ctrl;[DMB.ST];po;[DMB.SY] | [R];ctrl;[ISB] | [R];addr;po;[ISB] | [R];addr;[W] | [R];data;[W] | [R];ctrl;[W] | [R];addr;po;[W] | [Acq];po;[W] | [R];po-loc;[W] | [R];rmw;[W]) | co | rfe | fr)* (* Now the variant of the long edge ending with a [DMB.SY] is subsumed by the edge po;[DMB.SY] and we can delete it. Also rewrite [R];po-loc;[W] to fri (by per-thread-coherence *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | ([R];po-R-loc;[R])?; [R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])*; ([R];ctrl;[ISB] | [R];addr;po;[ISB] | [R];addr;[W] | [R];data;[W] | [R];ctrl;[W] | [R];addr;po;[W] | [Acq];po;[W] | fri | [R];rmw;[W]) | co | rfe | fr)* (* Split by definition of '?' *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | [R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])*; ([R];ctrl;[ISB] | [R];addr;po;[ISB] | [R];addr;[W] | [R];data;[W] | [R];ctrl;[W] | [R];addr;po;[W] | [Acq];po;[W] | fri | [R];rmw;[W]) | [R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi;[R] | (addr|data);rfi;[R];po-R-loc;[R])*; ([R];ctrl;[ISB] | [R];addr;po;[ISB] | [R];addr;[W] | [R];data;[W] | [R];ctrl;[W] | [R];addr;po;[W] | [Acq];po;[W] | fri | [R];rmw;[W]) | co | rfe | fr )* (* Now consider (W,R') in rfi;[R];po-R-loc;[R] Then there exists a read R such that (W,R) in rfi and (R,R') in po-R-loc. Let (W',R') in rf. Now there are two cases a) W = W' or b) W <> W'. a) Then (W,R') in rfi. b) W and W' must be coherence-related. Assume (W',W) in co. Then (R',W) in fr and there is a cycle in po;fr. So (W,W') in co. It cannot be (W',R) in po because otherwise cycle in po;fr, and it cannot be (R',W') in po because otherwise cycle in po;rf. By definition of the edge, W' not po-between R and R'. So W' and R' from different threads and it is (W',R') in rfe. Therefore (W,W');(W',R') in co;rfe, so (W,R') in co;rfe So rfi;[R];po-R-loc;[R] included in rfi | (co;rfe)&po-loc. Use this to strengthen the two long edges. *) subset ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | [R];(addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | [R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | co | rfe | fr )* (* Cleanup: the first long edge is subsumed by the combination of the following edges. addr;po;[ISB], addr;po;[W], [Acq];po;[R], ctrl;[ISB], [Acq];po;[W], ctrl;[W], addr;[W], data;[W], fr, rmw, (addr|data);rfi, co, rfe, rmw So can delete this edge. *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | [R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | co | rfe | fr )* (* The last long edge does not create cycles by itself since it is a subset of program order. Any cycle contained in the order above that has a cycle using this edge must be one that uses it in composition with more edges from the relation. Delete the edge and postcompose all edges from the relation with this one. *) only has a cycle if the following has a cycle ([DMB.SY];po | [DMB.SY];po;[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | [ISB|DMB.LD];po;[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Acq];po;[R|W];[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | [Rel];po;[Acq] | [Rel];po;[Acq];[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | [Xw];rfi;[Acq] | [Xw];rfi;[Acq];[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | rmw | addr | addr;[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | (addr|data);rfi;[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | co | rfe | rfe;[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | fr)* (* Some of these are easily subsumed by existing edges: The long edge starting with [DMB.SY] is subsumed by [DMB.SY];po The long edge starting with [ISB|DMB.LD];po;[R];po-R-loc is subsumed by [F];po;[W] and [ISB|DMB.LD];po;[R] and ctrl;[ISB] | addr;po;[ISB] The long edge starting with [Acq];po;[R|W] is subsumed by [Acq];po;[W] and [Acq];po;[R] and ctrl;[ISB] | addr;po;[ISB] The long edge starting with [Rel];po;[Acq] is subsumed by [Rel];po;[Acq], [Acq];po;[W], [Acq];po;[R], ctrl;[ISB], addr;po;[ISB] The long edge starting with [Xw];rfi;[Acq] is subsumed by [Xw];rfi;[Acq], [Acq];po;[W], [Acq];po;[R], ctrl;[ISB], addr;po;[ISB] The long edge starting with addr;[R];po-R-loc is subsumed by addr;po;[ISB] and addr;po;[W] *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | (addr|data);rfi;[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | co | rfe | rfe;[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | fr )* (* As shown before rfi;[R];po-R-loc;[R] included in (rfi | ((co;rfe)&po-loc)). Use this to strengthen first long edge *) subset ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | (addr|data);(rfi | ((co;rfe)&po-loc));[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | co | rfe | rfe;[R];po-R-loc;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | fr)* (* Now consider (W,R') in rfe;[R];po-R-loc;[R]. Then (W,R) in rfe for some read R and (R,R') in po-R-loc. Now there are two cases: a) (W,R') in rf or b) not. a) Then (W,R') in rfe. b) Then there is W' with (W',R') in rf and W <> W'. W and W' must be coherence-related. Assume the coherence is (W',W). Then it is (R',W) in fr and there is a cycle fr;rf;po. So the coherence must be (W,W'). It cannot be (W',R) in po because then there would be a cycle in po;fr. By definition of the edge, W' not po-between R and R'. And it cannot be (R',W') in po since then there would be a cycle in po;rf. So W' not from the same thread as R and R'. But then it is (W,R);(R,W'),(W',R') in rfe;fre;rfe. So rfe;[R];po-R-loc;[R] included in (rfe | rfe;fre;rfe). Use this to strengthen the second long edge.*) subset ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | (addr|data);(rfi | ((co;rfe)&po-loc));[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | co | rfe | (rfe | rfe;fre;rfe); (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | fr )* (* Split the first and the second long edge. *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | (addr|data);rfi;[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | (addr|data);((co;rfe)&po-loc);[R]; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | co | rfe | rfe; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | rfe;fre;rfe; (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) | fr )* (* Now there are four long edges, each with a different prefix. The first one starts with (addr|data);rfi. Since we already have (addr|data);rfi in the relation we can strengthen the order by deleting this prefix. The second edges starts with (addr|data);((co;rfe)&po-loc). Since we have the edges addr, data, co, rfe, can delete this prefix and strengthen the order. The third one starts with rfe. Since we have rfe in the relation, can strengthen the order by deleting this prefix. The fourth edge starts with rfe;fre;rfe. Since rfe and fr are already in the relation, can strengthen it by deleting this prefix. *) subset ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) (* E1 *) | (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) (* E2 *) | co | rfe | (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) (* E3 *) | (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) (* E4 *) | fr )* (* Now we have four copies of the same edge, can delete all but one. *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | (addr;[R] | addr;po;[R] | [Acq];po;[R] | ctrl;[R] | (addr|data);rfi | (addr|data);((co;rfe)&po-loc))*; [R]; (ctrl;[ISB] | addr;po;[ISB] | addr;[W] | data;[W] | ctrl;[W] | addr;po;[W] | [Acq];po;[W] | fri | rmw;[W]) (* E1 *) | co | rfe | fr )* (* The final long edge is subsumed by the combination of other edges already in the relation: addr;po;[ISB], [Acq];po;[R], ctrl;[ISB], (addr|data);rfi, addr, data, co, rfe addr;po;[W], [Acq];po;[W], ctrl;[W], addr;[W], data;[W], fri, rmw *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | co | rfe | fr )* (* Split co and fr. *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | ctrl;[W] | addr;po;[W] | (addr|data);rfi | coe | coi | rfe | fre | fri )* (* coi is acyclic itself. It can only contribute to cycles in composition with other edges. Postcompose every edge in the relation with coi and add EDGE;coi. *) has a cycle only if the following has a cycle ([DMB.SY];po | [DMB.SY];po;coi | po;[DMB.SY] | [F];po;[W] | [F];po;[W];coi | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Acq];po;[R|W];coi | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | rmw;coi | addr | addr;coi | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | addr;po;[W];coi | (addr|data);rfi | coe | coe;coi | rfe | fre | fre;coi | fri | fri;coi )* (* Most of those edges are subsumed by others. [DMB.SY];po;coi subsumed by [DMB.SY];po [F];po;[W];coi by [F];po;[W] [Acq];po;[W];coi by [Acq];po;[W] rmw;coi subsumed by fri addr;coi subsumed by addr;po;[W] addr;po;[W];coi subsumed by addr;po;[W] coe;coi subsumed by coe fre;coi subsumed by fre fri;coi subsumed by fri *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | coe | rfe | fre | fri )* (* fri is acyclic itself, so can only create cycles in composition with other edges. Postcompose all edges with fri and add EDGE;fri. *) has a cycle only if the following has a cycle ([DMB.SY];po | [DMB.SY];po;fri | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | [ISB|DMB.LD];po;[R];fri | ctrl;[F] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Acq];po;[R|W];fri | [Rel];po;[Acq] | [Rel];po;[Acq];fri | [Xw];rfi;[Acq] | [Xw];rfi;[Acq];fri | rmw | addr | addr;fri | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | (addr|data);rfi;fri | coe | rfe | rfe;fri | fre )* (* But these edges are subsumed by others in the relation. [DMB.SY];po;fri by [DMB.SY];po [ISB|DMB.LD];po;[R];fri by [F];po;[W] [Acq];po;[R|W];fri by [Acq];po;[R|W] [Rel];po;[Acq];fri by [Rel];po;[Acq], [Acq];po;[R|W] [Xw];rfi;[Acq];fri by [Xw];rfi;[Acq], [Acq];po;[R|W] addr;fri by addr;po;[W] (addr|data);rfi;fri by addr;po;[W], data;coi rfe;fri by coe *) = ([DMB.SY];po | po;[DMB.SY] | [F];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[F] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | coe | rfe | fre )* (* Cleanup *) = ([DMB.SY];po | po;[DMB.SY] | [DMB.LD|ISB];po;[W] | [DMB.ST];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[DMB.ST] | ctrl;[ISB] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | coe | rfe | fre )* (* Now the DMB.ST edges themselves are acyclic. Replace them by all possible compositions using them *) only has a cycle if the following has one ([DMB.SY];po | po;[DMB.SY] | [DMB.LD|ISB];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST];po;[W] | [R];addr;po;[ISB] | [ISB|DMB.LD];po;[R] | ctrl;[DMB.ST];po;[W] | ctrl;[ISB] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | coe | rfe | fre )* (* Now the ctrl;[DMB.ST];po;[W] edge is subsumed by ctrl;[W] *) = ([DMB.SY];po | po;[DMB.SY] | [DMB.LD|ISB];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST];po;[W] | [R];addr;po;[ISB] | [ISB];po;[R] | [DMB.LD];po;[R] | ctrl;[ISB] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | coe | rfe | fre )* (* Merge two ISB edges *) only has a cycle if the following has one ([DMB.SY];po | po;[DMB.SY] | [DMB.LD|ISB];po;[W] | [R];po;[DMB.LD] | [W];po;[DMB.ST];po;[W] | [R];(ctrl|(addr;po));[ISB] | [ISB];po;[R] | [DMB.LD];po;[R] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | coe | rfe | fre )* (* The ISB edges themselves are acyclic. Replace them by their possible compositions. *) only has a cycle if the following has one ([DMB.SY];po | po;[DMB.SY] | [DMB.LD];po;[W|R] | [R];po;[DMB.LD] | [W];po;[DMB.ST];po;[W] | [R];(ctrl|(addr;po));[ISB];po;[W|R] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | coe | rfe | fre )* (* Do the same with the DMB.LD *) only has a cycle if the following has one ([DMB.SY];po | po;[DMB.SY] | [R];po;[DMB.LD];po;[W|R] | [W];po;[DMB.ST];po;[W] | [R];(ctrl|(addr;po));[ISB];po;[W|R] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | coe | rfe | fre )* (* And the DMB.SY edges *) only has a cycle if the following has one (po;[DMB.SY];po | [R];po;[DMB.LD];po;[W|R] | [W];po;[DMB.ST];po;[W] | [R];(ctrl|(addr;po));[ISB];po;[W|R] | po;[Rel] | po;[Rel];coi | [Acq];po;[R|W] | [Rel];po;[Acq] | [Xw];rfi;[Acq] | rmw | addr | data | data;coi | ctrl;[W] | ctrl;[W];coi | addr;po;[W] | (addr|data);rfi | coe | rfe | fre )* (* Rearrange *) = (rfe | fre | coe | addr | data | ctrl; [W] | (ctrl| (addr; po)); [ISB]; po; [W|R] | addr; po; [W] | (ctrl | data); coi | (addr | data); rfi | rmw | [Xw];rfi;[Acq] | po;[DMB.SY];po | [Rel];po;[Acq] | [R];po;[DMB.LD];po;[W|R] | [Acq];po;[R|W] | [W];po;[DMB.ST];po;[W] | po;[Rel] | po;[Rel];coi )* (* (ctrl|(addr;po));[ISB];po;[W] is subsumed by ctrl;[W], addr;po;[W] *) = (rfe | fre | coe | addr | data | ctrl; [W] | (ctrl| (addr; po)); [ISB]; po; [R] | addr; po; [W] | (ctrl | data); coi | (addr | data); rfi | rmw | [Xw];rfi;[Acq] | po;[DMB.SY];po | [Rel];po;[Acq] | [R];po;[DMB.LD];po;[W|R] | [Acq];po;[R|W] | [W];po;[DMB.ST];po;[W] | po;[Rel] | po;[Rel];coi )* (* Apply Xw = range(rmw). And strengthen the DMB.LD and [Acq];po[R|W] rules. *) subset (rfe | fre | coe | addr | data | ctrl; [W] | (ctrl | (addr; po)); [ISB]; po; [R] | addr; po; [W] | (ctrl | data); coi | (addr | data); rfi | rmw | [range(rmw)];rfi;[Acq] | po;[DMB.SY];po | [Rel];po;[Acq] | [R];po;[DMB.LD];po | [Acq];po | [W];po;[DMB.ST];po;[W] | po;[Rel] | po;[Rel];coi )*