Require Import List Vbase 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.
Definition actid := nat.
Inductive read_access_type :=
| RATsc
| RATacq
| RATrlx
| RATna.
Inductive write_access_type :=
| WATsc
| WATrel
| WATrlx
| WATna.
Inductive rmw_access_type :=
| UATsc
| UATacq_rel
| UATacq
| UATrel
| UATrlx .
Inductive access_type :=
| ATna
| ATat.
Inductive act :=
| Askip
| Aalloc (l n : nat)
| Aload (typ : read_access_type) (l : nat) (v : nat)
| Astore (typ : write_access_type) (l : nat) (v : nat)
| Armw (typ : rmw_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 accesses_loc a l :=
match a with
| Askip | Aalloc _ _ ⇒ False
| Aload _ l' _
| Astore _ l' _
| Armw _ l' _ _ ⇒ l = l'
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 RATna _ _
| Astore WATna _ _ ⇒ true
| _ ⇒ false
end.
Is the action sequentially consistent?
Definition is_sc a :=
match a with
| Aload RATsc _ _
| Astore WATsc _ _
| Armw UATsc _ _ _ ⇒ true
| _ ⇒ false
end.
Is the action a release write or stronger?
Definition is_release_wtyp t :=
match t with WATsc | WATrel ⇒ true | _ ⇒ false end.
Definition is_release_utyp t :=
match t with UATsc | UATrel | UATacq_rel ⇒ true | _ ⇒ false end.
Definition is_release a :=
match a with
| Astore typ _ _ ⇒ is_release_wtyp typ
| Armw typ _ _ _ ⇒ is_release_utyp typ
| _ ⇒ false
end.
Is the action an acquire read or stronger?
Definition is_acquire_rtyp t :=
match t with RATsc | RATacq ⇒ true | _ ⇒ false end.
Definition is_acquire_utyp t :=
match t with UATsc | UATacq | UATacq_rel ⇒ true | _ ⇒ false end.
Definition is_acquire a :=
match a with
| Aload typ _ _ ⇒ is_acquire_rtyp typ
| Armw typ _ _ _ ⇒ is_acquire_utyp typ
| _ ⇒ false
end.
List of actions
Labeling function
"Sequence before" order
"Reads from" map
Memory order
Sequential consistency order
Definition synchronizes_with (a b : actid) :=
rf b = Some a ∧ is_release (lab a) ∧ is_acquire (lab b).
Definition imm_happens_before a b :=
sb a b ∨ synchronizes_with a b.
Definition happens_before :=
clos_trans _ imm_happens_before.
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)
∧ irreflexive mo
∧ (∀ l, restr_subset (fun a ⇒ is_writeL (lab a) l) happens_before mo).
Definition ConsistentSC :=
(∀ a b (MO: sc a b), is_sc (lab a) ∧ is_sc (lab b))
∧ 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.
Restriction of the SC relation for the SCrestriction axiom
Definition sc_restr a b :=
sc a b ∧ is_write (lab a) ∧ loc (lab a) = loc (lab b).
Definition SCrestriction :=
∀ a b (RF: rf b = Some a) (SC: is_sc (lab b)),
immediate sc_restr a b ∨
¬ is_sc (lab a)
∧ (∀ x (SC: immediate sc_restr 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 :=
∀ a la na (ALLOCa: lab a = Aalloc la na)
b lb nb (ALLOCb: lab b = Aalloc lb nb),
a = b ∨ la + na < lb ∨ lb + nb < la.
Definition AcyclicStrong :=
acyclic (fun a b ⇒ sb a b ∨ rf b = Some a ∨ sc a b).
Definition Consistent :=
<< FIN : ExecutionFinite >> ∧
<< ACYC: AcyclicStrong >> ∧
<< Cmo : ConsistentMO >> ∧
<< Csc : ConsistentSC >> ∧
<< Cscr: SCrestriction >> ∧
<< Crf : ConsistentRF_basic >> ∧
<< Crr : CoherentRR >> ∧
<< Cwr : CoherentWR >> ∧
<< Crw : CoherentRW >> ∧
<< Crmw: AtomicRMW >> ∧
<< Ca : ConsistentAlloc >>.
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.
sc a b ∧ is_write (lab a) ∧ loc (lab a) = loc (lab b).
Definition SCrestriction :=
∀ a b (RF: rf b = Some a) (SC: is_sc (lab b)),
immediate sc_restr a b ∨
¬ is_sc (lab a)
∧ (∀ x (SC: immediate sc_restr 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 :=
∀ a la na (ALLOCa: lab a = Aalloc la na)
b lb nb (ALLOCb: lab b = Aalloc lb nb),
a = b ∨ la + na < lb ∨ lb + nb < la.
Definition AcyclicStrong :=
acyclic (fun a b ⇒ sb a b ∨ rf b = Some a ∨ sc a b).
Definition Consistent :=
<< FIN : ExecutionFinite >> ∧
<< ACYC: AcyclicStrong >> ∧
<< Cmo : ConsistentMO >> ∧
<< Csc : ConsistentSC >> ∧
<< Cscr: SCrestriction >> ∧
<< Crf : ConsistentRF_basic >> ∧
<< Crr : CoherentRR >> ∧
<< Cwr : CoherentWR >> ∧
<< Crw : CoherentRW >> ∧
<< Crmw: AtomicRMW >> ∧
<< Ca : ConsistentAlloc >>.
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) l (Aa: accesses_loc (lab a) l),
∃ b l' n, lab b = Aalloc l' n ∧ happens_before b a ∧ l' ≤ l ≤ l' + n.
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