Formalisation of opsemsets

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

Definition of opsems

Definition restr_rel X (cond: XProp) (rel: relation X) (a b: X) :=
  rel a b cond a cond b.

Record opsem :=
  { Tid : nat ;
    Res : option nat ;
    Acts: list actid ;
    Lab : actidact ;
    Sb : actidactidProp ;
    Dsb : actidactidProp ;
    Asw : actidactidProp }.
Record witness :=
  { Rf: actidoption actid ;
    Mo: actidactidProp ;
    Sc: actidactidProp }.
Definition pre_execution mt mt2 mtsc o w :=
  Semiconsistent mt mt2 mtsc (Acts o) (Lab o) (Sb o) (Dsb o) (Asw o) (Rf w) (Mo w) (Sc w).

Definition defined_pre_exec mt2 o w :=
   DPE_MS: mem_safe mt2 (Acts o) (Lab o) (Sb o) (Asw o) (Rf w) (Mo w)
   DPE_IR: initialized_reads (Acts o) (Lab o) (Rf w)
   DPE_RF: race_free mt2 (Lab o) (Sb o) (Asw o) (Rf w) (Mo w) .

Definition pre_executable_opsem mt mt2 mtsc o :=
   w, pre_execution mt mt2 mtsc o w.

Definition Sbw o x y := Sb o x y Asw o x y.

Lemma pre_executable_sb_irrefl:
   mt mt2 mtsc o,
  pre_executable_opsem mt mt2 mtsc o
  irreflexive (Sb o).

Definition pref_opsem o1 o2 :=
   Pref_Tid : Tid o1 = Tid o2
   Pref_Res : Res o1 = None
                  Res o1 = Res o2 Acts o2 nil
                   a (IN : In a (Acts o2)) (EQ: thread (Lab o2 a) = Tid o2), In a (Acts o1)
   Pref_Nemp : Acts o1 nil
   Pref_ND : NoDup (Acts o1)
   Pref_Acts : a, In a (Acts o1) → In a (Acts o2)
   Pref_LabIn : a, In a (Acts o1) → Lab o1 a = Lab o2 a
   Pref_LabOut: a, ¬ In a (Acts o1) → Lab o1 a = Askip 0
   Pref_Sb : Sb o1 <-→ restr_rel (fun xIn x (Acts o1)) (Sb o2)
   Pref_Dsb : Dsb o1 <-→ restr_rel (fun xIn x (Acts o1)) (Dsb o2)
   Pref_Asw : Asw o1 <-→ restr_rel (fun xIn x (Acts o1)) (Asw o2)
   Pref_UCSb : upward_closed (Sb o2) (fun xIn x (Acts o1))
   Pref_UCAsw : upward_closed (Asw o2) (fun xIn x (Acts o1)) .

Lemma Pref_ExecutionFinite:
   o1 o2
         (PREF: pref_opsem o1 o2)
         (EF: ExecutionFinite (Acts o2) (Lab o2) (Sb o2) (Asw o2)),
    ExecutionFinite (Acts o1) (Lab o1) (Sb o1) (Asw o1).

Definition alt_read (a1 a2: act) :=
  ( tid typ l v1 v2, a1 = Aload tid typ l v1 a2 = Aload tid typ l v2)
  ( tid typ l v1 v2 v3, a1 = Aload tid RATrlx l v1 a2 = Armw tid typ l v2 v3).

Definition alt_read_final_one o1 o2 :=
   AFRO_Tid : Tid o1 = Tid o2
   AFRO_Res : Res o1 = if thread (Lab o1 a) == Tid o1 then None else Res o2
   AFRO_ND : NoDup (Acts o1)
   AFRO_Acts: (a: actid), In a (Acts o1) In a (Acts o2)
   AFRO_Max : max_elt (Sbw o1) a
   AFRO_Rd : alt_read (Lab o1 a) (Lab o2 a)
   AFRO_Lab : b, b aLab o1 b = Lab o2 b
   AFRO_Sb : Sb o1 <-→ Sb o2
   AFRO_Dsb : Dsb o1 <-→ Dsb o2
   AFRO_Asw : Asw o1 <-→ Asw o2 .

Lemma alt_read_thread_eq a1 a2 : alt_read a1 a2thread a2 = thread a2.

