"Roach motel" reorderings

Require Import Peano_dec List Vbase Relations ExtraRelations.
Require Import actions c11 cmon.
Set Implicit Arguments.

We say that two actions a and b are adjacent according to a relation rel if

every action directly reachable from b is directly reachable from a;
every action directly reachable from a, except for b, is also directly reachable by b ;
every action that reaches a directly can also reach b directly; and
every action that reaches b directly, except for a, can also reach a directly.

Note that adjacent actions are not necessarily related by rel.

Definition adjacent (rel: relation actid) (a b: actid) :=
  ≪ LA_ac : ∀ c, rel b c → rel a c ≫ ∧
  ≪ LA_ca : ∀ c, rel c b → c ≠ a → rel c a ≫ ∧
  ≪ LA_cb : ∀ c, rel c a → rel c b ≫ ∧
  ≪ LA_bc : ∀ c, rel a c → c ≠ b → rel b c ≫.

A weaker notion of adjacency, that drops conditions (ii) and (iv) from the previous definition.

Definition adjacentW (rel: relation actid) (a b: actid) :=
≪ LA_ac : ∀ c, rel b c → rel a c ≫ ∧
≪ LA_cb : ∀ c, rel c a → rel c b ≫.

An even weaker notion that uses clos_trans _ rel instead of rel in the conclusion.

Definition adjacentWW (rel: relation actid) (a b: actid) :=
  ≪ LA_ac : ∀ c, rel b c → clos_trans _ rel a c ≫ ∧
  ≪ LA_cb : ∀ c, rel c a → clos_trans _ rel c b ≫.

Ltac unfolds :=
  repeat match goal with |- context [?x] ⇒ unfold x end.

Lemma adjacent_weaken rel a b :
  adjacent rel a b → adjacentW rel a b.

Lemma adjacentW_weaken rel a b :
  adjacentW rel a b → adjacentWW rel a b.

Definition has_loc a :=
  match a with
    | Aalloc _ _ _
    | Aload _ _ _ _
    | Astore _ _ _ _
    | Armw _ _ _ _ _ ⇒ true
    | _ ⇒ false
  end.

Notation same_loc a b :=
  (≪ SL_A : has_loc a ≫ ∧
   ≪ SL_B : has_loc b ≫ ∧
   ≪ SL_Eq: loc a = loc b ≫).

Two distinct actions a and b are reorderable if

they belong to the same thread,
they do not access the same location,
a is not an acquire access or fence,
b is not a release access or fence,
if the model type mt is MThbUrfnaAcyclic or MThbUrfAcyclic, and a is a read, then b is not a write,
if a is a release fence, then b is not an atomic write,
if b is an acquire fence, then a is not an atomic read, and
a and b are not both SC actions.

Definition admissible_reordering mt acts lab (a b: actid) :=
  ≪ AR_Neq: a ≠ b ≫ ∧
  ≪ AR_In_a: In a acts ≫ ∧
  ≪ AR_In_b: In b acts ≫ ∧
  ≪ AR_ST: thread (lab a) = thread (lab b) ≫ ∧
  ≪ AR_SL: ¬ same_loc (lab a) (lab b) ≫ ∧
  ≪ AR_Not_Acq_Wr: ¬ is_acquire (lab a) ≫ ∧
  ≪ AR_Not_Rel_Ra: ¬ is_release (lab b) ≫ ∧
  ≪ AR_Arfna_RW: mt = MThbUrfnaAcyclic →
                  is_read (lab a) →
                  is_write (lab b) →
                  False ≫ ∧
  ≪ AR_Arf_RW: mt = MThbUrfAcyclic →
                is_read (lab a) →
                is_write (lab b) →
                False ≫ ∧
  ≪ AR_Not_Fence_Rel_Write: is_fence (lab a) →
                             is_release (lab a) →
                             is_write (lab b) →
                             ¬ is_na (lab b) →
                             False ≫ ∧
  ≪ AR_Not_Read_Fence_Acq: is_read (lab a) →
                            ¬ is_na (lab a) →
                            is_fence (lab b) →
                            is_acquire (lab b) →
                            False ≫ ∧
  ≪ AR_Not_Both_Sc: ¬ (is_sc (lab a) ∧ is_sc (lab b)) ≫.

The tactic xplit deals with all existential quantifiers and conjunctions in the goal.

Ltac xplit :=
  repeat match goal with
  | |- ∃ x, _ ⇒ eexists
  | |- _ ∧ _ ⇒ split
  end.

Lemma Crf_Read:
  ∀ lab rf
         (Crf: ConsistentRF lab rf)
         a b (RF: rf a = Some b),
    is_read (lab a).

Lemma Crf_Write:
  ∀ lab rf
         (Crf: ConsistentRF lab rf)
         a b (RF: rf a = Some b),
    is_write (lab b).

