Require Import List Vbase Vlistbase Relations.
Set Implicit Arguments.
Definition immediate X (rel : relation X) (a b: X) :=
rel a b ∧ (∀ c (R1: rel a c) (R2: rel c b), False).
Definition irreflexive X (rel : relation X) := ∀ x, rel x x → False.
Definition acyclic X (rel : relation X) := irreflexive (clos_trans X rel).
Definition is_total X (cond: X → Prop) (rel: relation X) :=
∀ a (IWa: cond a)
b (IWb: cond b) (NEQ: a ≠ b),
rel a b ∨ rel b a.
Definition restr_subset X (cond: X → Prop) (rel rel': relation X) :=
∀ a (IWa: cond a)
b (IWb: cond b) (REL: rel a b),
rel' a b.
Inductive model_type := Model_standard_c11 | Model_hb_rf_acyclic.
Definition with_mt A mt (x y: A) :=
match mt with
| Model_standard_c11 ⇒ x
| Model_hb_rf_acyclic ⇒ y
end.
Definition actid := nat.
Inductive access_type :=
| ATsc
| ATar
| ATacq
| ATrel
| ATrlx
| ATna.
Inductive act :=
| Askip
| Aalloc (l : nat)
| Aload (typ : access_type) (l : nat) (v : nat)
| Astore (typ : access_type) (l : nat) (v : nat)
| Armw (typ : access_type) (l : nat) (v v': nat).
Definition loc a :=
match a with
| Askip ⇒ 0
| Aalloc l
| Aload _ l _
| Astore _ l _
| Armw _ l _ _ ⇒ l
end.
Definition is_rmw a :=
match a with
| Askip | Aalloc _ | Aload _ _ _ | Astore _ _ _ ⇒ false
| Armw _ _ _ _ ⇒ true
end.
Definition is_write a :=
match a with
| Askip | Aalloc _ | Aload _ _ _ ⇒ false
| Astore _ _ _ | Armw _ _ _ _ ⇒ true
end.
Definition is_access a :=
match a with
| Askip | Aalloc _ ⇒ false
| Aload _ _ _ | Astore _ _ _ | Armw _ _ _ _ ⇒ true
end.
Definition is_writeL a l :=
match a with
| Astore _ l' _
| Armw _ l' _ _ ⇒ l' = l
| _ ⇒ False
end.
Definition is_writeLV a l v :=
match a with
| Astore _ l' v'
| Armw _ l' _ v' ⇒ l' = l ∧ v' = v
| _ ⇒ False
end.
Definition is_readLV a l v :=
match a with
| Aload _ l' v'
| Armw _ l' v' _ ⇒ l' = l ∧ v' = v
| _ ⇒ False
end.
Definition is_na a :=
match a with
| Aload ATna _ _
| Astore ATna _ _
| Armw ATna _ _ _ ⇒ true
| _ ⇒ false
end.
Is the action sequentially consistent?
Definition is_sc a :=
match a with
| Aload ATsc _ _
| Astore ATsc _ _
| Armw ATsc _ _ _ ⇒ true
| _ ⇒ false
end.
Is the action a release write or stronger?
Definition is_release a :=
match a with
| Astore ATsc _ _
| Astore ATar _ _
| Astore ATrel _ _
| Armw ATsc _ _ _
| Armw ATar _ _ _
| Armw ATrel _ _ _ ⇒ true
| _ ⇒ false
end.
Is the action an acquire read or stronger?
Definition is_acquire a :=
match a with
| Aload ATsc _ _
| Aload ATar _ _
| Aload ATacq _ _
| Armw ATsc _ _ _
| Armw ATar _ _ _
| Armw ATacq _ _ _ ⇒ true
| _ ⇒ false
end.
Is the action a relaxed write or an RMW with a relaxed write ?
Definition is_rlx_write a :=
match a with
| Astore ATacq _ _ ⇒ true
| Astore ATrlx _ _ ⇒ true
| Armw ATacq _ _ _ ⇒ true
| Armw ATrlx _ _ _ ⇒ true
| _ ⇒ false
end.
List of actions
Labeling function
"Sequence before" order
"Reads from" map
Memory order
Sequential consistency order
Definition sameThread (a b : actid) :=
∀ c (BAc: clos_refl_trans _ sb a c) (BBc: clos_refl_trans _ sb c b),
(∃! pre, sb pre c) ∧ (∃! post, sb c post).
Definition release_seq_elem (a b : actid) :=
sameThread a b ∨ is_rmw (lab b).
Definition release_seq (a b : actid) :=
a = b ∨
mo a b ∧ release_seq_elem a b
∧ ∀ c (MA: mo a c) (MB: mo c b), release_seq_elem a c.
Definition synchronizes_with (a b : actid) :=
is_release (lab a) ∧ is_acquire (lab b) ∧
∃ c, release_seq a c ∧ rf b = Some c.
Definition imm_happens_before a b :=
sb a b ∨ synchronizes_with a b.
Definition happens_before :=
clos_trans _ imm_happens_before.
Definition visible l a b :=
happens_before a b ∧
(∀ c (HB1: happens_before a c) (HB2: happens_before c b),
¬ is_writeL (lab c) l).
Definition ExecutionFinite :=
<< CLOlab: ∀ a, lab a ≠ Askip → In a acts >> ∧
<< CLOsb : ∀ a b, sb a b → In a acts ∧ In b acts >>.
Definition ConsistentMO :=
(∀ a b (MO: mo a b), ∃ l, is_writeL (lab a) l ∧ is_writeL (lab b) l)
∧ transitive _ mo
∧ (∀ l, is_total (fun a ⇒ is_writeL (lab a) l) mo)
∧ (∀ l, restr_subset (fun a ⇒ is_writeL (lab a) l) happens_before mo).
Definition ConsistentSC :=
transitive _ sc
∧ is_total (fun x ⇒ is_sc (lab x)) sc
∧ restr_subset (fun x ⇒ is_sc (lab x)) happens_before sc
∧ restr_subset (fun x ⇒ is_sc (lab x)) mo sc.
Definition ConsistentRF_basic :=
∀ a,
match rf a with
| None ⇒
∀ b (HB: happens_before b a)
l v (READ: is_readLV (lab a) l v)
(WRI: is_writeL (lab b) l), False
| Some b ⇒
∃ l v, is_readLV (lab a) l v ∧ is_writeLV (lab b) l v
end.
Definition ConsistentRF_no_future :=
∀ a b (RF: rf b = Some a) (HB: happens_before b a), False.
Definition ConsistentRF_na :=
∀ a b (RF: rf a = Some b) (NA: is_na (lab a) ∨ is_na (lab b)),
visible (loc (lab a)) b a.
Definition SCrestriction :=
∀ a b (RF: rf b = Some a) (SC: is_sc (lab b)),
immediate sc a b ∨
¬ is_sc (lab a) ∧ (∀ x (SC: immediate sc x b) (HB: happens_before a x), False).
Definition CoherentRR :=
∀ a b (HB: happens_before a b) (LOC: loc (lab a) = loc (lab b))
c (RFa: rf a = Some c) d (RFb: rf b = Some d) (MO: mo d c),
False.
Definition CoherentWR :=
∀ a b (HB: happens_before a b) (LOC: loc (lab a) = loc (lab b))
c (RF: rf b = Some c) (MO: mo c a),
False.
Definition CoherentRW :=
∀ a b (HB: happens_before a b) (LOC: loc (lab a) = loc (lab b))
c (RF: rf a = Some c) (MO: mo b c),
False.
Definition AtomicRMW :=
∀ a (RMW: is_rmw (lab a)) b (RF: rf a = Some b),
immediate mo b a.
Definition ConsistentAlloc :=
∀ l a (ALLOCa: lab a = Aalloc l) b (ALLOCb: lab b = Aalloc l),
a = b.
Definition IrreflexiveHB :=
irreflexive happens_before.
Definition AcyclicMedium :=
acyclic (fun a b ⇒ happens_before a b ∨
rf b = Some a ∧ (is_na (lab b) ∨ is_na (lab a))).
Definition AcyclicStrong :=
acyclic (fun a b ⇒ happens_before a b ∨ rf b = Some a).
Definition Consistent mt :=
<< FIN : ExecutionFinite >> ∧
<< IRR : IrreflexiveHB >> ∧
<< Cmo : ConsistentMO >> ∧
<< Csc : ConsistentSC >> ∧
<< Crf : ConsistentRF_basic >> ∧
<< Crf': with_mt mt ConsistentRF_no_future AcyclicStrong >> ∧
<< Cna : ConsistentRF_na >> ∧
<< Csc': SCrestriction >> ∧
<< Crr : CoherentRR >> ∧
<< Cwr : CoherentWR >> ∧
<< Crw : CoherentRW >> ∧
<< Crmw: AtomicRMW >> ∧
<< Ca : ConsistentAlloc >>.
Definition weakConsistent mt :=
<< FIN : ExecutionFinite >> ∧
<< IRR : IrreflexiveHB >> ∧
<< ACYC: with_mt mt AcyclicMedium AcyclicStrong >> ∧
<< Cmo : ConsistentMO >> ∧
<< Csc : ConsistentSC >> ∧
<< Crf : ConsistentRF_basic >> ∧
<< Crf': with_mt mt ConsistentRF_no_future True >> ∧
<< Csc': SCrestriction >> ∧
<< Crr : CoherentRR >> ∧
<< Cwr : CoherentWR >> ∧
<< Crw : CoherentRW >> ∧
<< Crmw: AtomicRMW >> ∧
<< Ca : ConsistentAlloc >>.
Lemma ConsistentWeaken :
Consistent Model_hb_rf_acyclic → Consistent Model_standard_c11.
Proof.
ins; red; red in H; des; intuition.
unfold with_mt in *; simpl.
by intros a b ? ?; eapply (Crf' a), (t_trans _ _ _ b); vauto.
Qed.
Lemma ConsistentWeaken2 mt :
Consistent mt → weakConsistent mt.
Proof.
ins; red; red in H; des; intuition; destruct mt; ins.
intros x H; apply (IRR x); revert H; generalize x at 1 3.
induction 1; desf; vauto; edestruct Cna; eauto using clos_trans.
Qed.
Lemma finiteRF :
∀ (FIN: ExecutionFinite)
(Crf: ConsistentRF_basic) a b,
rf a = Some b → In a acts ∧ In b acts.
Proof.
unfold ExecutionFinite; ins; desf.
specialize (Crf a); desf; desf.
generalize (CLOlab a); destruct (lab a); ins;
generalize (CLOlab b); destruct (lab b); ins; intuition congruence.
Qed.
Definition mem_safe :=
∀ a (IN: In a acts) (Aa: is_access (lab a)),
∃ b, lab b = Aalloc (loc (lab a)) ∧ happens_before b a.
Definition initialized_reads :=
∀ a (IN: In a acts) l v (Aa: is_readLV (lab a) l v), rf a ≠ None.
Definition race_free :=
∀ a (INa: In a acts) (Aa: is_access (lab a))
b (INb: In b acts) (Ab: is_access (lab b))
(LOC: loc (lab a) = loc (lab b)) (NEQ: a ≠ b)
(WRI: is_write (lab a) ∨ is_write (lab b))
(NA: is_na (lab a) ∨ is_na (lab b)),
happens_before a b ∨ happens_before b a.
End Consistency.
This page has been generated by coqdoc Imprint | Data protection