Monotonicity

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

Basic monotonicity properties

Monotonicity with respect to program order.

Lemma release_seq_mon_sb :
  ∀ mt2 lab sb rf mo a b (HB: release_seq mt2 lab sb rf mo a b)
    (sb' : relation actid) (MON: ∀ x y (SB: sb x y), sb' x y),
    release_seq mt2 lab sb' rf mo a b.

Lemma happens_before_mon_sb :
  ∀ mt2 lab sb asw rf mo a b (HB: happens_before mt2 lab sb asw rf mo a b)
    (sb' : relation actid) (MON: ∀ x y (SB: sb x y), sb' x y),
    happens_before mt2 lab sb' asw rf mo a b.

Monotonicity with respect to reads-from.

Lemma release_seq_mon_rf :
  ∀ mt2 lab sb rf mo a b (HB: release_seq mt2 lab sb rf mo a b)
    rf' (M: ∀ c d (RF: rf c = Some d), rf' c = Some d),
    release_seq mt2 lab sb rf' mo a b.

Lemma happens_before_mon_rf :
  ∀ rf rf' (M: ∀ c d (RF: rf c = Some d), rf' c = Some d)
    mt2 lab sb asw mo a b (HB : happens_before mt2 lab sb asw rf mo a b),
    happens_before mt2 lab sb asw rf' mo a b.

Domain restriction for reads-from map

In this subsection, we show that every semiconsistent execution can be turned into a consistent one by removing some rf edges (Theorem ConsistentRFrestrict).

Definition restrict_rf_once mt2 lab sb asw rf mo a :=
  if excluded_middle_informative
    (∃ b l, happens_before mt2 lab sb asw rf mo b a
                 ∧ is_writeL (lab b) l ∧ is_readL (lab a) l)
  then rf a else None.

We define a measure that is decreased by each restrict_rf_once step.

Definition restrict_measure acts (rf : actid → option actid) :=
  length (filter (fun x ⇒ match rf x with Some _ ⇒ true | None ⇒ false end) acts).

Lemma restrict_measure_rf :
  ∀ mt2 lab sb asw rf mo acts,
    restrict_measure acts (restrict_rf_once mt2 lab sb asw rf mo)
    ≤ restrict_measure acts rf.

Lemma restrict_measure_rf_dec :
  ∀ mt2 lab sb asw rf mo acts
         (INA: ∀ a b, rf a = Some b → In a acts)
         (NEQ: restrict_rf_once mt2 lab sb asw rf mo ≠ rf),
    restrict_measure acts (restrict_rf_once mt2 lab sb asw rf mo)
    < restrict_measure acts rf.

Perform restrict_rf_once n number of times.

Fixpoint restrict_rf_n n mt2 lab sb asw rf mo :=
  match n with
    | 0 ⇒ rf
    | S n ⇒ restrict_rf_once mt2 lab sb asw
               (restrict_rf_n n mt2 lab sb asw rf mo) mo
  end.

Lemma restrict_rf_nC :
  ∀ mt2 lab sb asw mo n rf,
    restrict_rf_once mt2 lab sb asw (restrict_rf_n n mt2 lab sb asw rf mo) mo =
    restrict_rf_n n mt2 lab sb asw (restrict_rf_once mt2 lab sb asw rf mo) mo.

Lemma restrict_rf_n_fix_helper :
  ∀ mt2 lab sb asw mo acts n rf
     (INA: ∀ a b, rf a = Some b → In a acts),
    restrict_rf_n (S n) mt2 lab sb asw rf mo = restrict_rf_n n mt2 lab sb asw rf mo
    ∨ restrict_measure acts (restrict_rf_n n mt2 lab sb asw rf mo) + n
       ≤ restrict_measure acts rf.

Lemma restrict_rf_n_fix_helper2 :
  ∀ mt2 lab sb asw mo acts n rf
     (INA: ∀ a b, rf a = Some b → In a acts)
     (GT: length acts < n),
    restrict_rf_n (S n) mt2 lab sb asw rf mo
    = restrict_rf_n n mt2 lab sb asw rf mo.

Given that restrict_rf_once always decrements the measure, we know that restrict_rf_n will reach a fixed point. We define restrict_rf to be that fixed point.

Definition restrict_rf mt2 (acts : list actid) lab sb asw rf mo :=
restrict_rf_n (S (length acts)) mt2 lab sb asw rf mo.

We prove various properties of the fixed point.

Lemma restrict_rf_n_unchanged :
  ∀ mt2 lab sb asw n rf mo a b l,
    happens_before mt2 lab sb asw (restrict_rf_n n mt2 lab sb asw rf mo) mo b a →
    is_writeL (lab b) l →
    is_readL (lab a) l →
  restrict_rf_n n mt2 lab sb asw rf mo a = rf a.