Lemma Cmo_Write1:
  ∀ lab mo
         (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    is_write (lab a).

Lemma Cmo_Write2:
  ∀ lab mo
         (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    is_write (lab b).

Lemma RS_Write1:
  ∀ mt2 lab sb rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b
         (RS: release_seq mt2 lab sb rf mo a b)
         (Wc: is_write (lab b)),
    is_write (lab a).

Lemma sync_release:
  ∀ mt2 lab sb rf mo flag a b,
  synchronizes_with mt2 lab sb rf mo flag a b →
  is_release (lab a).

Lemma sync_acquire:
∀ mt2 lab sb rf mo flag a b,
  synchronizes_with mt2 lab sb rf mo flag a b →
  is_acquire (lab b).

Hint Immediate sync_release sync_acquire : sync.

Lemma rf_eq_loc:
  ∀ lab rf (Crf: ConsistentRF lab rf)
         a b (RF: rf b = Some a),
    loc (lab a) = loc (lab b).

Lemma rf_has_loc1:
  ∀ lab rf (Crf: ConsistentRF lab rf)
         a b (RF: rf b = Some a),
    has_loc (lab a).

Lemma rf_has_loc2:
  ∀ lab rf (Crf: ConsistentRF lab rf)
         a b (RF: rf b = Some a),
    has_loc (lab b).

Lemma rf_same_loc:
  ∀ lab rf (Crf: ConsistentRF lab rf)
         a b (RF: rf b = Some a),
    same_loc (lab a) (lab b).

Lemma mo_eq_loc:
  ∀ lab mo (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    loc (lab a) = loc (lab b).

Lemma mo_has_loc1:
  ∀ lab mo (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    has_loc (lab a).

Lemma mo_has_loc2:
  ∀ lab mo (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    has_loc (lab b).

Lemma mo_same_loc:
  ∀ lab mo (Cmo: ConsistentMO lab mo)
         a b (MO: mo a b),
    same_loc (lab a) (lab b).

Hint Immediate
     rf_has_loc1 rf_has_loc2 rf_same_loc
     mo_has_loc1 mo_has_loc2 mo_same_loc : loc.

Lemma reordering_ct:
  ∀ rel a b (LA: adjacentWW rel a b)
             x y (Ct: clos_trans _ (rel UNION1 (a ,b )) x y),
    clos_trans _ rel x y ∨ a =x ∧ b =y.

Lemma reordering_rse:
  ∀ lab sb
         a b (LA: adjacentWW sb a b) mt2
         x y (RSE: release_seq_elem mt2 lab (sb UNION1 (a ,b )) x y),
    release_seq_elem mt2 lab sb x y ∨ a =x ∧ b =y.

Lemma reordering_st :
  ∀ lab sb
         a b (LA: adjacentWW sb a b) mt2
         x y (RS: same_thread mt2 lab (sb UNION1 (a ,b )) x y)
             (NEQ : x = a → y = b → False),
    same_thread mt2 lab sb x y.

Lemma reordering_rs:
  ∀ mt acts lab sb rf mo
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentWW sb a b) mt2
         x y (RS: release_seq mt2 lab (sb UNION1 (a ,b )) rf mo x y),
    release_seq mt2 lab sb rf mo x y.

Lemma reordering_sw:
  ∀ mt acts lab sb rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentWW sb a b) mt2
         x y (SW: synchronizes_with mt2 lab (sb UNION1 (a ,b )) rf mo true x y),
    synchronizes_with mt2 lab sb rf mo true x y.

Lemma reordering_hb_intermediate:
  ∀ mt acts lab sb rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentWW sb a b) mt2 asw
         x y (HB: happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x y),
    happens_before mt2 lab sb asw rf mo x y
    ∨ (x = a ∨ happens_before mt2 lab sb asw rf mo x a )
       ∧
       (y = b ∨ happens_before mt2 lab sb asw rf mo b y ).

Lemma reordering_hb_cycle:
  ∀ mt acts lab sb rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentWW sb a b) mt2 asw
         x (HB: happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x x),
    happens_before mt2 lab sb asw rf mo x x ∨
    happens_before mt2 lab sb asw rf mo b a.

Lemma reordering_hb_right:
  ∀ mt mt2 acts lab sb asw rf mo
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b)
         x (HB: happens_before mt2 lab sb asw rf mo x a),
    happens_before mt2 lab sb asw rf mo x b.

Lemma reordering_hb_left:
  ∀ mt mt2 acts lab sb asw rf mo
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b)
         y (HB: happens_before mt2 lab sb asw rf mo b y),
    happens_before mt2 lab sb asw rf mo a y.

Final reordering_hb lemma

Lemma reordering_hb:
  ∀ mt mt2 acts lab sb asw rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b)
         x y (HB: happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x y),
    happens_before mt2 lab sb asw rf mo x y ∨ (x =a ∧ y =b ).

Lemma hb_adjacentW:
  ∀ mt mt2 acts lab sb asw rf mo
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    adjacentW (happens_before mt2 lab sb asw rf mo) a b.

Lemma path_decomp_three_steps:
  ∀ X (eq_X_dec: ∀ (x y: X), {x =y } + {x ≠y })
         rel x y
         (XY: clos_trans X rel x y),
    rel x y ∨
    (∃ z, rel x z ∧ rel z y ) ∨
    (∃ z t, z ≠ y ∧ t ≠ x ∧ rel x z ∧ clos_trans X rel z t ∧ rel t y ).

