Require Import Classical List Permutation Relations Peano_dec Setoid Omega.
Require Import Vbase extralib ExtraRelations cactions WMModels SCresults.
Set Implicit Arguments.

Lemma ModelTSO_SRA :
lab sb rf mo
(C: ModelTSO lab sb rf mo),
acyclic (sb +++ rf_external sb rf +++ mo).

Lemma hbWW_in_mo sb rf mo
(ChbI : irreflexive (happens_before sb rf))
(Cmohb : irreflexive (mo;; happens_before sb rf))
dom (CmoF : is_total dom mo) x (Wx: dom x) y (Wy: dom y)
(HB: happens_before sb rf x y) :
mo x y.

## Equivalent TSO definitions

The two presented TSO-coherence definitions are equivalent.

Theorem ModelTSO_simplify :
lab sb (T: transitive sb) rf mo,
ModelTSO lab sb rf mo
ModelTSO_simpl lab sb rf mo.

## Reducing TSO to SC

Given a TSO-coherent execution, it is also SC-coherent if an additional irreflexivity condition holds.

Definition sb_minus (sb : relation actid) rf mo x y :=
immediate sb x y ¬ mo x y c (MO: mo x c) (RF: rf y = Some c), False.

Lemma sb_minusI acts
sb (sbT: transitive sb) (sbI : irreflexive sb)
(sbD: a b, sb a b In b acts)
rf mo (IRR: irreflexive mo) x y
(X: clos_trans (immediate (clos_trans (sb +++ rf_external sb rf +++ mo))) x y) :
clos_trans (sb_minus sb rf mo +++ rf_external sb rf +++ mo) x y.

Lemma ModelTSO_to_SC :
acts lab sb (FIN: ExecutionFinite acts lab sb) (T: transitive sb) rf mo
(C: ModelTSO lab sb rf mo),
ModelSC_bigmo_simpl lab sb rf mo
irreflexive (reads_before lab rf mo ;; mo ;;
eqv_rel (fun xis_write_only (lab x)) ;;
sb_minus sb rf mo ;; eqv_rel (fun x¬ is_write (lab x)) ;;
clos_refl sb).

## Soundness and completeness of write-read reordering

Lemma rf_external_reorder lab sb rf a b
(Crf: ConsistentRF_dom lab rf)
(LOC: loc (lab a) loc (lab b)) :
rf_external (reorder sb b a) rf <--> rf_external sb rf.

