Require Import Peano_dec List Permutation Vbase Relations ExtraRelations.
Require Import extralib actions c11.
Set Implicit Arguments.
Definition restr_rel X (cond: X → Prop) (rel: relation X) (a b: X) :=
rel a b ∧ cond a ∧ cond b.
Record opsem :=
{ Tid : nat ;
Res : option nat ;
Acts: list actid ;
Lab : actid → act ;
Sb : actid → actid → Prop ;
Dsb : actid → actid → Prop ;
Asw : actid → actid → Prop }.
Record witness :=
{ Rf: actid → option actid ;
Mo: actid → actid → Prop ;
Sc: actid → actid → Prop }.
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 x ⇒ In x (Acts o1)) (Sb o2) ≫ ∧
≪ Pref_Dsb : Dsb o1 <-→ restr_rel (fun x ⇒ In x (Acts o1)) (Dsb o2) ≫ ∧
≪ Pref_Asw : Asw o1 <-→ restr_rel (fun x ⇒ In x (Acts o1)) (Asw o2) ≫ ∧
≪ Pref_UCSb : upward_closed (Sb o2) (fun x ⇒ In x (Acts o1)) ≫ ∧
≪ Pref_UCAsw : upward_closed (Asw o2) (fun x ⇒ In 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 :=
∃ a,
≪ 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 ≠ a → Lab 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 a2 → thread a2 = thread a2.
Opsems should be finite.
We require the sb order to be acyclic. This may be enforced by a hypothesis
on the existence of an execution.
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 ≫.
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,
∃ or,
≪ 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 b → In b (Acts or) ≫ ∧
≪ Rec_Lab: ∀ b, In b (Acts o) → ¬ clos_trans _ (Sbw o) a b → a ≠ b → Lab or b = Lab o b ≫ ∧
≪ Rec_Sb: (restr_rel (fun x ⇒ In 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 x ⇒ In 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 x ⇒ In 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}+{x≠y}) (l: list X) (ND: NoDup l) (P: X → Prop),
∃ 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