Lemma restrict_rf_unfold :
  ∀ mt2 acts rf lab sb asw mo
         (FIN: ExecutionFinite acts lab sb asw)
         (Crf: ConsistentRF lab rf) a,
  restrict_rf mt2 acts lab sb asw rf mo a =
  if excluded_middle_informative
    (∃ b l, happens_before mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo b a
                 ∧ is_writeL (lab b) l ∧ is_readL (lab a) l)
  then rf a else None.

Lemma restrict_rf_mon :
  ∀ mt2 acts lab sb asw rf mo a b,
    restrict_rf mt2 acts lab sb asw rf mo a = Some b →
    rf a = Some b.

Happens-before is unaffected by restrict_rf.

Lemma happens_before_restrict_rf :
  ∀ mt2 acts lab sb asw rf mo a b,
    happens_before mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo a b →
    happens_before mt2 lab sb asw rf mo a b.

Finally, we show our main theorem, that for every semiconsistent execution there exists a consistent execution that differs only in the rf component.

Theorem Consistent_restrict_rf :
  ∀ mt (MT: mt ≠ MTorig) mt2 mtsc acts lab sb dsb asw rf mo sc,
    Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc →
  Consistent mt mt2 mtsc acts lab sb dsb asw (restrict_rf mt2 acts lab sb asw rf mo) mo sc.

Theorem racy_restrict_rf mt2 acts lab sb asw rf mo :
  racy mt2 lab sb asw rf mo →
  racy mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo.

Corollary race_free_restrict_rf mt2 acts lab sb asw rf mo :
  race_free mt2 lab sb asw (restrict_rf mt2 acts lab sb asw rf mo) mo →
  race_free mt2 lab sb asw rf mo.

Label monotonicity

Definition RATord x y :=
  match x, y with
    | RATna, RATna ⇒ true
    | RATna, _ ⇒ false
    | _, RATna ⇒ false
    | RATrlx, _ ⇒ true
    | _, RATrlx ⇒ false
    | RATacq, _ ⇒ true
    | _, RATacq ⇒ false
    | RATsc, RATsc ⇒ true
  end.

Definition WATord x y :=
  match x, y with
    | WATna, WATna ⇒ true
    | WATna, _ ⇒ false
    | _, WATna ⇒ false
    | WATrlx, _ ⇒ true
    | _, WATrlx ⇒ false
    | WATrel, _ ⇒ true
    | _, WATrel ⇒ false
    | WATsc, WATsc ⇒ true
  end.

Definition UATord x y :=
  match x, y with
    | UATrlx, _ ⇒ true
    | _, UATrlx ⇒ false
    | UATacq, UATrel ⇒ false
    | UATacq, _ ⇒ true
    | UATrel, UATacq ⇒ false
    | UATrel, _ ⇒ true
    | UATrel_acq, UATrel_acq ⇒ true
    | UATrel_acq, UATsc ⇒ true
    | UATsc, UATsc ⇒ true
    | _, _ ⇒ false
  end.

Definition FATord x y :=
  match x, y with
    | FATacq, FATrel ⇒ false
    | FATacq, _ ⇒ true
    | FATrel, FATacq ⇒ false
    | FATrel, _ ⇒ true
    | FATrel_acq, FATrel_acq ⇒ true
    | FATrel_acq, FATsc ⇒ true
    | FATsc, FATsc ⇒ true
    | _, _ ⇒ false
  end.

Definition act_ord x y :=
  match x, y with
    | Askip tid, Askip tid' ⇒ tid = tid'
    | Askip tid, Afence tid' typ ⇒ tid = tid'
    | Aalloc tid l n, Aalloc tid' l' n' ⇒
      tid = tid' ∧ l = l' ∧ n = n'
    | Aload tid typ l v, Aload tid' typ' l' v' ⇒
      tid = tid' ∧ RATord typ typ' ∧ l = l' ∧ v = v'
    | Astore tid typ l v, Astore tid' typ' l' v' ⇒
      tid = tid' ∧ WATord typ typ' ∧ l = l' ∧ v = v'
    | Armw tid typ l v w, Armw tid' typ' l' v' w' ⇒
      tid = tid' ∧ UATord typ typ' ∧ l = l' ∧ v = v' ∧ w = w'
    | Afence tid typ, Afence tid' typ' ⇒
      tid = tid' ∧ FATord typ typ'
    | _, _ ⇒ False
  end.

Lemma act_ord_refl x : act_ord x x.

Section act_ord_lemmas.

Variables x y : act.
Hypothesis (AO : act_ord x y).