Lemma irreflexive_reorder A (r r' : relation A) a b :
irreflexive (r ;; r')
¬ r a b
irreflexive (r ;; reorder r' a b).

Lemma irreflexive_reorder2 A (r r' : relation A) a b :
irreflexive (r ;; reorder r' a b)
¬ r b a
irreflexive (r ;; r').

Theorem reorderWR_sound_TSO :
lab sb rf mo a b
(C: ModelTSO_simpl lab (reorder sb a b) rf mo)
(Wa: is_write_only (lab a))
(LOC: loc (lab a) loc (lab b))
(Esb1: x, sb a x x = b sb b x)
(Esb2: x, sb x b x = a sb x a),
ModelTSO_simpl lab sb rf mo.

Reordering an adjacent write-read pair is complete under TSO provided there is no mo ;; rf_external from the store to the load.

Theorem reorderWR_complete_TSO :
lab sb rf mo a b
(C: ModelTSO_simpl lab sb rf mo)
(Wa: is_write_only (lab a))
(LOC: loc (lab a) loc (lab b))
(Esb1: x, sb a x x = b sb b x)
(Esb2: x, sb x b x = a sb x a)
(COND: ¬ (mo ;; rf_external sb rf) a b),
ModelTSO_simpl lab (reorder sb a b) rf mo.

## Soundness and completeness of read-after-write elimination

Lemma rf_external_elimRaW lab (sb' sb : relation actid) rf' a b
(Crf: ConsistentRF_dom lab rf')
(Esb2: x, sb x b x = a sb x a)
(EQsb: sb' <--> restr_rel (fun xx b) sb) :
rf_external sb (fun xif x == b then Some a else rf' x) <-->
rf_external sb' rf'.

Lemma reads_before_elimRaW lab' mo' rf' a b l v
(CrfD: ConsistentRF_dom lab' rf')
(CmoD: ConsistentMO_big_dom lab' mo')
(WRI: is_writeLV (lab' a) l v)
(LAB: lab' b = Askip) :
(fun xif x == b then Aload l v else lab' x)
(fun xif x == b then Some a else rf' x) mo' <-->
reads_before lab' rf' mo' +++ (fun x yx=b mo' a y l = loc (lab' y)).

Eliminating a redundant load after an adjacent previous store is sound under TSO.

Lemma elimRaW_sound_TSO :
lab' sb' rf' mo'
(C: ModelTSO_simpl lab' sb' rf' mo')
a l v (Wa: is_writeLV (lab' a) l v)
b
(sb : relation actid)
(Esb1: x, sb a x x = b sb b x)
(Esb2: x, sb x b x = a sb x a)
(T: transitive sb)
(IRR: irreflexive sb)
(EQsb: sb' <--> restr_rel (fun xx b) sb) lab
(LAB: lab = fun xif x == b then Aload l v else lab' x),
ModelTSO_simpl lab sb
(fun xif x == b then Some a else rf' x) mo'.

Eliminating a redundant load after an adjacent previous store is also complete under TSO.

Lemma elimRaW_complete_TSO :
lab' sb' rf' mo'
a l v (Wa: is_writeLV (lab' a) l v)
b
(sb : relation actid)
(Esb2: x, sb x b x = a sb x a)
(EQsb: sb' <--> restr_rel (fun xx b) sb)
(RFb : rf' b = None) lab rf
(EQlab : lab = fun xif x == b then Aload l v else lab' x)
(EQrf : rf = fun xif x == b then Some a else rf' x)
(C: ModelTSO_simpl lab sb rf mo'),
ModelTSO_simpl lab' sb' rf' mo'.

## Equivalent TSO definition in terms of transformations

The allowed transformations on plain executions under TSO are:

Inductive TSO_transform (pe pe' : plain_exec) : Prop :=
| TSO_transform_reorderWR ll1 l1 l2 ll2 a b
(Wa: is_write_only (pe.(pe_lab) a))
(LOC: loc (pe.(pe_lab) a) loc (pe.(pe_lab) b))
(EQinit : pe_inits pe' = pe_inits pe)
(EQlab : pe_lab pe' = pe_lab pe)
(EQ : pe.(pe_threads) = ll1 ++ (l1 ++ a :: b :: l2) :: ll2)
(EQ : pe'.(pe_threads) = ll1 ++ (l1 ++ b :: a :: l2) :: ll2)
| TSO_transform_elimRaW ll1 l1 l2 ll2 a b l v
(Wa: pe.(pe_lab) a = Astore l v)
(Rb: pe.(pe_lab) b = Aload l v)
(EQinit : pe'.(pe_inits) = pe.(pe_inits))
(EQ : pe.(pe_threads) = ll1 ++ (l1 ++ a :: b :: l2) :: ll2)
(EQ': pe'.(pe_threads) = ll1 ++ (l1 ++ a :: l2) :: ll2)
(LAB': x, x b pe'.(pe_lab) x = pe.(pe_lab) x).

These transformations preserve wellformedness.
The transformations decrease the following metric.

Fixpoint metric A lab n (l : list A) :=
match l with
| nil ⇒ 0
| x :: l
n + metric lab (S n) l
else metric lab (S n) l
end.

Lemma TSO_transform_metric pe pe' :
TSO_transform pe pe'
n,
< metric pe.(pe_lab) n (concat pe.(pe_threads)).

Lemma mk_po_elim init ll1 l1 a b l2 ll2 :
NoDup (init ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2))
mk_po init (ll1 ++ (l1 ++ a :: l2) :: ll2) <-->
restr_rel (fun x : actidx b)
(mk_po init (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)).

We show that the transformations are sound with respect to the TSO memory model.

Lemma TSO_transform_sound :
pe pe'
(T: TSO_transform pe pe')
(WF: pe_wellformed pe)
(C: Consistent ModelTSO pe'),
Consistent ModelTSO pe.
We show that in any TSO-coherent execution that is not SC-incoherent, it is possible to apply a transformation that preserves TSO-coherence.
Lemma TSO_transform_possible :
linit ll lab rf mo
(TSO: ModelTSO lab (mk_po linit ll) rf mo)
(WF: pe_wellformed (PlainExec linit ll lab))
(NSC: ¬ ModelSC_bigmo_simpl lab (mk_po linit ll) rf mo),
ll' lab' rf' mo',
TSO_transform (PlainExec linit ll lab) (PlainExec linit ll' lab')
ModelTSO_simpl lab' (mk_po linit ll') rf' mo'.

Our main theorem: TSO is equivalent to this set of transformations over SC.