Opsem sets axioms

Section OpsemSets.

Variable oss: opsemProp.

Opsems should be finite.
Definition oss_ef :=
   o, oss oExecutionFinite (Acts o) (Lab o) (Sb o) (Asw o).

The dependent sequenced before relation, dsb, should be consistent with respect to sb.
Definition oss_dsb :=
   o, oss oConsistentDSB (Lab o) (Sb o) (Dsb o).

We require the sb order to be acyclic. This may be enforced by a hypothesis on the existence of an execution.
Definition oss_sbw_acyc :=
   o, oss oacyclic (Sbw o).

Opsemsets are closed by prefix.
Opsemsets are closed by changing the value read by a sb-final read instruction.
Definition AFR_closed :=
  upward_closed alt_read_final_one oss.

Definition oss_defined mt mt2 mtsc :=
   o (OSS: oss o)
         w (PEX: pre_execution mt mt2 mtsc o w),
    defined_pre_exec mt2 o w.

Definition DefinedOSS mt mt2 mtsc :=
   DOSS_ND: o (OSS: oss o), NoDup (Acts o)
   DOSS_EF: oss_ef
   DOSS_ACYC: oss_sbw_acyc
   DOSS_Pref: Pref_closed
   DOSS_AFR: AFR_closed
   DOSS_Def: oss_defined mt mt2 mtsc .

Receptivity gives an alternative view of the prefix-closed/AFR-closed condition, by supposing that the program provides a behavior for any value read by any read instruction. This translates to the existence of an alternative opsems, which is equal to the original opsem except for what sb-follows the modified read instruction. Both notions are equivalent.

Definition is_any_read a tid typ l :=
  ( v, a = Aload tid typ l v)
  ( typ' v1 v2, a = Armw tid typ' l v1 v2) typ = RATrlx.

Definition AR_receptivity :=
   o (OSS: oss o)
         a tid typ l (LRead: is_any_read (Lab o a) tid typ l) vor,
     Rec_OSSR: oss or
     Rec_Tid : Tid or = Tid o
     Pref_Res : (Res or = None
                   b, In b (Acts o) clos_refl_trans _ (Sbw o) a b
                    thread (Lab o b) = Tid o)
                  Res or = Res o
                   b, In b (Acts or) →
                            ¬ clos_refl_trans _ (Sbw o) a b
                            thread (Lab or b) = Tid o
                            In b (Acts o)
     Rec_AR: Lab or a = Aload tid typ l vor
     Rec_In: b, In b (Acts o) → ¬ clos_trans _ (Sbw o) a bIn b (Acts or)
     Rec_Lab: b, In b (Acts o) → ¬ clos_trans _ (Sbw o) a ba bLab or b = Lab o b
     Rec_Sb: (restr_rel (fun xIn x (Acts o) ¬ clos_trans _ (Sbw o) a x) (Sb o))
                <-→ (restr_rel (fun x¬ clos_trans _ (Sbw o) a x) (Sb or))
     Rec_Dsb: (restr_rel (fun xIn x (Acts o) ¬ clos_trans _ (Sbw o) a x) (Dsb o))
                <-→ (restr_rel (fun x¬ clos_trans _ (Sbw o) a x) (Dsb or))
     Rec_Asw: (restr_rel (fun xIn x (Acts o) ¬ clos_trans _ (Sbw o) a x) (Asw o))
                <-→ (restr_rel (fun x¬ clos_trans _ (Sbw o) a x) (Asw or)) .

Require Import Classical.

Lemma Receptivity_implies_AFR:
   (EF: oss_ef) (DSB: oss_dsb) (PREF: Pref_closed) (Recept: AR_receptivity), AFR_closed.

Lemma filter_Prop:
   X (eq_X_dec: (x y: X), {x=y}+{xy}) (l: list X) (ND: NoDup l) (P: XProp),
     l', NoDup l' x, In x l' In x l P x.

Require Import ClassicalDescription.

Lemma AFR_implies_Receptivity:
   (ND: o (OSS: oss o), NoDup (Acts o))
         (EF: oss_ef) (ACYC: oss_sbw_acyc)
         (PREF: Pref_closed) (AFR: AFR_closed), AR_receptivity.

End OpsemSets.

This page has been generated by coqdoc