Ltac tac :=
  generalize AO; unfold act_ord; desf; ins; desf;
  match goal with
   | typ : write_access_type |- _ ⇒ solve [destruct typ; ins; desf]
   | typ : read_access_type |- _ ⇒ solve [destruct typ; ins; desf]
   | typ : rmw_access_type |- _ ⇒ solve [destruct typ; ins; desf]
   | typ : fence_access_type |- _ ⇒ solve [destruct typ; ins; desf]
  end.

Lemma act_ord_loc : loc x = loc y.

Lemma act_ord_thread : thread x = thread y.

Lemma act_ord_na : is_na x → is_na y.

Lemma act_ord_na_rev : is_na y → is_na x.

Lemma act_ord_sc : is_sc x → is_sc y.

Lemma act_ord_rmw : is_rmw x → is_rmw y.

Lemma act_ord_rmw_rev : is_rmw y → is_rmw x.

Lemma act_ord_writeLV_rev l v : is_writeLV y l v → is_writeLV x l v.

Lemma act_ord_readLV_rev l v : is_readLV y l v → is_readLV x l v.

Lemma act_ord_write : is_write x → is_write y.

Lemma act_ord_writeL l : is_writeL x l → is_writeL y l.

Lemma act_ord_writeL_rev l : is_writeL y l → is_writeL x l.

Lemma act_ord_writeLV l v : is_writeLV x l v → is_writeLV y l v.

Lemma act_ord_access : is_access x → is_access y.

Lemma act_ord_readL l : is_readL x l → is_readL y l.

Lemma act_ord_readLV l v : is_readLV x l v → is_readLV y l v.

Lemma act_ord_release_write : is_release_write x → is_release_write y.

Lemma act_ord_release_fence : is_release_fence x → is_release_fence y.

Lemma act_ord_acquire_read : is_acquire_read x → is_acquire_read y.

Lemma act_ord_acquire_fence : is_acquire_fence x → is_acquire_fence y.

End act_ord_lemmas.

Hint Resolve act_ord_na act_ord_na_rev act_ord_sc
  act_ord_rmw act_ord_write act_ord_writeL act_ord_writeLV
  act_ord_access act_ord_readL act_ord_readLV
  act_ord_release_write act_ord_release_fence
  act_ord_acquire_read act_ord_acquire_fence : act_ord_lemmas.

Release sequences are monotone.

Lemma release_seq_mon :
  ∀ lab lab' (LO: ∀ a, act_ord (lab' a) (lab a))
    (sb sb' : relation actid) (SBO: ∀ a b, sb' a b → sb a b)
    rf rf' (RFO: ∀ c d (RF: rf' c = Some d), rf c = Some d)
    mt2 mo a b
    (RS: release_seq mt2 lab' sb' rf' mo a b),
  release_seq mt2 lab sb rf mo a b.

The happens-before relation is monotone.

Lemma happens_before_mon :
  ∀ lab lab' (LO: ∀ a, act_ord (lab' a) (lab a))
    (sb sb' : relation actid) (SBO: ∀ a b, sb' a b → sb a b)
    mt2 asw rf mo a b (HB: happens_before mt2 lab' sb' asw rf mo a b),
  happens_before mt2 lab sb asw rf mo a b.

Next comes the main theorem of this section. For any sufficiently corrected model, removing synchronisation from consistent executions preserves their consistency. We first prove this theorem for all axioms except ConsistentRF_dom_some; then using Theorem ConsistentRFrestrict, we extend it to all the axioms.

Theorem Semiconsistent_mon :
  ∀ mt (MT: mt ≠ MTorig) mt2 mtsc (MTSC: mtsc ≠ MTSCorig) acts lab sb dsb asw rf mo sc
    (CONS: Semiconsistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
    lab' (LO: ∀ a, act_ord (lab' a) (lab a))
    (sb' : relation actid) (SBO: ∀ a b, sb' a b → sb a b)
    (CSb': ConsistentSB lab' sb') (DSBO: inclusion _ dsb (clos_trans _ sb')),
  ∃ sc',
    Semiconsistent mt mt2 mtsc acts lab' sb' dsb asw rf mo sc'.

Corollary Consistent_mon :
  ∀ mt (MT: mt ≠ MTorig) mt2 mtsc (MTSC: mtsc ≠ MTSCorig)
         acts lab sb dsb asw rf mo sc
    (CONS: Consistent mt mt2 mtsc acts lab sb dsb asw rf mo sc)
    lab' (LO: ∀ a, act_ord (lab' a) (lab a))
    (sb' : relation actid) (SBO: ∀ a b, sb' a b → sb a b)
    (CSb': ConsistentSB lab' sb') (DSBO: inclusion _ dsb (clos_trans _ sb')),
  ∃ rf' sc',
    Consistent mt mt2 mtsc acts lab' sb' dsb asw rf' mo sc'.

This page has been generated by coqdoc