Lemma reordering_acyclic_hb:
  ∀ mt mt2 acts lab sb asw rf mo
         (IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    irreflexive (happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo).

Lemma hb_admissible_union:
  ∀ mt mt2 acts lab sb asw rf mo
         (IRR: irreflexive (happens_before mt2 lab sb asw rf mo))
         (Crf: ConsistentRF lab rf)
         (Cmo: ConsistentMO lab mo)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo
    <-→ happens_before mt2 lab sb asw rf mo UNION1 (a ,b ).

We develop separate lemmas for the acyclity axioms.

MTorig

Lemma acyclicity_orig:
  ∀ mt2 mtsc acts lab sb dsb asw rf mo sc
         (CONS: Semiconsistent MTorig mt2 mtsc acts lab sb dsb asw rf mo sc)
         a b,
    ConsistentRF_na mt2 lab (sb UNION1 (a ,b )) asw rf mo.

MThbUrfnaAcyclic and MThbUrfAcyclic

Lemma decomp_path_sbUrf_UNION:
  ∀ sb rf P a b x y
         (PATH: clos_trans actid (fun x y ⇒ (sb UNION1 (a ,b )) x y ∨ rf y = Some x ∧ P x y) x y),
    clos_trans _ (fun x y ⇒ sb x y ∨ rf y = Some x ∧ P x y) x y
    ∨ clos_refl_trans _ (fun x y ⇒ sb x y ∨ rf y = Some x ∧ P x y) x a
       ∧ clos_refl_trans _ (fun x y ⇒ sb x y ∨ rf y = Some x ∧ P x y) b y.

We prove the acyclicity result parametrically with respect to any restriction of the reads from relation.

Lemma acyclicity_relUrf:
  ∀ mt acts lab rel rf P
         (ACYC: acyclic (fun x y ⇒ rel x y ∨ rf y = Some x ∧ P x y))
         (Crf: ConsistentRF lab rf)
         a b (AR: admissible_reordering mt acts lab a b)
             (LA: adjacentW rel a b)
         (ABNRW: ¬ (is_read (lab a) ∧ is_write (lab b))),
    acyclic (fun x y ⇒ (rel UNION1 (a ,b )) x y ∨ rf y = Some x ∧ P x y).

The two acyclity lemmas are deduced by instantiation of the parametric lemma.

Lemma acyclicity_hbUrf:
  ∀ mt2 mtsc acts lab sb dsb asw rf mo sc
         (CONS: Semiconsistent MThbUrfAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc)
         a b (AR: admissible_reordering MThbUrfAcyclic acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    acyclic (fun x y ⇒ happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x y ∨ rf y = Some x)
    ∨ is_read (lab a) ∧ is_write (lab b).

Lemma acyclicity_hbUrfna:
  ∀ mt2 mtsc acts lab sb dsb asw rf mo sc
         (CONS: Semiconsistent MThbUrfnaAcyclic mt2 mtsc acts lab sb dsb asw rf mo sc)
         a b (AR: admissible_reordering MThbUrfnaAcyclic acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    acyclic (fun x y ⇒ happens_before mt2 lab (sb UNION1 (a ,b )) asw rf mo x y ∨ rfna lab rf x y)
    ∨ is_read (lab a) ∧ is_write (lab b).

We prove the main theorem of this section, that the admissible reorderings preserve semiconsistent executions and data races.

Theorem Semiconsistent_reordering :
  ∀ mt mt2 mtsc acts lab sb dsb asw rf mo sc
         (CONS: Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    ≪ CONS': Semiconsistent mt mt2 mtsc acts lab (sb UNION1 (a ,b )) dsb asw rf mo sc ≫ ∧
    ≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab (sb UNION1 (a ,b )) asw rf mo ≫.

Using restrict_rf, we can lift this theorem to preserve consistent executions.

Theorem Consistent_reordering :
  ∀ mt (MT: mt ≠ MTorig) mt2 mtsc acts lab sb dsb asw rf mo sc
         (CONS: Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
         a b (AR: admissible_reordering mt acts lab a b)
             (LASB: adjacentWW sb a b)
             (LAASW: adjacentWW asw a b),
    ∃ rf',
      ≪ CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a ,b )) dsb asw rf' mo sc ≫ ∧
      ≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab (sb UNION1 (a ,b )) asw rf mo ≫.

Note that the theorem above requires a weaker adjacency condition. The theorem shown in the paper is a simple corollary.

Corollary Consistent_reordering_paper :
  ∀ mt mt2 mtsc acts lab sb dsb asw rf mo sc a b,
    Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc →
    admissible_reordering mt acts lab a b →
    adjacent sb a b →
    adjacent asw a b →
    mt ≠ MTorig →
  ∃ rf',
    ≪ CONS': Consistent mt mt2 mtsc acts lab (sb UNION1 (a ,b )) dsb asw rf' mo sc ≫ ∧
    ≪ RACE: racy mt2 lab sb asw rf mo → racy mt2 lab (sb UNION1 (a ,b )) asw rf mo ≫.

This page has been generated by coqdoc